Error message for constructor variables implicitly escaping into sizes

[ollef]

This currently crashes the compiler:

type Vect (n : Nat) t where
    Nil : forall t. Vect Zero t
    Cons : forall n t. t -> Vect n t -> Vect (Succ n) t

It's an illegal type (without boxed), because the compiler can't determine the size of the type from its parameters. This is the case because the size depends on variables (n and t) local to the constructors. It would work if we implemented #134, but there are other similar cases that still won't work.

We should add a proper error message for variables escaping from constructor types into the size calculation function instead of crashing.