Optimize unification inner loop

[ttuegel]

The inner loop of the unification code has poor performance because using MaybeT involves sequencing many binds (>>=) in the underlying monad. We will separate the code which identifies unification problems from the code which solves the unification problem. A simplified schematic of the current code is:

unify
    :: TermLike variable
    -> TermLike variable
    -> MaybeT unifier (Pattern variable)
unify term1 term2 = 
    matchAndUnify1 term1 term2
    <|> matchAndUnify2 term1 term2
    <|> matchAndUnify3 term1 term2
    ...

unify could mean maybeTermAnd or maybeTermEquals.

We will split each matchAndUnifyN into a pair:

matchN :: TermLike variable -> TermLike variable -> Maybe problem
matchN = ...
{-# INLINE matchN #-}

unifyN :: problem -> unifier (Pattern variable)

problem stands for a data type representing each type of unification problem. It will be different for each pair of new functions. It is important that the matchN functions be inlined to make the pattern matching code more efficient, but they should be very small functions anyway. unify will take this simplified form:

unify term1 term2
  | Just problem1 <- match1 term1 term2 = unify1 problem1 & lift
  | Just problem2 <- match2 term1 term2 = unify2 problem2 & lift
  | Just problem3 <- match3 term1 term2 = unify3 problem3 & lift
  ...
  | otherwise = empty