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