#344: arrow notation: incorrect scope of existential dictionaries
-------------------------------------+--------------------------------------
Reporter: nobody | Owner: ross
Type: bug | Status: new
Priority: normal | Milestone: 6.8 branch
Component: Compiler (Type checker) | Version: 6.4
Severity: normal | Resolution: None
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown
Os: Unknown |
-------------------------------------+--------------------------------------
Changes (by ross):
* cc: Ross, Paterson, <[EMAIL PROTECTED]> (removed)
* cc: [EMAIL PROTECTED] (added)
* summary: double-panic with GADTs => arrow notation: incorrect scope of
existential dictionaries
Comment:
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/344#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
