Zulip Chat Archive

Stream: lean4

Topic: coeSort?


view this post on Zulip Jason Gross (Mar 12 2021 at 15:20):

What are the cases where I should have to insert coeSort manually? (I thought Lean was supposed to automatically insert coercions to sort?)

view this post on Zulip Mario Carneiro (Mar 12 2021 at 15:23):

You shouldn't... is there a specific case that came up where you did?

view this post on Zulip Jason Gross (Mar 12 2021 at 15:33):

axiom foo : Type
axiom f : foo -> Sort _
instance : CoeSort foo (Sort _) := { coe := f }
axiom g : Sort _ -> Sort _
axiom ff : foo
#check g ff
/-
application type mismatch
  g ff
argument
  ff
has type
  foo : Type
but is expected to have type
  Sort ?u.35 : Type ?u.35
-/

view this post on Zulip Jason Gross (Mar 12 2021 at 15:35):

Should I report this as a bug? (I assume the issue is that sort coercion search get triggered in places known statically to contain a sort, but at locations where type inference results in the sort constraint, instead non-sort coercion search gets triggered only if there are no metavars.)

view this post on Zulip Mario Carneiro (Mar 12 2021 at 15:42):

Ah, well that's a Coe to Sort, not a CoeSort ;)

view this post on Zulip Mario Carneiro (Mar 12 2021 at 15:43):

I think CoeSort is used only when you use a term where a type is expected, like fun a : x => .. where x : T

view this post on Zulip Mario Carneiro (Mar 12 2021 at 15:43):

If it's just a regular coercion then Coe gets invoked instead, whether the target is Sort or any other T'

view this post on Zulip Mario Carneiro (Mar 12 2021 at 15:44):

IIRC there is a typeclass instance turning has_coe_to_sort A instances into has_coe A Sort* instances in lean 3, not sure if that is still happening in lean 4


Last updated: May 07 2021 at 12:15 UTC