Too-eager variable capture in forall types

[japple]

h's type is ineffable: GHCi infers Capture a, but listing that type in the souce code fails the typecheck. Listing no type allows the following:

{-# OPTIONS_GHC -fglasgow-exts #-}

data Capture a = Base a
               | Capture (Capture (forall x . Divide x -> Divide a))

g :: Capture (forall a . Divide a -> Divide a)
g = Base id

h = Capture g

l :: Capture a
l = h

m :: Capture Int
m = h

data Divide a where
    Pint :: Int -> Divide Int
    Pbool :: Bool -> Divide Bool

foo :: Capture a -> Divide a
foo (Capture (Base f)) = f (Pbool True)

unfoo :: Divide a -> a
unfoo (Pint x) = x
unfoo (Pbool x) = x

oops = unfoo (foo h) -- Illegal instruction
oopsAgain = unfoo (foo l) -- Illegal instruction
oopsOnceMore = unfoo (foo m)
{-
<interactive>: internal error: interpretBCO: hit a CASEFAIL
    (GHC version 6.6 for i386_unknown_linux)
    Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
Aborted
-}

[igloo]

I'm seeing

<interactive>: internal error: stg_ap_v_ret
    (GHC version 6.6 for x86_64_unknown_linux)
    Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

for oops/oopsAgain rather than Illegal instruction, and the same CASEFAIL as the submitter for oopsOnceMore. HEAD is the same.

I'm not quite sure what's going on here. Is the monomorphism restriction allowing the a to be unified with the x in h?

Sounds like one for you, Simon!

[simonpj]

Always try -dcore-lint first! That nails it to the desugarer, and/or the typechecker. I'll take it.

Simon

[simonpj]

This is a plain bug in the type checker. The program should clearly be rejected. I've fixed the bug.

MERGE to 6.6.1 branch

Tue Feb 6 16:54:56 GMT 2007 simonpj@…

Check for escape when unifying forall-types

Simon

[igloo]

Merged.