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

[Matthieu Sozeau]

Le 29 janv. 10 à 02:56, oleg at okmij.org a écrit :

>
> Here is a bit more simplified version of the example. The example has
> no value level recursion and no overt recursive types, and no  
> impredicative
> polymorphism. The key is the observation, made earlier, that two types
> 	c (c ()) and R (c ())
> unify when c = R. Although the GADTs R c below is not recursive, when
> we instantiate c = R, it becomes recursive, with the negative
> occurrence. The trouble is imminent.
>
> We reach the conclusion that an instance of a non-recursive GADT
> can be a recursive type. GADT may harbor recursion, so to speak.
>
> The code below, when loaded into GHCi 6.10.4, diverges on
> type-checking. It type-checks when we comment-out absurd.
>
>
> {-# LANGUAGE GADTs, EmptyDataDecls #-}
>
> data False				-- No constructors
>
> data R c where				-- Not recursive
>    R :: (c (c ()) -> False) -> R (c ())

Thanks Oleg,

   that's a bit simpler indeed. However, I'm skeptical on
the scoping of c here. Correct me if I'm wrong but in R's
constructor [c] is applied to () so it has to be a type
constructor variable of kind :: * -> s. But [c] is also
applied to [c ()] so we must have s = * and c :: * -> *.
Now given the application [R (c ())] we must have
[R :: * -> *]. Then in [data R c] we must have [c :: *],
hence a contradiction?

   My intuition would be that the declaration is informally
equivalent to the impredicative:

data R (c :: *) where
   R :: forall c' :: * -> *, (c' (c' ()) -> False) -> R (c' ()).

-- Matthieu