RE: Invariants about UnivCo?

2017-10-11 Thread Simon Peyton Jones via ghc-devs
3) I confirmed that the lack of cobox uniques in the dump output was indeed due 
to `ppr_co' deferring to `ppr @IfaceType'; it does that (at least) for every 
coercion with a head of `TyConAppCo'. With a tiny kludgy patch I was able to 
persist those uniques just for debugging purposes.

Would you like to offer a patch?

I eventually gave up on the via-iface-type route for debug printing.  See 
TyCoRep.pprPrecType, which checks for debugStyle and if so calls a simple but 
direct debug_ppr_ty.  Not beautiful, but very direct.  For debugging it’s 
terrible if tidying and other stuff goes on.

Maybe we want the same for coercions?

Simon

From: Nicolas Frisby [mailto:nicolas.fri...@gmail.com]
Sent: 09 October 2017 03:50
To: Richard Eisenberg 
Cc: Simon Peyton Jones ; ghc-devs@haskell.org
Subject: Re: Invariants about UnivCo?


Yep, that's the current question: why does preferring `EvCoercion (TransCo 
UnivCo (TransCo co UnivCo))` to `EvCast (EvCoercion co) UnivCo` seem to matter? 
In my scenario, `co` is the evidence for a Given equality type. And the 
coercion I'm building is also a Given constraint's evidence -- I'm simplifying 
Givens.

The only hard indication I currently have of what "goes wrong" is the ASSERT 
failure described in the previous email.

I'm planning to spend some time investigating. I would appreciate any cycles 
you spend on it!

On Sun, Oct 8, 2017, 18:53 Richard Eisenberg 
mailto:r...@cs.brynmawr.edu>> wrote:
Thanks for this status report. If I'm to boil it down to the question you seem 
to be asking: What does changing EvCast ... to EvCoercion ... fix the problem? 
I'm not sure of the answer at this point, but I want to make sure I understand 
the question before I go digging for an answer. It's always possible a Note is 
wrong!

Thanks for this!

Richard

On Oct 7, 2017, at 8:19 PM, Nicolas Frisby 
mailto:nicolas.fri...@gmail.com>> wrote:

I can happily report some progress: I'm seeing no more Core lint errors!

1) Thank you both Richard and Simon for your pointers -- 
-fprint-typechecker-elaboration in particular was a revelation.

2) Simon, I intend to match the spirit of the favor you requested, but not to 
the letter. My goal with this project is to write a typechecker plugin for 
achieving row types _without_ editing GHC's source code. I'm keeping an 
annotated bibliography of things I've studied (papers, guide/wiki/blog, source 
Notes, etc). (It's nice to put a bunch of related notes in the same text file!) 
I'm also logging my epiphanies, which I do intend to write-up in some kind of 
document (probably on the dev wiki). I'm planning a section for suggesting 
which Notes should be adjusted/expanded, but I don't anticipate feeling 
comfortable enough to actually edit the Notes myself. This is unfortunately 
just a hobby project. My intent is to offer you, Richard, and other experts the 
details of what wasn't clear to me.

3) I confirmed that the lack of cobox uniques in the dump output was indeed due 
to `ppr_co' deferring to `ppr @IfaceType'; it does that (at least) for every 
coercion with a head of `TyConAppCo'. With a tiny kludgy patch I was able to 
persist those uniques just for debugging purposes.

4) My top-level error is an "out of scope cobox" Lint error, but (once I 
patched the dumper) the output of -fprint-typechecker-elaboration showed 
sufficient bindings for all of the cobox occurrences, even the one that the 
Lint error was flagging! Stymied, I finally did a -DDEBUG build of the 
ghc-8.2.2-rc1 tag and used that. It ultimately lead to me finding my mistakes. 
(New wisdom: always use a DEBUG build when authoring a plugin. (... Duh.))

4a) ASSERT failures showed that I was invoking `substTy' without correctly 
initializing the `InScopeSet'. I also was ignorant that I should be using 
`extendTvSubstAndInScope' instead of just `extendTvSubst'. I don't think this 
was relevant to my particular Lint error, but I fixed it if only to see further 
ASSERT failures.

4b) Fixing my `InScopeSet's ASSERT failure revealed another: `extendIdSubst' 
was being called with a CoVar! That's something that my plugin code absolutely 
does not do, so at that point I knew that some higher-level operation I was 
doing was knocking the rest of GHC's pipeline off the rails. (In particular, I 
traced this ASSERT callstack to extendIdSubst called from simpleOptExpr called 
from mkInlineUnfoldingWithArity called from DsBinds. I stopped there.)

