[Haskell-cafe] Non-termination of type-checking

[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=1405

-- Matthieu