Error message in class argument

Stream: lean4

[Patrick Massot]

I think that auto-implicit arguments make it hard to understand what happens when you make a typo in a type class argument.

example {α : Type} [foo α] : true :=
 rfl

gives error

invalid binder annotation, type is not a class instance
  ?m.10
use the command `set_option checkBinderAnnotations false` to disable the check

which becomes a much clearer unknown identifier 'foo' when disabling autoImplicit.

[Scott Morrison]

I regularly find this one unhelpful, too.