Take strict fields into account in coverage checking
ClosedPublic

Authored by RyanGlScott on Aug 22 2018, 10:20 AM.

Details

Summary

The current pattern-match coverage checker implements the
formalism presented in the GADTs Meet Their Match paper in a
fairly faithful matter. However, it was discovered recently that
there is a class of unreachable patterns that
GADTs Meet Their Match does not handle: unreachable code due to
strict argument types, as demonstrated in Trac #15305. This patch
therefore goes off-script a little and implements an extension to
the formalism presented in the paper to handle this case.

Essentially, when determining if each constructor can be matched on,
GHC checks if its associated term and type constraints are
satisfiable. This patch introduces a new form of constraint,
NonVoid(ty), and checks if each constructor's strict argument types
satisfy NonVoid. If any of them do not, then that constructor is
deemed uninhabitable, and thus cannot be matched on. For the full
story of how this works, see
Note [Extensions to GADTs Meet Their Match].

Along the way, I did a little bit of much-needed refactoring. In
particular, several functions in Check were passing a triple of
(ValAbs, ComplexEq, Bag EvVar) around to represent a constructor
and its constraints. Now that we're adding yet another form of
constraint to the mix, I thought it appropriate to turn this into
a proper data type, which I call InhabitationCandidate.

Test Plan

make test TEST=T15305

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.
RyanGlScott created this revision.Aug 22 2018, 10:20 AM
  • Grammar fix
RyanGlScott planned changes to this revision.Aug 22 2018, 2:06 PM

Ack, I should have ran ./validate before submitting, since I failed to take into account that data types that are {-# SOURCE #-} imported from .hs-boot files (like the imported DynFlags in Outputable) appear different to the coverage checker than non-{-# SOURCE #-}-imported things, since tyConDataCons returns different things for them. I think I can work around this pretty easily, though.

  • Skip abstract tycons in inhabitationCandidates

OK, now things should be good to go.

simonpj requested changes to this revision.Aug 22 2018, 3:39 PM

Good! The main issue is whether it makes sense to factor out the non-void check as a separate function (I hope so), and making the comments match the code.

compiler/deSugar/Check.hs
432–434

This sequence of calling inhabitationCandidates and then checking for satisfiability is superficially similar to the code in nonVoid below in pmIsSatisfiable. Can anything be shared?

653

Could you factor this out into

nonVoid :: Type -> PmM Bool

which does what it sounds like? That would connect the code with the comments! Then pmIsSatisfiable might be more perspicuous

non_voids <- mapM nonVoiid strict_arg_tys
pure $ if and non_voids -- Check if each strict argument type
                                      -- is inhabitable
               then Just (term_cs, ty_cs)
               else Nothing
1418

But in fact we *don't* conjure up a new form of constraint! We just call nonVoid.

Making the Note match the code would be good.

This revision now requires changes to proceed.Aug 22 2018, 3:39 PM
RyanGlScott marked 3 inline comments as done.
compiler/deSugar/Check.hs
432–434

The code in checkEmptyCase' and nonVoid does share a passing similarity, but only that, I think. There's enough little differences (using pmIsSatisfiable vs. tmTyCsAreSatisfiable, different return types, using concatMapM vs. forM) to the point that if you did try to factor out the code, I think you'd simply obscure what's really going on.

1418

I've revised the language in the Note. Is this to your liking now?

Much, much better! Thank you.

Thus engaged, I made some more refactoring suggestions. But even if you like them (I hope you will) they could be a separate patch.

compiler/deSugar/Check.hs
441–442

Refactoring suggestion: instead of [(va, all_ty_cs, tm_state')] return ValVec [v] (MkDelta all_ty_cs tm_state').

Or even Uncovered (ValVec ...).

Simpler, more direct, elimiantes a subsequent map.

445

Refactoring suggestion: make pmIsSatisfiable return a Delta. So much nicer!

633

Again tmTyCsArSatisfiable could return a Maybe Delta.

639

I expected mapM. Is traverse the same as mapM in this context. (My unfamiliarity with the traverse world.) Any reason not to use mapM, or is it just a style you prefer?

650

These first two args are just a Delta

652

add

True => it might be inhabitable
False => it is definitely empty
659

mapM again, but with the arguments flipped.

If it were me I'd say mapM candidateIsInhabitable cands, and pull out that lambda into a separate function with its own type and comment. That function is a useful abstraction in its own right.

(This is independent of mapM vs traverse, which I'm relaxed about.)

1374

perhpas again these two fields can be combined into a Delta

1420

Not quite true: I think it returns False if it is definitely uninhabited, and True if unsure.

1420

Also, I believe that throughout "uninhabited" means "uninhabited except by bottom". Correct? If so it'd be good to say so, esp in the specification of nonVoid.

RyanGlScott marked 12 inline comments as done.
compiler/deSugar/Check.hs
441–442

I decided to inline the ValVec part only.

639

traverse is just a more general version of mapM (with an Applicative constraint instead of a Monad constraint). I prefer traverse, since Applicative is now a superclass of Monad, which means that mapM only exists as a method of Traversable for historical reasons, much like the pure/return distinction.

659

I factored out that lambda into cand_tm_ty_cs_are_satisfiable.

1374

I'm going to decline this suggestion, for a handful of reasons:

  1. Each InhabitationCandidate specifically takes a single ComplexEq, whereas a Delta contains a TmState, which stores a list of ComplexEqs. I think using Delta here might obscure this fact.
  2. If I did store a Delta in InhabitationCandidate, I'd have to muddy up pmIsSatisfiable by explicitly digging out the ComplexEqs from the Delta and use tmOracle instead of the simpler solveOneEq.
  3. Actually turning a ComplexEq into a TmState in mkOneConFull is surprisingly annoying. AFAICT, the only way to accomplish this is by way of solveOneEq, but that returns a Maybe TmState instead of a TmState, so we'd have to extract the underlying TmState with fromJust or something like this. Blegh.

If we decide to store multiple term constraints per InhabitationCandidate in the future, maybe we can revisit this, but for now, I'm inclined to leave this part alone.

Looking good. Just a couple more suggestions

compiler/deSugar/Check.hs
631

Now that it returns a Delta surely it should *take* Delta!! That is, combine the first and third args into Delta! (All you need do then, I think, is to make pmInitialTmTyCs return a Delta. That saves code in mkInitialUncovered too. All good.

1374

Ah, yes. Delta is the accumulated, ambient constraints. The ones in an InhabitationCandidate are just the extra constraints from this particular pattern match. I'd missed that.

RyanGlScott marked 6 inline comments as done.
compiler/deSugar/Check.hs
631

I decided to take your advice, but instead combine the second and fourth args into a Delta (the first and third args come from an InhabitationCandidate and are awkward to stuff into a Delta, for the same reasons I cited when I decided not to put a Delta in an InhabitationCandidate).

simonpj added inline comments.Aug 23 2018, 5:49 PM
compiler/deSugar/Check.hs
631

Ah yes, I mis counted. I meant second and fourth! So much nicer now.

In that case, I believe I've addressed all of your concerns now. Is this patch ready to land?

simonpj accepted this revision.Aug 24 2018, 3:09 AM

In that case, I believe I've addressed all of your concerns now. Is this patch ready to land?

Yes! Lovely

This revision is now accepted and ready to land.Aug 24 2018, 3:09 AM
This revision was automatically updated to reflect the committed changes.