On Nov 18, 2015, at 12:19 PM, Jan Bracker <jan.brac...@googlemail.com> wrote:
> 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? That's what it seems to be, in this particular case. But I'd be nervous with this result and would want further examination. My next port of call in your shoes would be to run with -ddump-tc-trace. I'm afraid I don't have the time right now to walk through that with you, though -- sorry! Richard > > 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 *** >>> <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@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
