In our type reconstruction algorithm from the lecture, type reconstruction is done by solving a unification problem. Your task is to implement type unification according to Robinson's algorithm in Funnel.

Here's the abstract syntax of types:

  Type = TVar String
       | Arrow Type Type
       | TCon String {Type}

Types are implemented according to the visitor pattern. Now try to find a good representation for substitutions. A substitution is a set of equations t == T where type variable t does not occur in type T.

You should implement function mgu:

  def mgu(T: Type, T': Type)(s: Subst): Subst = ... 

which takes two types T and T' and a substitution s and returns a new substitution s' so that

• s' T == s' T', and
• s' s = s'.

Finally, you should implement function tp which makes use of the allready defined function mgu:

  def tp(env: Env, E: Tree, T: Type)(s: Subst): Subst = ...

You can use the framework provided in Unify.fnl