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
