[GHC] #3872: New way to make the simplifier diverge

[GHC]

#3872: New way to make the simplifier diverge
---------------------------------+------------------------------------------
    Reporter:  simonpj           |        Owner:              
        Type:  bug               |       Status:  new         
    Priority:  normal            |    Milestone:  _|_         
   Component:  Compiler          |      Version:  6.12.1      
    Keywords:                    |   Difficulty:              
          Os:  Unknown/Multiple  |     Testcase:              
Architecture:  Unknown/Multiple  |      Failure:  None/Unknown
---------------------------------+------------------------------------------
 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
 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3872>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler