Opened 14 years ago

Last modified 4 years ago

#344 new bug (None)

arrow notation: incorrect scope of existential dictionaries

Reported by: nobody Owned by: ross
Priority: lowest Milestone:
Component: Compiler (Type checker) Version: 6.4
Keywords: Arrows Cc: ross@…, abcz2.uprola@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

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>

Attachments (1)

GHCbug.2.lhs (865 bytes) - added by nobody 14 years ago.

Download all attachments as: .zip

Change History (33)

Changed 14 years ago by nobody

Attachment: GHCbug.2.lhs added

comment:1 Changed 14 years ago by 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>

comment:2 Changed 14 years ago by 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

comment:3 Changed 14 years ago by 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>

comment:4 Changed 13 years ago by simonpj

Architecture: Unknown
Description: modified (diff)
difficulty: Unknown
Milestone: 6.8
Operating System: Unknown

comment:5 Changed 13 years ago by 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?

comment:6 Changed 12 years ago by simonmar

Cc: Ross Paterson <ross@…> added

comment:7 Changed 12 years ago by simonpj

Owner: changed from simonpj to ross
Status: assignednew

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

comment:8 Changed 12 years ago by ross

Cc: ross@… added; Ross Paterson <ross@…> removed
Summary: double-panic with GADTsarrow notation: incorrect scope of existential dictionaries

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.

comment:9 Changed 11 years ago by igloo

Milestone: 6.8 branch6.10 branch

comment:10 Changed 11 years ago by 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

comment:11 Changed 11 years ago by simonmar

Architecture: UnknownUnknown/Multiple

comment:12 Changed 11 years ago by simonmar

Operating System: UnknownUnknown/Multiple

comment:13 Changed 10 years ago by igloo

Milestone: 6.10 branch6.12 branch

comment:14 Changed 10 years ago by simonmar

Type of failure: None/Unknown

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.

comment:15 Changed 10 years ago by simonmar

Type of failure: None/UnknownCompile-time crash

comment:16 Changed 9 years ago by igloo

Milestone: 6.12 branch6.12.3

comment:17 Changed 9 years ago by igloo

Milestone: 6.12.36.14.1
Priority: normallow

comment:18 Changed 9 years ago by igloo

Milestone: 7.0.17.0.2

comment:19 Changed 8 years ago by igloo

Milestone: 7.0.27.2.1

comment:20 Changed 8 years ago by igloo

Milestone: 7.2.17.4.1

comment:21 Changed 8 years ago by igloo

Milestone: 7.4.17.6.1
Priority: lowlowest

comment:22 Changed 7 years ago by danbst

Cc: abcz2.uprola@… added

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?

comment:23 Changed 7 years ago by 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.

comment:24 Changed 7 years ago by ross

Alternatively, it could be translated as

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

comment:25 Changed 7 years ago by igloo

Milestone: 7.6.17.6.2

comment:26 Changed 6 years ago by simonpj@…

commit c3ad38d7dc39ef583ddfb586413baa2e57ca3ee8

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Mon Mar 4 09:40:56 2013 +0000

    Rearrange the typechecking of arrows, especially arrow "forms"
    
    The typechecking of arrow forms (in GHC 7.6) is known to be bogus, as
    described in Trac #5609, because it marches down tuple types that may
    not yet be fully worked out, depending on when constraint solving
    happens.  Moreover, coercions are generated and simply discarded.  The
    fact that it works at all is a miracle.
    
    This refactoring is based on a conversation with Ross, where we
    rearranged the typing of the argument stack, so that the arrows
    have the form
       a (env, (arg1, (arg2, ...(argn, ())))) res
    rather than
       a (arg1, (arg2, ...(argn, env))) res
    as it was before.
    
    This is vastly simpler to typecheck; just look at the beautiful,
    simple type checking of arrow forms now!
    
    We need a new HsCmdCast to capture the coercions generated from
    the argument stack.
    
    This leaves us in a better position to tackle the open arrow tickets
     * Trac #5777 still fails.  (I was hoping this patch would cure it.)
     * Trac #5609 is too complicated for me to grok.  Ross?
     * Trac #344
     * Trac #5333

 compiler/deSugar/Coverage.lhs     |    3 +
 compiler/deSugar/DsArrows.lhs     |  486 +++++++++++++++++++++----------------
 compiler/hsSyn/HsExpr.lhs         |   13 +-
 compiler/hsSyn/HsUtils.lhs        |    7 +-
 compiler/parser/Parser.y.pp       |    4 +-
 compiler/parser/RdrHsSyn.lhs      |    4 +-
 compiler/rename/RnExpr.lhs        |    4 +-
 compiler/rename/RnTypes.lhs       |    2 +-
 compiler/typecheck/TcArrows.lhs   |  272 ++++++++++-----------
 compiler/typecheck/TcHsSyn.lhs    |    6 +-
 docs/users_guide/glasgow_exts.xml |   48 +++--
 11 files changed, 461 insertions(+), 388 deletions(-)

comment:27 Changed 5 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:28 Changed 5 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:29 Changed 5 years ago by thoughtpolice

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:30 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:31 Changed 4 years ago by thomie

Keywords: Arrows added

comment:32 Changed 4 years ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.