Opened 2 years ago

Last modified 2 years ago

#11435 new bug

Evidence from TC Plugin triggers core-lint warning

Reported by: jbracker Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.2
Keywords: core-lint warning evidence type-checker plugin Cc:
Operating System: Linux Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The attached plugin and program produce a core-lint warning that refers to evidence the plugin did not produce.

High-Level description of what the plugin does and what happens

'flatFilter' produces the following ambiguous wanted constraints:

  Polymonad (Reader '["thres" :-> Int]) n (Reader '["thres" :-> Int]) (CNonCanonical)
  Polymonad (Reader '["thres" :-> Int]) m n (CNonCanonical)
  Polymonad Identity Identity m

To solve these the plugin does the following:

  1. It produces two type equality constraints:
      n ~ Identity (CNonCanonical)
      m ~ Reader '["thres" :-> Int] (CNonCanonical)
    
  2. As a result of these equality constraints the GHC constraint solver creates the following wanted constraint:
    Polymonad (Reader '["thres" :-> Int]) Identity (Reader '["thres" :-> Int]) (CNonCanonical)
    
    GHCs constraint solver can not pick an instance because several instances overlap:
    P.Monad f => Polymonad f Identity f
    ( Effect m, E.Inv m f (Unit m), f ~ Plus m f (Unit m)) => Polymonad (m (f :: [*])) Identity (m (f :: [*]))
    
    By trying to produce evidence for either of these instances the plugin determines that only the second instance is actually applicable and therefore selects it and produces evidence.

With this the constraints are solved and the type checking/constraint solving stage is done. During core linting we get the following error:

*** Core Lint errors : in result of Simplifier ***
<no location info>: Warning:
    [RHS of ds_a66V :: (Set '["thres" :-> Int], Set (Unit Reader))]
    Bad getNth:
      Nth:0
        (Nth:2
           (Sub (Sym (TFCo:R:Inv[]Readerfg[0] <'["thres" :-> Int]>_N <'[]>_N))
            ; (Inv
                 <Reader>_N <'["thres" :-> Int]>_N (Sym TFCo:R:Unit[]Reader[0]))_R
            ; Sub
                (TFCo:R:Inv[]Readerfg[0] <'["thres" :-> Int]>_N <Unit Reader>_N)))
      Split '["thres" :-> Int] '[] (Union '["thres" :-> Int] '[])
      Split
        '["thres" :-> Int]
        (Unit Reader)
        (Union '["thres" :-> Int] (Unit Reader))

As can be seen in the plugin [Check for 'Nth' constructor] the evidence produced by the plugin does not contain the 'Nth' constructor for coercions/evidence anywhere. Thus, the produced evidence seems to trigger GHC to produce these 'bad' coercions/evidence somewhere.

Building the Example

The example should be self-contained and reproduces the error whenever you try to build it. You can find it here or in the attachment: https://github.com/jbracker/polymonad-plugin/tree/master/examples/core-error

You just have to download the three files and run "cabal install" to reproduce the error. There is a high-level explanation of what is going on above and in the 'Main.hs' from line 83. The plugin 'MinimalPlugin.hs' is still around 600 lines long, but I have added a lot of comments to make it comprehensible.

I suppose the most interesting part is the production of evidence in 'MinimalPlugin.hs' from line 198. I have added checks to see if the evidence I produce contains the 'Nth' constructors the core-lint warning refers to in line 130 and 556 of the plugin, but the evidence produced does not contain them. So somehow the evidence triggers GHC to produce evidence that the core-linter warns about.

Attachments (1)

core-error.zip (9.6 KB) - added by jbracker 2 years ago.
Files of the core warning example

Download all attachments as: .zip

Change History (6)

Changed 2 years ago by jbracker

Attachment: core-error.zip added

Files of the core warning example

comment:1 Changed 2 years ago by goldfire

This thread sheds some light: https://mail.haskell.org/pipermail/ghc-devs/2015-November/010513.html Given that this ticket is the same issue as the one you raised there, it would be helpful for you to include that link when posting.

I notice that the problem occurs in the result of the simplifier. Could it be coercion optimization? Try with -fno-opt-coercion. Also, try with -O0. Does -fprint-explicit-kinds -fprint-explicit-foralls change the output? The report is made against GHC 7.10.2. Is that accurate? Has anyone reproduced with HEAD?

comment:2 Changed 2 years ago by thomie

-fno-opt-coercion makes the problem go away. Tested with ghc-7.10.3.

The plugin doesn't compile with GHC 8 or HEAD, without significant changes.

comment:3 Changed 2 years ago by goldfire

Drat. Sounds like a proper GHC bug.

Post the output with -fprint-explicit-kinds -fprint-explicit-foralls -ddump-tc -ddump-tc-trace -dverbose-core2core. Thanks!

comment:4 in reply to:  3 Changed 2 years ago by thomie

Replying to goldfire:

Post the output with -fprint-explicit-kinds -fprint-explicit-foralls -ddump-tc -ddump-tc-trace -dverbose-core2core. Thanks!

The resulting file is too big to attach here (15 Mb). Here is how you can generate it yourself with ghc-7.10.3:

git clone https://github.com/jbracker/polymonad-plugin
cd polymonad-plugin/examples/core-error
cabal sandbox init
cabal install --dependencies-only   # only takes a few seconds
cabal build --ghc-options='-fprint-explicit-kinds -fprint-explicit-foralls -ddump-tc -ddump-tc-trace -dverbose-core2core' > dump 2>&1

comment:5 in reply to:  2 Changed 2 years ago by jbracker

It's the same with ghc-7.10.2. The warning disappears when compiled with -fno-opt-coercion.

Replying to thomie:

-fno-opt-coercion makes the problem go away. Tested with ghc-7.10.3.

The plugin doesn't compile with GHC 8 or HEAD, without significant changes.

Note: See TracTickets for help on using tickets.