Local types

[janmasrovira]

It is often the case that we define a top level type that we only use in a function. It is also likely that we use tuples or generic sum types (such as either) in places where an adhoc type would be more adequate. In order to solve that, it would be useful to have the option to define types in a local scope.

Syntax: In a let expression, we would include a new kind of item, which would have the same syntax as top level type declarations. I.e.

let {
  type T : Type {
    t : T
  };
  id : T -> T;
  id t := t;
} in ...

If we don't allow free variables in local type definitions, it should not be hard to implement. We can trivially lift all local types to the top level. If free variables can appear, then it becomes more involved and we would need to do something similar to lambda lifting. Because of that, it makes sense to implement this in two stages.