Evidence from TC Plugin triggers core-lint warning

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)

1. 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.

Trac metadata

Trac field	Value
Version	7.10.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture