This is an example @JasonGross, why this is useful I have no idea:
Class M (n : nat).
Definition equiv1 `{M} : Type. Admitted.
Fail Definition equiv2 `{!M} : Type.
Generalizable Variables n.
Definition equiv3 `{!M n} : Type. Admitted.
This is an example @JasonGross, why this is useful I have no idea:
Class M (n : nat).
Definition equiv1 `{M} : Type. Admitted.
Fail Definition equiv2 `{!M} : Type.
Generalizable Variables n.
Definition equiv3 `{!M n} : Type. Admitted.