[Haskell-cafe] My Unification Sorrows

[Stefan O'Rear]

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