Context {R: ringType} (U V: lmodType R).
Implicit Types (u v : {linear U -> V}).

Definition linear_zero : {linear U -> V} := [linear of 0].
Definition linear_neg u : {linear U -> V} := [linear of \- u].
Definition linear_add u v := [linear of u \+ v].

The following term contains unresolved implicit arguments:
  (fun u => [linear of \- u])
More precisely:
- ?l: Cannot infer an internal placeholder of type
  "GRing.Scale.law (R:=R) (V:=V)  *:%R" in
  environment:
  R : ringType
  U, V : lmodType R
  u : {linear U -> V}