Bits and bobs in the Coercible solver.
ClosedPublic

Authored by goldfire on Jun 8 2015, 9:36 PM.

Details

Summary

These are various fixes to the Coercible solver, as prompted
by work in updating the ICFP paper on Coercible to a JFP paper.

Please check the updates around matchableGivens, near matchClassInst
in TcInteract and canDecomposableTyConApp in TcCanonical.

Test Plan

validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Branch
master
Lint
Lint SkippedExcuse: lint hangs
Unit
Unit Tests Skipped
Build Status
Buildable 4424
Build 4459: GHC Patch Validation (amd64/Linux)
goldfire updated this revision to Diff 3164.Jun 8 2015, 9:36 PM
goldfire retitled this revision from to Bits and bobs in the Coercible solver..
goldfire updated this object.
goldfire edited the test plan for this revision. (Show Details)
goldfire added reviewers: austin, simonpj.
goldfire updated the Trac tickets for this revision.
simonpj edited edge metadata.Jun 9 2015, 5:46 AM

You didn't modify the comments with isDistinctTyCon in TyCon. When exactly are two TyCons "distinct"? I think Int and Age are not distinct, so maybe it's this: if S and T are both distinct, and S ~R T, then S=T? Specifically, not newtypes, but data types and data families.

Ditto isDecomposableTyCon.

Also, in canEqFailure, why do we recurse to can_eq_nc when the coercion is non-Refl?

compiler/typecheck/TcCanonical.hs
612

Whoa! Why not use canEqFailure here? Is there some mysterious reason why not?

648

These THREE conditions are terribly convoluted, especially since it is followed by ANOTHER case involving ReprEq and isDistinctTyCon. (Admittedly when tc1/=tc2.)

I wonder if this code might be better in canDecomposableTyConAppOK, which deals with the tc1=tc2 and same-length tys situation? It also has cases for G/W/D.

691

In this context ~R would be better than Coercible, esp given the previous example.

706

This note is desperately hard to understand. EXAMPLES!

707–708

I think that the implication here is that only Givens use NthCo; so we never decompose [G] N t1 ~ N t2, where N is a newtype. Say so! And we need to clarity the relationship between isDiistinctTyCon and isNewTyCon.

709

Example!

711

This is flat-out false. Right at the top of can_eq_nc we have

can_eq_nc' _flat _rdr_env _envs ev eq_rel
          (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _
  | isDecomposableTyCon tc1
  , isDecomposableTyCon tc2
  = canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2

So the types are not flat!

I think the comment is weird. If we see [W] (N s ~R N t), then decomposing to [W] s ~r t, where r comes from the role of N, is a great idea, even if N's data constructor is in scope!

You can see how confused I am

goldfire updated this revision to Diff 3181.Jun 9 2015, 7:06 AM
goldfire edited edge metadata.

Fix import statement

In D968#25918, @simonpj wrote:

You didn't modify the comments with isDistinctTyCon in TyCon. When exactly are two TyCons "distinct"? I think Int and Age are not distinct, so maybe it's this: if S and T are both distinct, and S ~R T, then S=T? Specifically, not newtypes, but data types and data families.

You're right. I updated part of the comment, but not the part you were looking at. Fixed.

Ditto isDecomposableTyCon.

OK.

Also, in canEqFailure, why do we recurse to can_eq_nc when the coercion is non-Refl?

Historical reasons. Fixed.

compiler/typecheck/TcCanonical.hs
612

Because can_eq_app is only called on already-flattened things. canEqFailure would just flatten again, which is silly. Will add comment.

648

Added some comments. I think having all the checks up front is easier than spreading them between two functions.

711

I'm afraid your comment is flat-out false. Above the case you cite are two clauses that unwrap newtypes (assuming imported constructors and no perverse recursiveness). can_eq_nc' unwraps vanilla synonyms, checks for reflexivity and then, fairly soon in, unwraps newtypes.

Decomposing is a bad idea. I've beefed up the comment, hopefully dispelling your confusion.

goldfire updated this revision to Diff 3182.Jun 9 2015, 11:15 AM

Response to SPJ's comments

goldfire updated this revision to Diff 3183.Jun 9 2015, 3:09 PM

Fix egregious error in matchableGivens stuff

goldfire updated this revision to Diff 3184.Jun 9 2015, 3:54 PM
  • Testsuite wibble around decomposing newtypes.

This actually improves an error message.

bgamari added inline comments.Jun 15 2015, 7:20 AM
compiler/typecheck/TcCanonical.hs
685

I believe (T a) should be (TF a).

goldfire updated this revision to Diff 3254.Jun 15 2015, 8:00 PM
goldfire marked 2 inline comments as done.

Write up Note [Decomposing equalities] in TcCanonical, as well
as a few more minor simplifications.

goldfire updated this revision to Diff 3255.Jun 15 2015, 8:02 PM
  • Fix typo in comment
simonpj accepted this revision.Jun 16 2015, 2:41 AM
simonpj edited edge metadata.

Let's land this!

compiler/typecheck/TcCanonical.hs
649

So it sounds as if (not (isNewTyCon tc1)) would do. But that's not quite right, is it?

726

Add the (IO Int ~R IO Age) example here! It's totally compelling!

So the question becomes: is it ever *bad* to decompose wanted newtypes? And that is the tricky case.

820

Worth adding a pointer to Trac #10534 here, or perhaps even the example itself

861

But alas the comment does not explain why we flatten! It should.

compiler/types/TyCon.hs
1334

Can you remind us what "generative wrt nominal equality" means. I think you mean that if S tys ~N R tys, and S,T are "decomposable" TyCons, then S=T? It would e great to use the same language, as isDistinctTyCon. Indeed we might consider changing nomenclature.

This revision is now accepted and ready to land.Jun 16 2015, 2:41 AM

More comments

compiler/types/TyCon.hs
1213

Point to the hew carefully written Notes in TcCanonical!!!
Same for isGenerative

1240

Let's rename isDistinctAlgRhs; it seems like a hangover from isDistinctTyCon. isInjectiveRhs? Interestingly it seems to be only used at representational role.

compiler/types/Unify.hs
286

I like this, but it's quite a separate change isn't it? Two patches?

goldfire marked 2 inline comments as done.Jun 16 2015, 8:02 AM

Just validating locally now. (Phab's validation has done something very strange in TcSMonad!)

compiler/typecheck/TcCanonical.hs
820

I added the pointer. Once you think of the problem, I don't think this case is all too subtle.

goldfire closed this revision.Jun 16 2015, 1:33 PM

This one has landed.