Invariants about UnivCo?

[Nicolas Frisby]

[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

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170919/84686e1d/attachment.html>