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"