Begin adding linearity and linear functions to Links.

This commit includes:

 - The (sub)kinds are enriched to distinguish between linear and
   unlimited types.

 - Usage of variables is tracked, and unlimited usage introduces either
   kind restrictions on type variables or type errors, as appropriate.

 - Linear functions (-@, ~@, &c.) and linear lambda expressions
   (linfun..) are introduced.  Unlimited lambda expressions cannot close
   over variables of linear type.

Significant work remains.  In particular, there is no parser support for
annotating type variables as linear or unlimited.  Thus, for instance,
while it is perfect reasonable to have the definition

  fun twice(x){(x,x)}

you cannot add the inferred type signature

  sig twice: (a::Unl) -> (a::Unl,a::Unl)