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 <mat...@mattam.org> wrote: > 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=1405 > > -- Matthieu > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe