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

[Ryan Ingram]

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 <mattam at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>