Am Freitag 29 Januar 2010 23:26:28 schrieb Matthieu Sozeau:
Le 29 janv. 10 à 02:56, oleg@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.
The c in "data R c" has nothing to do with the c in "R :: (c (c ()) -> False) -> R (c ())" It would probably have been less confusing to declare it data R :: * -> * where R :: (c (c ()) -> False) -> R (c ())
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