Haskell program aborts with "loop" but I think it shouldn't

Question

I have this Haskell code which when compiled with GHC and run, aborts with a loop detected.

data Foo = Foo ()
 deriving (Eq,Show)

type Foop = Foo -> ((),Foo)

noOp :: Foop
noOp st = ((),st)

someOp :: Foop
someOp st@(Foo x) = ((),st)

(<+>) :: Foop -> Foop -> Foop
(<+>) f g st = let ((_,st'),(_,st'')) = ((f st),(g st')) in ((),st'')

main = print $ (noOp <+> someOp) $ Foo ()

I think it shouldn't, and here are some modifications. Each of them makes the loop go away:

• change data Foo to newtype Foo
• change (noOp <+> someOp) to (someOp <+> noOp)
• remove the deconstruction @(Foo x)

Is this a bug in GHC or is it my lack of understanding the evaluation process?

Answer 1

• Pattern match (_, _) demands WHNF of (f st, g st'). Easy.
• Pattern match (_, (_,_)) demands WHNF of g st'. Here's the problem, because g is strict, hence it first needs st' in WHNF too. The runtime finds st' in the pattern ((_,st'), (_,_)), so before it can actually traverse down into st' it needs to WHNF both of the tuples. Because g is strict however, this first requires st'... and so on.

If you match the result of g with a lazy irrefutable pattern

(<+>) f g st = let ((_,st'), ~(_,st'')) = (f st, g st') in ((),st'')

then the problem goes away, because this is evaluated thus:

• Pattern match (_, _) demands WHNF of (f st, g st'). Easy.
• Pattern match (_, ~(_,_)) demands nothing more for the time being.
• Pattern match ((_,st'), ~(_,_)) demands WHNF of f st. Fortunately, we can fulfill this, because st does not depend on the pattern.
• Now we've satisfied the pattern match, the runtime can already proceed with the in ((),st''). Only at this point is the irrefutable pattern ~(_,st'') forced, but this is now not a problem anymore because st' is available here, so it's just a matter of computing g once.

The fixes you've tried all amount to making g non-strict:

remove the deconstruction @(Foo _)

Without that, g doesn't really need to look at its argument to construct the result skeleton, i.e. the tuple match (_,st'') can then succeed without first requiring WHNF of st'.

change data Foo to newtype Foo

This has the effect that the Foo constructor doesn't actually exist at runtime, so there's nothing that the pattern st@(Foo _) would force.

change noOp <+> someOp to someOp <+> noOp

As I said, the loop only comes about because g is strict. If you put f in its position, which is not strict, then there's no problem.