Coercion on type class

Stream: new members

[Alexander Niederbühl]

I have defined the following type class:

class ToFloat (α : Type u) where
  toFloat : α → Float

I did expect this to work:

instance [ToFloat α]: Coe α Float where
  coe x := ToFloat.toFloat x

But I'm getting

cannot find synthesization order for instance @instCoeFloat with type
{α : Type u_1} → [inst : ToFloat α] → Coe α Float
all remaining arguments have metavariables:
ToFloat ?α

What does this mean, is it not possible?

[Alex J. Best]

This is as Coe has the first argument (alpha), as a semi-out param (meaning that Lean will go looking for instances even if alpha is not yet known when inserting Coes). You probably should use CoeHead in place of Coe

[Alexander Niederbühl]

Great, that works. Thanks you!