See http://www.haskell.org/pipermail/haskell/2006-September/018497.html On Fri, 12 Nov 2010, Petr Pudlak wrote:

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

-- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''

On 11/12/10 4:53 PM, Ryan Ingram wrote:

...

From http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/bugs.html#bugs-ghc:

GHC's inliner can be persuaded into non-termination using the standard way to encode recursion via a data type:

More specifically, since your bad2 does not look recursive, the inliner will get inline happy and apply the definition of bad1, but then it'll see a constant case match that it can reduce statically, and <loop> { okay, let's start with bad1 } bad1 b@(C f) = f b { mmm, tasty tasty sugar } bad1 = \b -> case b of C f -> f b { ha, dare you to optimize that further } { okay, now let's co compile bad2 } bad2 = bad1 (C bad1) { oh look, it's nonrecursive so let's start inlining } bad2 = (\b -> case b of C f -> f b) (C bad1) { oh look, an application we can evaluate statically } bad2 = let b = (C bad1) in case b of C f -> f b { meh, let's ignore sharing for now } bad2 = case (C bad1) of C f -> f (C bad1) { oh look, a case analysis we can evaluate statically } bad2 = let f = bad1 in f (C bad1) { oh look, f is only used once so we can substitute the let } { and if we didn't ignore sharing before, then we'd see that b is only used once now, so we could substitute that let too } bad2 = bad1 (C bad1) { oh look, it's nonrecursive so let's start inlining } -- Live well, ~wren