New way to make the simplifier diverge
GHC's simplifier can go into a loop if you use fixpoints in a funny way, as documented here http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html\#bugs-ghc (12.2.1, third bullet). But GADTs provide new opportunities. This ticket records one, thanks to Ryan Ingram and Matthieu Sozeau:
{-# LANGUAGE GADTs #-}
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
Trac metadata
Trac field | Value |
---|---|
Version | 6.12.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |