synthInstances & universe metavariables

Stream: lean4 dev

[Reid Barton]

Lean 4 seems to apply instances even when they will later lead to unsolvable universe unification problems.
I believe Lean 3 did not do this (based on trying to port some mathlib file).

set_option pp.universes true

structure X (α : Sort _) where
  x : α

class C (α : Sort _) where
  h : α → α

instance MyInstance (α : Type _) : C α where
  h := id

instance (priority := low) MyInstance2 (α : Sort _) : C α where
  h := id

universe u

set_option trace.Meta.synthInstance true in
def f {α : Sort u} : X α → X α := C.h