No error reported about wrong use of `\use \coerce`

[sxhya]

\instance FreeMonoidConstr (S : \Set) : Monoid \cowith
  | E => List S
  | ide => nil
  | * (a1 : List S) (a2 : List S) => a1 ++ a2
  | ide-left => idp
  | ide-right => ++_nil
  | *-assoc => ++-assoc

\use \coerce letter {S : \Set} (s : S) : FreeMonoidConstr S => s :: nil