Support for user-defined ADTs

[ilyasergey]

• Automatic generation of recursion principles
• Check for well-foundedness

[jjcnn]

Custom ADTs have now been added to the language. The ADTs are checked and added in the new phase ADTChecker.

There is still no support for inductive or polymorphic ADTs, and there doesn't seem to be much point to having polymorphic ADTs without inductive ones, so inductive ones should be added first.

The intention is for ADTChecker to generate the necessary recursion principles for inductive ADTs, and add them to the library that defines the ADT. This should allow us to remove the current recursion principles altogether, which would make the interaction between parser, ADTChecker and typechecker more clean.

The issue is currently blocked by issue #179, because without caching of typechecked libraries we have nowhere to place the generated recursion principles.

[jjcnn]

We should restrict inductive ADTs to be uniformly recursive. This would prevent the user from defining types such as

type 'A MyType =
| Foo of 'A ((Pair 'A 'A) MyType)

type 'A 'B MyType2 =
| Bar of 'A ('B 'A MyType2)

Restricting inductive ADTs to be uniform makes it much, much easier to generate fold functions for the types, not to mention making typechecking easier.

[jjcnn]

The subtyping relation implemented by type_assignable currently assumes that type variables for ADTs cannot occur in contravariant positions. This assumption holds for all predefined ADTs, but will not hold in general for user-defined polymorphic ADTs. For example:

type ('A, 'B) MyType =
  | Foo of ('A -> 'B)

Type variables in contravariant positions either needs to not be allowed, or needs to be properly implemented in type_assignable.