Thanks for the reply Richard, I really appreciate it. Your email actually buzzed my phone just as I was opening my laptop to draft this email. I'm optimistic that I may have identified part of the issue. * Note [Coercion evidence terms] in TcEvidence.hs lists an INVARIANT that the evidence for t1 ~# t2 must be built with EvCoercion. I'm very confident that I am instead building it with a by-fiat EvCast: this is what I meant by "by using UnivCo to cast coboxes" in my previous email. I'm optimistic that fixing this up will help. Does it sound promising/ring any bells for you? Thanks. -Nick On Wed, Sep 20, 2017 at 7:47 PM Richard Eisenberg wrote:

...

On Sep 19, 2017, at 9:50 AM, Nicolas Frisby wrote:

Questions:

1) Is there a robust way to ensure that covar's uniques are always printed? (Is the pprIface reuse with a free cobox part of the issue here?)

Try rebasing. I ran into a similar issue not long ago and revised the code around printing coercions. Also, -fprint-explicit-kinds might help. An occurrence of a tyvar is also an implicit occurrence of all the free variables in its kinds.

...

2) Is my plugin asking for this kind of trouble by using UnivCo to cast

coboxes?

No. `UnivCo`s should work fine. You might potentially be asking for "shoot the gorillas" problems (it has been suggested that we refrain from "launching the rockets", as that event seems a mite too likely these days, unsafeCoerceIO or no; I propose this new formulation, inspired by an utterance by Simon PJ about how when you're tackling bugs, sometimes you shoot one gorilla only to find more behind it... but then he remarked that one, of course, would never want to actually shoot a gorilla.), but I think Core Lint should be OK.

...

3) If I spent the effort to create non-UnivCo coercions where possible,

would that likely help? This is currently an "eventually" task, but I haven't seen an urgency for it yet. I could bump its priority if it might help. E.G. I'm using UnivCo to cast entire givens when all I'm doing is reducing a type family application somewhere "deep" within the given's predtype. I could, with considerable effort, instead wrap a single, localized UnivCo within a bunch of non-UnivCo "lifting" coercion constructors. Would that likely help?

I don't think this line of inquiry will be helpful.

...

3) Is there a usual suspect for this kind of situation where a cobox

binding is seemingly dropped (by the typechecker) even though there's an occurrence of it?

Not for me.

I hope this helps! Richard

...

Thank you for your time. -Nick _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Bah. I misparsed the note; it doesn't rule out casting coboxes. However, it does refer to Note [Bind new Givens immediately] in TcRnTypes, which indicates that maybe I should be explicitly binding an evidence variable when adjusting given constraints of type t1 ~# t2... Thanks for the castCoercionKind tip On Wed, Sep 20, 2017 at 7:59 PM Richard Eisenberg wrote:

On Sep 20, 2017, at 8:52 PM, Nicolas Frisby wrote:

* Note [Coercion evidence terms] in TcEvidence.hs lists an INVARIANT that the evidence for t1 ~# t2 must be built with EvCoercion. I'm very confident that I am instead building it with a by-fiat EvCast: this is what I meant by "by using UnivCo to cast coboxes" in my previous email.

Hm. If you break an INVARIANT, anything can happen. Perhaps you've hit it. I think instead of using EvCast, you should use Coercion.castCoercionKind, but I'm not sure without knowing more details.

Richard

I'm optimistic that fixing this up will help. Does it sound promising/ring any bells for you?

Thanks. -Nick

On Wed, Sep 20, 2017 at 7:47 PM Richard Eisenberg wrote:

...

...

On Sep 19, 2017, at 9:50 AM, Nicolas Frisby wrote:

Questions:

1) Is there a robust way to ensure that covar's uniques are always printed? (Is the pprIface reuse with a free cobox part of the issue here?)

Try rebasing. I ran into a similar issue not long ago and revised the code around printing coercions. Also, -fprint-explicit-kinds might help. An occurrence of a tyvar is also an implicit occurrence of all the free variables in its kinds.

...

2) Is my plugin asking for this kind of trouble by using UnivCo to cast

coboxes?

No. `UnivCo`s should work fine. You might potentially be asking for "shoot the gorillas" problems (it has been suggested that we refrain from "launching the rockets", as that event seems a mite too likely these days, unsafeCoerceIO or no; I propose this new formulation, inspired by an utterance by Simon PJ about how when you're tackling bugs, sometimes you shoot one gorilla only to find more behind it... but then he remarked that one, of course, would never want to actually shoot a gorilla.), but I think Core Lint should be OK.

...

3) If I spent the effort to create non-UnivCo coercions where possible,

would that likely help? This is currently an "eventually" task, but I haven't seen an urgency for it yet. I could bump its priority if it might help. E.G. I'm using UnivCo to cast entire givens when all I'm doing is reducing a type family application somewhere "deep" within the given's predtype. I could, with considerable effort, instead wrap a single, localized UnivCo within a bunch of non-UnivCo "lifting" coercion constructors. Would that likely help?

I don't think this line of inquiry will be helpful.

...

3) Is there a usual suspect for this kind of situation where a cobox

binding is seemingly dropped (by the typechecker) even though there's an occurrence of it?

Not for me.

I hope this helps! Richard

...

Thank you for your time. -Nick _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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 excerpt is here: https://github.com/nfrisby/coxswain/issues/3#issuecomment-334972227 I have not figured out exactly why that change matters, but it does seem a reasonable preference to require. In particular, Note [Coercion evidence terms] in TcEvidence.hs explicitly says that `EvCast (EvCoercion co1) co2` is a valid form of evidence for ~#. So perhaps that Note deserves elaboration --- I'm guessing the missing part may be specific to Givens? -Nick On Thu, Sep 21, 2017 at 2:59 AM Simon Peyton Jones wrote:

Some thoughts

- Read Note [Coercion holes] in TyCoRep.

- As you’ll see, generally we don’t create value-bindings for (unboxed) coercions of type t1 ~# t2. (yes for boxed ones t1 ~ t2). Reasons in the Note. Exception: for superclasses of Givens we do create (co :: a ~# b) = sc_sel1 d

where d is some dictionary with a superclass of type (a ~# b).

Side note: the use of “cobox” is wildly unhelpful. These Ids are specifically *unboxed*! I’m going to change it to just “co”.

- You appear to have bindings like[G] cobox_a67J = CO Sym cobox_a654. That is suspicious. Who is creating them? It may not actually be wrong but it’s suspicious. The time it’d be outright wrong is if you dropped the ev-binds on the floor.

Ha! runTcSEqualites makes up an ev_binds_var, and solves the equalities – but it should be the case that no value bindings end up in the ev_binds_var. (reason: we are solving equalities in a type signature, so there is no place to put the evidence bindigns) I suggest you add a DEBUG-only assertion to check this.

- Do -ddump-tc -fprint-typechecker-elaboration; that should show you the evidence binds.

Can I ask you a favour? Separately from your branch, can you start a branch of small patches to GHC that include

- Extra assertions, such as that above - *Notes* that explain things you wish you’d known earlier, with references to those Notes from the places you were studying when you that information would have been useful

Richard and I know too much! – your learning curve is very valuable and I don’t want to lose it.

Keeping this separate from your branch is useful : you can commit (via Phab) these updates right away, so they aren’t predicated on adding row types to GHC.

Simon

*From:* ghc-devs [mailto:ghc-devs-bounces@haskell.org] *On Behalf Of *Nicolas Frisby *Sent:* 19 September 2017 16:51 *To:* ghc-devs@haskell.org *Subject:* Invariants about UnivCo?

[I summarize with some direct questions at the bottom of this email.]

I spent time last night trying to eliminate -dcore-lint errors from my record and variant library using the coxswain row types plugin. I made some progress, but I'm currently stuck, as discussed on this github Issue.

https://github.com/nfrisby/coxswain/issues/3#issuecomment-330577609 https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnfrisby%2Fcoxswain%2Fissues%2F3%23issuecomment-330577609&data=02%7C01%7Csimonpj%40microsoft.com%7Cde0675bbb584495a2f8008d4ff764c72%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636414330952932223&sdata=lPLcpIlb%2BhivQdCUoVOPUgYDHeEDaMX660NQS%2BQyyBw%3D&reserved=0

Here's the relevant bit:

The latest unresolved -dcore-lint error is an out-of-scope cobox co var. I'm certainly not creating it *directly* (there are no U(plugin:coxswain,... in the Core Lint warning), but I have to wonder if my somewhat loose use of UnivCo is violating some assumptions somewhere that's causing GHC to drop the co var binding or overlook this occurrence of it on a renaming/subst pass. I checked UnivCo for source comments looking for anything it should *not* be used for, but I didn't find an obvious explanation along those lines.

I haven't yet been able to effectively distill the test case.

I'm doing this all at -O0.

With `-ddump-tc-trace`, I can see the offending cobox (cobox_a67M) is present in an "implication evbinds" listing after a "solveImplication end }" delimiter, but that's the last obvious binding of it.

[G] cobox_a67J = CO Sym cobox_a654,

[G] cobox_a67M

= cobox_a67J `cast` U(plugin:coxswain,...)

cobox_a654 is introduced by a GADT pattern match.

I'm also not seeing obvious occurrences of cobox_a67M, but I think the reason is that I'm seeing several (Sym cobox) with no uniques printed (even with `-dppr-debug`). Those are probably the cobox in question, but I can't confirm.

Questions:

1) Is there a robust way to ensure that covar's uniques are always printed? (Is the pprIface reuse with a free cobox part of the issue here?)

2) Is my plugin asking for this kind of trouble by using UnivCo to cast coboxes?

3) If I spent the effort to create non-UnivCo coercions where possible, would that likely help? This is currently an "eventually" task, but I haven't seen an urgency for it yet. I could bump its priority if it might help. E.G. I'm using UnivCo to cast entire givens when all I'm doing is reducing a type family application somewhere "deep" within the given's predtype. I could, with considerable effort, instead wrap a single, localized UnivCo within a bunch of non-UnivCo "lifting" coercion constructors. Would that likely help?

3) Is there a usual suspect for this kind of situation where a cobox binding is seemingly dropped (by the typechecker) even though there's an occurrence of it?

Thank you for your time. -Nick

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 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 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 excerpt is here: https://github.com/nfrisby/coxswain/issues/3#issuecomment-334972227

I have not figured out exactly why that change matters, but it does seem a reasonable preference to require. In particular, Note [Coercion evidence terms] in TcEvidence.hs explicitly says that `EvCast (EvCoercion co1) co2` is a valid form of evidence for ~#. So perhaps that Note deserves elaboration --- I'm guessing the missing part may be specific to Givens?

-Nick

On Thu, Sep 21, 2017 at 2:59 AM Simon Peyton Jones wrote:

...

Some thoughts

- Read Note [Coercion holes] in TyCoRep.

- As you’ll see, generally we don’t create value-bindings for (unboxed) coercions of type t1 ~# t2. (yes for boxed ones t1 ~ t2). Reasons in the Note. Exception: for superclasses of Givens we do create (co :: a ~# b) = sc_sel1 d

where d is some dictionary with a superclass of type (a ~# b).

Side note: the use of “cobox” is wildly unhelpful. These Ids are specifically *unboxed*! I’m going to change it to just “co”.

- You appear to have bindings like[G] cobox_a67J = CO Sym cobox_a654. That is suspicious. Who is creating them? It may not actually be wrong but it’s suspicious. The time it’d be outright wrong is if you dropped the ev-binds on the floor.

Ha! runTcSEqualites makes up an ev_binds_var, and solves the equalities – but it should be the case that no value bindings end up in the ev_binds_var. (reason: we are solving equalities in a type signature, so there is no place to put the evidence bindigns) I suggest you add a DEBUG-only assertion to check this.

- Do -ddump-tc -fprint-typechecker-elaboration; that should show you the evidence binds.

Can I ask you a favour? Separately from your branch, can you start a branch of small patches to GHC that include

- Extra assertions, such as that above - *Notes* that explain things you wish you’d known earlier, with references to those Notes from the places you were studying when you that information would have been useful

Richard and I know too much! – your learning curve is very valuable and I don’t want to lose it.

Keeping this separate from your branch is useful : you can commit (via Phab) these updates right away, so they aren’t predicated on adding row types to GHC.

Simon

*From:* ghc-devs [mailto:ghc-devs-bounces@haskell.org] *On Behalf Of *Nicolas Frisby *Sent:* 19 September 2017 16:51 *To:* ghc-devs@haskell.org *Subject:* Invariants about UnivCo?

[I summarize with some direct questions at the bottom of this email.]

I spent time last night trying to eliminate -dcore-lint errors from my record and variant library using the coxswain row types plugin. I made some progress, but I'm currently stuck, as discussed on this github Issue.

https://github.com/nfrisby/coxswain/issues/3#issuecomment-330577609 https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnfrisby%2Fcoxswain%2Fissues%2F3%23issuecomment-330577609&data=02%7C01%7Csimonpj%40microsoft.com%7Cde0675bbb584495a2f8008d4ff764c72%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636414330952932223&sdata=lPLcpIlb%2BhivQdCUoVOPUgYDHeEDaMX660NQS%2BQyyBw%3D&reserved=0

Here's the relevant bit:

The latest unresolved -dcore-lint error is an out-of-scope cobox co var. I'm certainly not creating it *directly* (there are no U(plugin:coxswain,... in the Core Lint warning), but I have to wonder if my somewhat loose use of UnivCo is violating some assumptions somewhere that's causing GHC to drop the co var binding or overlook this occurrence of it on a renaming/subst pass. I checked UnivCo for source comments looking for anything it should *not* be used for, but I didn't find an obvious explanation along those lines.

I haven't yet been able to effectively distill the test case.

I'm doing this all at -O0.

With `-ddump-tc-trace`, I can see the offending cobox (cobox_a67M) is present in an "implication evbinds" listing after a "solveImplication end }" delimiter, but that's the last obvious binding of it.

[G] cobox_a67J = CO Sym cobox_a654,

[G] cobox_a67M

= cobox_a67J `cast` U(plugin:coxswain,...)

cobox_a654 is introduced by a GADT pattern match.

I'm also not seeing obvious occurrences of cobox_a67M, but I think the reason is that I'm seeing several (Sym cobox) with no uniques printed (even with `-dppr-debug`). Those are probably the cobox in question, but I can't confirm.

Questions:

1) Is there a robust way to ensure that covar's uniques are always printed? (Is the pprIface reuse with a free cobox part of the issue here?)

2) Is my plugin asking for this kind of trouble by using UnivCo to cast coboxes?

3) If I spent the effort to create non-UnivCo coercions where possible, would that likely help? This is currently an "eventually" task, but I haven't seen an urgency for it yet. I could bump its priority if it might help. E.G. I'm using UnivCo to cast entire givens when all I'm doing is reducing a type family application somewhere "deep" within the given's predtype. I could, with considerable effort, instead wrap a single, localized UnivCo within a bunch of non-UnivCo "lifting" coercion constructors. Would that likely help?

3) Is there a usual suspect for this kind of situation where a cobox binding is seemingly dropped (by the typechecker) even though there's an occurrence of it?

Thank you for your time. -Nick

