failed to synthesize ?

Stream: new members

[Anders Larsson]

Why does this work in Lean 3 but not in Lean 4?

constant a : Type
constant b : a → a

/tmp/lean_4_bad.lean:2:0: error: failed to synthesize
  Inhabited (a → _root_.a)

[Henrik Böving]

It does not work because the instance instance {α : Sort u} : Inhabited (α → α) := ⟨id⟩ seems to be missing from Lean 4 stdlib right now, add it and Lean will happily accept.

[Henrik Böving]

However this is maybe something we might actually want per default? CC @Sebastian Ullrich

[Anders Larsson]

It works, indeed. Thank you.

[Reid Barton]

constant has a quite different meaning in Lean 3

[Alex J. Best]

There is already https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L224 FYI, which would be a conflicting instance in most cases

[Henrik Böving]

If we were to prioritize that one higher though there should be no issue right?

[Alex J. Best]

The instance you suggest is "missing" from lean 3 too (at least I can't find a set of mathlib imports that makes this work):

variable {α : Type*}
#check (by apply_instance : inhabited (α → α))

so even if it wouldn't be an issue, it begs the question why would anyone ever want / need the type of functions from a type to itself to be inhabited when the type itself wasn't inhabited.
It just seems very niche, and seems to me a bit confusing that inhabiting alpha would change the default of α → α so much