[Haskell-cafe] an evil type hangs GHC

[Petr Pudlak]

On Fri, Nov 12, 2010 at 07:52:53PM +0100, Petr Pudlak wrote:
>Hi, I was playing with the following example I found in D.A.Turner's 
>paper Total Functional Programming:
>
>>data Bad a = C (Bad a -> a)
>>
>>bad1 :: Bad a -> a
>>bad1 b@(C f) = f b
>>
>>bad2 :: a
>>bad2 = bad1 (C bad1)
>
>To my surprise, instead of creating a bottom valued function (an 
>infinite loop), I managed to send the GHC compiler (ver. 6.12.1) to 
>an infinite loop. Could anybody suggest an explanation? Is this a GHC 
>bug? Or is this "Bad" data type so evil that type checking fails?
>
>    Thanks,
>    Petr

PS: The following code compiles, the difference is just in modifying 
"bad2" to include an argument:

> data Bad a = C (Bad a -> a)
> 
> bad1 :: Bad a -> a
> bad1 b@(C f) = f b
> 
> bad2 :: (a -> a) -> a
> bad2 f = bad1 (C $ f . bad1)

[BTW, "bad2" has the type of the Y combinator and indeed works as 
expected:

> factorial :: (Int -> Int) -> Int -> Int
> factorial _ 0 = 1
> factorial r n = n * (r (n-1))
> 
> main :: IO ()
> main = print $ map (bad2 factorial) [1..10]

... so one can get general recursion just by crafting such a strange 
data type.]
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20101112/2e4a7fed/attachment.bin