Opened 8 years ago

Last modified 6 years ago

#3872 new bug

New way to make the simplifier diverge

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 6.12.1
Keywords: Cc: anton.nik@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


GHC's simplifier can go into a loop if you use fixpoints in a funny way, as documented here (12.2.1, third bullet). But GADTs provide new opportunities. This ticket records one, thanks to Ryan Ingram and Matthieu Sozeau:

module Contr where

newtype I f = I (f ())
data R o a where R :: (a (I a) -> o) -> R o (I a)

run :: R o (I (R o)) -> R o (I (R o)) -> o
run x (R f) = f x
rir :: (R o) (I (R o))
rir = R (\x -> run x x)

absurd :: a
absurd = run rir rir

Now the simplifier can loop. Look:

run rir rir

= {inline run}
  case rir of R f -> f rir

= {case of known constructor}
  let { f = \x -> run x x } in f rir

= {inline f}
  run rir rir

Change History (2)

comment:1 Changed 7 years ago by lelf

Cc: anton.nik@… added

comment:2 Changed 6 years ago by simonpj

See also #5400

Note: See TracTickets for help on using tickets.