On Wed, Apr 04, 2007 at 07:16:35PM -0700, Paul Berg wrote:
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"
I honestly don't understand the algorithm. (And I don't have tapl!!) So, ... quickcheck! You've seen my occurs-free unifier; now write an Arbitrary instance for trees and check that they always give the same result. "The chance of a common bug is neglible.". Stefan