Bug in GHC type system

Hi,

I have found a three-line program that will cause recent GHC type checker 
to diverge. The program is admittedly pathological, so here's the story:

As part of my PhD thesis I am investigating a backend virtual machine for 
functional programs where

  * beta reduction is explicit,
  * consequently, (->) is a free type constructor that can be mixed with
    (*) and (+) in arbitrary mutual recursion.

In such a system, is possible to define a well-typed, effective Y 
combinator. Of course, the reduction strategy has to be hand-coded 
explicitly. Since the lazy strategy is not the worst choice, I tried to 
abuse the Haskell type system for an experiment:

> y f = w w
>   where w x = f (x x)

This is, naturally, rejected by the type checker because of recursive type 
equations of the form:

> t = t -> u

But one can put a datatype constructor in between:

> newtype Auto a = { self :: Auto a -> a }
> y f = self w w
>   where w = Auto (\x -> f (self x x))

Sadly, I cannot load this program into GHCi or compile it with GHC. HUGS 
(as of November 2003) has no such problem, and computes the factorial 
function:

> let fac f x = if x == 0 then 1 else x * f (x - 1)
>  in y fac 10


Technical details:

  x86 PC with AMD Athlon XP CPU
  SuSE 9.0 Linux with kernel 2.6.10
  ghc-6.2.2

  also observed for 6.4 on a different machine

The log of `ghc -v -C Ups.hs` is attached. The compiler hangs after the

> *** Simplify:

line, slowly consuming unbounded amounts of heap (presumably due to a 
divergent type unification). The last two log lines are issued only after 
a ^C signal. If 'newtype' is replaced by 'data', one more line of 
statistics

>     Result size = 17

is issued before the compiler hangs, too.


Greetings,

Baltasar Trancon y Widemann

Ups.hs
Description: Text document

Ups.log
Description: Text document

_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs