On Fri, Jan 29, 2010 at 8:56 AM, <o...@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 > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe