Matthieu Sozeau mattam at mattam.org
Wed Jan 27 11:27:38 EST 2010

```Dear Haskellers,

while trying to encode a paradox recently found in Coq if one has
impredicativity and adds injectivity of type constructors  I
stumbled on an apparent loop in the type checker when using GADTs,

> 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