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