Implementations for unrestricted functions are considered valid for linear functions

[aDifferentJT]

While this works for interfaces like:

interface Iface a where
  f : a -> ()
  g : (() -> a) -> ()
  h : ((a -> ()) -> ()) -> ()

the following code should not compile:

interface Iface a where
  create : a

Iface (a -> (a, a)) where
  create x = (x, x)

dup' : (1 _ : a) -> (a, a)
dup' = create

This is basically the problem of variance, if we consider linear functions a subtype of unrestricted functions then some interfaces are covariant, some contravariant and some invariant, though I'd rather not drag that in, instead I suggest we just make these incompatible.

[mb64]

This is fixed by #879. The compiler now says:

Error: While processing right hand side of dup'. Can't find an implementation for Iface ((1 _ : a) -> (a, a)).

test.idr:8:8--8:14
   |
 8 | dup' = create
   |        ^^^^^^