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

[Daniel Fischer]

Am Freitag 29 Januar 2010 23:26:28 schrieb 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.

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