kind of type variables must be given explicitely

[maeder]

currently "forall a . ..." or "var a" introduce a type variable of kind Type (without warning) that does not shadow a normal variable named "a".

The user is supposed to write "a : Type" explicitly. This needs to be adjusted in the language summary as well.

With forall and var both normal and type variables may be introduced. This (almost) forces the name space of classes and types to be disjoint in order to decide what kind of variable is declared.

I don't think the name space of types (incl. type variables) and functions (incl. normal variables) should be disjoint, but maybe a warning should be emitted for non-shadowing variables.

Another question is, if forall bindings of type variables may occur in subformulas like in

. true => forall a: Type ; x: a . x = x

[maeder]

type variable declaration within forall following a dot are now forbidden. Warnings are issued for overlapping identifiers for normal and type variables.