Overhaul the Overhauled Pattern Match Checker

Overhaul the Overhauled Pattern Match Checker

* Changed the representation of Value Set Abstractions. Instead of
using a prefix tree, we now use a list of Value Vector Abstractions.
The set of constraints Delta for every Value Vector Abstraction is the
oracle state so that we solve everything only once.

* Instead of doing everything lazily, we prune at once (and in general
everything is much stricter). Hence, an example written with pattern
guards is checked in almost the same time as the equivalent with
pattern matching.

* Do not store the covered and the divergent sets at all. Since what we
only need is a yes/no (does this clause cover anything? Does it force
any thunk?) We just keep a boolean for each.

* Removed flags `-Wtoo-many-guards` and `-ffull-guard-reasoning`.
Replaced with `fmax-pmcheck-iterations=n`. Still debatable what should
the default `n` be.

* When a guard is for sure not going to contribute anything, we treat
it as such: The oracle is not called and cases `CGuard`, `UGuard` and
`DGuard` from the paper are not happening at all (the generation of a
fresh variable, the unfolding of the pattern list etc.). his combined
with the above seems to be enough to drop the memory increase for test
T783 down to 18.7%.

* Do not export function `dsPmWarn` (it is now called directly from
within `checkSingle` and `checkMatches`).

* Make `PmExprVar` hold a `Name` instead of an `Id`. The term oracle
does not handle type information so using `Id` was a waste of
time/space.

* Added testcases T11195, T11303b (data families) and T11374

The patch addresses at least the following:
Trac #11195, #11276, #11303, #11374, #11162

Test Plan: validate

Reviewers: goldfire, bgamari, hvr, austin

Subscribers: simonpj, thomie

Differential Revision: https://phabricator.haskell.org/D1795

1 files changed, 189 insertions, 0 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/T11195.hs b/testsuite/tests/pmcheck/should_compile/T11195.hs
new file mode 100644
index 0000000000..593223f5fc
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T11195.hs
@@ -0,0 +1,189 @@
+{-# OPTIONS_GHC -Woverlapping-patterns -Wincomplete-patterns #-}
+
+module T11195 where
+
+import TyCoRep
+import Coercion
+import Type hiding( substTyVarBndr, substTy, extendTCvSubst )
+import TcType       ( exactTyCoVarsOfType )
+import CoAxiom
+import VarSet
+import VarEnv
+import Pair
+import InstEnv
+
+type NormalCo    = Coercion
+type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity
+type SymFlag = Bool
+type ReprFlag = Bool
+
+chooseRole :: ReprFlag -> Role -> Role
+chooseRole = undefined
+
+wrapRole :: ReprFlag -> Role -> Coercion -> Coercion
+wrapRole = undefined
+
+wrapSym :: SymFlag -> Coercion -> Coercion
+wrapSym = undefined
+
+optForAllCoBndr :: LiftingContext -> Bool
+                -> TyVar -> Coercion -> (LiftingContext, TyVar, Coercion)
+optForAllCoBndr = undefined
+
+opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
+opt_trans = undefined
+
+opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
+         -> Type -> Type -> Coercion
+opt_univ = undefined
+
+opt_co3 :: LiftingContext -> SymFlag -> Maybe Role
+        -> Role -> Coercion -> NormalCo
+opt_co3 = undefined
+
+opt_co2 :: LiftingContext -> SymFlag -> Role -> Coercion -> NormalCo
+opt_co2 = undefined
+
+compatible_co :: Coercion -> Coercion -> Bool
+compatible_co = undefined
+
+etaTyConAppCo_maybe = undefined
+etaAppCo_maybe = undefined
+etaForAllCo_maybe = undefined
+
+matchAxiom = undefined
+checkAxInstCo = undefined
+isAxiom_maybe = undefined
+isCohLeft_maybe = undefined
+isCohRight_maybe = undefined
+
+opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
+opt_transList is = zipWith (opt_trans is)
+
+opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
+opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
+  | d1 == d2
+  , co1 `compatible_co` co2 = undefined
+
+opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
+  | d1 == d2
+  , co1 `compatible_co` co2 = undefined
+
+-- Push transitivity inside instantiation
+opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
+  | ty1 `eqCoercion` ty2
+  , co1 `compatible_co` co2 = undefined
+
+opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
+                  in_co2@(UnivCo p2 r2 _tyl2 tyr2)
+  | Just prov' <- opt_trans_prov p1 p2 = undefined
+  where
+    -- if the provenances are different, opt'ing will be very confusing
+    opt_trans_prov UnsafeCoerceProv UnsafeCoerceProv
+      = Just UnsafeCoerceProv
+    opt_trans_prov (PhantomProv kco1) (PhantomProv kco2)
+      = Just $ PhantomProv $ opt_trans is kco1 kco2
+    opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
+      = Just $ ProofIrrelProv $ opt_trans is kco1 kco2
+    opt_trans_prov (PluginProv str1) (PluginProv str2)
+      | str1 == str2 = Just p1
+    opt_trans_prov _ _ = Nothing
+
+-- Push transitivity down through matching top-level constructors.
+opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1)
+                  in_co2@(TyConAppCo r2 tc2 cos2)
+  | tc1 == tc2 = undefined
+
+opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
+  = undefined
+
+-- Eta rules
+opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
+  | Just cos2 <- etaTyConAppCo_maybe tc co2 = undefined
+
+opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
+  | Just cos1 <- etaTyConAppCo_maybe tc co1 = undefined
+
+opt_trans_rule is co1@(AppCo co1a co1b) co2
+  | Just (co2a,co2b) <- etaAppCo_maybe co2 = undefined
+
+opt_trans_rule is co1 co2@(AppCo co2a co2b)
+  | Just (co1a,co1b) <- etaAppCo_maybe co1 = undefined
+
+-- Push transitivity inside forall
+opt_trans_rule is co1 co2
+  | ForAllCo tv1 eta1 r1 <- co1
+  , Just (tv2,eta2,r2) <- etaForAllCo_maybe co2 = undefined
+
+  | ForAllCo tv2 eta2 r2 <- co2
+  , Just (tv1,eta1,r1) <- etaForAllCo_maybe co1 = undefined
+
+  where
+  push_trans tv1 eta1 r1 tv2 eta2 r2 = undefined
+
+-- Push transitivity inside axioms
+opt_trans_rule is co1 co2
+  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
+  , True <- sym
+  , Just cos2 <- matchAxiom sym con ind co2
+  , let newAxInst = AxiomInstCo con ind
+                      (opt_transList is (map mkSymCo cos2) cos1)
+  , Nothing <- checkAxInstCo newAxInst
+  = undefined
+
+  -- TrPushAxR
+  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
+  , False <- sym
+  , Just cos2 <- matchAxiom sym con ind co2
+  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
+  , Nothing <- checkAxInstCo newAxInst
+  = undefined
+
+  -- TrPushSymAxL
+  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
+  , True <- sym
+  , Just cos1 <- matchAxiom (not sym) con ind co1
+  , let newAxInst = AxiomInstCo con ind
+                      (opt_transList is cos2 (map mkSymCo cos1))
+  , Nothing <- checkAxInstCo newAxInst
+  = undefined
+
+  -- TrPushAxL
+  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
+  , False <- sym
+  , Just cos1 <- matchAxiom (not sym) con ind co1
+  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
+  , Nothing <- checkAxInstCo newAxInst
+  = undefined
+
+  -- TrPushAxSym/TrPushSymAx
+  | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
+  , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
+  , con1 == con2
+  , ind1 == ind2
+  , sym1 == not sym2
+  , let branch = coAxiomNthBranch con1 ind1
+        qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
+        lhs  = coAxNthLHS con1 ind1
+        rhs  = coAxBranchRHS branch
+        pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
+  , all (`elemVarSet` pivot_tvs) qtvs
+  = undefined
+  where
+    co1_is_axiom_maybe = isAxiom_maybe co1
+    co2_is_axiom_maybe = isAxiom_maybe co2
+    role = coercionRole co1 -- should be the same as coercionRole co2!
+
+opt_trans_rule is co1 co2
+  | Just (lco, lh) <- isCohRight_maybe co1
+  , Just (rco, rh) <- isCohLeft_maybe co2
+  , (coercionType lh) `eqType` (coercionType rh)
+  = undefined
+
+opt_trans_rule _ co1 co2        -- Identity rule
+  | (Pair ty1 _, r) <- coercionKindRole co1
+  , Pair _ ty2 <- coercionKind co2
+  , ty1 `eqType` ty2
+  = undefined
+
+opt_trans_rule _ _ _ = Nothing