coeSort?

Stream: lean4

[Jason Gross]

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

[Mario Carneiro]

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

[Jason Gross]

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
-/

[Jason Gross]

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.)

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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