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

[Martin Sulzmann]

On Fri, Jan 29, 2010 at 8:56 AM, <oleg at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100129/d295e8a9/attachment.html