On Fri, Jan 29, 2010 at 8:56 AM,
<oleg@okmij.org> wrote:
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 ())
-- instantiate c to R, so (c (c ())) and R (c ()) coincide
-- and we obtain a recursive type
-- mu R. (R (R ()) -> False) -> R (R ())
cond_false :: R (R ()) -> False
cond_false x@(R f) = f x
absurd :: False
absurd = cond_false (R cond_false)
GHC (the compiler terminates)
The following variants terminate, either with GHCi or GHC,
absurd1 :: False
absurd1 = let x = (R cond_false)
in cond_false x
absurd2 = R cond_false
absurd3 x = cond_false x
absurd4 :: False
absurd4 = absurd3 absurd2
This suggests there's a bug in the type checker.
If i scribble down the type equation, I can't see
why the type checker should loop here.
-Martin