Yeah, here's a program which causes GHC to hang on compilation, but causes no problem for hugs. Does this qualify as higher-order unification?
newtype X a = X (X a -> a)
selfapp :: X a -> a selfapp self@(X f) = f self
omega :: a omega = selfapp (X selfapp)
loop = omega :: ()
y f = (f . selfapp) (X (f . selfapp))
fact0 f n = if n==0 then 1 else n * f (n-1)
fact = y fact0
-- Lyle Kopnicky
Carl Witty wrote:
On Tue, 2004-08-31 at 10:00, Chung-chieh Shan wrote:
The rationale for disallowing matching partially-applied type synonyms
is that higher-order unification is undecidable.
Higher-order unification is worse than just undecidable (after all, GHC's extended Haskell already includes constructs which are undecidable, which means that sometimes the compiler will loop forever); it's ambiguous. There can be multiple unifiers, none of which is the most general. See my earlier Haskell-cafe message for the trouble this can cause (search for "<technical note>"):
http://www.haskell.org/pipermail/haskell-cafe/2004-March/005965.html
Carl Witty
_______________________________________________ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
