Bad UX when there is an implicit argument

[codyroux]

In, e.g.

inductive Total {α} : α → Prop where
| any a : Total a

derive_generator ∃ a, Total a

We get the following error:

?m.1 is expected to be a variable.

Ideally we'd create an implicit argument to the generator in this case, but a shorter term fix would be to make the error a bit more transparent, e.g.

(suggestion: use @Total instead of Total, and give all arguments)

[codyroux]

We should be calling the metavariable instantiation routine here, which would provide a reasonably clear error message.