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

Matthew Brecknell matthew at brecknell.net
Wed Jan 27 19:49:13 EST 2010

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:



More information about the Haskell-Cafe mailing list