CylinderTypes branch: Unification does not seem to respect normalisation

[alexarice]

In #17 I have implemented some reduction relations. We would expect that unification is able to unify definitionally equal terms but this does not seem to be the case. I believe a fallback case of the unification algorithm has gone missing somewhere between all the different branches (in particular the case that tries to completely unfold both values).

An example of this not working can be seen in the current (as of Web 07 Apr) version of #17 with the unification algorithm giving the following error:

Typing error:

The expression:

 unitor g

has type:

  [comp g (id y) => g]

but was expected to have type:

 [g => _ C x y f g a]

even though we get the following reduction above:

Checking definition: test
Checking complete for test
Type: {C : Cat} {x : [C]} {y : [C]} (f : [x => y]) -> [x => y]
Term: \{C}. \{x}. \{y}. \f. comp f (id y)
Type unfolded: {C : Cat} {x : [C]} {y : [C]} (f : [x => y]) -> [x => y]
Term unfolded: \{C}. \{x}. \{y}. \f. f

[alexarice]

This was caused by the reduction not correctly functioning on top level definitions