Formalise type abstraction (`E_type_abstraction`)
The implementation of the LIGO type checker permits the following typing rule:
| ( E_type_abstraction { type_binder = tvar; result }
, T_for_all { ty_binder = tvar'; kind; type_ } )
when TypeVar.equal tvar tvar' ->
let ctx, pos = Context.mark ctx in
let ctx, result =
check ~ctx:Context.(ctx |:: C_type_var (tvar', kind)) result type_
in
( Context.drop_until ctx ~pos
, let%bind result = result in
return @@ E_type_abstraction { type_binder = tvar; result } )
This behaviour of the type system needs to be reflected in the formalisation