JonasDuregard

No special cases please! :) An expression like Cons x xs is (from the perspective of the type checker) just a function application, so if you can type check function...

That is what I meant by them being just function applications. The case you need to think about is EConstr. It is currently wildly incorrect (type constructors are not the...

Regarding "finding the next element", that is the job of the interpreter. The type checker has no notion of this, it traverses the expression it type checks not the values...

Regarding recursion, it's a bit tricky when polymorphism is involved. It seems the standard approach for `let x = e1 in e2` is something like this: 1. Introduce a new...