[Haskell-cafe] Re: Non-termination of type-checking
Matthieu Sozeau
mattam at mattam.org
Fri Jan 29 17:26:28 EST 2010
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
More information about the Haskell-Cafe
mailing list