5) The first suspect turned out to be the culprit: I was using my plugin's 
by-fiat coercions in the most naive possible way, always simply `EvCast ev 
(fiatCoercion ty0 ty1)`. In particular, I was even doing that to create new 
Given unlifted equality witnesses from existing Given unlifted equality 
witnesses when simplifying Given constraints (e.g. for example reducing a 
plugin-specific type family application on one side of an unlifted equality 
type ~#).

In summary, I see no more ASSERT failures or Lint errors having now changed my 
plugin to pr

RE: Invariants about UnivCo?

2017-10-11 Thread Simon Peyton Jones via ghc-devs
5) The first suspect turned out to be the culprit: I was using my plugin's 
by-fiat coercions in the most naive possible way, always simply `EvCast ev 
(fiatCoercion ty0 ty1)`. In particular, I was even doing that to create new 
Given unlifted equality witnesses from existing Given unlifted equality 
witnesses when simplifying Given constraints (e.g. for example reducing a 
plugin-specific type family application on one side of an unlifted equality 
type ~#).

I don’t understand the issue here at all. Can you give a concrete example?

Simon
From: Nicolas Frisby [mailto:nicolas.fri...@gmail.com]
Sent: 09 October 2017 03:50
To: Richard Eisenberg 
Cc: Simon Peyton Jones ; ghc-devs@haskell.org
Subject: Re: Invariants about UnivCo?


Yep, that's the current question: why does preferring `EvCoercion (TransCo 
UnivCo (TransCo co UnivCo))` to `EvCast (EvCoercion co) UnivCo` seem to matter? 
In my scenario, `co` is the evidence for a Given equality type. And the 
coercion I'm building is also a Given constraint's evidence -- I'm simplifying 
Givens.

The only hard indication I currently have of what "goes wrong" is the ASSERT 
failure described in the previous email.

I'm planning to spend some time investigating. I would appreciate any cycles 
you spend on it!

On Sun, Oct 8, 2017, 18:53 Richard Eisenberg 
mailto:r...@cs.brynmawr.edu>> wrote:
Thanks for this status report. If I'm to boil it down to the question you seem 
to be asking: What does changing EvCast ... to EvCoercion ... fix the problem? 
I'm not sure of the answer at this point, but I want to make sure I understand 
the question before I go digging for an answer. It's always possible a Note is 
wrong!

Thanks for this!

Richard

On Oct 7, 2017, at 8:19 PM, Nicolas Frisby 
mailto:nicolas.fri...@gmail.com>> wrote:

I can happily report some progress: I'm seeing no more Core lint errors!

1) Thank you both Richard and Simon for your pointers -- 
-fprint-typechecker-elaboration in particular was a revelation.

2) Simon, I intend to match the spirit of the favor you requested, but not to 
the letter. My goal with this project is to write a typechecker plugin for 
achieving row types _without_ editing GHC's source code. I'm keeping an 
annotated bibliography of things I've studied (papers, guide/wiki/blog, source 
Notes, etc). (It's nice to put a bunch of related notes in the same text file!) 
I'm also logging my epiphanies, which I do intend to write-up in some kind of 
document (probably on the dev wiki). I'm planning a section for suggesting 
which Notes should be adjusted/expanded, but I don't anticipate feeling 
comfortable enough to actually edit the Notes myself. This is unfortunately 
just a hobby project. My intent is to offer you, Richard, and other experts the 
details of what wasn't clear to me.

3) I confirmed that the lack of cobox uniques in the dump output was indeed due 
to `ppr_co' deferring to `ppr @IfaceType'; it does that (at least) for every 
coercion with a head of `TyConAppCo'. With a tiny kludgy patch I was able to 
persist those uniques just for debugging purposes.

4) My top-level error is an "out of scope cobox" Lint error, but (once I 
patched the dumper) the output of -fprint-typechecker-elaboration showed 
sufficient bindings for all of the cobox occurrences, even the one that the 
Lint error was flagging! Stymied, I finally did a -DDEBUG build of the 
ghc-8.2.2-rc1 tag and used that. It ultimately lead to me finding my mistakes. 
(New wisdom: always use a DEBUG build when authoring a plugin. (... Duh.))

4a) ASSERT failures showed that I was invoking `substTy' without correctly 
initializing the `InScopeSet'. I also was ignorant that I should be using 
`extendTvSubstAndInScope' instead of just `extendTvSubst'. I don't think this 
was relevant to my particular Lint error, but I fixed it if only to see further 
ASSERT failures.

4b) Fixing my `InScopeSet's ASSERT failure revealed another: `extendIdSubst' 
was being called with a CoVar! That's something that my plugin code absolutely 
does not do, so at that point I knew that some higher-level operation I was 
doing was knocking the rest of GHC's pipeline off the rails. (In particular, I 
traced this ASSERT callstack to extendIdSubst called from simpleOptExpr called 
from mkInlineUnfoldingWithArity called from DsBinds. I stopped there.)

5) The first suspect turned out to be the culprit: I was using my plugin's 
by-fiat coercions in the most naive possible way, always simply `EvCast ev 
(fiatCoercion ty0 ty1)`. In particular, I was even doing that to create new 
Given unlifted equality witnesses from existing Given unlifted equality 
witnesses when simplifying Given constraints (e.g. for example reducing a 
plugin-specific type family application on one side of an unlifted equality 
type ~#).

In summary, I see no more ASSERT failures or Lint errors having now changed my 
plugin to prefer `EvCoercion (TransCo U (TransCo co U))` to `EvCast (EvCoercion 
co) U`. The actual diff exce

RE: More windows

2017-10-11 Thread Ben Gamari
Simon Peyton Jones via ghc-devs  writes:

> Any ideas anyone? When I restart the build, it gets past the blockage
> (which seems highly specific). But it’s jolly annoying.
>
Hi Simon,

Perhaps let's try this,

 1. download and run the procmon tool from [1]
 2. from the "Filter" menu select the "Filter..." option
 3. select "Path" in the first drop-down
 4. select "contains" in the second drop-down
 5. enter "ghc-cabal.exe" in the third text box
 6. select "Include in the fourth drop-down
 8. click the "Add" button
 7. click the "Ok" button

Now you should be logging events pertaining to the file in question. Now
simply run `./validate` to try to reproduce the issue.

With luck this will produce a handful of events, some of which ought to
point to the process that it responsible for meddling with the GHC
build.

Now export this log,

 1. select "Save" from the "File" menu
 2. select the "Events displayed using current filter" option
 3. select the "CSV" format, select a path that will be easy to file
 4. return this file to me (perhaps via GitHub Gist [2]?)

Hopefully this will give us some insight into what is happening.

Cheers,

- Ben


[1] https://docs.microsoft.com/en-us/sysinternals/downloads/procmon
[2] https://gist.github.com/


signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs