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-boun...@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

Reply via email to