deriving DecidableEq in parametric inductive

Stream: lean4

[Horațiu Cheval]

I would have expected

inductive Wrapper (α : Type)
| mk : α → Wrapper α
deriving DecidableEq

to return an error since it is clearly false for arbitrary α. But it seems that Lean will try to synthesize instances on a cases by cases basis after an instantiation of α.

example (n m : Wrapper (Nat)) : Bool := if n = m then true else false
example (n m : Wrapper (Nat → Nat)) : Bool := if n = m then true else false

The first line works, while the second rightfully throws a failed to synthesize typeclass. Am I understanding this right?

[Sébastien Michelland]

The derived instance for Wrapper is indeed parametrized by the instance for α:

#print instDecidableEqWrapper
-- def instDecidableEqWrapper : {α : Type} → [inst : DecidableEq α] → DecidableEq (Wrapper α) :=
--   fun {α} [DecidableEq α] => [anonymous]