[GHC] #11435: Evidence from TC Plugin triggers core-lint warning

[GHC]

#11435: Evidence from TC Plugin triggers core-lint warning
-------------------------------------+-------------------------------------
           Reporter:  jbracker       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.2
           Keywords:  core-lint      |  Operating System:  Linux
  warning evidence type-checker      |
  plugin                             |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11435>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler