[Haskell-cafe] Non-termination of type-checking

[Matthew Brecknell]

Ryan Ingram wrote:
> The compiler doesn't loop for me with GHC6.10.4; I think GADTs still
> had some bugs in GHC6.8.
> 
> That said, this is pretty scary.  Here's a simplified version that
> shows this paradox with just a single GADT and no other extensions.
> No use of "fix" or recursion anywhere!
> 
> {-# 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

I think that's essentially the same as this:

data Fix a = Fix { unFix :: Fix a -> a }

run :: Fix a -> Fix a -> a
run x f = unFix f x

rir :: Fix a
rir = Fix (\x -> run x x)

absurd :: a
absurd = run rir rir

Non-positive recursive occurrences in type definitions provide various
ways to encode the Y-combinator in a typed lambda calculus, without the
need for any recursive "let" primitive. Haskell allows such non-positive
occurrences, but for strong normalisation, languages like Coq must
disallow them.

If you change "data" to "newtype" in the above, the GHC 6.10.4 compiler
(but not GHCi) will loop. I think this is just a case of the infelicity
documented here:

http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html

Regards,
Matthew