[Haskell-cafe] Higher-order unification

[Lyle Kopnicky]

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
>
>
>  
>