arrow notation: incorrect scope of existential dictionaries

[nobody]

ghc-6.4: panic! (the `impossible' happened, GHC version
6.4):
        cgPanic
    deref{v a1yz}
    static binds for:
    local binds for:
    SRT labelghc-6.4: panic! (the `impossible'
happened, GHC version 6.4):
        initC: srt

Please report it as a compiler bug to
glasgow-haskell-bugs@haskell.org,
or http://sourceforge.net/projects/ghc/.

I've attached a test driver that can reproduce the problem.

-- Esa Pulkkinen <esa.pulkkinen@kotiposti.net>

[nobody]

Logged In: NO 

Fwiw, here's a trimmed-down version of the above program.

{-# OPTIONS -farrows -fglasgow-exts #-}
class Foo a where foo :: a -> ()
data Bar = forall a. Foo a => Bar a

get :: Bar -> ()
get = proc x -> case x of Bar a -> do foo -< a

-- Thomas Jäger <ThJaeger@gmail.com>

[nobody]

Logged In: NO 

The short version is a great help.

I think this program should yield a type error. The value of foo
here is a component of the local variable x, and therefore
should
be unavailable to the left of -<.  I've no idea how to
implement it,
though -- presumably a constraint on the free type vars on the
left of -<.

-- Ross

[nobody]

Logged In: NO 

Thank you, this information allowed me to find a workaround.
I need to just use -<< instead of -< for this, and the
problem disappears.

-- Esa Pulkkinen <esa.pulkkinen@kotiposti.net>

[igloo]

I can't reproduce this in 6.6, but I also can't get anything that the compiler accepts. I'm not sure if that's expected?

[simonpj]

Dear Ross,

As I understand it, this is a significant (i.e. not trivially fixable) bug in the typechecking of arrow syntax: we need to gather separate constraint sets to the left of -< and elsewhere. Or something; I'm not quite sure what.

Is that right? Can you update the description of the bug so that it describes the actual problem (it's nothing to do with GADTs)?

What do you want to do about it? The current state of affairs (arrow-syntax programs can pass the typechecker but generate bogus code) is rather unsatisfactory.

Thanks

Simon

[ross]

Both examples are rejected by GHC 6.6 and 6.8 (and they should be), but with confusing error messages. For Thomas's simpler example

{-# OPTIONS -farrows -fglasgow-exts #-}
class Foo a where foo :: a -> ()
data Bar = forall a. Foo a => Bar a

get :: Bar -> ()
get = proc x -> case x of Bar a -> do foo -< a

the message is

    Ambiguous type variable `a' in the constraint:
      `Foo a' arising from use of `foo' at ArrBug.hs:8:38-40
    Probable fix: add a type signature that fixes these type variable(s)

Thomas's example is equivalent to defining get as

get :: Bar -> ()
get = arr (\ x -> case x of Bar a -> a) >>> foo

and should fail in a similar way: the type of an expression on the right of -< escapes the scope of the local pattern binding (proc or <-) and thus must not contain quantified type variables bound by those patterns. (I don't know how to achieve that, though.)

However, here's a variation that fails core lint:

get = proc x -> case x of Bar a -> do {y <- id -< a; id -< foo a}

This is translated to

get = arr (\ x -> case x of Bar a -> a) >>>
      id &&& id >>>
      arr (\ (y, a) -> foo a)

The last expression needs foo, but it doesn't get passed through the bypass arrow like a does. A simple solution might be to say that this should be rejected on the same grounds as the previous example: the expression to the right of the first -<, namely a, allows a quantified type variable to escape.

[simonpj]

Ross says: This will be a hard one, because it needs an intimate understanding of both the type checker and the arrow desugarer. Certainly not before the 19th (Sept 08).

Fair enough. If you could get to it before 6.10.2 that would be great.

Simon

[simonmar]

To summarise, here's the program that fails core lint:

{-# OPTIONS -farrows -fglasgow-exts -dcore-lint #-}
module GHCbug where

class Foo a where foo :: a -> ()
data Bar = forall a. Foo a => Bar a

get :: Bar -> ()
get = proc x -> case x of Bar a -> do {y <- id -< a; id -< foo a}

Still failing in 6.12.1 RC.

[danbst]

Even smaller, which fails core-lint

{-# LANGUAGE Arrows, ExistentialQuantification #-}
{-# OPTIONS -dcore-lint #-}
module GHCbug where

class Foo a where foo :: a -> ()
data Bar = forall a. Foo a => Bar a

get :: Bar -> ()
get = proc x -> case x of Bar a -> id -< foo a

but I cannot figure, 1) what it should be desugared to:

get = arr (\x -> case x of Bar a -> foo a) >>> id

? 2) why does it compile without -dcore-lint? What part of GHC is bug hidden in?

[ross]

1) It would need to be desugared to something that passed the Foo dictionary explicitly, approximately:

get = arr (\x -> case x of Bar d a -> (d,a)) >>> arr (\(d,a) -> foo d a) >>> id

2) core-lint failures are usually either bugs in the desugarer or failure of the typechecker to reject something that should be rejected. The original report was a typechecker bug (now fixed); this one is a desugarer bug.

[ross]

Alternatively, it could be translated as

get = arr (\x -> case x of Bar a -> (foo,a)) >>> arr (\(foo,a) -> foo a) >>> id