Explanation of a core-lint warning (Bad getNth)

Simon Peyton Jones simonpj at microsoft.com
Fri Jan 15 14:15:38 UTC 2016 

Maybe put this all on a ticket?

Everyone: would someone like to dig into this?  I’m so under water that I just can’t

Simon

From: Jan Bracker [mailto:jan.bracker at googlemail.com]
Sent: 15 January 2016 14:03
To: Simon Peyton Jones <simonpj at microsoft.com>
Cc: Richard Eisenberg <eir at cis.upenn.edu>; ghc-devs at haskell.org
Subject: Re: Explanation of a core-lint warning (Bad getNth)

I have condensed a self-contained plugin and an example application that reproduces the error. You can find it here:
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 in [1]. The plugin [2] 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 [3]. I have added checks to see if the evidence I produce contains the 'Nth' constructors the core-linter refers to [4,5], but the evidence produced does not contain them. So somehow the evidence triggers GHC to produce evidence that the core-linter warns about.

I hope this is comprehensible and you can help me with what is going on.

Best,
Jan

[1] https://github.com/jbracker/polymonad-plugin/blob/master/examples/core-error/Main.hs#L83
[2] https://github.com/jbracker/polymonad-plugin/blob/master/examples/core-error/MinimalPlugin.hs
[3] https://github.com/jbracker/polymonad-plugin/blob/master/examples/core-error/MinimalPlugin.hs#L198
[4] https://github.com/jbracker/polymonad-plugin/blob/master/examples/core-error/MinimalPlugin.hs#L130
[5] https://github.com/jbracker/polymonad-plugin/blob/master/examples/core-error/MinimalPlugin.hs#L556

2015-11-20 9:57 GMT+00:00 Simon Peyton Jones <simonpj at microsoft.com<mailto:simonpj at microsoft.com>>:
I don’t know how to help either, because there’s no way to reproduce it.  Can you find a Haskell program that, when GHC compiles it, produces this Lint error?  Or does it require your plugin?  If the latter, it’s hard to know what your plugin might be doing…

So I feel a bit stalled on how to help.

Simon

From: ghc-devs [mailto:ghc-devs-bounces at haskell.org<mailto:ghc-devs-bounces at haskell.org>] On Behalf Of Richard Eisenberg
Sent: 18 November 2015 17:14
To: Jan Bracker
Cc: ghc-devs at haskell.org<mailto:ghc-devs at haskell.org>
Subject: Re: Explanation of a core-lint warning (Bad getNth)

Ah yes. I looked too quickly. Note that there are two NthCo's listed. Its the outermost that's the problem, which is deconstructing the Union. But it's doing so to prove that '["thres" :-> Int] ~ '["thres" :-> Int] which is rather easy to prove without NthCo. I'm not sure why GHC is doing this.

Richard

On Nov 18, 2015, at 12:11 PM, Jan Bracker <jan.bracker at googlemail.com<mailto:jan.bracker at googlemail.com>> wrote:

Hi Richard,

No "Split" is a class and is defined here: http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect-State.html#t:Split<https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fhackage.haskell.org%2fpackage%2feffect-monad-0.6.1%2fdocs%2fControl-Effect-State.html%23t%3aSplit&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c7aa4db864c994205421c08d2f03ba9ca%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=FKQH9CvKCu6KszP1JbOnXOiu4DhhdgpRPWol6zQG41o%3d>
"Union" is a type function (synonym that refers to a type function call): http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect-Writer.html#t:Union<https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fhackage.haskell.org%2fpackage%2feffect-monad-0.6.1%2fdocs%2fControl-Effect-Writer.html%23t%3aUnion&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c7aa4db864c994205421c08d2f03ba9ca%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=%2f174TvSeTQ8J%2bAw3VXtSzNKsy8JpFsfDffQvkD7WtkE%3d>

thank you for your quick reply!

Best,
Jan

2015-11-18 17:05 GMT+00:00 Richard Eisenberg <eir at cis.upenn.edu<mailto:eir at cis.upenn.edu>>:
I took just a quick look at this. Is Split a type family? The NthCo coercion form takes apart a composite equality into its pieces. For example, if we know (Maybe a ~ Maybe b), then NthCo:0 will tell us that (a ~ b). In your case, it looks like GHC is trying to deduce (Union '["thres" :-> Int] []) ~ (Union '["thres" :-> Int] (Unit Reader)) from an equality of two (Split ...) types. If Split is a type family, this deduction is unsound. That may be what Core Lint is worried about.

I'm not surprised that the executable would run with an error. But it might not in the future. If -dcore-lint fails, it means that there is a potential type safety issue in the Core code, and this should be taken seriously.

I hope this helps!
Richard

On Nov 18, 2015, at 11:35 AM, Jan Bracker <jan.bracker at googlemail.com<mailto:jan.bracker at googlemail.com>> wrote:

Hi,

I am using the type checker plugin interface and I am trying to produce some evidence for type class instances. During compilation of one of my examples I get this core-lint error:

*** Core Lint errors : in result of Simplifier ***
<no location info>: Warning:
    [RHS of ds_a6bY :: (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))

I suppose "getNth" refers to the constructor "EvTupleSel" from "EvTerm", "TcNthCo" from "TcCoercion" or to "NthCo" from "Coercion". But I never produce evidence of the shape "getNth".  My evidence production code can be found at [1] and the only place where evidence of this shape can come from is my "evaluateType" function [2] that calls "normaliseType" from the GHC module "FamInstEnv". You can reproduce the error by checking out commit 144525886ec107af6f1283b26b19f8125c980aa4 from [3] and running "make effect-example" in the top directory of the repository (GHC 7.10 or better is required and a sandbox is automatically created).

The core-lint error does not seem to have any negative consequences when ignored. The produced executable works fine. Can somebody explain why it appears and maybe how I can fix it?

Thank you!
Jan

[1] https://github.com/jbracker/polymonad-plugin/blob/144525886ec107af6f1283b26b19f8125c980aa4/src/Control/Polymonad/Plugin/Evidence.hs#L177
[2] https://github.com/jbracker/polymonad-plugin/blob/144525886ec107af6f1283b26b19f8125c980aa4/src/Control/Polymonad/Plugin/Evaluate.hs#L29
[3] https://github.com/jbracker/polymonad-plugin
_______________________________________________
ghc-devs mailing list
ghc-devs at haskell.org<mailto:ghc-devs at haskell.org>
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.org%2fcgi-bin%2fmailman%2flistinfo%2fghc-devs&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c7aa4db864c994205421c08d2f03ba9ca%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=tediRvsqUcgRC%2bw5GVLOmxMMHWvYS%2bYai8rQbOtj7yM%3d>




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160115/5b52a7c0/attachment-0001.html>

More information about the ghc-devs mailing list