How does CoeOut work?

Stream: lean4

[Kenny Lau]

Why does this fail? I thought this is exactly what CoeOut is designed for

abbrev Set (α : Type) := α → Prop
axiom IntermediateField (K L : Type) : Type
axiom IntermediateField.toSet {K L : Type} : IntermediateField K L → Set L
axiom Test {α : Type} (s : Set α) : Prop

variable {K L : Type} (F : IntermediateField K L)

instance : CoeTC (IntermediateField K L) (Set L) := ⟨(·.toSet)⟩

#check Test F -- fails

instance : CoeOut (IntermediateField K L) (Set L) := ⟨(·)⟩

#check Test F -- fails

[Aaron Liu]

Maybe it's the metavariables

[Aaron Liu]

Since you're coercing to Set ?_ which has a metavariable

[Kenny Lau]

@Aaron Liu yes, but that's a semiOutParam, and the mvar IntermediateField K L has been resolved

[Aaron Liu]

what does the trace say?

[Kenny Lau]

@Aaron Liu after 30 lines it says:

[Meta.isDefEq.assign] ✅️ ?m.15 := Set L ▶
[Meta.isDefEq.assign] ✅️ ?m.17 := instCoeOutIntermediateFieldSet ▶

abbrev Set (α : Type) := α → Prop
axiom IntermediateField (K L : Type) : Type
axiom IntermediateField.toSet {K L : Type} : IntermediateField K L → Set L
axiom Test {α : Type} (s : Set α) : Prop

variable {K L : Type} (F : IntermediateField K L)

instance : CoeOut (IntermediateField K L) (Set L) := ⟨(·.toSet)⟩

set_option trace.Meta.isDefEq.assign true
#check Test F -- fails

[Aaron Liu]

certainly very interesting