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
-- ryan
On Wed, Jan 27, 2010 at 8:27 AM, Matthieu Sozeau
Dear Haskellers,
while trying to encode a paradox recently found in Coq if one has impredicativity and adds injectivity of type constructors [1] I stumbled on an apparent loop in the type checker when using GADTs, Rank2Types and EmptyDataDecls.
{-# OPTIONS -XGADTs -XRank2Types -XEmptyDataDecls #-}
module Impred where
The identity type
data ID a = ID a
I is from (* -> *) to *, we use a partial application of [ID] here.
data I f where I1 :: I ID
The usual reification of type equality into a term.
data Equ a b where Eqrefl :: Equ a a
The empty type
data False
This uses impredicativity: Rdef embeds a (* -> *) -> * object into R x :: *.
data R x where Rdef :: (forall a. Equ x (I a) -> a x -> False) -> R x
r_eqv1 :: forall p. R (I p) -> p (I p) -> False r_eqv1 (Rdef f) pip = f Eqrefl pip
r_eqv2 :: forall p. (p (I p) -> False) -> R (I p) r_eqv2 f = Rdef (\ eq ax -> case eq of -- Uses injectivity of type constructors Eqrefl -> f ax)
r_eqv_not_R_1 :: R (I R) -> R (I R) -> False r_eqv_not_R_1 = r_eqv1
r_eqv_not_R_2 :: (R (I R) -> False) -> R (I R) r_eqv_not_R_2 = r_eqv2
rir :: R (I R) rir = r_eqv_not_R_2 (\ rir -> r_eqv_not_R_1 rir rir)
Type checking seems to loop here with ghc-6.8.3, which is a bit strange given the simplicity of the typing problem. Maybe it triggers a constraint with something above?
-- Loops -- absurd :: False -- absurd = r_eqv_not_R_1 rir rir
[1] http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/4322/focus=...
-- Matthieu _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe