zonkCt tries to maintain the canonical form of a Ct.
ClosedPublic

Authored by christiaanb on Feb 8 2017, 3:43 AM.

Details

Summary

For example,

  • a CDictCan should stay a CDictCan;
  • a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
  • a CHoleCan should stay a CHoleCan

Why? For CDicteqCan see Trac Trac #11525.

Test Plan

Validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
christiaanb created this revision.Feb 8 2017, 3:43 AM
christiaanb edited the summary of this revision. (Show Details)Feb 8 2017, 3:59 AM
christiaanb added a reviewer: adamgundry.
simonpj requested changes to this revision.Feb 8 2017, 4:03 AM

I'd much prefer to follow comment:7 on Trac Trac #11525. Was there some reason you chose not to do that?

This revision now requires changes to proceed.Feb 8 2017, 4:03 AM
christiaanb updated this revision to Diff 11032.Feb 8 2017, 4:19 AM
christiaanb edited edge metadata.
  • Fix T11525 test case

I'd much prefer to follow comment:7 on Trac Trac #11525. Was there some reason you chose not to do that?

Initially I tried to add the following clause to zonkCt:

zonkCt ct@(CDictCan { cc_ev = ev })
  = do { ev' <- zonkCtEvidence ev
       ; return $ ct { cc_ev = ev' } }

but then the testsuite regresses with:

T7474.hs:16:11: error:
    • Could not deduce (C' (T a) p) arising from a use of ‘c’
      from the context: C' (T a) p
        bound by the inferred type of f :: C' (T a) p => E a -> p
        at T7474.hs:16:1-13
      or from: C a
        bound by a pattern with constructor:
                   E :: forall p. C p => T (T p) -> E p,
                 in an equation for ‘f’
        at T7474.hs:16:4-6
    • In the expression: c d
      In an equation for ‘f’: f (E d) = c d

*** unexpected failure for T7474(normal)

Changing it to:

zonkCt ct@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = args })
  = do { ev' <- zonkCtEvidence ev
       ; if ctev_pred ev' `eqType` mkTyConApp (classTyCon cls) args
         then return $ ct { cc_ev = ev' }
         else return (mkNonCanonical ev') }

, however, doesn't solve the problem of Trac #11525; although the testsuite passes.

Given that I'm completely unfamiliar with this part of the code, I gave up trying to fix zonkCt, as I have no idea of where to look.
That is why tried the route of the current patch, where I just run canonicalize pass again.
If you could give me a hint as how to fix zonkCt for the CDictCan case, I'm wanting to give it another try.

I mostly submitted this patch because I saw that the 8.2 branch is being cut soon, and I'd really like a fix for Trac #11525 to be in 8.2.1.

It seems that

zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
  = do { ev'   <- zonkCtEvidence ev
       ; args' <- mapM zonkTcType args
       ; return $ ct { cc_ev = ev', cc_tyargs = args' } }

Solves both Trac #11525, and passes the testsuite.
However, as this is the result of trial-and-error, I'm somewhat uncomfortable with it.

It seems that... works

Great! That's just what I intendedin comment:7, though perhaps not well explained. Do that for CDictCan. For CTyEqCan

zonkCt ct@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = ev })
 = do { tv_ty' <- zonkTcTyVar tv
          ; ev' <- zonkCtEvidence 
          ; case getTyVar_maybe tv_ty' of
                Just tv' -> do { rhs' <- zonkTcType rhs
                                      ; return (ct { cc_tyvar = tv', cc_rhs = rhs', cc_ev = ev' }) }
                Nothing -> return (mkNonCanonical ev') }

and similarly for CHoleCan.

Add comments:

Note [zonkCt behaviour]
~~~~~~~~~~~~~~~
zonkCt tries to maintain the canonical form of a Ct.  For example,
  - a CDictCan should stay a CDictCan; 
  - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.).
  - a CHoleCan should stay a CHoleCan

Why?  For CDicteqCan see Trac #11525.
For CHoleCan, once we forget that it's a hole, we can never recover that info.

NB: we do not expect to see any CFunEqCans, because zonkCt is only
called on unflattened constraints.

Sound OK?

Sound OK?

Yes, I'll do that, thanks.

  • Add a test for Trac #11525
  • zonkCt tries to maintain the canonical form of a Ct.
christiaanb retitled this revision from Run canonicalize pass after type-checker plugins are done to zonkCt tries to maintain the canonical form of a Ct..Feb 8 2017, 12:09 PM
christiaanb edited the summary of this revision. (Show Details)
bgamari added inline comments.Feb 8 2017, 2:04 PM
compiler/typecheck/TcMType.hs
1367

Is this something we should panic on in that case?

christiaanb added inline comments.Feb 8 2017, 4:05 PM
compiler/typecheck/TcMType.hs
1367

I guess that depends on whether a CFunEqCan at this stage could lead to unsoundness, in that case I think a panic would be warrented. If not, I would prefer an ASSERT so that it is only triggered in a Debug compiler; that way, code in the wild can keep on compiling.

bgamari added inline comments.Feb 8 2017, 4:06 PM
compiler/typecheck/TcMType.hs
1367

That sounds fine to me.

bgamari requested changes to this revision.Feb 8 2017, 10:38 PM

Perhaps you could add the ASSERT then?

This revision now requires changes to proceed.Feb 8 2017, 10:38 PM
simonpj accepted this revision.Feb 9 2017, 3:58 AM

By all means add the ASSERT (with an explanation). Then good.

compiler/typecheck/TcMType.hs
1364

CDictEqCan (capitalisation). Perhaps summarise the issue here?

1369

"Constraints are always re-flattened etc" add "by the canonicaliser in TcCanonical"

christiaanb edited edge metadata.
christiaanb retitled this revision from zonkCt tries to maintain the canonical form of a Ct. to zonkCt tries to maintain the canonical form of a Ct..
  • zonkCt tries to maintain the canonical form of a Ct.
  • zonkCt tries to maintain the canonical form of a Ct.
bgamari accepted this revision.Feb 9 2017, 11:04 PM

Looks good. Thanks @christianbb!

This revision is now accepted and ready to land.Feb 9 2017, 11:04 PM
This revision was automatically updated to reflect the committed changes.