[Haskell-cafe] My Unification Sorrows

[Paul Berg]

I believe I may have found a solution (I *think* it's correct):

The occurs check needs to stay, but be modified for infinite types.
When the occurs check is true, instead of failing, we should keep the
constraint, but skip performing substitution on the rest of the list
of constraints.  This allows us to not fall into the trap of an
infinite substitution loop.  So, unify becomes, in the case of
infinite types:

-- | Given a list of constraints, unify those constraints,
-- finding values for the type variables
unify :: (Monad m, Functor m) => [Constraint] -> m [Constraint]
unify []                                   = return []
unify ((t1 ,          t2)           :rest)
  | t1 == t2                               = unify rest
unify ((tyS,          tyX@(TVar _)) :rest)
-- | tyX `occursIn` tyS                     = fail "Infinite Type"
  | tyX `occursIn` tyS                     = fmap ((tyX,tyS):) (unify rest)
  | otherwise                              = fmap ((tyX,tyS):) (unify
$ substinconstr tyX tyS rest)
unify ((tyX@(TVar _), tyT)          :rest) = unify $ (tyT,tyX) : rest
unify ((tyS1 :-> tyS2,tyT1 :-> tyT2):rest) = unify $ (tyS1,tyT1) :
(tyS2,tyT2) : rest
unify _                                    = fail "Unsolvable"