Cannot find synthesization order for instance

Stream: lean4

[Ben]

As part of something I get this weird message

class Thing (T U: Type) extends Coe T U

instance (T U: Type) [t: Thing T U] : Coe T U := t.toCoe

with

cannot find synthesization order for instance instCoeOfThing with type
  (T U : Type) → [t : Thing T U] → Coe T U
all remaining arguments have metavariables:
  Thing ?T U

Anyone know what is going on here?

[Aaron Liu]

See the docstring for docs#semiOutParam

[Aaron Liu]

Also see https://lean-lang.org/doc/reference/latest/Type-Classes/Instance-Synthesis/#class-output-parameters

[Robin Arnez]

i.e.

class Thing (T : semiOutParam Type) (U : Type) extends Coe T U

instance {T U : Type} [t : Thing T U] : Coe T U := t.toCoe