subject:"RE\: Explanation of a core\-lint warning \(Bad getNth\)"

RE: Explanation of a core-lint warning (Bad getNth)

2016-01-15 Thread Simon Peyton Jones

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<mailto: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<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<mailto: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<mailto: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<mailto: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<mailto:j

Re: Explanation of a core-lint warning (Bad getNth)

2016-01-15 Thread Jan Bracker

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)

2016-01-15 Thread Jan Bracker

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)

2016-01-15 Thread Thomas Miedema

On Fri, Jan 15, 2016 at 3:03 PM, Jan Bracker 
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)

2016-01-15 Thread Jan Bracker

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 :

>
>
> On Fri, Jan 15, 2016 at 3:03 PM, Jan Bracker 
> 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)

2016-01-15 Thread Thomas Miedema

I can reproduce the problem with 7.10.3. Since the compiler got completely
rewritten, the plugin for sure doesn't work with 8.0.

In case anyone else wants to take look at this bug, I can say the plugin
contains a lot of hopefully helpful comments.

On Sat, Jan 16, 2016 at 12:49 AM, Jan Bracker 
wrote:

> Seems like 'effect-monad' is bitrotting a bit...
>

I submitted this pull request:
https://github.com/dorchard/effect-monad/pull/5
___
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)

2015-11-20 Thread Simon Peyton Jones

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<mailto: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<mailto: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<mailto: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 _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

Re: Explanation of a core-lint warning (Bad getNth)

2015-11-18 Thread Jan Bracker

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 :

> 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 
> 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 :
>
>> 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 
>> 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)

2015-11-18 Thread Richard Eisenberg


On Nov 18, 2015, at 12:19 PM, Jan Bracker  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 :
> 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  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 :
>> 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  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)

2015-11-18 Thread Richard Eisenberg

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  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 :
> 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  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)

2015-11-18 Thread Richard Eisenberg

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  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)

2015-11-18 Thread Jan Bracker

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 :

> 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 
> 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)

Re: Explanation of a core-lint warning (Bad getNth)

Re: Explanation of a core-lint warning (Bad getNth)

Re: Explanation of a core-lint warning (Bad getNth)

Re: Explanation of a core-lint warning (Bad getNth)

Re: Explanation of a core-lint warning (Bad getNth)

RE: Explanation of a core-lint warning (Bad getNth)

Re: Explanation of a core-lint warning (Bad getNth)

Re: Explanation of a core-lint warning (Bad getNth)

Re: Explanation of a core-lint warning (Bad getNth)

Re: Explanation of a core-lint warning (Bad getNth)

Re: Explanation of a core-lint warning (Bad getNth)

12 matches

Site Navigation

Mail list logo

Footer information