[Haskell-cafe] Re: Non-termination of type-checking
Martin Sulzmann
martin.sulzmann.haskell at googlemail.com
Fri Jan 29 14:41:43 EST 2010
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
More information about the Haskell-Cafe
mailing list