Re: Help needed: Restrictions of proc-notation with RebindableSyntax
Simon, Richard, thank you for your answer! I don't have time to look into the GHC sources right now, but I will set aside some time after the holidays and take a close look at what the exact restrictions on proc-notation are and document them. Since you suggested a rewrite of GHC's handling of proc-syntax, are there any opinions on integrating generalized arrows (Joseph 2014) in the process? I think they would greatly improve arrows! I don't know if I have the time to attempt this, but if I find the time I would give it a try. Why wasn't this integrated while it was still actively developed? Best, Jan [Joseph 2014] https://www2.eecs.berkeley.edu/Pubs/TechRpts/ 2014/EECS-2014-130.pdf 2016-11-29 12:41 GMT+00:00 Simon Peyton Jones <simo...@microsoft.com>: > Jan, > > > > Type checking and desugaring for arrow syntax has received Absolutely No > Love for several years. I do not understand how it works very well, and I > would not be at all surprised if it is broken in corner cases. > > > > It really needs someone to look at it carefully, document it better, and > perhaps refactor it – esp by using a different data type rather than > piggy-backing on HsExpr. > > > > In the light of that understanding, I think rebindable syntax will be > easier. > > > > I don’t know if you are up for that, but it’s a rather un-tended part of > GHC. > > > > Thanks > > > > Simon > > > > *From:* ghc-devs [mailto:ghc-devs-boun...@haskell.org] *On Behalf Of *Richard > Eisenberg > *Sent:* 28 November 2016 22:30 > *To:* Jan Bracker <jan.brac...@googlemail.com> > *Cc:* ghc-devs@haskell.org > *Subject:* Help needed: Restrictions of proc-notation with > RebindableSyntax > > > > Jan’s question is a good one, but I don’t know enough about procs to be > able to answer. I do know that the answer can be found by looking for uses > of `tcSyntaxOp` in the TcArrows module but I just can’t translate it > all to source Haskell, having roughly 0 understanding of this end of the > language. > > > > Can anyone else help Jan here? > > > > Richard > > > > On Nov 23, 2016, at 4:34 AM, Jan Bracker via ghc-devs < > ghc-devs@haskell.org> wrote: > > > > Hello, > > > > I want to use the proc-notation together with RebindableSyntax. So far > what I am trying to do is working fine, but I would like to know what the > exact restrictions on the supplied functions are. I am introducing > additional indices and constraints on the operations. The documentation [1] > says the details are in flux and that I should ask directly. > > > > Best, > > Jan > > > > [1] https://downloads.haskell.org/~ghc/latest/docs/html/ > users_guide/glasgow_exts.html#rebindable-syntax-and-the- > implicit-prelude-import > <https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fdownloads.haskell.org%2F~ghc%2Flatest%2Fdocs%2Fhtml%2Fusers_guide%2Fglasgow_exts.html%23rebindable-syntax-and-the-implicit-prelude-import=02%7C01%7Csimonpj%40microsoft.com%7C80e472cedf78463bd18408d417de1af5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63615969010476=ygqePSmgcPKnPmKDBfZplkyjG9BIDBO1L1MWHNpqw88%3D=0> > > ___ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
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 <simo...@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-boun...@haskell.org] *On Behalf Of *Richard > Eisenberg > *Sent:* 18 November 2015 17:14 > *To:* Jan Bracker > *Cc:* ghc-devs@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.brac...@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=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c7aa4db864c994205421c08d2f03ba9ca%7c72f988bf86f141af91ab2d7cd011db47%7c1=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=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c7aa4db864c994205421c08d2f03ba9ca%7c72f988bf86f141af91ab2d7cd011db47%7c1=%2f174TvSeTQ8J%2bAw3VXtSzNKsy8JpFsfDffQvkD7WtkE%3d> > > > > thank you for your quick reply! > > > > Best, > > Jan > > > > 2015-11-18 17:05 GMT+00:00 Richard Eisenberg <e...@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.brac...@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 c
Re: Explanation of a core-lint warning (Bad getNth)
I have created Ticket #11435. I am still not sure if I am producing incorrect evidence or if there really is an issue with GHC, but I would expect GHC to tell me if the evidence I produced does not make sense. [1] https://ghc.haskell.org/trac/ghc/ticket/11435 2016-01-15 14:15 GMT+00:00 Simon Peyton Jones <simo...@microsoft.com>: > 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.brac...@googlemail.com] > *Sent:* 15 January 2016 14:03 > *To:* Simon Peyton Jones <simo...@microsoft.com> > *Cc:* Richard Eisenberg <e...@cis.upenn.edu>; ghc-devs@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 <simo...@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-boun...@haskell.org] *On Behalf Of *Richard > Eisenberg > *Sent:* 18 November 2015 17:14 > *To:* Jan Bracker > *Cc:* ghc-devs@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.brac...@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=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c7aa4db864c994205421c08d2f03ba9ca%7c72f988bf86f141af91ab2d7cd011db47%7c1=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=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c7aa4db864c994205421c08d2f03ba9ca%7c72f988bf86f141af91ab2d7cd011db47%7c1=%2f174TvSeTQ8J%2bAw3VXtSzNKsy8JpFsfDffQvkD7WtkE%3d> > > > > thank you for your quick reply! > > > > Best, > > Jan > > > > 2015-11-18 17:05 GMT+00:00 Richard Eisenberg <e...@cis.upenn.edu>: > > I took just a quick look at
Re: Explanation of a core-lint warning (Bad getNth)
Hard-coding the exact base version was a stupid mistake, sorry. I relaxed that and reattached a new version of the files to the ticket. It seems that 'effect-monad's dependency on 'type-level-sets' is a bit to liberal, because the module structure and exports of that package changed between versions. I hard-coded the correct version of 'type-level-set' into the cabal file of the example. I did not get this, because I share a sandbox between my main project and the examples (and its been around for some time now). Seems like 'effect-monad' is bitrotting a bit... I did not test these changes on 7.10.3, because I currently only have version 7.10.2 installed. 2016-01-15 22:30 GMT+00:00 Thomas Miedema <thomasmied...@gmail.com>: > > > On Fri, Jan 15, 2016 at 3:03 PM, Jan Bracker <jan.brac...@googlemail.com> > wrote: > >> You just have to download the three files and run "cabal install" to >> reproduce the error. >> > > It's never that easy, is it? Can you try in a cabal sandbox, with > ghc-7.10.3. I'm getting: > > > > cabal: Could not resolve dependencies: > trying: core-error-0.1 (user goal) > next goal: base (dependency of core-error-0.1) > rejecting: base-4.8.2.0/installed-0d6... (conflict: core-error => > base==4.8.1.0) > rejecting: base-4.8.1.0, base-4.8.0.0, base-4.7.0.2, base-4.7.0.1, > base-4.7.0.0, base-4.6.0.1, base-4.6.0.0, base-4.5.1.0, base-4.5.0.0, > base-4.4.1.0, base-4.4.0.0, base-4.3.1.0, base-4.3.0.0, base-4.2.0.2, > base-4.2.0.1, base-4.2.0.0, base-4.1.0.0, base-4.0.0.0, base-3.0.3.2, > base-3.0.3.1 (constraint from main config /home/thomas/.cabal/config > requires > installed instance) > Dependency tree exhaustively searched. > > > > After relaxing the depenency on base (or is the problem only reproducible > with base 4.8.1.0 that, in case we are done here), I get: > > > > > > Preprocessing library effect-monad-0.6.1... > > src/Control/Effect/State.hs:4:14: Warning: > -XOverlappingInstances is deprecated: instead use per-instance pragmas > OVERLAPPING/OVERLAPPABLE/OVERLAPS > [ 1 of 17] Compiling Control.Effect.Helpers.List ( > src/Control/Effect/Helpers/List.hs, > dist/build/Control/Effect/Helpers/List.o ) > [ 2 of 17] Compiling Control.Effect.Cond ( src/Control/Effect/Cond.hs, > dist/build/Control/Effect/Cond.o ) > [ 3 of 17] Compiling Control.Effect ( src/Control/Effect.hs, > dist/build/Control/Effect.o ) > [ 4 of 17] Compiling Control.Effect.Counter ( > src/Control/Effect/Counter.hs, dist/build/Control/Effect/Counter.o ) > [ 5 of 17] Compiling Control.Effect.CounterNat ( > src/Control/Effect/CounterNat.hs, dist/build/Control/Effect/CounterNat.o ) > [ 6 of 17] Compiling Control.Effect.Maybe ( src/Control/Effect/Maybe.hs, > dist/build/Control/Effect/Maybe.o ) > [ 7 of 17] Compiling Control.Effect.Monad ( src/Control/Effect/Monad.hs, > dist/build/Control/Effect/Monad.o ) > [ 8 of 17] Compiling Control.Effect.Parameterised ( > src/Control/Effect/Parameterised.hs, > dist/build/Control/Effect/Parameterised.o ) > [ 9 of 17] Compiling Control.Effect.Reader ( src/Control/Effect/Reader.hs, > dist/build/Control/Effect/Reader.o ) > > src/Control/Effect/Reader.hs:33:8: > Not in scope: type constructor or class ‘Var’ > > src/Control/Effect/Reader.hs:33:28: > Not in scope: type constructor or class ‘:->’ > > src/Control/Effect/Reader.hs:34:5: > Not in scope: data constructor ‘Var’ > > src/Control/Effect/Reader.hs:34:24: > Not in scope: data constructor ‘Var’ > > src/Control/Effect/Reader.hs:34:28: > Not in scope: data constructor ‘:->’ > Failed to install effect-monad-0.6.1 > > > > > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Explanation of a core-lint warning (Bad getNth)
As far as I understand your explanation this should not lead to an error, although it is not the most obvious coercion. Is that right? Do you or anybody else have a suggestion on how to resolve this issue? 2015-11-18 17:13 GMT+00:00 Richard Eisenberg <e...@cis.upenn.edu>: > 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.brac...@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 > "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 > > thank you for your quick reply! > > Best, > Jan > > 2015-11-18 17:05 GMT+00:00 Richard Eisenberg <e...@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.brac...@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 *** >> : 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 >> _N <'["thres" :-> Int]>_N (Sym >> TFCo:R:Unit[]Reader[0]))_R >> ; Sub >> (TFCo:R:Inv[]Readerfg[0] <'["thres" :-> Int]>_N > 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@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> >> >> > > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Explanation of a core-lint warning (Bad getNth)
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 "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 thank you for your quick reply! Best, Jan 2015-11-18 17:05 GMT+00:00 Richard Eisenberg <e...@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.brac...@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 *** > : 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 > _N <'["thres" :-> Int]>_N (Sym > TFCo:R:Unit[]Reader[0]))_R > ; Sub > (TFCo:R:Inv[]Readerfg[0] <'["thres" :-> Int]>_N 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@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Explanation of a core-lint warning (Bad getNth)
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 *** : 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 _N <'["thres" :-> Int]>_N (Sym TFCo:R:Unit[]Reader[0]))_R ; Sub (TFCo:R:Inv[]Readerfg[0] <'["thres" :-> Int]>_N _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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Type Checker Plugin: Producing the correct evidence
Hello, I am using type checker plugins to select specific instances in a program. My current problem concerns the following instance: class Polymonad m n p where (>>=) :: m a -> (a -> n b) -> p b instance ( Effect m, E.Inv m f (Unit m), f ~ Plus m f (Unit m)) => Polymonad (m (f :: [*])) Identity (m (f :: [*])) where ma >>= f = ma E.>>= (E.return . runIdentity . f) 'E', 'Unit' and 'Plus' refer to the module 'Control.Effect' [5] from the 'effect-monad' package. At some point in my example program [2] GHC is uncertain which instance to use for the '>>=' operator. The wanted constraint is: [W] $dPolymonad_a5Qp :: Polymonad (State '[n :-> (a :! 'W)]) Identity (State '[n :-> (a :! 'W)]) (CNonCanonical) To select the instance above I produce the following evidence: $fPolymonadmIdentitym @[State, '[n :-> (a :! 'W)]] [$fEffect[]State @[] []] 'State' is from the module 'Control.Effect.State' [4]. This works so far, but during the core-lint phase I get the following error message: : Warning: [RHS of $dPolymonad_a5Qp :: Polymonad (State '[n_a5PL :-> (a_a5PM :! 'W)]) Identity (State '[n_a5PL :-> (a_a5PM :! 'W)])] The type of this binder doesn't match the type of its RHS: $dPolymonad_a5Qp Binder's type: Polymonad (State '[n_a5PL :-> (a_a5PM :! 'W)]) Identity (State '[n_a5PL :-> (a_a5PM :! 'W)]) Rhs type: (Inv State '[n_a5PL :-> (a_a5PM :! 'W)] (Unit State), '[n_a5PL :-> (a_a5PM :! 'W)] ~ Plus State '[n_a5PL :-> (a_a5PM :! 'W)] (Unit State)) => Polymonad (State '[n_a5PL :-> (a_a5PM :! 'W)]) Identity (State '[n_a5PL :-> (a_a5PM :! 'W)]) Which I parse as a missing proof that the instance constraints are fulfilled by the evidence. >From this I have a few questions: 1. Why doesn't the type checker prove these type equality constraints for me? (or how can I get the type checker to do so?) I checked them on paper and the constraints are solvable and the equalities are true. 2. If I can't get the type checker to solve this for me, how do I produce appropriate evidence? 3. Another issue I see is that I would need to expand the type synonym 'E.Inv' to see what constraints it contains. I there an easy way to do so in GHC? I could not find appropriate functionality. It would be very useful for me if there was a function 'Type -> TcM Type' that evaluates the type as far as possible (by evaluate I mean expand synonyms, evaluate type functions and remove equalities that hold). The example program [2] and the plugin I am developing can be found [1] on GitHub (Commit fefc149ec6e1c1a3c3c2597c66d176854b94287d ). This is how I produce the evidence for my selected instance [3]. I hope this abstract description of my problem is enough. Best regards, Jan Bracker [1] https://github.com/jbracker/polymonad-plugin [2] https://github.com/jbracker/polymonad-plugin/blob/master/examples/effect/MainPolymonad.hs [3] https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymonad/Plugin/Evidence.hs [4] http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect-State.html [5] http://hackage.haskell.org/package/effect-monad-0.6.1/docs/Control-Effect.html ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Evaluating types and determining instantiability of an instance
Hello, I am trying to write a type checker plugin and I noticed that I keep trying to reimplement functionality that GHC type system already implements, but I can't seem to find a way to access the functionality. Part of these features I already asked in another (previous) email [1] to the mailing list and I am sorry if this will duplicate part of that discussion. 1. Is there a function in the type system which I can use to evaluate type functions and expand type synonyms (including associated instances)? Ideally I would want something that looks like this 'Type -> TcM Type'. I know that this kind of evaluation is not necessarily possible (e.g. type variables that can't be matched against in a type function application), but it would be helpful if the function could at least evaluate/expand as far as is possible in the current context. That way I don't have to manually lookup type family instances or type synonyms and make mistakes by doing so. This would also ease the support for the different type system extensions available, which I currently have to manually reimplement. 2. If I have an instance and a number of type arguments for that instance, is there an easy way to check if that instance is instantiated by those arguments? Something of the form '[Ct] -> ClsInst -> [Type] -> TcM (Maybe EvTerm)' would be useful. This function would take the given and derived constraints and deliver evidence for the instantiation if it is possible or return nothing if it is not. Again, if there are some open type variables I know this is not always possible in general and I am aware that this, in its full generality, requires a call to the constraint solver. But currently I am manually walking through the instance constraints to check if they are instantiated given the arguments [3] and then I also manually produce evidence [2]. In that process I ignore type equalities, type synonym and type families, because that would require me to implement question 1. I suspect this kind of functionality should exists somewhere within the GHC API. I would want this function to work with type arguments, whose only type variables already occur in the given and derived constraints. I think in that case it should always be possible to determine if the instance is instantiated. Best regards, Jan Bracker [1] https://mail.haskell.org/pipermail/ghc-devs/2015-November/010342.html [2] https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymonad/Plugin/Evidence.hs#L29 [3] https://github.com/jbracker/polymonad-plugin/blob/master/src/Control/Polymonad/Plugin/Instance.hs#L141 ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Proposed changes to typechecker plugins API
Hi Adam, Hi Eric,
At least for what I want to use them for [1] it would be nice if there was
an easy way to say:
If you are stuck on solving Constraint a b TypeC, then you should pick,
e.g.:
- a ~ TypeA and b ~ TypeB (What I am actually trying to say is: use
the instance Constraint TypeA TypeB TypeC)
- a ~ b
Currently I am producing equality constraints, like this:
mkDerivedTypeEqCt :: TcTyVar - TcType - TcPluginM Ct
mkDerivedTypeEqCt tyVar ty = do
(_, lclEnv) - getEnvs
return $ CTyEqCan
{ cc_ev = CtDerived -- :: CtEvidence
{ ctev_pred = ty -- :: TcPredType
-- This matches type-wise, but I have no idea what actually belongs
here.
, ctev_loc = mkGivenLoc topTcLevel (UnifyForAllSkol [tyVar] ty)
lclEnv -- :: CtLoc
-- Again no idea what actually belongs here:
-- topTcLevel :: TcLevel
-- To what does this relate? I guess top level
-- is ok for equality constraints
-- (UnifyForAllSkol [tyVar] ty) :: SkolemInfo
-- This one matches what we have at disposal (no idea if it is
the right one).
-- lclEnv :: TcLclEnv
-- I just use the only one I know.
}
, cc_tyvar = tyVar -- :: TcTyVar
, cc_rhs = ty -- :: TcType
, cc_eq_rel = NomEq -- :: EqRel
-- Alternative would be ReprEq. Whats the difference?
}
Which seems to be working, but still leaves a lot of open questions (see
comments).
Maybe my problems using the API are more related to missing documentation,
then lack of API functionality.
Jan
[1]: https://mail.haskell.org/pipermail/ghc-devs/2015-February/008414.html
On Wed, 27 May 2015 07:13:37, Eric Seidel wrote:
Hi Adam,
I like the addition of the new* functions for creating constraints, that
should make for a much nicer API than dealing directly with the
CtEvidence constructors!
I'm not so convinced however about embedding arbitrary CoreExprs in
EvTerms. First of all, it feels a bit strange to generate CoreExprs
before the desugarer (and we would have to add a `MonadThings TcPluginM`
instance to generate Integer and String CoreExprs).
But more importantly, based on your wiki page [1], it sounds like what
we really want is a nice API for creating dictionaries.
Eric
[1]:
https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#EmbeddingCoreExprinEvTerm
On Wed, May 27, 2015, at 01:33, Adam Gundry wrote:
Hi devs,
I thought I should flag up some proposed changes relating to typechecker
plugins, which Christiaan, Iavor and I have been discussing. The quick
summary:
* make it possible for plugins to create constraints (Phab:D909);
* make it easier for plugins to define special type families;
* embed CoreExpr in EvTerm.
For more details, see the wiki page:
https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Post-7.10changestoTcPluginMAPI
Questions/review/comments very welcome.
Adam
--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Fwd: EvTerms and how they are used
Hi Adam,
again thank you for your extensive and patient answer!
It's a bit hard to know exactly what is going on without the full code,
but I think what is happening is this: you have an unsolved constraint
`Polymonad Identity n_abpq Identity` and your plugin provides an
evidence term of type `Polymonad Identity Identity Identity`, but of
course this is ill-typed, because `n_abpq` is not `Identity`. Hence Core
Lint quite reasonably complains.
I would have thought the constraint solver would derive that 'obviously'
`n_abpq` needs to be unified with `Identity` and substitutes.
I'm not sure exactly what you are trying to do, but I think the right
way to approach this problem is to simulate a functional dependency on
Polymonad (in fact, can you use an actual functional dependency)?
That is exactly what I _don't_ want to do. I am trying to achieve a more
general version of monads, called polymonads as it was introduced here [1].
When confronted with the constraint `Polymonad Identity n_abpq Identity`,
do
not try to solve it directly, but instead notice that you must have
`n_abpq ~ Identity`. Your plugin can emit this as an additional derived
constraint, which will allow GHC's built-in solver to instantiate the
unification variable `n_abpq` and then solve the original constraint
using the existing instance. No manual evidence generation needed!
Yes, that makes perfect sense! I was so gridlocked, I did not see this as a
possibility to solve the problem.
Out of interest, can you say anything about your aims here? I'm keen to
find out about the range of applications of typechecker plugins.
I want to make Polymonads as proposed in [1] usable in Haskell. They
generalize
the bind operator to a more general signature `M a - (a - N b) - P b`.
Polymonads
subsume the standard Monad as well as indexed or parameterized monad,
without
relying on functional dependencies, which can be limiting (there may be
different
requirement depending on the monad being implemented).
Currently I am providing a type class for this:
class Polymonad m n p where
(=) :: m a - (a - n b) - p b
As the paper points out in section 4.2 (Ambiguity), type inference breaks
down,
because the constraint solver is not able to solve the ambiguity. Here a
small example:
-- Return operator for the IO polymonad
instance Polymonad Identity Identity IO where
-- ...
-- Identity polymonad
instance Polymonad Identity Identity Identity where
-- ...
return :: (Polymonad Identity Identity m) = a - m a
return x = Identity x = Identity
test :: Identity Bool
test = do
x - return True
return x
For this example GHC already gives the following ambiguity errors:
Main.hs:134:3:
No instance for (Polymonad m0 n0 Identity)
arising from a do statement
The type variables ‘m0’, ‘n0’ are ambiguous
Note: there is a potential instance available:
instance Polymonad Identity Identity Identity
-- Defined in ‘Polymonad’
In a stmt of a 'do' block: x - return True
In the expression:
do { x - return True;
return x }
In an equation for ‘test’:
test
= do { x - return True;
return x }
Main.hs:134:8:
No instance for (Polymonad Identity Identity m0)
arising from a use of ‘return’
The type variable ‘m0’ is ambiguous
Note: there are several potential instances:
instance Polymonad Identity Identity Identity
-- Defined in ‘Polymonad’
instance Polymonad Identity Identity IO -- Defined at Main.hs:85:10
In a stmt of a 'do' block: x - return True
In the expression:
do { x - return True;
return x }
In an equation for ‘test’:
test
= do { x - return True;
return x }
Main.hs:135:3:
No instance for (Polymonad Identity Identity n0)
arising from a use of ‘return’
The type variable ‘n0’ is ambiguous
Note: there are several potential instances:
instance Polymonad Identity Identity Identity
-- Defined in ‘Polymonad’
instance Polymonad Identity Identity IO -- Defined at Main.hs:85:10
In a stmt of a 'do' block: return x
In the expression:
do { x - return True;
return x }
In an equation for ‘test’:
test
= do { x - return True;
return x }
Of course, in the given example we can fix the ambiguity by adding type
annotations.
But as soon as the examples become bigger that is not possible anymore.
Using the approach of the paper [1] these constraints are solvable
unambiguously.
That's what I am working on.
All the best,
Jan
[1]: http://arxiv.org/pdf/1406.2060v1.pdf
On 26/02/15 10:07, Jan Bracker wrote:
Hi Adam,
thank you for your quick and detailed answer! I think I understand how
to construct evidence for typeclass constraints now. But trying to apply
this, I still have some problems.
I have something along the following lines:
class Polymonad m n p
EvTerms and how they are used
Hello, I am trying to use the new type checker plugins [1] that are implemented in head. When successful a plugin has to return a [(EvTerm, Ct)] for the solved constraints. The documentation on EvTerms is scarce [2,3,4] and I could not find papers that explain them (many talk about 'evidence', but they never get concrete). So far I have figured out that EvDFunApp DFunId [Type] [EvTerm] selects a certain instance to be used for a constraint, though I don't know what the list of EvTerms in the end is for. I am also a bit unclear on how the [Type] is used.If I turn on '-dcore-lint' I get errors. So I still seem to be using it wrong. I have also asked in IRC, but did not get a response to my question. I am sorry if this is the wrong mailing list to ask. If there is a more apropriate place just point it out. Best, Jan [1]: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker [2]: http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/TcEvidence.html#t:EvTerm [3]: http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/libraries/ghc-7.11.20150225/src/TcEvidence.html#EvTerm [4]: http://haskell.inf.elte.hu/docs/7.11.20150225.noWin32/html/users_guide/compiler-plugins.html ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