_______________________________________________

ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/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.frisby@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:rae@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.frisby@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 excerpt is here: https://github.com/nfrisby/coxswain/issues/3#issuecomment-334972227https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnfrisby%2Fcoxswain%2Fissues%2F3%23issuecomment-334972227&data=02%7C01%7Csimonpj%40microsoft.com%7C2b0edffd514b4da49abc08d50ec07ff9%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636431142301735979&sdata=Ng6o4ODbLXNJVlngL0qnBv1EQ5Sn9TJMPK79M99zGTg%3D&reserved=0 I have not figured out exactly why that change matters, but it does seem a reasonable preference to require. In particular, Note [Coercion evidence terms] in TcEvidence.hs explicitly says that `EvCast (EvCoercion co1) co2` is a valid form of evidence for ~#. So perhaps that Note deserves elaboration --- I'm guessing the missing part may be specific to Givens? -Nick On Thu, Sep 21, 2017 at 2:59 AM Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: Some thoughts * Read Note [Coercion holes] in TyCoRep. * As you’ll see, generally we don’t create value-bindings for (unboxed) coercions of type t1 ~# t2. (yes for boxed ones t1 ~ t2). Reasons in the Note. Exception: for superclasses of Givens we do create (co :: a ~# b) = sc_sel1 d where d is some dictionary with a superclass of type (a ~# b). Side note: the use of “cobox” is wildly unhelpful. These Ids are specifically unboxed! I’m going to change it to just “co”. * You appear to have bindings like[G] cobox_a67J = CO Sym cobox_a654. That is suspicious. Who is creating them? It may not actually be wrong but it’s suspicious. The time it’d be outright wrong is if you dropped the ev-binds on the floor. Ha! runTcSEqualites makes up an ev_binds_var, and solves the equalities – but it should be the case that no value bindings end up in the ev_binds_var. (reason: we are solving equalities in a type signature, so there is no place to put the evidence bindigns) I suggest you add a DEBUG-only assertion to check this. * Do -ddump-tc -fprint-typechecker-elaboration; that should show you the evidence binds. Can I ask you a favour? Separately from your branch, can you start a branch of small patches to GHC that include * Extra assertions, such as that above * Notes that explain things you wish you’d known earlier, with references to those Notes from the places you were studying when you that information would have been useful Richard and I know too much! – your learning curve is very valuable and I don’t want to lose it. Keeping this separate from your branch is useful : you can commit (via Phab) these updates right away, so they aren’t predicated on adding row types to GHC. Simon From: ghc-devs [mailto:ghc-devs-bounces@haskell.orgmailto:ghc-devs-bounces@haskell.org] On Behalf Of Nicolas Frisby Sent: 19 September 2017 16:51 To: ghc-devs@haskell.orgmailto:ghc-devs@haskell.org Subject: Invariants about UnivCo? [I summarize with some direct questions at the bottom of this email.] I spent time last night trying to eliminate -dcore-lint errors from my record and variant library using the coxswain row types plugin. I made some progress, but I'm currently stuck, as discussed on this github Issue. https://github.com/nfrisby/coxswain/issues/3#issuecomment-330577609https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnfrisby%2Fcoxswain%2Fissues%2F3%23issuecomment-330577609&data=02%7C01%7Csimonpj%40microsoft.com%7Cde0675bbb584495a2f8008d4ff764c72%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636414330952932223&sdata=lPLcpIlb%2BhivQdCUoVOPUgYDHeEDaMX660NQS%2BQyyBw%3D&reserved=0 Here's the relevant bit: The latest unresolved -dcore-lint error is an out-of-scope cobox co var. I'm certainly not creating it directly (there are no U(plugin:coxswain,... in the Core Lint warning), but I have to wonder if my somewhat loose use of UnivCo is violating some assumptions somewhere that's causing GHC to drop the co var binding or overlook this occurrence of it on a renaming/subst pass. I checked UnivCo for source comments looking for anything it should not be used for, but I didn't find an obvious explanation along those lines. I haven't yet been able to effectively distill the test case. I'm doing this all at -O0. With `-ddump-tc-trace`, I can see the offending cobox (cobox_a67M) is present in an "implication evbinds" listing after a "solveImplication end }" delimiter, but that's the last obvious binding of it. [G] cobox_a67J = CO Sym cobox_a654, [G] cobox_a67M = cobox_a67J `cast` U(plugin:coxswain,...) cobox_a654 is introduced by a GADT pattern match. I'm also not seeing obvious occurrences of cobox_a67M, but I think the reason is that I'm seeing several (Sym cobox) with no uniques printed (even with `-dppr-debug`). Those are probably the cobox in question, but I can't confirm. Questions: 1) Is there a robust way to ensure that covar's uniques are always printed? (Is the pprIface reuse with a free cobox part of the issue here?) 2) Is my plugin asking for this kind of trouble by using UnivCo to cast coboxes? 3) If I spent the effort to create non-UnivCo coercions where possible, would that likely help? This is currently an "eventually" task, but I haven't seen an urgency for it yet. I could bump its priority if it might help. E.G. I'm using UnivCo to cast entire givens when all I'm doing is reducing a type family application somewhere "deep" within the given's predtype. I could, with considerable effort, instead wrap a single, localized UnivCo within a bunch of non-UnivCo "lifting" coercion constructors. Would that likely help? 3) Is there a usual suspect for this kind of situation where a cobox binding is seemingly dropped (by the typechecker) even though there's an occurrence of it? Thank you for your time. -Nick _______________________________________________ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devshttps://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7C2b0edffd514b4da49abc08d50ec07ff9%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636431142301735979&sdata=cwFHlK9YaeaZqNxGvRuHRDeMKMCs0NsDi3lq5UZDZ1g%3D&reserved=0