[Git][ghc/ghc][wip/pmcheck-ncon] Add `PmNCons` to `Check` for correct warnings in the presence of `COMPLETE` groups

Sebastian Graf gitlab at gitlab.haskell.org
Wed May 29 11:05:44 UTC 2019



Sebastian Graf pushed to branch wip/pmcheck-ncon at Glasgow Haskell Compiler / GHC


Commits:
4e2f1875 by Sebastian Graf at 2019-05-29T11:05:21Z
Add `PmNCons` to `Check` for correct warnings in the presence of `COMPLETE` groups

Previously, we had an elaborate mechanism for selecting the warnings to
generate in the presence of different `COMPLETE` matching groups that,
albeit finely-tuned, produced wrong results from an end user's
perspective in some cases (#13363).

The underlying issue is that at the point where the `ConVar` case has to
commit to a particular `COMPLETE` group, there's not enough information
to do so and the status quo was to just enumerate all possible complete
sets nondeterministically.
The `getResult` function would then pick the outcome according to
metrics defined in accordance to the user's guide. But crucially, it
lacked knowledge about the order in which affected clauses appear,
leading to the surprising behavior in #13363.

The introduction of an `PmNCons` variant in `PmPat` fixes this: Instead
of committing to a particular `COMPLETE` group in the `ConVar` case,
we now split off the matching constructor incrementally and record the
newly covered case in `PmNCons`.
After all clauses have been processed this way, we filter out any value
vector abstractions from the uncovered set involving `PmNCons` whose set
of covered constructors completely overlap a `COMPLETE` set.

- - - - -


18 changed files:

- compiler/deSugar/Check.hs
- compiler/deSugar/PmExpr.hs
- compiler/deSugar/PmPpr.hs
- compiler/deSugar/TmOracle.hs
- compiler/utils/Binary.hs
- compiler/utils/Outputable.hs
- docs/users_guide/glasgow_exts.rst
- libraries/binary
- + testsuite/tests/perf/compiler/ManyAlternatives.hs
- + testsuite/tests/pmcheck/complete_sigs/T13363a.hs
- + testsuite/tests/pmcheck/complete_sigs/T13363a.stderr
- + testsuite/tests/pmcheck/complete_sigs/T13363b.hs
- + testsuite/tests/pmcheck/complete_sigs/T13363b.stderr
- testsuite/tests/pmcheck/complete_sigs/all.T
- testsuite/tests/pmcheck/should_compile/all.T
- + testsuite/tests/pmcheck/should_compile/pmc008.hs
- + testsuite/tests/pmcheck/should_compile/pmc009.hs
- + testsuite/tests/pmcheck/should_compile/pmc010.hs


Changes:

=====================================
compiler/deSugar/Check.hs
=====================================
@@ -55,20 +55,19 @@ import TyCoRep
 import Type
 import UniqSupply
 import DsUtils       (isTrueLHsExpr)
-import Maybes        (expectJust)
+import Maybes        (MaybeT (..), expectJust)
 import qualified GHC.LanguageExtensions as LangExt
 
-import Data.List     (find)
+import Data.List     (find, (\\))
 import Data.Maybe    (catMaybes, isJust, fromMaybe)
-import Control.Monad (forM, when, forM_, zipWithM, filterM)
+import Control.Monad (forM, when, guard, forM_, zipWithM, filterM)
+import Control.Monad.Trans.Class (lift)
 import Coercion
 import TcEvidence
 import TcSimplify    (tcNormalise)
 import IOEnv
 import qualified Data.Semigroup as Semi
 
-import ListT (ListT(..), fold, select)
-
 {-
 This module checks pattern matches for:
 \begin{enumerate}
@@ -91,72 +90,33 @@ The algorithm is based on the paper:
 %************************************************************************
 -}
 
--- We use the non-determinism monad to apply the algorithm to several
--- possible sets of constructors. Users can specify complete sets of
--- constructors by using COMPLETE pragmas.
--- The algorithm only picks out constructor
--- sets deep in the bowels which makes a simpler `mapM` more difficult to
--- implement. The non-determinism is only used in one place, see the ConVar
--- case in `pmCheckHd`.
-
-type PmM a = ListT DsM a
+type PmM = DsM
 
-liftD :: DsM a -> PmM a
-liftD m = ListT $ \sk fk -> m >>= \a -> sk a fk
-
--- Pick the first match complete covered match or otherwise the "best" match.
--- The best match is the one with the least uncovered clauses, ties broken
--- by the number of inaccessible clauses followed by number of redundant
--- clauses.
---
--- This is specified in the
--- "Disambiguating between multiple ``COMPLETE`` pragmas" section of the
--- users' guide. If you update the implementation of this function, make sure
--- to update that section of the users' guide as well.
-getResult :: PmM PmResult -> DsM PmResult
-getResult ls
-  = do { res <- fold ls goM (pure Nothing)
-       ; case res of
-            Nothing -> panic "getResult is empty"
-            Just a  -> return a }
-  where
-    goM :: PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult)
-    goM mpm dpm = do { pmr <- dpm
-                     ; return $ Just $ go pmr mpm }
-
-    -- Careful not to force unecessary results
-    go :: Maybe PmResult -> PmResult -> PmResult
-    go Nothing rs = rs
-    go (Just old@(PmResult prov rs (UncoveredPatterns us) is)) new
-      | null us && null rs && null is = old
-      | otherwise =
-        let PmResult prov' rs' (UncoveredPatterns us') is' = new
-        in case compareLength us us'
-                `mappend` (compareLength is is')
-                `mappend` (compareLength rs rs')
-                `mappend` (compare prov prov') of
-              GT  -> new
-              EQ  -> new
-              LT  -> old
-    go (Just (PmResult _ _ (TypeOfUncovered _) _)) _new
-      = panic "getResult: No inhabitation candidates"
-
-data PatTy = PAT | VA -- Used only as a kind, to index PmPat
+-- | Used only as a kind, to index PmPat
+data PatTy = PAT | VA
 
 -- The *arity* of a PatVec [p1,..,pn] is
 -- the number of p1..pn that are not Guards
 
 data PmPat :: PatTy -> * where
+  -- | For the arguments' meaning see 'HsPat.ConPatOut'.
   PmCon  :: { pm_con_con     :: ConLike
             , pm_con_arg_tys :: [Type]
             , pm_con_tvs     :: [TyVar]
             , pm_con_dicts   :: [EvVar]
             , pm_con_args    :: [PmPat t] } -> PmPat t
-            -- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs
   PmVar  :: { pm_var_id   :: Id } -> PmPat t
-  PmLit  :: { pm_lit_lit  :: PmLit } -> PmPat t -- See Note [Literals in PmPat]
+  -- | See Note [Literals in PmPat]
+  PmLit  :: { pm_lit_lit  :: PmLit } -> PmPat t
+  -- | Literal values the wrapped 'Id' cannot take on.
+  -- See Note [PmNLit and PmNCon].
   PmNLit :: { pm_lit_id   :: Id
             , pm_lit_not  :: [PmLit] } -> PmPat 'VA
+  -- | Top-level 'ConLike's the wrapped 'Id' cannot take on.
+  -- See Note [PmNLit and PmNCon].
+  PmNCon :: { pm_con_id   :: Id
+            , pm_con_grps :: [[ConLike]]
+            , pm_con_not  :: [ConLike] } -> PmPat 'VA
   PmGrd  :: { pm_grd_pv   :: PatVec
             , pm_grd_expr :: PmExpr } -> PmPat 'PAT
   -- | A fake guard pattern (True <- _) used to represent cases we cannot handle.
@@ -199,8 +159,7 @@ data Covered = Covered | NotCovered
   deriving Show
 
 instance Outputable Covered where
-  ppr (Covered) = text "Covered"
-  ppr (NotCovered) = text "NotCovered"
+  ppr = text . show
 
 -- Like the or monoid for booleans
 -- Covered = True, Uncovered = False
@@ -217,8 +176,7 @@ data Diverged = Diverged | NotDiverged
   deriving Show
 
 instance Outputable Diverged where
-  ppr Diverged = text "Diverged"
-  ppr NotDiverged = text "NotDiverged"
+  ppr = text . show
 
 instance Semi.Semigroup Diverged where
   Diverged <> _ = Diverged
@@ -229,51 +187,26 @@ instance Monoid Diverged where
   mempty = NotDiverged
   mappend = (Semi.<>)
 
--- | When we learned that a given match group is complete
-data Provenance =
-                  FromBuiltin -- ^  From the original definition of the type
-                              --    constructor.
-                | FromComplete -- ^ From a user-provided @COMPLETE@ pragma
-  deriving (Show, Eq, Ord)
-
-instance Outputable Provenance where
-  ppr  = text . show
-
-instance Semi.Semigroup Provenance where
-  FromComplete <> _ = FromComplete
-  _ <> FromComplete = FromComplete
-  _ <> _ = FromBuiltin
-
-instance Monoid Provenance where
-  mempty = FromBuiltin
-  mappend = (Semi.<>)
-
 data PartialResult = PartialResult {
-                        presultProvenance :: Provenance
-                         -- keep track of provenance because we don't want
-                         -- to warn about redundant matches if the result
-                         -- is contaminated with a COMPLETE pragma
-                      , presultCovered :: Covered
+                        presultCovered :: Covered
                       , presultUncovered :: Uncovered
                       , presultDivergent :: Diverged }
 
 instance Outputable PartialResult where
-  ppr (PartialResult prov c vsa d)
-           = text "PartialResult" <+> ppr prov <+> ppr c
-                                  <+> ppr d <+> ppr vsa
+  ppr (PartialResult c vsa d)
+           = text "PartialResult" <+> ppr c <+> ppr d <+> ppr vsa
 
 
 instance Semi.Semigroup PartialResult where
-  (PartialResult prov1 cs1 vsa1 ds1)
-    <> (PartialResult prov2 cs2 vsa2 ds2)
-      = PartialResult (prov1 Semi.<> prov2)
-                      (cs1 Semi.<> cs2)
+  (PartialResult cs1 vsa1 ds1)
+    <> (PartialResult cs2 vsa2 ds2)
+      = PartialResult (cs1 Semi.<> cs2)
                       (vsa1 Semi.<> vsa2)
                       (ds1 Semi.<> ds2)
 
 
 instance Monoid PartialResult where
-  mempty = PartialResult mempty mempty [] mempty
+  mempty = PartialResult mempty [] mempty
   mappend = (Semi.<>)
 
 -- newtype ChoiceOf a = ChoiceOf [a]
@@ -291,15 +224,13 @@ instance Monoid PartialResult where
 --
 data PmResult =
   PmResult {
-      pmresultProvenance   :: Provenance
-    , pmresultRedundant    :: [Located [LPat GhcTc]]
+      pmresultRedundant    :: [Located [LPat GhcTc]]
     , pmresultUncovered    :: UncoveredCandidates
     , pmresultInaccessible :: [Located [LPat GhcTc]] }
 
 instance Outputable PmResult where
   ppr pmr = hang (text "PmResult") 2 $ vcat
-    [ text "pmresultProvenance" <+> ppr (pmresultProvenance pmr)
-    , text "pmresultRedundant" <+> ppr (pmresultRedundant pmr)
+    [ text "pmresultRedundant" <+> ppr (pmresultRedundant pmr)
     , text "pmresultUncovered" <+> ppr (pmresultUncovered pmr)
     , text "pmresultInaccessible" <+> ppr (pmresultInaccessible pmr)
     ]
@@ -324,11 +255,11 @@ instance Outputable UncoveredCandidates where
 
 -- | The empty pattern check result
 emptyPmResult :: PmResult
-emptyPmResult = PmResult FromBuiltin [] (UncoveredPatterns []) []
+emptyPmResult = PmResult [] (UncoveredPatterns []) []
 
 -- | Non-exhaustive empty case with unknown/trivial inhabitants
 uncoveredWithTy :: Type -> PmResult
-uncoveredWithTy ty = PmResult FromBuiltin [] (TypeOfUncovered ty) []
+uncoveredWithTy ty = PmResult [] (TypeOfUncovered ty) []
 
 {-
 %************************************************************************
@@ -341,8 +272,8 @@ uncoveredWithTy ty = PmResult FromBuiltin [] (TypeOfUncovered ty) []
 -- | Check a single pattern binding (let)
 checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
 checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
-  tracePmD "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
-  mb_pm_res <- tryM (getResult (checkSingle' locn var p))
+  tracePm "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
+  mb_pm_res <- tryM (checkSingle' locn var p)
   case mb_pm_res of
     Left  _   -> warnPmIters dflags ctxt
     Right res -> dsPmWarn dflags ctxt res
@@ -350,25 +281,25 @@ checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
 -- | Check a single pattern binding (let)
 checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> PmM PmResult
 checkSingle' locn var p = do
-  liftD resetPmIterDs -- set the iter-no to zero
-  fam_insts <- liftD dsGetFamInstEnvs
-  clause    <- liftD $ translatePat fam_insts p
+  resetPmIterDs -- set the iter-no to zero
+  fam_insts <- dsGetFamInstEnvs
+  clause    <- translatePat fam_insts p
   missing   <- mkInitialUncovered [var]
   tracePm "checkSingle': missing" (vcat (map pprValVecDebug missing))
                                   -- no guards
-  PartialResult prov cs us ds <- runMany (pmcheckI clause []) missing
-  let us' = UncoveredPatterns us
+  PartialResult cs us ds <- runMany (pmcheckI clause []) missing
+  us' <- UncoveredPatterns <$> normaliseUncovered us
   return $ case (cs,ds) of
-    (Covered,  _    )         -> PmResult prov [] us' [] -- useful
-    (NotCovered, NotDiverged) -> PmResult prov m  us' [] -- redundant
-    (NotCovered, Diverged )   -> PmResult prov [] us' m  -- inaccessible rhs
+    (Covered,  _    )         -> PmResult [] us' [] -- useful
+    (NotCovered, NotDiverged) -> PmResult m  us' [] -- redundant
+    (NotCovered, Diverged )   -> PmResult [] us' m  -- inaccessible rhs
   where m = [cL locn [cL locn p]]
 
 -- | Exhaustive for guard matches, is used for guards in pattern bindings and
 -- in @MultiIf@ expressions.
 checkGuardMatches :: HsMatchContext Name          -- Match context
                   -> GRHSs GhcTc (LHsExpr GhcTc)  -- Guarded RHSs
-                  -> DsM ()
+                  -> PmM ()
 checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do
     dflags <- getDynFlags
     let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss)
@@ -383,14 +314,14 @@ checkGuardMatches _ (XGRHSs _) = panic "checkGuardMatches"
 
 -- | Check a matchgroup (case, functions, etc.)
 checkMatches :: DynFlags -> DsMatchContext
-             -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
+             -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM ()
 checkMatches dflags ctxt vars matches = do
-  tracePmD "checkMatches" (hang (vcat [ppr ctxt
+  tracePm "checkMatches" (hang (vcat [ppr ctxt
                                , ppr vars
                                , text "Matches:"])
                                2
                                (vcat (map ppr matches)))
-  mb_pm_res <- tryM $ getResult $ case matches of
+  mb_pm_res <- tryM $ case matches of
     -- Check EmptyCase separately
     -- See Note [Checking EmptyCase Expressions]
     [] | [var] <- vars -> checkEmptyCase' var
@@ -405,38 +336,36 @@ checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM PmResult
 checkMatches' vars matches
   | null matches = panic "checkMatches': EmptyCase"
   | otherwise = do
-      liftD resetPmIterDs -- set the iter-no to zero
+      resetPmIterDs -- set the iter-no to zero
       missing    <- mkInitialUncovered vars
       tracePm "checkMatches': missing" (vcat (map pprValVecDebug missing))
-      (prov, rs,us,ds) <- go matches missing
+      (rs,us,ds) <- go matches missing
+      us' <- normaliseUncovered us
       return $ PmResult {
-                   pmresultProvenance   = prov
-                 , pmresultRedundant    = map hsLMatchToLPats rs
-                 , pmresultUncovered    = UncoveredPatterns us
+                   pmresultRedundant    = map hsLMatchToLPats rs
+                 , pmresultUncovered    = UncoveredPatterns us'
                  , pmresultInaccessible = map hsLMatchToLPats ds }
   where
     go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
-       -> PmM (Provenance
-              , [LMatch GhcTc (LHsExpr GhcTc)]
+       -> PmM ( [LMatch GhcTc (LHsExpr GhcTc)]
               , Uncovered
               , [LMatch GhcTc (LHsExpr GhcTc)])
-    go []     missing = return (mempty, [], missing, [])
+    go []     missing = return ([], missing, [])
     go (m:ms) missing = do
       tracePm "checkMatches': go" (ppr m $$ ppr missing)
-      fam_insts          <- liftD dsGetFamInstEnvs
-      (clause, guards)   <- liftD $ translateMatch fam_insts m
-      r@(PartialResult prov cs missing' ds)
+      fam_insts          <- dsGetFamInstEnvs
+      (clause, guards)   <- translateMatch fam_insts m
+      r@(PartialResult cs missing' ds)
         <- runMany (pmcheckI clause guards) missing
       tracePm "checkMatches': go: res" (ppr r)
-      (ms_prov, rs, final_u, is)  <- go ms missing'
-      let final_prov = prov `mappend` ms_prov
+      (rs, final_u, is)  <- go ms missing'
       return $ case (cs, ds) of
         -- useful
-        (Covered,  _    )        -> (final_prov,  rs, final_u,   is)
+        (Covered,  _    )        -> (rs, final_u,   is)
         -- redundant
-        (NotCovered, NotDiverged) -> (final_prov, m:rs, final_u,is)
+        (NotCovered, NotDiverged) -> (m:rs, final_u,is)
         -- inaccessible
-        (NotCovered, Diverged )   -> (final_prov,  rs, final_u, m:is)
+        (NotCovered, Diverged )   -> (rs, final_u, m:is)
 
     hsLMatchToLPats :: LMatch id body -> Located [LPat id]
     hsLMatchToLPats (dL->L l (Match { m_pats = pats })) = cL l pats
@@ -464,7 +393,7 @@ checkEmptyCase' var = do
         pure $ fmap (ValVec [va]) mb_sat
       return $ if null missing_m
         then emptyPmResult
-        else PmResult FromBuiltin [] (UncoveredPatterns missing_m) []
+        else PmResult [] (UncoveredPatterns missing_m) []
 
 -- | Returns 'True' if the argument 'Type' is a fully saturated application of
 -- a closed type constructor.
@@ -515,7 +444,7 @@ pmTopNormaliseType_maybe :: FamInstEnvs -> Bag EvVar -> Type
 -- is a type family with a variable result kind. I (Richard E) can't think
 -- of a way to cause trouble here, though.
 pmTopNormaliseType_maybe env ty_cs typ
-  = do (_, mb_typ') <- liftD $ initTcDsForSolver $ tcNormalise ty_cs typ
+  = do (_, mb_typ') <- initTcDsForSolver $ tcNormalise ty_cs typ
          -- Before proceeding, we chuck typ into the constraint solver, in case
          -- solving for given equalities may reduce typ some. See
          -- "Wrinkle: local equalities" in
@@ -578,8 +507,8 @@ pmTopNormaliseType_maybe env ty_cs typ
 -- for why this is done.)
 pmInitialTmTyCs :: PmM Delta
 pmInitialTmTyCs = do
-  ty_cs  <- liftD getDictsDs
-  tm_cs  <- map toComplex . bagToList <$> liftD getTmCsDs
+  ty_cs  <- getDictsDs
+  tm_cs  <- map toComplex . bagToList <$> getTmCsDs
   sat_ty <- tyOracle ty_cs
   let initTyCs = if sat_ty then ty_cs else emptyBag
       initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
@@ -670,12 +599,63 @@ tmTyCsAreSatisfiable
                                                  , delta_tm_cs = term_cs }
            _unsat               -> Nothing
 
+-- | This weeds out patterns with 'PmNCon's where at least one COMPLETE set is
+-- rendered vacuous by equality constraints.
+--
+-- This is quite costly due to the many oracle queries, so we only call this
+-- on the final uncovered set.
+normaliseUncovered :: Uncovered -> PmM Uncovered
+normaliseUncovered us = do
+  let valvec_inhabited p (ValVec vva delta) = runMaybeT $ do
+        vva' <- traverse (valabs_inhabited p delta) vva
+        pure (ValVec vva' delta)
+      valabs_inhabited p delta v = case v :: ValAbs of
+        pm at PmCon{ pm_con_args = args } -> do
+          args' <- traverse (valabs_inhabited p delta) args
+          pure pm { pm_con_args = args' }
+        PmVar x
+          | let ncons = [ (cl, tys) | PmAltConLike cl tys <- lookupRefutableAltCons x (delta_tm_cs delta) ]
+          , ((cl,tys):_) <- ncons
+          -> do
+            -- This is the reason why we store @tys@ in 'PmAltConLike'
+            grps <- lift (allCompleteMatches cl tys)
+            var_inh p delta x (map fst ncons) grps
+        PmNCon x grps ncons -> var_inh p delta x ncons grps
+        _ -> pure v
+      var_inh p delta x ncons grps = do
+        let grp_inh = filterM (p delta x) . (ncons \\)
+        incomplete_grps <- traverse grp_inh grps
+        -- If all cons of any COMPLETE set are matched, the ValVec is vacuous.
+        guard (all notNull incomplete_grps)
+        -- If there's a unique singleton incomplete group, turn it into a
+        -- `PmCon` for better readability of warning messages.
+        case incomplete_grps of
+          [[con]] -> do
+            -- We don't want to simplify to a `PmCon` (which won't normalise any
+            -- further) when @p@ is just the @cheap_inh_test at . Thus, we have to
+            -- assert satisfiability here, even if @actual_inh_test@ already did
+            -- so.
+            ic <- MaybeT $ mkOneSatisfiableConFull delta x con
+            pure (ic_val_abs ic)
+          _        -> pure (PmNCon x grps ncons)
+
+  -- We'll first do a cheap sweep without consulting the oracles
+  let cheap_inh_test _ _ _ = pure True
+  us1 <- mapMaybeM (valvec_inhabited cheap_inh_test) us
+  -- Then we'll do another pass trying to weed out the rest with (in)equalities
+  let actual_inh_test delta x con = do
+        lift (tracePm "nrm" (ppr con <+> ppr x <+> ppr (delta_tm_cs delta)))
+        isJust <$> lift (mkOneSatisfiableConFull delta x con)
+  us2 <- mapMaybeM (valvec_inhabited actual_inh_test) us1
+  tracePm "normaliseUncovered" (vcat (map pprValVecDebug us2))
+  pure us2
+
 -- | Implements two performance optimizations, as described in the
 -- \"Strict argument type constraints\" section of
 -- @Note [Extensions to GADTs Meet Their Match]@.
 checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> PmM Bool
 checkAllNonVoid rec_ts amb_cs strict_arg_tys = do
-  fam_insts <- liftD dsGetFamInstEnvs
+  fam_insts <- dsGetFamInstEnvs
   let definitely_inhabited =
         definitelyInhabitedType fam_insts (delta_ty_cs amb_cs)
   tys_to_check <- filterOutM definitely_inhabited strict_arg_tys
@@ -832,7 +812,7 @@ equalities (such as i ~ Int) that may be in scope.
 inhabitationCandidates :: Bag EvVar -> Type
                        -> PmM (Either Type (TyCon, [InhabitationCandidate]))
 inhabitationCandidates ty_cs ty = do
-  fam_insts   <- liftD dsGetFamInstEnvs
+  fam_insts   <- dsGetFamInstEnvs
   mb_norm_res <- pmTopNormaliseType_maybe fam_insts ty_cs ty
   case mb_norm_res of
     Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
@@ -856,7 +836,7 @@ inhabitationCandidates ty_cs ty = do
         |  tc `elem` trivially_inhabited
         -> case dcs of
              []    -> return (Left src_ty)
-             (_:_) -> do var <- liftD $ mkPmId core_ty
+             (_:_) -> do var <- mkPmId core_ty
                          let va = build_tm (PmVar var) dcs
                          return $ Right (tc, [InhabitationCandidate
                            { ic_val_abs = va, ic_tm_ct = mkIdEq var
@@ -866,7 +846,7 @@ inhabitationCandidates ty_cs ty = do
            -- Don't consider abstract tycons since we don't know what their
            -- constructors are, which makes the results of coverage checking
            -- them extremely misleading.
-        -> liftD $ do
+        -> do
              var  <- mkPmId core_ty -- it would be wrong to unify x
              alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
              return $ Right
@@ -932,7 +912,7 @@ truePattern = nullaryConPattern (RealDataCon trueDataCon)
 {-# INLINE truePattern #-}
 
 -- | Generate a `canFail` pattern vector of a specific type
-mkCanFailPmPat :: Type -> DsM PatVec
+mkCanFailPmPat :: Type -> PmM PatVec
 mkCanFailPmPat ty = do
   var <- mkPmVar ty
   return [var, PmFake]
@@ -967,7 +947,7 @@ mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit }
 -- -----------------------------------------------------------------------
 -- * Transform (Pat Id) into of (PmPat Id)
 
-translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec
+translatePat :: FamInstEnvs -> Pat GhcTc -> PmM PatVec
 translatePat fam_insts pat = case pat of
   WildPat  ty  -> mkPmVars [ty]
   VarPat _ id  -> return [PmVar (unLoc id)]
@@ -1179,12 +1159,12 @@ from translation in pattern matcher.
 
 -- | Translate a list of patterns (Note: each pattern is translated
 -- to a pattern vector but we do not concatenate the results).
-translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> DsM [PatVec]
+translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> PmM [PatVec]
 translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
 
 -- | Translate a constructor pattern
 translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
-                   -> ConLike -> HsConPatDetails GhcTc -> DsM PatVec
+                   -> ConLike -> HsConPatDetails GhcTc -> PmM PatVec
 translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
   = concat <$> translatePatVec fam_insts (map unLoc ps)
 translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
@@ -1240,11 +1220,12 @@ translateConPatVec fam_insts  univ_tys  ex_tvs c (RecCon (HsRecFields fs _))
 
 -- Translate a single match
 translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc)
-               -> DsM (PatVec,[PatVec])
+               -> PmM (PatVec,[PatVec])
 translateMatch fam_insts (dL->L _ (Match { m_pats = lpats, m_grhss = grhss })) =
   do
   pats'   <- concat <$> translatePatVec fam_insts pats
   guards' <- mapM (translateGuards fam_insts) guards
+  -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr guards, ppr guards'])
   return (pats', guards')
   where
     extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
@@ -1259,11 +1240,11 @@ translateMatch _ _ = panic "translateMatch"
 -- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
 
 -- | Translate a list of guard statements to a pattern vector
-translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
+translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> PmM PatVec
 translateGuards fam_insts guards = do
   all_guards <- concat <$> mapM (translateGuard fam_insts) guards
   let
-    shouldKeep :: Pattern -> DsM Bool
+    shouldKeep :: Pattern -> PmM Bool
     shouldKeep p
       | PmVar {} <- p = pure True
       | PmCon {} <- p = (&&)
@@ -1288,7 +1269,7 @@ translateGuards fam_insts guards = do
       pure (PmFake : kept)
 
 -- | Check whether a pattern can fail to match
-cantFailPattern :: Pattern -> DsM Bool
+cantFailPattern :: Pattern -> PmM Bool
 cantFailPattern PmVar {}      = pure True
 cantFailPattern PmCon { pm_con_con = c, pm_con_arg_tys = tys, pm_con_args = ps}
   = (&&) <$> singleMatchConstructor c tys <*> allM cantFailPattern ps
@@ -1296,7 +1277,7 @@ cantFailPattern (PmGrd pv _e) = allM cantFailPattern pv
 cantFailPattern _             = pure False
 
 -- | Translate a guard statement to Pattern
-translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
+translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> PmM PatVec
 translateGuard fam_insts guard = case guard of
   BodyStmt _   e _ _ -> translateBoolGuard e
   LetStmt  _   binds -> translateLet (unLoc binds)
@@ -1309,18 +1290,18 @@ translateGuard fam_insts guard = case guard of
   XStmtLR         {} -> panic "translateGuard RecStmt"
 
 -- | Translate let-bindings
-translateLet :: HsLocalBinds GhcTc -> DsM PatVec
+translateLet :: HsLocalBinds GhcTc -> PmM PatVec
 translateLet _binds = return []
 
 -- | Translate a pattern guard
-translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
+translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> PmM PatVec
 translateBind fam_insts (dL->L _ p) e = do
   ps <- translatePat fam_insts p
   g <- mkGuard ps (unLoc e)
   return [g]
 
 -- | Translate a boolean guard
-translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
+translateBoolGuard :: LHsExpr GhcTc -> PmM PatVec
 translateBoolGuard e
   | isJust (isTrueLHsExpr e) = return []
     -- The formal thing to do would be to generate (True <- True)
@@ -1421,10 +1402,17 @@ efficiently, which gave rise to #11276. The original approach translated
 
     pat |> co    ===>    x (pat <- (e |> co))
 
-Instead, we now check whether the coercion is a hole or if it is just refl, in
-which case we can drop it. Unfortunately, data families generate useful
-coercions so guards are still generated in these cases and checking data
-families is not really efficient.
+Why did we do this seemingly unnecessary expansion in the first place?
+The reason is that the type of @pat |> co@ (which is the type of the value
+abstraction we match against) might be different than that of @pat at . Data
+instances such as @Sing (a :: Bool)@ are a good example of this: If we would
+just drop the coercion, we'd get a type error when matching @pat@ against its
+value abstraction, with the result being that pmIsSatisfiable decides that every
+possible data constructor fitting @pat@ is rejected as uninhabitated, leading to
+a lot of false warnings.
+
+But we can check whether the coercion is a hole or if it is just refl, in
+which case we can drop it.
 
 %************************************************************************
 %*                                                                      *
@@ -1441,6 +1429,7 @@ families is not really efficient.
 pmPatType :: PmPat p -> Type
 pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
   = conLikeResTy con tys
+pmPatType (PmNCon { pm_con_id  = x }) = idType x
 pmPatType (PmVar  { pm_var_id  = x }) = idType x
 pmPatType (PmLit  { pm_lit_lit = l }) = pmLitType l
 pmPatType (PmNLit { pm_lit_id  = x }) = idType x
@@ -1471,10 +1460,13 @@ checker adheres to. Since the paper's publication, there have been some
 additional features added to the coverage checker which are not described in
 the paper. This Note serves as a reference for these new features.
 
------
--- Strict argument type constraints
------
+* Handling of uninhabited fields like `!Void`.
+  See Note [Strict argument type constraints]
+* Efficient handling of literal splitting, large enumerations and accurate
+  redundancy warnings for `COMPLETE` groups. See Note [PmNLit and PmNCon]
 
+Note [Strict argument type constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In the ConVar case of clause processing, each conlike K traditionally
 generates two different forms of constraints:
 
@@ -1594,8 +1586,43 @@ intuition formal, we say that a type is definitely inhabitable (DI) if:
     1. C has no equality constraints (since they might be unsatisfiable)
     2. C has no strict argument types (since they might be uninhabitable)
 
-It's relatively cheap to cheap if a type is DI, so before we call `nonVoid`
+It's relatively cheap to check if a type is DI, so before we call `nonVoid`
 on a list of strict argument types, we filter out all of the DI ones.
+
+Note [PmNLit and PmNCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+TLDR:
+* 'PmNLit' is an efficient encoding of literals we already matched on.
+  Important for checking redundancy without blowing up the term oracle.
+* 'PmNCon' is an efficient encoding of all constructors we already matched on.
+  Important for proper redundancy and completeness checks while being more
+  efficient than the `ConVar` split in GADTs Meet Their Match.
+
+GADTs Meet Their Match handled literals by desugaring to guard expressions,
+effectively encoding the knowledge in the term oracle. As it turned out, this
+doesn't scale (#11303, cf. Note [Literals in PmPat]), so we adopted an approach
+that encodes negative information about literals as a 'PmNLit', which encodes
+literal values the carried variable may no longer take on.
+
+The counterpart for constructor values is 'PmNCon', where we associate
+with a variable the topmost 'ConLike's it surely can't be. This is in contrast
+to GADTs Meet Their Match, where instead the `ConVar` case would split the value
+vector abstraction on all possible constructors from a `COMPLETE` group.
+In fact, we used to do just that, but committing to a particular `COMPLETE`
+group in `ConVar`, even nondeterministically, led to misleading redundancy
+warnings (#13363).
+Apart from that, splitting on huge enumerations in the presence of a catch-all
+case is a huge waste of resources.
+
+Note that since we have pattern guards, the term oracle must also be able to
+cope with negative equations involving literals and constructors, cf.
+Note [Refutable shapes] in TmOracle. Since we don't want to put too much strain
+on the term oracle with repeated coverage checks against all `COMPLETE` groups,
+we only do so once at the end in 'normaliseUncovered'.
+
+Peter Sestoft was probably the first to describe positive and negative
+information about terms in this manner in ML Pattern Match Compilation and
+Partial Evaluation.
 -}
 
 instance Outputable InhabitationCandidate where
@@ -1610,7 +1637,7 @@ instance Outputable InhabitationCandidate where
 
 -- | Generate an 'InhabitationCandidate' for a given conlike (generate
 -- fresh variables of the appropriate type for arguments)
-mkOneConFull :: Id -> ConLike -> DsM InhabitationCandidate
+mkOneConFull :: Id -> ConLike -> PmM InhabitationCandidate
 --  *  x :: T tys, where T is an algebraic data type
 --     NB: in the case of a data family, T is the *representation* TyCon
 --     e.g.   data instance T (a,b) = T1 a b
@@ -1660,22 +1687,30 @@ mkOneConFull x con = do
            , ic_strict_arg_tys = strict_arg_tys
            }
 
+-- | 'mkOneConFull' and immediately check whether the resulting
+-- 'InhabitationCandidat' @ic@ is inhabited by consulting 'pmIsSatisfiable'.
+-- Return @Just ic@ if it is.
+mkOneSatisfiableConFull :: Delta -> Id -> ConLike -> PmM (Maybe InhabitationCandidate)
+mkOneSatisfiableConFull delta x con = do
+  ic <- mkOneConFull x con
+  (ic <$) <$> pmIsSatisfiable delta (ic_tm_ct ic) (ic_ty_cs ic) (ic_strict_arg_tys ic)
+
 -- ----------------------------------------------------------------------------
 -- * More smart constructors and fresh variable generation
 
 -- | Create a guard pattern
-mkGuard :: PatVec -> HsExpr GhcTc -> DsM Pattern
+mkGuard :: PatVec -> HsExpr GhcTc -> PmM Pattern
 mkGuard pv e = do
   res <- allM cantFailPattern pv
   let expr = hsExprToPmExpr e
-  tracePmD "mkGuard" (vcat [ppr pv, ppr e, ppr res, ppr expr])
+  tracePm "mkGuard" (vcat [ppr pv, ppr e, ppr res, ppr expr])
   if | res                    -> pure (PmGrd pv expr)
      | PmExprOther {} <- expr -> pure PmFake
      | otherwise              -> pure (PmGrd pv expr)
 
--- | Create a term equality of the form: `(x ~ lit)`
-mkPosEq :: Id -> PmLit -> ComplexEq
-mkPosEq x l = (PmExprVar (idName x), PmExprLit l)
+-- | Create a term equality of the form: `(x ~ e)`
+mkPosEq :: Id -> PmExpr -> ComplexEq
+mkPosEq x e = (PmExprVar (idName x), e)
 {-# INLINE mkPosEq #-}
 
 -- | Create a term equality of the form: `(x ~ x)`
@@ -1686,17 +1721,17 @@ mkIdEq x = (PmExprVar name, PmExprVar name)
 {-# INLINE mkIdEq #-}
 
 -- | Generate a variable pattern of a given type
-mkPmVar :: Type -> DsM (PmPat p)
+mkPmVar :: Type -> PmM (PmPat p)
 mkPmVar ty = PmVar <$> mkPmId ty
 {-# INLINE mkPmVar #-}
 
 -- | Generate many variable patterns, given a list of types
-mkPmVars :: [Type] -> DsM PatVec
+mkPmVars :: [Type] -> PmM PatVec
 mkPmVars tys = mapM mkPmVar tys
 {-# INLINE mkPmVars #-}
 
 -- | Generate a fresh `Id` of a given type
-mkPmId :: Type -> DsM Id
+mkPmId :: Type -> PmM Id
 mkPmId ty = getUniqueM >>= \unique ->
   let occname = mkVarOccFS $ fsLit "$pm"
       name    = mkInternalName unique occname noSrcSpan
@@ -1705,7 +1740,7 @@ mkPmId ty = getUniqueM >>= \unique ->
 -- | Generate a fresh term variable of a given and return it in two forms:
 -- * A variable pattern
 -- * A variable expression
-mkPmId2Forms :: Type -> DsM (Pattern, LHsExpr GhcTc)
+mkPmId2Forms :: Type -> PmM (Pattern, LHsExpr GhcTc)
 mkPmId2Forms ty = do
   x <- mkPmId ty
   return (PmVar x, noLoc (HsVar noExt (noLoc x)))
@@ -1717,6 +1752,7 @@ mkPmId2Forms ty = do
 vaToPmExpr :: ValAbs -> PmExpr
 vaToPmExpr (PmCon  { pm_con_con = c, pm_con_args = ps })
   = PmExprCon c (map vaToPmExpr ps)
+vaToPmExpr (PmNCon { pm_con_id  = x }) = PmExprVar (idName x)
 vaToPmExpr (PmVar  { pm_var_id  = x }) = PmExprVar (idName x)
 vaToPmExpr (PmLit  { pm_lit_lit = l }) = PmExprLit l
 vaToPmExpr (PmNLit { pm_lit_id  = x }) = PmExprVar (idName x)
@@ -1744,9 +1780,9 @@ coercePmPat PmFake     = [] -- drop the guards
 -- | Check whether a 'ConLike' has the /single match/ property, i.e. whether
 -- it is the only possible match in the given context. See also
 -- 'allCompleteMatches' and Note [Single match constructors].
-singleMatchConstructor :: ConLike -> [Type] -> DsM Bool
+singleMatchConstructor :: ConLike -> [Type] -> PmM Bool
 singleMatchConstructor cl tys =
-  any (isSingleton . snd) <$> allCompleteMatches cl tys
+  any isSingleton <$> allCompleteMatches cl tys
 
 {-
 Note [Single match constructors]
@@ -1781,20 +1817,18 @@ translation step. See #15753 for why this yields surprising results.
 --  2. From `COMPLETE` pragmas which have the same type as the result
 --     type constructor. Note that we only use `COMPLETE` pragmas
 --     *all* of whose pattern types match. See #14135
-allCompleteMatches :: ConLike -> [Type] -> DsM [(Provenance, [ConLike])]
+allCompleteMatches :: ConLike -> [Type] -> DsM [[ConLike]]
 allCompleteMatches cl tys = do
   let fam = case cl of
            RealDataCon dc ->
-            [(FromBuiltin, map RealDataCon (tyConDataCons (dataConTyCon dc)))]
+            [map RealDataCon (tyConDataCons (dataConTyCon dc))]
            PatSynCon _    -> []
       ty  = conLikeResTy cl tys
   pragmas <- case splitTyConApp_maybe ty of
                Just (tc, _) -> dsGetCompleteMatches tc
                Nothing      -> return []
-  let fams cm = (FromComplete,) <$>
-                mapM dsLookupConLike (completeMatchConLikes cm)
-  from_pragma <- filter (\(_,m) -> isValidCompleteMatch ty m) <$>
-                mapM fams pragmas
+  let fams cm = mapM dsLookupConLike (completeMatchConLikes cm)
+  from_pragma <- filter (isValidCompleteMatch ty) <$> mapM fams pragmas
   let final_groups = fam ++ from_pragma
   return final_groups
     where
@@ -1886,8 +1920,7 @@ nameType name ty = do
 -- | Check whether a set of type constraints is satisfiable.
 tyOracle :: Bag EvVar -> PmM Bool
 tyOracle evs
-  = liftD $
-    do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
+  = do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
        ; case res of
             Just sat -> return sat
             Nothing  -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
@@ -1969,7 +2002,7 @@ mkInitialUncovered vars = do
 -- limit is not exceeded and call `pmcheck`
 pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
 pmcheckI ps guards vva = do
-  n <- liftD incrCheckPmIterDs
+  n <- incrCheckPmIterDs
   tracePm "pmCheck" (ppr n <> colon <+> pprPatVec ps
                         $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
                         $$ pprValVecDebug vva)
@@ -1981,7 +2014,7 @@ pmcheckI ps guards vva = do
 -- | Increase the counter for elapsed algorithm iterations, check that the
 -- limit is not exceeded and call `pmcheckGuards`
 pmcheckGuardsI :: [PatVec] -> ValVec -> PmM PartialResult
-pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva
+pmcheckGuardsI gvs vva = incrCheckPmIterDs >> pmcheckGuards gvs vva
 {-# INLINE pmcheckGuardsI #-}
 
 -- | Increase the counter for elapsed algorithm iterations, check that the
@@ -1989,7 +2022,7 @@ pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva
 pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
            -> PmM PartialResult
 pmcheckHdI p ps guards va vva = do
-  n <- liftD incrCheckPmIterDs
+  n <- incrCheckPmIterDs
   tracePm "pmCheckHdI" (ppr n <> colon <+> pprPmPatDebug p
                         $$ pprPatVec ps
                         $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
@@ -2019,10 +2052,12 @@ pmcheck (PmFake : ps) guards vva =
 pmcheck (p : ps) guards (ValVec vas delta)
   | PmGrd { pm_grd_pv = pv, pm_grd_expr = e } <- p
   = do
-      y <- liftD $ mkPmId (pmPatType p)
+      tracePm "PmGrd: pmPatType" (hcat [ppr p, ppr (pmPatType p)])
+      y <- mkPmId (pmPatType p)
       let tm_state = extendSubst y e (delta_tm_cs delta)
           delta'   = delta { delta_tm_cs = tm_state }
-      utail <$> pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
+      pr <- pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
+      pure $ utail pr
 
 pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons"
 pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil"
@@ -2034,10 +2069,9 @@ pmcheck (p:ps) guards (ValVec (va:vva) delta)
 pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
 pmcheckGuards []       vva = return (usimple [vva])
 pmcheckGuards (gv:gvs) vva = do
-  (PartialResult prov1 cs vsa ds) <- pmcheckI gv [] vva
-  (PartialResult prov2 css vsas dss) <- runMany (pmcheckGuardsI gvs) vsa
-  return $ PartialResult (prov1 `mappend` prov2)
-                         (cs `mappend` css)
+  (PartialResult cs vsa ds) <- pmcheckI gv [] vva
+  (PartialResult css vsas dss) <- runMany (pmcheckGuardsI gvs) vsa
+  return $ PartialResult (cs `mappend` css)
                          vsas
                          (ds `mappend` dss)
 
@@ -2073,7 +2107,7 @@ pmcheckHd ( p@(PmCon { pm_con_con = c1, pm_con_tvs = ex_tvs1
           | otherwise  = Just <$> to_evvar tv1 tv2
     evvars <- (listToBag . catMaybes) <$>
               ASSERT(ex_tvs1 `equalLength` ex_tvs2)
-              liftD (zipWithM mb_to_evvar ex_tvs1 ex_tvs2)
+              (zipWithM mb_to_evvar ex_tvs1 ex_tvs2)
     let delta' = delta { delta_ty_cs = evvars `unionBags` delta_ty_cs delta }
     kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
       <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta')
@@ -2085,45 +2119,52 @@ pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva =
     False -> return $ ucon va (usimple [vva])
 
 -- ConVar
-pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
-          ps guards
-          (PmVar x) (ValVec vva delta) = do
-  (prov, complete_match) <- select =<< liftD (allCompleteMatches con tys)
-
-  cons_cs <- mapM (liftD . mkOneConFull x) complete_match
-
-  inst_vsa <- flip mapMaybeM cons_cs $
-      \InhabitationCandidate{ ic_val_abs = va, ic_tm_ct = tm_ct
-                            , ic_ty_cs = ty_cs
-                            , ic_strict_arg_tys = strict_arg_tys } -> do
-    mb_sat <- pmIsSatisfiable delta tm_ct ty_cs strict_arg_tys
-    pure $ fmap (ValVec (va:vva)) mb_sat
-
-  set_provenance prov .
-    force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
-      runMany (pmcheckI (p:ps) guards) inst_vsa
+pmcheckHd p at PmCon{} ps guards (PmVar x) vva@(ValVec _ delta) = do
+  groups <- allCompleteMatches (pm_con_con p) (pm_con_arg_tys p)
+  force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
+    pmcheckHd p ps guards (PmNCon x groups []) vva
+
+-- ConNCon
+pmcheckHd p at PmCon{} ps guards va at PmNCon{} (ValVec vva delta) = do
+  -- Split the value vector into two value vectors: One representing the current
+  -- constructor, the other representing everything but the current constructor
+  -- (and the already known impossible constructors).
+  let con   = pm_con_con p
+  let x     = pm_con_id va
+  let grps  = pm_con_grps va
+  let ncons = pm_con_not va
+
+  -- For the value vector of the current constructor, we directly recurse into
+  -- checking the the current case, so we get back a PartialResult
+  ic <- mkOneConFull x con
+  pr_con <- fmap (fromMaybe mempty) $ runMaybeT $ do
+    guard (con `notElem` ncons)
+    delta' <- MaybeT $ pmIsSatisfiable delta (ic_tm_ct ic) (ic_ty_cs ic) (ic_strict_arg_tys ic)
+    lift $ tracePm "success" (ppr (delta_tm_cs delta))
+    lift $ pmcheckHdI p ps guards (ic_val_abs ic) (ValVec vva delta')
+
+  let ncons' = con : ncons
+  let us_incomplete
+        | let nalt = PmAltConLike (pm_con_con p) (pm_con_arg_tys p)
+        , Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x nalt
+        = [ValVec (PmNCon x grps ncons' : vva) (delta { delta_tm_cs = tm_state })]
+        | otherwise = []
+  tracePm "ConNCon" (vcat [ppr p, ppr x, ppr ncons', ppr pr_con, ppr us_incomplete, ppr us_incomplete])
+
+  -- Combine both into a single PartialResult
+  let pr_combined = mkUnion pr_con (usimple us_incomplete)
+  pure pr_combined
 
 -- LitVar
-pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
+pmcheckHd p at PmLit{} ps guards (PmVar x) vva@(ValVec _ delta)
   = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
-      mkUnion non_matched <$>
-        case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of
-          Just tm_state -> pmcheckHdI p ps guards (PmLit l) $
-                             ValVec vva (delta {delta_tm_cs = tm_state})
-          Nothing       -> return mempty
-  where
-    -- See Note [Refutable shapes] in TmOracle
-    us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l)
-       = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
-       | otherwise = []
-
-    non_matched = usimple us
+      pmcheckHd p ps guards (PmNLit x []) vva
 
 -- LitNLit
 pmcheckHd (p@(PmLit l)) ps guards
           (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta)
   | all (not . eqPmLit l) lits
-  , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l)
+  , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x (PmExprLit l))
     -- Both guards check the same so it would be sufficient to have only
     -- the second one. Nevertheless, it is much cheaper to check whether
     -- the literal is in the list so we check it first, to avoid calling
@@ -2149,7 +2190,7 @@ pmcheckHd (p@(PmLit l)) ps guards
 
 -- LitCon
 pmcheckHd p at PmLit{} ps guards va at PmCon{} (ValVec vva delta)
-  = do y <- liftD $ mkPmId (pmPatType va)
+  = do y <- mkPmId (pmPatType va)
        -- Analogous to the ConVar case, we have to case split the value
        -- abstraction on possible literals. We do so by introducing a fresh
        -- variable that is equated to the constructor. LitVar will then take
@@ -2160,7 +2201,7 @@ pmcheckHd p at PmLit{} ps guards va at PmCon{} (ValVec vva delta)
 
 -- ConLit
 pmcheckHd p at PmCon{} ps guards (PmLit l) (ValVec vva delta)
-  = do y <- liftD $ mkPmId (pmPatType p)
+  = do y <- mkPmId (pmPatType p)
        -- This desugars to the ConVar case by introducing a fresh variable that
        -- is equated to the literal via a constraint. ConVar will then properly
        -- case split on all possible constructors.
@@ -2172,6 +2213,10 @@ pmcheckHd p at PmCon{} ps guards (PmLit l) (ValVec vva delta)
 pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
   = pmcheckHdI p ps guards (PmVar x) vva
 
+-- LitNCon
+pmcheckHd (p@(PmLit {})) ps guards (PmNCon { pm_con_id = x }) vva
+  = pmcheckHdI p ps guards (PmVar x) vva
+
 -- Impossible: handled by pmcheck
 pmcheckHd PmFake     _ _ _ _ = panic "pmcheckHd: Fake"
 pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
@@ -2355,9 +2400,6 @@ force_if :: Bool -> PartialResult -> PartialResult
 force_if True  pres = forces pres
 force_if False pres = pres
 
-set_provenance :: Provenance -> PartialResult -> PartialResult
-set_provenance prov pr = pr { presultProvenance = prov }
-
 -- ----------------------------------------------------------------------------
 -- * Propagation of term constraints inwards when checking nested matches
 
@@ -2365,7 +2407,7 @@ set_provenance prov pr = pr { presultProvenance = prov }
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When checking a match it would be great to have all type and term information
 available so we can get more precise results. For this reason we have functions
-`addDictsDs' and `addTmCsDs' in PmMonad that store in the environment type and
+`addDictsDs' and `addTmCsDs' in DsMonad that store in the environment type and
 term constraints (respectively) as we go deeper.
 
 The type constraints we propagate inwards are collected by `collectEvVarsPats'
@@ -2489,8 +2531,8 @@ substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr)
 dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
 dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
   = when (flag_i || flag_u) $ do
-      let exists_r = flag_i && notNull redundant && onlyBuiltin
-          exists_i = flag_i && notNull inaccessible && onlyBuiltin && not is_rec_upd
+      let exists_r = flag_i && notNull redundant
+          exists_i = flag_i && notNull inaccessible && not is_rec_upd
           exists_u = flag_u && (case uncovered of
                                   TypeOfUncovered   _ -> True
                                   UncoveredPatterns u -> notNull u)
@@ -2507,8 +2549,7 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
           UncoveredPatterns candidates -> pprEqns candidates
   where
     PmResult
-      { pmresultProvenance = prov
-      , pmresultRedundant = redundant
+      { pmresultRedundant = redundant
       , pmresultUncovered = uncovered
       , pmresultInaccessible = inaccessible } = pm_result
 
@@ -2519,8 +2560,6 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
     is_rec_upd = case kind of { RecUpd -> True; _ -> False }
        -- See Note [Inaccessible warnings for record updates]
 
-    onlyBuiltin = prov == FromBuiltin
-
     maxPatterns = maxUncoveredPatterns dflags
 
     -- Print a single clause (for redundant/with-inaccessible-rhs)
@@ -2694,11 +2733,7 @@ involved.
 -- Debugging Infrastructre
 
 tracePm :: String -> SDoc -> PmM ()
-tracePm herald doc = liftD $ tracePmD herald doc
-
-
-tracePmD :: String -> SDoc -> DsM ()
-tracePmD herald doc = do
+tracePm herald doc = do
   dflags <- getDynFlags
   printer <- mkPrintUnqualifiedDs
   liftIO $ dumpIfSet_dyn_printer printer dflags
@@ -2708,6 +2743,8 @@ tracePmD herald doc = do
 pprPmPatDebug :: PmPat a -> SDoc
 pprPmPatDebug (PmCon cc _arg_tys _con_tvs _con_dicts con_args)
   = hsep [text "PmCon", ppr cc, hsep (map pprPmPatDebug con_args)]
+pprPmPatDebug (PmNCon x _ sets)
+  = hsep [text "PmNCon", ppr x, ppr sets]
 pprPmPatDebug (PmVar vid) = text "PmVar" <+> ppr vid
 pprPmPatDebug (PmLit li)  = text "PmLit" <+> ppr li
 pprPmPatDebug (PmNLit i nl) = text "PmNLit" <+> ppr i <+> ppr nl
@@ -2728,3 +2765,5 @@ pprValAbs ps = hang (text "ValAbs:") 2
 pprValVecDebug :: ValVec -> SDoc
 pprValVecDebug (ValVec vas _d) = text "ValVec" <+>
                                   parens (pprValAbs vas)
+                                  $$ (ppr (delta_tm_cs _d))
+                                  -- <not a haddock> $$ (ppr (delta_ty_cs _d))


=====================================
compiler/deSugar/PmExpr.hs
=====================================
@@ -9,7 +9,7 @@ Haskell expressions (as used by the pattern matching checker) and utilities.
 
 module PmExpr (
         PmExpr(..), PmLit(..), PmAltCon(..), SimpleEq, ComplexEq, toComplex,
-        eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
+        eqPmLit, pmExprToAlt, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
         substComplexEq
     ) where
 
@@ -89,6 +89,13 @@ instance Eq PmAltCon where
   PmAltLit l1        == PmAltLit l2        = eqPmLit l1 l2
   _                  == _                  = False
 
+pmExprToAlt :: PmExpr -> Maybe PmAltCon
+-- Note how this deliberately chooses bogus argument types for PmAltConLike.
+-- This is only safe for doing lookup in a 'PmRefutEnv'!
+pmExprToAlt (PmExprCon cl _) = Just (PmAltConLike cl [])
+pmExprToAlt (PmExprLit l)    = Just (PmAltLit l)
+pmExprToAlt _                = Nothing
+
 {- Note [Undecidable Equality for Overloaded Literals]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Equality on overloaded literals is undecidable in the general case. Consider


=====================================
compiler/deSugar/PmPpr.hs
=====================================
@@ -35,6 +35,9 @@ import TmOracle
 --     where p is not one of {3, 4}
 --           q is not one of {0, 5}
 -- @
+--
+-- When the set of refutable shapes contains more than 3 elements, the
+-- additional elements are indicated by "...".
 pprUncovered :: ([PmExpr], PmRefutEnv) -> SDoc
 pprUncovered (expr_vec, refuts)
   | null cs   = fsep vec -- there are no literal constraints
@@ -45,11 +48,15 @@ pprUncovered (expr_vec, refuts)
     (vec,cs) = runPmPpr sdoc_vec (prettifyRefuts refuts)
 
 -- | Output refutable shapes of a variable in the form of @var is not one of {2,
--- Nothing, 3}@.
+-- Nothing, 3}@. Will never print more than 3 refutable shapes, the tail is
+-- indicated by an ellipsis.
 pprRefutableShapes :: (SDoc,[PmAltCon]) -> SDoc
 pprRefutableShapes (var, alts)
-  = var <+> text "is not one of" <+> braces (pprWithCommas ppr_alt alts)
+  = var <+> text "is not one of" <+> format_alts alts
   where
+    format_alts = braces . fsep . punctuate comma . shorten . map ppr_alt
+    shorten (a:b:c:_:_) = a:b:c:[text "..."]
+    shorten xs          = xs
     ppr_alt (PmAltLit lit)      = ppr lit
     ppr_alt (PmAltConLike cl _) = ppr cl
 


=====================================
compiler/deSugar/TmOracle.hs
=====================================
@@ -13,7 +13,8 @@ module TmOracle (
 
         -- re-exported from PmExpr
         PmExpr(..), PmLit(..), PmAltCon(..), SimpleEq, ComplexEq, PmVarEnv,
-        PmRefutEnv, eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
+        PmRefutEnv, eqPmLit, pmExprToAlt, isNotPmExprOther, lhsExprToPmExpr,
+        hsExprToPmExpr,
 
         -- the term oracle
         tmOracle, TmState, initialTmState, wrapUpTmState, solveOneEq, extendSubst, canDiverge,
@@ -31,6 +32,9 @@ import PmExpr
 
 import Id
 import Name
+import NameEnv
+import UniqFM
+import UniqDFM
 import Type
 import HsLit
 import TcHsSyn
@@ -40,8 +44,6 @@ import Util
 import Maybes
 import Outputable
 
-import NameEnv
-
 {-
 %************************************************************************
 %*                                                                      *
@@ -97,6 +99,15 @@ data TmState = TmS
   -- those of @y at .
   }
 
+instance Outputable TmState where
+  ppr state = braces (fsep (punctuate comma (facts ++ pos ++ neg)))
+    where
+      facts = map pos_eq (tm_facts state)
+      pos   = map pos_eq (nonDetUFMToList (tm_pos state))
+      neg   = map neg_eq (udfmToList (tm_neg state))
+      pos_eq (l, r) = ppr l <+> char '~' <+> ppr r
+      neg_eq (l, r) = ppr l <+> char '≁' <+> ppr r
+
 -- | Initial state of the oracle.
 initialTmState :: TmState
 initialTmState = TmS [] emptyNameEnv emptyDNameEnv
@@ -144,7 +155,7 @@ varIn x e = case e of
 -- @x@ and @e@ are completely substituted before!
 isRefutable :: Name -> PmExpr -> PmRefutEnv -> Bool
 isRefutable x e env
-  = fromMaybe False $ elem <$> exprToAlt e <*> lookupDNameEnv env x
+  = fromMaybe False $ elem <$> pmExprToAlt e <*> lookupDNameEnv env x
 
 -- | Solve a complex equality (top-level).
 solveOneEq :: TmState -> ComplexEq -> Maybe TmState
@@ -152,18 +163,11 @@ solveOneEq solver_env at TmS{ tm_pos = pos } complex
   = solveComplexEq solver_env       -- do the actual *merging* with existing state
   $ applySubstComplexEq pos complex -- replace everything we already know
 
-exprToAlt :: PmExpr -> Maybe PmAltCon
--- Note how this deliberately chooses bogus argument types for PmAltConLike.
--- This is only safe for doing lookup in a 'PmRefutEnv'!
-exprToAlt (PmExprCon cl _) = Just (PmAltConLike cl [])
-exprToAlt (PmExprLit l)    = Just (PmAltLit l)
-exprToAlt _                = Nothing
-
 -- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the
 -- 'TmState' and return @Nothing@ if that leads to a contradiction.
 addSolveRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState
 addSolveRefutableAltCon original at TmS{ tm_pos = pos, tm_neg = neg } x nalt
-  = case exprToAlt e of
+  = case pmExprToAlt e of
       Nothing         -> Just extended -- Not solved yet
       Just alt                         -- We have a solution
         | alt == nalt -> Nothing       -- ... which is contradictory
@@ -193,7 +197,7 @@ lookupRefutableAltCons x TmS { tm_neg = neg }
 --             it to the tmstate; the result may or may not be
 --             satisfiable
 solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
-solveComplexEq solver_state eq@(e1, e2) = case eq of
+solveComplexEq solver_state eq@(e1, e2) = {-pprTraceWith "solveComplexEq" (\mb_sat -> ppr eq $$ ppr mb_sat) $-} case eq of
   -- We cannot do a thing about these cases
   (PmExprOther _,_)            -> Just solver_state
   (_,PmExprOther _)            -> Just solver_state


=====================================
compiler/utils/Binary.hs
=====================================
@@ -724,7 +724,6 @@ putTypeRep bh (Fun arg res) = do
     put_ bh (3 :: Word8)
     putTypeRep bh arg
     putTypeRep bh res
-putTypeRep _ _ = fail "Binary.putTypeRep: Impossible"
 
 getSomeTypeRep :: BinHandle -> IO SomeTypeRep
 getSomeTypeRep bh = do


=====================================
compiler/utils/Outputable.hs
=====================================
@@ -81,8 +81,8 @@ module Outputable (
 
         -- * Error handling and debugging utilities
         pprPanic, pprSorry, assertPprPanic, pprPgmError,
-        pprTrace, pprTraceDebug, pprTraceIt, warnPprTrace, pprSTrace,
-        pprTraceException, pprTraceM,
+        pprTrace, pprTraceDebug, pprTraceWith, pprTraceIt, warnPprTrace,
+        pprSTrace, pprTraceException, pprTraceM,
         trace, pgmError, panic, sorry, assertPanic,
         pprDebugAndThen, callStackDoc,
     ) where
@@ -1196,9 +1196,15 @@ pprTrace str doc x
 pprTraceM :: Applicative f => String -> SDoc -> f ()
 pprTraceM str doc = pprTrace str doc (pure ())
 
+-- | @pprTraceWith desc f x@ is equivalent to @pprTrace desc (f x) x at .
+-- This allows you to print details from the returned value as well as from
+-- ambient variables.
+pprTraceWith :: Outputable a => String -> (a -> SDoc) -> a -> a
+pprTraceWith desc f x = pprTrace desc (f x) x
+
 -- | @pprTraceIt desc x@ is equivalent to @pprTrace desc (ppr x) x@
 pprTraceIt :: Outputable a => String -> a -> a
-pprTraceIt desc x = pprTrace desc (ppr x) x
+pprTraceIt desc x = pprTraceWith desc ppr x
 
 -- | @pprTraceException desc x action@ runs action, printing a message
 -- if it throws an exception.


=====================================
docs/users_guide/glasgow_exts.rst
=====================================
@@ -15419,49 +15419,6 @@ the user must provide a type signature. ::
     foo :: [a] -> Int
     foo T = 5
 
-.. _multiple-complete-pragmas:
-
-Disambiguating between multiple ``COMPLETE`` pragmas
-----------------------------------------------------
-
-What should happen if there are multiple ``COMPLETE`` sets that apply to a
-single set of patterns? Consider this example: ::
-
-  data T = MkT1 | MkT2 | MkT2Internal
-  {-# COMPLETE MkT1, MkT2 #-}
-  {-# COMPLETE MkT1, MkT2Internal #-}
-
-  f :: T -> Bool
-  f MkT1 = True
-  f MkT2 = False
-
-Which ``COMPLETE`` pragma should be used when checking the coverage of the
-patterns in ``f``? If we pick the ``COMPLETE`` set that covers ``MkT1`` and
-``MkT2``, then ``f`` is exhaustive, but if we pick the other ``COMPLETE`` set
-that covers ``MkT1`` and ``MkT2Internal``, then ``f`` is *not* exhaustive,
-since it fails to match ``MkT2Internal``. An intuitive way to solve this
-dilemma is to recognize that picking the former ``COMPLETE`` set produces the
-fewest number of uncovered pattern clauses, and thus is the better choice.
-
-GHC disambiguates between multiple ``COMPLETE`` sets based on this rationale.
-To make things more formal, when the pattern-match checker requests a set of
-constructors for some data type constructor ``T``, the checker returns:
-
-* The original set of data constructors for ``T``
-* Any ``COMPLETE`` sets of type ``T``
-
-GHC then checks for pattern coverage using each of these sets. If any of these
-sets passes the pattern coverage checker with no warnings, then we are done. If
-each set produces at least one warning, then GHC must pick one of the sets of
-warnings depending on how good the results are. The results are prioritized in
-this order:
-
-1. Fewest uncovered clauses
-2. Fewest redundant clauses
-3. Fewest inaccessible clauses
-4. Whether the match comes from the original set of data constructors or from a
-   ``COMPLETE`` pragma (prioritizing the former over the latter)
-
 .. _overlap-pragma:
 
 ``OVERLAPPING``, ``OVERLAPPABLE``, ``OVERLAPS``, and ``INCOHERENT`` pragmas


=====================================
libraries/binary
=====================================
@@ -1 +1 @@
-Subproject commit 94855814e2e4f7a0f191ffa5b4c98ee0147e3174
+Subproject commit e707cab7cb61bebd311632fd46d508ef2f524c6e


=====================================
testsuite/tests/perf/compiler/ManyAlternatives.hs
=====================================
@@ -0,0 +1,2005 @@
+module ManyAlternatives where
+
+data A1000 = A0
+  | A0001
+  | A0002
+  | A0003
+  | A0004
+  | A0005
+  | A0006
+  | A0007
+  | A0008
+  | A0009
+  | A0010
+  | A0011
+  | A0012
+  | A0013
+  | A0014
+  | A0015
+  | A0016
+  | A0017
+  | A0018
+  | A0019
+  | A0020
+  | A0021
+  | A0022
+  | A0023
+  | A0024
+  | A0025
+  | A0026
+  | A0027
+  | A0028
+  | A0029
+  | A0030
+  | A0031
+  | A0032
+  | A0033
+  | A0034
+  | A0035
+  | A0036
+  | A0037
+  | A0038
+  | A0039
+  | A0040
+  | A0041
+  | A0042
+  | A0043
+  | A0044
+  | A0045
+  | A0046
+  | A0047
+  | A0048
+  | A0049
+  | A0050
+  | A0051
+  | A0052
+  | A0053
+  | A0054
+  | A0055
+  | A0056
+  | A0057
+  | A0058
+  | A0059
+  | A0060
+  | A0061
+  | A0062
+  | A0063
+  | A0064
+  | A0065
+  | A0066
+  | A0067
+  | A0068
+  | A0069
+  | A0070
+  | A0071
+  | A0072
+  | A0073
+  | A0074
+  | A0075
+  | A0076
+  | A0077
+  | A0078
+  | A0079
+  | A0080
+  | A0081
+  | A0082
+  | A0083
+  | A0084
+  | A0085
+  | A0086
+  | A0087
+  | A0088
+  | A0089
+  | A0090
+  | A0091
+  | A0092
+  | A0093
+  | A0094
+  | A0095
+  | A0096
+  | A0097
+  | A0098
+  | A0099
+  | A0100
+  | A0101
+  | A0102
+  | A0103
+  | A0104
+  | A0105
+  | A0106
+  | A0107
+  | A0108
+  | A0109
+  | A0110
+  | A0111
+  | A0112
+  | A0113
+  | A0114
+  | A0115
+  | A0116
+  | A0117
+  | A0118
+  | A0119
+  | A0120
+  | A0121
+  | A0122
+  | A0123
+  | A0124
+  | A0125
+  | A0126
+  | A0127
+  | A0128
+  | A0129
+  | A0130
+  | A0131
+  | A0132
+  | A0133
+  | A0134
+  | A0135
+  | A0136
+  | A0137
+  | A0138
+  | A0139
+  | A0140
+  | A0141
+  | A0142
+  | A0143
+  | A0144
+  | A0145
+  | A0146
+  | A0147
+  | A0148
+  | A0149
+  | A0150
+  | A0151
+  | A0152
+  | A0153
+  | A0154
+  | A0155
+  | A0156
+  | A0157
+  | A0158
+  | A0159
+  | A0160
+  | A0161
+  | A0162
+  | A0163
+  | A0164
+  | A0165
+  | A0166
+  | A0167
+  | A0168
+  | A0169
+  | A0170
+  | A0171
+  | A0172
+  | A0173
+  | A0174
+  | A0175
+  | A0176
+  | A0177
+  | A0178
+  | A0179
+  | A0180
+  | A0181
+  | A0182
+  | A0183
+  | A0184
+  | A0185
+  | A0186
+  | A0187
+  | A0188
+  | A0189
+  | A0190
+  | A0191
+  | A0192
+  | A0193
+  | A0194
+  | A0195
+  | A0196
+  | A0197
+  | A0198
+  | A0199
+  | A0200
+  | A0201
+  | A0202
+  | A0203
+  | A0204
+  | A0205
+  | A0206
+  | A0207
+  | A0208
+  | A0209
+  | A0210
+  | A0211
+  | A0212
+  | A0213
+  | A0214
+  | A0215
+  | A0216
+  | A0217
+  | A0218
+  | A0219
+  | A0220
+  | A0221
+  | A0222
+  | A0223
+  | A0224
+  | A0225
+  | A0226
+  | A0227
+  | A0228
+  | A0229
+  | A0230
+  | A0231
+  | A0232
+  | A0233
+  | A0234
+  | A0235
+  | A0236
+  | A0237
+  | A0238
+  | A0239
+  | A0240
+  | A0241
+  | A0242
+  | A0243
+  | A0244
+  | A0245
+  | A0246
+  | A0247
+  | A0248
+  | A0249
+  | A0250
+  | A0251
+  | A0252
+  | A0253
+  | A0254
+  | A0255
+  | A0256
+  | A0257
+  | A0258
+  | A0259
+  | A0260
+  | A0261
+  | A0262
+  | A0263
+  | A0264
+  | A0265
+  | A0266
+  | A0267
+  | A0268
+  | A0269
+  | A0270
+  | A0271
+  | A0272
+  | A0273
+  | A0274
+  | A0275
+  | A0276
+  | A0277
+  | A0278
+  | A0279
+  | A0280
+  | A0281
+  | A0282
+  | A0283
+  | A0284
+  | A0285
+  | A0286
+  | A0287
+  | A0288
+  | A0289
+  | A0290
+  | A0291
+  | A0292
+  | A0293
+  | A0294
+  | A0295
+  | A0296
+  | A0297
+  | A0298
+  | A0299
+  | A0300
+  | A0301
+  | A0302
+  | A0303
+  | A0304
+  | A0305
+  | A0306
+  | A0307
+  | A0308
+  | A0309
+  | A0310
+  | A0311
+  | A0312
+  | A0313
+  | A0314
+  | A0315
+  | A0316
+  | A0317
+  | A0318
+  | A0319
+  | A0320
+  | A0321
+  | A0322
+  | A0323
+  | A0324
+  | A0325
+  | A0326
+  | A0327
+  | A0328
+  | A0329
+  | A0330
+  | A0331
+  | A0332
+  | A0333
+  | A0334
+  | A0335
+  | A0336
+  | A0337
+  | A0338
+  | A0339
+  | A0340
+  | A0341
+  | A0342
+  | A0343
+  | A0344
+  | A0345
+  | A0346
+  | A0347
+  | A0348
+  | A0349
+  | A0350
+  | A0351
+  | A0352
+  | A0353
+  | A0354
+  | A0355
+  | A0356
+  | A0357
+  | A0358
+  | A0359
+  | A0360
+  | A0361
+  | A0362
+  | A0363
+  | A0364
+  | A0365
+  | A0366
+  | A0367
+  | A0368
+  | A0369
+  | A0370
+  | A0371
+  | A0372
+  | A0373
+  | A0374
+  | A0375
+  | A0376
+  | A0377
+  | A0378
+  | A0379
+  | A0380
+  | A0381
+  | A0382
+  | A0383
+  | A0384
+  | A0385
+  | A0386
+  | A0387
+  | A0388
+  | A0389
+  | A0390
+  | A0391
+  | A0392
+  | A0393
+  | A0394
+  | A0395
+  | A0396
+  | A0397
+  | A0398
+  | A0399
+  | A0400
+  | A0401
+  | A0402
+  | A0403
+  | A0404
+  | A0405
+  | A0406
+  | A0407
+  | A0408
+  | A0409
+  | A0410
+  | A0411
+  | A0412
+  | A0413
+  | A0414
+  | A0415
+  | A0416
+  | A0417
+  | A0418
+  | A0419
+  | A0420
+  | A0421
+  | A0422
+  | A0423
+  | A0424
+  | A0425
+  | A0426
+  | A0427
+  | A0428
+  | A0429
+  | A0430
+  | A0431
+  | A0432
+  | A0433
+  | A0434
+  | A0435
+  | A0436
+  | A0437
+  | A0438
+  | A0439
+  | A0440
+  | A0441
+  | A0442
+  | A0443
+  | A0444
+  | A0445
+  | A0446
+  | A0447
+  | A0448
+  | A0449
+  | A0450
+  | A0451
+  | A0452
+  | A0453
+  | A0454
+  | A0455
+  | A0456
+  | A0457
+  | A0458
+  | A0459
+  | A0460
+  | A0461
+  | A0462
+  | A0463
+  | A0464
+  | A0465
+  | A0466
+  | A0467
+  | A0468
+  | A0469
+  | A0470
+  | A0471
+  | A0472
+  | A0473
+  | A0474
+  | A0475
+  | A0476
+  | A0477
+  | A0478
+  | A0479
+  | A0480
+  | A0481
+  | A0482
+  | A0483
+  | A0484
+  | A0485
+  | A0486
+  | A0487
+  | A0488
+  | A0489
+  | A0490
+  | A0491
+  | A0492
+  | A0493
+  | A0494
+  | A0495
+  | A0496
+  | A0497
+  | A0498
+  | A0499
+  | A0500
+  | A0501
+  | A0502
+  | A0503
+  | A0504
+  | A0505
+  | A0506
+  | A0507
+  | A0508
+  | A0509
+  | A0510
+  | A0511
+  | A0512
+  | A0513
+  | A0514
+  | A0515
+  | A0516
+  | A0517
+  | A0518
+  | A0519
+  | A0520
+  | A0521
+  | A0522
+  | A0523
+  | A0524
+  | A0525
+  | A0526
+  | A0527
+  | A0528
+  | A0529
+  | A0530
+  | A0531
+  | A0532
+  | A0533
+  | A0534
+  | A0535
+  | A0536
+  | A0537
+  | A0538
+  | A0539
+  | A0540
+  | A0541
+  | A0542
+  | A0543
+  | A0544
+  | A0545
+  | A0546
+  | A0547
+  | A0548
+  | A0549
+  | A0550
+  | A0551
+  | A0552
+  | A0553
+  | A0554
+  | A0555
+  | A0556
+  | A0557
+  | A0558
+  | A0559
+  | A0560
+  | A0561
+  | A0562
+  | A0563
+  | A0564
+  | A0565
+  | A0566
+  | A0567
+  | A0568
+  | A0569
+  | A0570
+  | A0571
+  | A0572
+  | A0573
+  | A0574
+  | A0575
+  | A0576
+  | A0577
+  | A0578
+  | A0579
+  | A0580
+  | A0581
+  | A0582
+  | A0583
+  | A0584
+  | A0585
+  | A0586
+  | A0587
+  | A0588
+  | A0589
+  | A0590
+  | A0591
+  | A0592
+  | A0593
+  | A0594
+  | A0595
+  | A0596
+  | A0597
+  | A0598
+  | A0599
+  | A0600
+  | A0601
+  | A0602
+  | A0603
+  | A0604
+  | A0605
+  | A0606
+  | A0607
+  | A0608
+  | A0609
+  | A0610
+  | A0611
+  | A0612
+  | A0613
+  | A0614
+  | A0615
+  | A0616
+  | A0617
+  | A0618
+  | A0619
+  | A0620
+  | A0621
+  | A0622
+  | A0623
+  | A0624
+  | A0625
+  | A0626
+  | A0627
+  | A0628
+  | A0629
+  | A0630
+  | A0631
+  | A0632
+  | A0633
+  | A0634
+  | A0635
+  | A0636
+  | A0637
+  | A0638
+  | A0639
+  | A0640
+  | A0641
+  | A0642
+  | A0643
+  | A0644
+  | A0645
+  | A0646
+  | A0647
+  | A0648
+  | A0649
+  | A0650
+  | A0651
+  | A0652
+  | A0653
+  | A0654
+  | A0655
+  | A0656
+  | A0657
+  | A0658
+  | A0659
+  | A0660
+  | A0661
+  | A0662
+  | A0663
+  | A0664
+  | A0665
+  | A0666
+  | A0667
+  | A0668
+  | A0669
+  | A0670
+  | A0671
+  | A0672
+  | A0673
+  | A0674
+  | A0675
+  | A0676
+  | A0677
+  | A0678
+  | A0679
+  | A0680
+  | A0681
+  | A0682
+  | A0683
+  | A0684
+  | A0685
+  | A0686
+  | A0687
+  | A0688
+  | A0689
+  | A0690
+  | A0691
+  | A0692
+  | A0693
+  | A0694
+  | A0695
+  | A0696
+  | A0697
+  | A0698
+  | A0699
+  | A0700
+  | A0701
+  | A0702
+  | A0703
+  | A0704
+  | A0705
+  | A0706
+  | A0707
+  | A0708
+  | A0709
+  | A0710
+  | A0711
+  | A0712
+  | A0713
+  | A0714
+  | A0715
+  | A0716
+  | A0717
+  | A0718
+  | A0719
+  | A0720
+  | A0721
+  | A0722
+  | A0723
+  | A0724
+  | A0725
+  | A0726
+  | A0727
+  | A0728
+  | A0729
+  | A0730
+  | A0731
+  | A0732
+  | A0733
+  | A0734
+  | A0735
+  | A0736
+  | A0737
+  | A0738
+  | A0739
+  | A0740
+  | A0741
+  | A0742
+  | A0743
+  | A0744
+  | A0745
+  | A0746
+  | A0747
+  | A0748
+  | A0749
+  | A0750
+  | A0751
+  | A0752
+  | A0753
+  | A0754
+  | A0755
+  | A0756
+  | A0757
+  | A0758
+  | A0759
+  | A0760
+  | A0761
+  | A0762
+  | A0763
+  | A0764
+  | A0765
+  | A0766
+  | A0767
+  | A0768
+  | A0769
+  | A0770
+  | A0771
+  | A0772
+  | A0773
+  | A0774
+  | A0775
+  | A0776
+  | A0777
+  | A0778
+  | A0779
+  | A0780
+  | A0781
+  | A0782
+  | A0783
+  | A0784
+  | A0785
+  | A0786
+  | A0787
+  | A0788
+  | A0789
+  | A0790
+  | A0791
+  | A0792
+  | A0793
+  | A0794
+  | A0795
+  | A0796
+  | A0797
+  | A0798
+  | A0799
+  | A0800
+  | A0801
+  | A0802
+  | A0803
+  | A0804
+  | A0805
+  | A0806
+  | A0807
+  | A0808
+  | A0809
+  | A0810
+  | A0811
+  | A0812
+  | A0813
+  | A0814
+  | A0815
+  | A0816
+  | A0817
+  | A0818
+  | A0819
+  | A0820
+  | A0821
+  | A0822
+  | A0823
+  | A0824
+  | A0825
+  | A0826
+  | A0827
+  | A0828
+  | A0829
+  | A0830
+  | A0831
+  | A0832
+  | A0833
+  | A0834
+  | A0835
+  | A0836
+  | A0837
+  | A0838
+  | A0839
+  | A0840
+  | A0841
+  | A0842
+  | A0843
+  | A0844
+  | A0845
+  | A0846
+  | A0847
+  | A0848
+  | A0849
+  | A0850
+  | A0851
+  | A0852
+  | A0853
+  | A0854
+  | A0855
+  | A0856
+  | A0857
+  | A0858
+  | A0859
+  | A0860
+  | A0861
+  | A0862
+  | A0863
+  | A0864
+  | A0865
+  | A0866
+  | A0867
+  | A0868
+  | A0869
+  | A0870
+  | A0871
+  | A0872
+  | A0873
+  | A0874
+  | A0875
+  | A0876
+  | A0877
+  | A0878
+  | A0879
+  | A0880
+  | A0881
+  | A0882
+  | A0883
+  | A0884
+  | A0885
+  | A0886
+  | A0887
+  | A0888
+  | A0889
+  | A0890
+  | A0891
+  | A0892
+  | A0893
+  | A0894
+  | A0895
+  | A0896
+  | A0897
+  | A0898
+  | A0899
+  | A0900
+  | A0901
+  | A0902
+  | A0903
+  | A0904
+  | A0905
+  | A0906
+  | A0907
+  | A0908
+  | A0909
+  | A0910
+  | A0911
+  | A0912
+  | A0913
+  | A0914
+  | A0915
+  | A0916
+  | A0917
+  | A0918
+  | A0919
+  | A0920
+  | A0921
+  | A0922
+  | A0923
+  | A0924
+  | A0925
+  | A0926
+  | A0927
+  | A0928
+  | A0929
+  | A0930
+  | A0931
+  | A0932
+  | A0933
+  | A0934
+  | A0935
+  | A0936
+  | A0937
+  | A0938
+  | A0939
+  | A0940
+  | A0941
+  | A0942
+  | A0943
+  | A0944
+  | A0945
+  | A0946
+  | A0947
+  | A0948
+  | A0949
+  | A0950
+  | A0951
+  | A0952
+  | A0953
+  | A0954
+  | A0955
+  | A0956
+  | A0957
+  | A0958
+  | A0959
+  | A0960
+  | A0961
+  | A0962
+  | A0963
+  | A0964
+  | A0965
+  | A0966
+  | A0967
+  | A0968
+  | A0969
+  | A0970
+  | A0971
+  | A0972
+  | A0973
+  | A0974
+  | A0975
+  | A0976
+  | A0977
+  | A0978
+  | A0979
+  | A0980
+  | A0981
+  | A0982
+  | A0983
+  | A0984
+  | A0985
+  | A0986
+  | A0987
+  | A0988
+  | A0989
+  | A0990
+  | A0991
+  | A0992
+  | A0993
+  | A0994
+  | A0995
+  | A0996
+  | A0997
+  | A0998
+  | A0999
+  | A1000
+
+f :: A1000 -> Int
+f A0001 = 1990001
+f A0002 = 1990002
+f A0003 = 1990003
+f A0004 = 1990004
+f A0005 = 1990005
+f A0006 = 1990006
+f A0007 = 1990007
+f A0008 = 1990008
+f A0009 = 1990009
+f A0010 = 1990010
+f A0011 = 1990011
+f A0012 = 1990012
+f A0013 = 1990013
+f A0014 = 1990014
+f A0015 = 1990015
+f A0016 = 1990016
+f A0017 = 1990017
+f A0018 = 1990018
+f A0019 = 1990019
+f A0020 = 1990020
+f A0021 = 1990021
+f A0022 = 1990022
+f A0023 = 1990023
+f A0024 = 1990024
+f A0025 = 1990025
+f A0026 = 1990026
+f A0027 = 1990027
+f A0028 = 1990028
+f A0029 = 1990029
+f A0030 = 1990030
+f A0031 = 1990031
+f A0032 = 1990032
+f A0033 = 1990033
+f A0034 = 1990034
+f A0035 = 1990035
+f A0036 = 1990036
+f A0037 = 1990037
+f A0038 = 1990038
+f A0039 = 1990039
+f A0040 = 1990040
+f A0041 = 1990041
+f A0042 = 1990042
+f A0043 = 1990043
+f A0044 = 1990044
+f A0045 = 1990045
+f A0046 = 1990046
+f A0047 = 1990047
+f A0048 = 1990048
+f A0049 = 1990049
+f A0050 = 1990050
+f A0051 = 1990051
+f A0052 = 1990052
+f A0053 = 1990053
+f A0054 = 1990054
+f A0055 = 1990055
+f A0056 = 1990056
+f A0057 = 1990057
+f A0058 = 1990058
+f A0059 = 1990059
+f A0060 = 1990060
+f A0061 = 1990061
+f A0062 = 1990062
+f A0063 = 1990063
+f A0064 = 1990064
+f A0065 = 1990065
+f A0066 = 1990066
+f A0067 = 1990067
+f A0068 = 1990068
+f A0069 = 1990069
+f A0070 = 1990070
+f A0071 = 1990071
+f A0072 = 1990072
+f A0073 = 1990073
+f A0074 = 1990074
+f A0075 = 1990075
+f A0076 = 1990076
+f A0077 = 1990077
+f A0078 = 1990078
+f A0079 = 1990079
+f A0080 = 1990080
+f A0081 = 1990081
+f A0082 = 1990082
+f A0083 = 1990083
+f A0084 = 1990084
+f A0085 = 1990085
+f A0086 = 1990086
+f A0087 = 1990087
+f A0088 = 1990088
+f A0089 = 1990089
+f A0090 = 1990090
+f A0091 = 1990091
+f A0092 = 1990092
+f A0093 = 1990093
+f A0094 = 1990094
+f A0095 = 1990095
+f A0096 = 1990096
+f A0097 = 1990097
+f A0098 = 1990098
+f A0099 = 1990099
+f A0100 = 1990100
+f A0101 = 1990101
+f A0102 = 1990102
+f A0103 = 1990103
+f A0104 = 1990104
+f A0105 = 1990105
+f A0106 = 1990106
+f A0107 = 1990107
+f A0108 = 1990108
+f A0109 = 1990109
+f A0110 = 1990110
+f A0111 = 1990111
+f A0112 = 1990112
+f A0113 = 1990113
+f A0114 = 1990114
+f A0115 = 1990115
+f A0116 = 1990116
+f A0117 = 1990117
+f A0118 = 1990118
+f A0119 = 1990119
+f A0120 = 1990120
+f A0121 = 1990121
+f A0122 = 1990122
+f A0123 = 1990123
+f A0124 = 1990124
+f A0125 = 1990125
+f A0126 = 1990126
+f A0127 = 1990127
+f A0128 = 1990128
+f A0129 = 1990129
+f A0130 = 1990130
+f A0131 = 1990131
+f A0132 = 1990132
+f A0133 = 1990133
+f A0134 = 1990134
+f A0135 = 1990135
+f A0136 = 1990136
+f A0137 = 1990137
+f A0138 = 1990138
+f A0139 = 1990139
+f A0140 = 1990140
+f A0141 = 1990141
+f A0142 = 1990142
+f A0143 = 1990143
+f A0144 = 1990144
+f A0145 = 1990145
+f A0146 = 1990146
+f A0147 = 1990147
+f A0148 = 1990148
+f A0149 = 1990149
+f A0150 = 1990150
+f A0151 = 1990151
+f A0152 = 1990152
+f A0153 = 1990153
+f A0154 = 1990154
+f A0155 = 1990155
+f A0156 = 1990156
+f A0157 = 1990157
+f A0158 = 1990158
+f A0159 = 1990159
+f A0160 = 1990160
+f A0161 = 1990161
+f A0162 = 1990162
+f A0163 = 1990163
+f A0164 = 1990164
+f A0165 = 1990165
+f A0166 = 1990166
+f A0167 = 1990167
+f A0168 = 1990168
+f A0169 = 1990169
+f A0170 = 1990170
+f A0171 = 1990171
+f A0172 = 1990172
+f A0173 = 1990173
+f A0174 = 1990174
+f A0175 = 1990175
+f A0176 = 1990176
+f A0177 = 1990177
+f A0178 = 1990178
+f A0179 = 1990179
+f A0180 = 1990180
+f A0181 = 1990181
+f A0182 = 1990182
+f A0183 = 1990183
+f A0184 = 1990184
+f A0185 = 1990185
+f A0186 = 1990186
+f A0187 = 1990187
+f A0188 = 1990188
+f A0189 = 1990189
+f A0190 = 1990190
+f A0191 = 1990191
+f A0192 = 1990192
+f A0193 = 1990193
+f A0194 = 1990194
+f A0195 = 1990195
+f A0196 = 1990196
+f A0197 = 1990197
+f A0198 = 1990198
+f A0199 = 1990199
+f A0200 = 1990200
+f A0201 = 1990201
+f A0202 = 1990202
+f A0203 = 1990203
+f A0204 = 1990204
+f A0205 = 1990205
+f A0206 = 1990206
+f A0207 = 1990207
+f A0208 = 1990208
+f A0209 = 1990209
+f A0210 = 1990210
+f A0211 = 1990211
+f A0212 = 1990212
+f A0213 = 1990213
+f A0214 = 1990214
+f A0215 = 1990215
+f A0216 = 1990216
+f A0217 = 1990217
+f A0218 = 1990218
+f A0219 = 1990219
+f A0220 = 1990220
+f A0221 = 1990221
+f A0222 = 1990222
+f A0223 = 1990223
+f A0224 = 1990224
+f A0225 = 1990225
+f A0226 = 1990226
+f A0227 = 1990227
+f A0228 = 1990228
+f A0229 = 1990229
+f A0230 = 1990230
+f A0231 = 1990231
+f A0232 = 1990232
+f A0233 = 1990233
+f A0234 = 1990234
+f A0235 = 1990235
+f A0236 = 1990236
+f A0237 = 1990237
+f A0238 = 1990238
+f A0239 = 1990239
+f A0240 = 1990240
+f A0241 = 1990241
+f A0242 = 1990242
+f A0243 = 1990243
+f A0244 = 1990244
+f A0245 = 1990245
+f A0246 = 1990246
+f A0247 = 1990247
+f A0248 = 1990248
+f A0249 = 1990249
+f A0250 = 1990250
+f A0251 = 1990251
+f A0252 = 1990252
+f A0253 = 1990253
+f A0254 = 1990254
+f A0255 = 1990255
+f A0256 = 1990256
+f A0257 = 1990257
+f A0258 = 1990258
+f A0259 = 1990259
+f A0260 = 1990260
+f A0261 = 1990261
+f A0262 = 1990262
+f A0263 = 1990263
+f A0264 = 1990264
+f A0265 = 1990265
+f A0266 = 1990266
+f A0267 = 1990267
+f A0268 = 1990268
+f A0269 = 1990269
+f A0270 = 1990270
+f A0271 = 1990271
+f A0272 = 1990272
+f A0273 = 1990273
+f A0274 = 1990274
+f A0275 = 1990275
+f A0276 = 1990276
+f A0277 = 1990277
+f A0278 = 1990278
+f A0279 = 1990279
+f A0280 = 1990280
+f A0281 = 1990281
+f A0282 = 1990282
+f A0283 = 1990283
+f A0284 = 1990284
+f A0285 = 1990285
+f A0286 = 1990286
+f A0287 = 1990287
+f A0288 = 1990288
+f A0289 = 1990289
+f A0290 = 1990290
+f A0291 = 1990291
+f A0292 = 1990292
+f A0293 = 1990293
+f A0294 = 1990294
+f A0295 = 1990295
+f A0296 = 1990296
+f A0297 = 1990297
+f A0298 = 1990298
+f A0299 = 1990299
+f A0300 = 1990300
+f A0301 = 1990301
+f A0302 = 1990302
+f A0303 = 1990303
+f A0304 = 1990304
+f A0305 = 1990305
+f A0306 = 1990306
+f A0307 = 1990307
+f A0308 = 1990308
+f A0309 = 1990309
+f A0310 = 1990310
+f A0311 = 1990311
+f A0312 = 1990312
+f A0313 = 1990313
+f A0314 = 1990314
+f A0315 = 1990315
+f A0316 = 1990316
+f A0317 = 1990317
+f A0318 = 1990318
+f A0319 = 1990319
+f A0320 = 1990320
+f A0321 = 1990321
+f A0322 = 1990322
+f A0323 = 1990323
+f A0324 = 1990324
+f A0325 = 1990325
+f A0326 = 1990326
+f A0327 = 1990327
+f A0328 = 1990328
+f A0329 = 1990329
+f A0330 = 1990330
+f A0331 = 1990331
+f A0332 = 1990332
+f A0333 = 1990333
+f A0334 = 1990334
+f A0335 = 1990335
+f A0336 = 1990336
+f A0337 = 1990337
+f A0338 = 1990338
+f A0339 = 1990339
+f A0340 = 1990340
+f A0341 = 1990341
+f A0342 = 1990342
+f A0343 = 1990343
+f A0344 = 1990344
+f A0345 = 1990345
+f A0346 = 1990346
+f A0347 = 1990347
+f A0348 = 1990348
+f A0349 = 1990349
+f A0350 = 1990350
+f A0351 = 1990351
+f A0352 = 1990352
+f A0353 = 1990353
+f A0354 = 1990354
+f A0355 = 1990355
+f A0356 = 1990356
+f A0357 = 1990357
+f A0358 = 1990358
+f A0359 = 1990359
+f A0360 = 1990360
+f A0361 = 1990361
+f A0362 = 1990362
+f A0363 = 1990363
+f A0364 = 1990364
+f A0365 = 1990365
+f A0366 = 1990366
+f A0367 = 1990367
+f A0368 = 1990368
+f A0369 = 1990369
+f A0370 = 1990370
+f A0371 = 1990371
+f A0372 = 1990372
+f A0373 = 1990373
+f A0374 = 1990374
+f A0375 = 1990375
+f A0376 = 1990376
+f A0377 = 1990377
+f A0378 = 1990378
+f A0379 = 1990379
+f A0380 = 1990380
+f A0381 = 1990381
+f A0382 = 1990382
+f A0383 = 1990383
+f A0384 = 1990384
+f A0385 = 1990385
+f A0386 = 1990386
+f A0387 = 1990387
+f A0388 = 1990388
+f A0389 = 1990389
+f A0390 = 1990390
+f A0391 = 1990391
+f A0392 = 1990392
+f A0393 = 1990393
+f A0394 = 1990394
+f A0395 = 1990395
+f A0396 = 1990396
+f A0397 = 1990397
+f A0398 = 1990398
+f A0399 = 1990399
+f A0400 = 1990400
+f A0401 = 1990401
+f A0402 = 1990402
+f A0403 = 1990403
+f A0404 = 1990404
+f A0405 = 1990405
+f A0406 = 1990406
+f A0407 = 1990407
+f A0408 = 1990408
+f A0409 = 1990409
+f A0410 = 1990410
+f A0411 = 1990411
+f A0412 = 1990412
+f A0413 = 1990413
+f A0414 = 1990414
+f A0415 = 1990415
+f A0416 = 1990416
+f A0417 = 1990417
+f A0418 = 1990418
+f A0419 = 1990419
+f A0420 = 1990420
+f A0421 = 1990421
+f A0422 = 1990422
+f A0423 = 1990423
+f A0424 = 1990424
+f A0425 = 1990425
+f A0426 = 1990426
+f A0427 = 1990427
+f A0428 = 1990428
+f A0429 = 1990429
+f A0430 = 1990430
+f A0431 = 1990431
+f A0432 = 1990432
+f A0433 = 1990433
+f A0434 = 1990434
+f A0435 = 1990435
+f A0436 = 1990436
+f A0437 = 1990437
+f A0438 = 1990438
+f A0439 = 1990439
+f A0440 = 1990440
+f A0441 = 1990441
+f A0442 = 1990442
+f A0443 = 1990443
+f A0444 = 1990444
+f A0445 = 1990445
+f A0446 = 1990446
+f A0447 = 1990447
+f A0448 = 1990448
+f A0449 = 1990449
+f A0450 = 1990450
+f A0451 = 1990451
+f A0452 = 1990452
+f A0453 = 1990453
+f A0454 = 1990454
+f A0455 = 1990455
+f A0456 = 1990456
+f A0457 = 1990457
+f A0458 = 1990458
+f A0459 = 1990459
+f A0460 = 1990460
+f A0461 = 1990461
+f A0462 = 1990462
+f A0463 = 1990463
+f A0464 = 1990464
+f A0465 = 1990465
+f A0466 = 1990466
+f A0467 = 1990467
+f A0468 = 1990468
+f A0469 = 1990469
+f A0470 = 1990470
+f A0471 = 1990471
+f A0472 = 1990472
+f A0473 = 1990473
+f A0474 = 1990474
+f A0475 = 1990475
+f A0476 = 1990476
+f A0477 = 1990477
+f A0478 = 1990478
+f A0479 = 1990479
+f A0480 = 1990480
+f A0481 = 1990481
+f A0482 = 1990482
+f A0483 = 1990483
+f A0484 = 1990484
+f A0485 = 1990485
+f A0486 = 1990486
+f A0487 = 1990487
+f A0488 = 1990488
+f A0489 = 1990489
+f A0490 = 1990490
+f A0491 = 1990491
+f A0492 = 1990492
+f A0493 = 1990493
+f A0494 = 1990494
+f A0495 = 1990495
+f A0496 = 1990496
+f A0497 = 1990497
+f A0498 = 1990498
+f A0499 = 1990499
+f A0500 = 1990500
+f A0501 = 1990501
+f A0502 = 1990502
+f A0503 = 1990503
+f A0504 = 1990504
+f A0505 = 1990505
+f A0506 = 1990506
+f A0507 = 1990507
+f A0508 = 1990508
+f A0509 = 1990509
+f A0510 = 1990510
+f A0511 = 1990511
+f A0512 = 1990512
+f A0513 = 1990513
+f A0514 = 1990514
+f A0515 = 1990515
+f A0516 = 1990516
+f A0517 = 1990517
+f A0518 = 1990518
+f A0519 = 1990519
+f A0520 = 1990520
+f A0521 = 1990521
+f A0522 = 1990522
+f A0523 = 1990523
+f A0524 = 1990524
+f A0525 = 1990525
+f A0526 = 1990526
+f A0527 = 1990527
+f A0528 = 1990528
+f A0529 = 1990529
+f A0530 = 1990530
+f A0531 = 1990531
+f A0532 = 1990532
+f A0533 = 1990533
+f A0534 = 1990534
+f A0535 = 1990535
+f A0536 = 1990536
+f A0537 = 1990537
+f A0538 = 1990538
+f A0539 = 1990539
+f A0540 = 1990540
+f A0541 = 1990541
+f A0542 = 1990542
+f A0543 = 1990543
+f A0544 = 1990544
+f A0545 = 1990545
+f A0546 = 1990546
+f A0547 = 1990547
+f A0548 = 1990548
+f A0549 = 1990549
+f A0550 = 1990550
+f A0551 = 1990551
+f A0552 = 1990552
+f A0553 = 1990553
+f A0554 = 1990554
+f A0555 = 1990555
+f A0556 = 1990556
+f A0557 = 1990557
+f A0558 = 1990558
+f A0559 = 1990559
+f A0560 = 1990560
+f A0561 = 1990561
+f A0562 = 1990562
+f A0563 = 1990563
+f A0564 = 1990564
+f A0565 = 1990565
+f A0566 = 1990566
+f A0567 = 1990567
+f A0568 = 1990568
+f A0569 = 1990569
+f A0570 = 1990570
+f A0571 = 1990571
+f A0572 = 1990572
+f A0573 = 1990573
+f A0574 = 1990574
+f A0575 = 1990575
+f A0576 = 1990576
+f A0577 = 1990577
+f A0578 = 1990578
+f A0579 = 1990579
+f A0580 = 1990580
+f A0581 = 1990581
+f A0582 = 1990582
+f A0583 = 1990583
+f A0584 = 1990584
+f A0585 = 1990585
+f A0586 = 1990586
+f A0587 = 1990587
+f A0588 = 1990588
+f A0589 = 1990589
+f A0590 = 1990590
+f A0591 = 1990591
+f A0592 = 1990592
+f A0593 = 1990593
+f A0594 = 1990594
+f A0595 = 1990595
+f A0596 = 1990596
+f A0597 = 1990597
+f A0598 = 1990598
+f A0599 = 1990599
+f A0600 = 1990600
+f A0601 = 1990601
+f A0602 = 1990602
+f A0603 = 1990603
+f A0604 = 1990604
+f A0605 = 1990605
+f A0606 = 1990606
+f A0607 = 1990607
+f A0608 = 1990608
+f A0609 = 1990609
+f A0610 = 1990610
+f A0611 = 1990611
+f A0612 = 1990612
+f A0613 = 1990613
+f A0614 = 1990614
+f A0615 = 1990615
+f A0616 = 1990616
+f A0617 = 1990617
+f A0618 = 1990618
+f A0619 = 1990619
+f A0620 = 1990620
+f A0621 = 1990621
+f A0622 = 1990622
+f A0623 = 1990623
+f A0624 = 1990624
+f A0625 = 1990625
+f A0626 = 1990626
+f A0627 = 1990627
+f A0628 = 1990628
+f A0629 = 1990629
+f A0630 = 1990630
+f A0631 = 1990631
+f A0632 = 1990632
+f A0633 = 1990633
+f A0634 = 1990634
+f A0635 = 1990635
+f A0636 = 1990636
+f A0637 = 1990637
+f A0638 = 1990638
+f A0639 = 1990639
+f A0640 = 1990640
+f A0641 = 1990641
+f A0642 = 1990642
+f A0643 = 1990643
+f A0644 = 1990644
+f A0645 = 1990645
+f A0646 = 1990646
+f A0647 = 1990647
+f A0648 = 1990648
+f A0649 = 1990649
+f A0650 = 1990650
+f A0651 = 1990651
+f A0652 = 1990652
+f A0653 = 1990653
+f A0654 = 1990654
+f A0655 = 1990655
+f A0656 = 1990656
+f A0657 = 1990657
+f A0658 = 1990658
+f A0659 = 1990659
+f A0660 = 1990660
+f A0661 = 1990661
+f A0662 = 1990662
+f A0663 = 1990663
+f A0664 = 1990664
+f A0665 = 1990665
+f A0666 = 1990666
+f A0667 = 1990667
+f A0668 = 1990668
+f A0669 = 1990669
+f A0670 = 1990670
+f A0671 = 1990671
+f A0672 = 1990672
+f A0673 = 1990673
+f A0674 = 1990674
+f A0675 = 1990675
+f A0676 = 1990676
+f A0677 = 1990677
+f A0678 = 1990678
+f A0679 = 1990679
+f A0680 = 1990680
+f A0681 = 1990681
+f A0682 = 1990682
+f A0683 = 1990683
+f A0684 = 1990684
+f A0685 = 1990685
+f A0686 = 1990686
+f A0687 = 1990687
+f A0688 = 1990688
+f A0689 = 1990689
+f A0690 = 1990690
+f A0691 = 1990691
+f A0692 = 1990692
+f A0693 = 1990693
+f A0694 = 1990694
+f A0695 = 1990695
+f A0696 = 1990696
+f A0697 = 1990697
+f A0698 = 1990698
+f A0699 = 1990699
+f A0700 = 1990700
+f A0701 = 1990701
+f A0702 = 1990702
+f A0703 = 1990703
+f A0704 = 1990704
+f A0705 = 1990705
+f A0706 = 1990706
+f A0707 = 1990707
+f A0708 = 1990708
+f A0709 = 1990709
+f A0710 = 1990710
+f A0711 = 1990711
+f A0712 = 1990712
+f A0713 = 1990713
+f A0714 = 1990714
+f A0715 = 1990715
+f A0716 = 1990716
+f A0717 = 1990717
+f A0718 = 1990718
+f A0719 = 1990719
+f A0720 = 1990720
+f A0721 = 1990721
+f A0722 = 1990722
+f A0723 = 1990723
+f A0724 = 1990724
+f A0725 = 1990725
+f A0726 = 1990726
+f A0727 = 1990727
+f A0728 = 1990728
+f A0729 = 1990729
+f A0730 = 1990730
+f A0731 = 1990731
+f A0732 = 1990732
+f A0733 = 1990733
+f A0734 = 1990734
+f A0735 = 1990735
+f A0736 = 1990736
+f A0737 = 1990737
+f A0738 = 1990738
+f A0739 = 1990739
+f A0740 = 1990740
+f A0741 = 1990741
+f A0742 = 1990742
+f A0743 = 1990743
+f A0744 = 1990744
+f A0745 = 1990745
+f A0746 = 1990746
+f A0747 = 1990747
+f A0748 = 1990748
+f A0749 = 1990749
+f A0750 = 1990750
+f A0751 = 1990751
+f A0752 = 1990752
+f A0753 = 1990753
+f A0754 = 1990754
+f A0755 = 1990755
+f A0756 = 1990756
+f A0757 = 1990757
+f A0758 = 1990758
+f A0759 = 1990759
+f A0760 = 1990760
+f A0761 = 1990761
+f A0762 = 1990762
+f A0763 = 1990763
+f A0764 = 1990764
+f A0765 = 1990765
+f A0766 = 1990766
+f A0767 = 1990767
+f A0768 = 1990768
+f A0769 = 1990769
+f A0770 = 1990770
+f A0771 = 1990771
+f A0772 = 1990772
+f A0773 = 1990773
+f A0774 = 1990774
+f A0775 = 1990775
+f A0776 = 1990776
+f A0777 = 1990777
+f A0778 = 1990778
+f A0779 = 1990779
+f A0780 = 1990780
+f A0781 = 1990781
+f A0782 = 1990782
+f A0783 = 1990783
+f A0784 = 1990784
+f A0785 = 1990785
+f A0786 = 1990786
+f A0787 = 1990787
+f A0788 = 1990788
+f A0789 = 1990789
+f A0790 = 1990790
+f A0791 = 1990791
+f A0792 = 1990792
+f A0793 = 1990793
+f A0794 = 1990794
+f A0795 = 1990795
+f A0796 = 1990796
+f A0797 = 1990797
+f A0798 = 1990798
+f A0799 = 1990799
+f A0800 = 1990800
+f A0801 = 1990801
+f A0802 = 1990802
+f A0803 = 1990803
+f A0804 = 1990804
+f A0805 = 1990805
+f A0806 = 1990806
+f A0807 = 1990807
+f A0808 = 1990808
+f A0809 = 1990809
+f A0810 = 1990810
+f A0811 = 1990811
+f A0812 = 1990812
+f A0813 = 1990813
+f A0814 = 1990814
+f A0815 = 1990815
+f A0816 = 1990816
+f A0817 = 1990817
+f A0818 = 1990818
+f A0819 = 1990819
+f A0820 = 1990820
+f A0821 = 1990821
+f A0822 = 1990822
+f A0823 = 1990823
+f A0824 = 1990824
+f A0825 = 1990825
+f A0826 = 1990826
+f A0827 = 1990827
+f A0828 = 1990828
+f A0829 = 1990829
+f A0830 = 1990830
+f A0831 = 1990831
+f A0832 = 1990832
+f A0833 = 1990833
+f A0834 = 1990834
+f A0835 = 1990835
+f A0836 = 1990836
+f A0837 = 1990837
+f A0838 = 1990838
+f A0839 = 1990839
+f A0840 = 1990840
+f A0841 = 1990841
+f A0842 = 1990842
+f A0843 = 1990843
+f A0844 = 1990844
+f A0845 = 1990845
+f A0846 = 1990846
+f A0847 = 1990847
+f A0848 = 1990848
+f A0849 = 1990849
+f A0850 = 1990850
+f A0851 = 1990851
+f A0852 = 1990852
+f A0853 = 1990853
+f A0854 = 1990854
+f A0855 = 1990855
+f A0856 = 1990856
+f A0857 = 1990857
+f A0858 = 1990858
+f A0859 = 1990859
+f A0860 = 1990860
+f A0861 = 1990861
+f A0862 = 1990862
+f A0863 = 1990863
+f A0864 = 1990864
+f A0865 = 1990865
+f A0866 = 1990866
+f A0867 = 1990867
+f A0868 = 1990868
+f A0869 = 1990869
+f A0870 = 1990870
+f A0871 = 1990871
+f A0872 = 1990872
+f A0873 = 1990873
+f A0874 = 1990874
+f A0875 = 1990875
+f A0876 = 1990876
+f A0877 = 1990877
+f A0878 = 1990878
+f A0879 = 1990879
+f A0880 = 1990880
+f A0881 = 1990881
+f A0882 = 1990882
+f A0883 = 1990883
+f A0884 = 1990884
+f A0885 = 1990885
+f A0886 = 1990886
+f A0887 = 1990887
+f A0888 = 1990888
+f A0889 = 1990889
+f A0890 = 1990890
+f A0891 = 1990891
+f A0892 = 1990892
+f A0893 = 1990893
+f A0894 = 1990894
+f A0895 = 1990895
+f A0896 = 1990896
+f A0897 = 1990897
+f A0898 = 1990898
+f A0899 = 1990899
+f A0900 = 1990900
+f A0901 = 1990901
+f A0902 = 1990902
+f A0903 = 1990903
+f A0904 = 1990904
+f A0905 = 1990905
+f A0906 = 1990906
+f A0907 = 1990907
+f A0908 = 1990908
+f A0909 = 1990909
+f A0910 = 1990910
+f A0911 = 1990911
+f A0912 = 1990912
+f A0913 = 1990913
+f A0914 = 1990914
+f A0915 = 1990915
+f A0916 = 1990916
+f A0917 = 1990917
+f A0918 = 1990918
+f A0919 = 1990919
+f A0920 = 1990920
+f A0921 = 1990921
+f A0922 = 1990922
+f A0923 = 1990923
+f A0924 = 1990924
+f A0925 = 1990925
+f A0926 = 1990926
+f A0927 = 1990927
+f A0928 = 1990928
+f A0929 = 1990929
+f A0930 = 1990930
+f A0931 = 1990931
+f A0932 = 1990932
+f A0933 = 1990933
+f A0934 = 1990934
+f A0935 = 1990935
+f A0936 = 1990936
+f A0937 = 1990937
+f A0938 = 1990938
+f A0939 = 1990939
+f A0940 = 1990940
+f A0941 = 1990941
+f A0942 = 1990942
+f A0943 = 1990943
+f A0944 = 1990944
+f A0945 = 1990945
+f A0946 = 1990946
+f A0947 = 1990947
+f A0948 = 1990948
+f A0949 = 1990949
+f A0950 = 1990950
+f A0951 = 1990951
+f A0952 = 1990952
+f A0953 = 1990953
+f A0954 = 1990954
+f A0955 = 1990955
+f A0956 = 1990956
+f A0957 = 1990957
+f A0958 = 1990958
+f A0959 = 1990959
+f A0960 = 1990960
+f A0961 = 1990961
+f A0962 = 1990962
+f A0963 = 1990963
+f A0964 = 1990964
+f A0965 = 1990965
+f A0966 = 1990966
+f A0967 = 1990967
+f A0968 = 1990968
+f A0969 = 1990969
+f A0970 = 1990970
+f A0971 = 1990971
+f A0972 = 1990972
+f A0973 = 1990973
+f A0974 = 1990974
+f A0975 = 1990975
+f A0976 = 1990976
+f A0977 = 1990977
+f A0978 = 1990978
+f A0979 = 1990979
+f A0980 = 1990980
+f A0981 = 1990981
+f A0982 = 1990982
+f A0983 = 1990983
+f A0984 = 1990984
+f A0985 = 1990985
+f A0986 = 1990986
+f A0987 = 1990987
+f A0988 = 1990988
+f A0989 = 1990989
+f A0990 = 1990990
+f A0991 = 1990991
+f A0992 = 1990992
+f A0993 = 1990993
+f A0994 = 1990994
+f A0995 = 1990995
+f A0996 = 1990996
+f A0997 = 1990997
+f A0998 = 1990998
+f A0999 = 1990999
+f A1000 = 1991000


=====================================
testsuite/tests/pmcheck/complete_sigs/T13363a.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lib where
+
+data Boolean = F | T
+  deriving Eq
+
+pattern TooGoodToBeTrue :: Boolean
+pattern TooGoodToBeTrue = T
+{-# COMPLETE F, TooGoodToBeTrue #-}
+
+catchAll :: Boolean -> Int
+catchAll F               = 0
+catchAll TooGoodToBeTrue = 1
+catchAll _               = error "impossible"


=====================================
testsuite/tests/pmcheck/complete_sigs/T13363a.stderr
=====================================
@@ -0,0 +1,7 @@
+
+testsuite/tests/pmcheck/complete_sigs/T13363a.hs:15:1: warning: [-Woverlapping-patterns]
+    Pattern match is redundant
+    In an equation for `catchAll': catchAll _ = ...
+   |
+14 | catchAll _               = error "impossible"
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^


=====================================
testsuite/tests/pmcheck/complete_sigs/T13363b.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lib where
+
+data T = A | B | C
+  deriving Eq
+
+pattern BC :: T
+pattern BC = C
+
+{-# COMPLETE A, BC #-}
+
+f A  = 1
+f B  = 2
+f BC = 3
+f _  = error "impossible"


=====================================
testsuite/tests/pmcheck/complete_sigs/T13363b.stderr
=====================================
@@ -0,0 +1,7 @@
+
+testsuite/tests/pmcheck/complete_sigs/T13363b.hs:16:1: warning: [-Woverlapping-patterns]
+    Pattern match is redundant
+    In an equation for `f': f _ = ...
+   |
+16 | f _  = error "impossible"
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^


=====================================
testsuite/tests/pmcheck/complete_sigs/all.T
=====================================
@@ -14,4 +14,6 @@ test('completesig13', normal, compile, [''])
 test('completesig14', normal, compile, [''])
 test('completesig15', normal, compile_fail, [''])
 test('T14059a', normal, compile, [''])
-test('T14253', expect_broken(14253), compile, [''])
+test('T14253', normal, compile, [''])
+test('T13363a', normal, compile, ['-Wall'])
+test('T13363b', normal, compile, ['-Wall'])


=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -92,6 +92,12 @@ test('pmc006', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('pmc007', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc008', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc009', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc010', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11245', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T12957', [], compile, ['-fwarn-overlapping-patterns'])


=====================================
testsuite/tests/pmcheck/should_compile/pmc008.hs
=====================================
@@ -0,0 +1,9 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-}
+
+module PMC008 where
+
+-- complete match, but because of the guard, the information that `x` is not
+-- `Just` has to flow through the term oracle.
+foo :: Maybe Int -> Int
+foo x | Just y <- x = y
+foo Nothing = 43


=====================================
testsuite/tests/pmcheck/should_compile/pmc009.hs
=====================================
@@ -0,0 +1,7 @@
+module Lib where
+
+data D = A | B
+
+f :: D -> D -> D
+f A A = A
+f B B = B


=====================================
testsuite/tests/pmcheck/should_compile/pmc010.hs
=====================================
@@ -0,0 +1,9 @@
+module Lib where
+
+data D = A | B | C | D
+
+f :: D -> D -> D
+f A A = A
+f B B = B
+f C C = C
+f D D = D



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/4e2f1875d8dd5c2fa92c9c84531c55b5b73e2dd6

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/4e2f1875d8dd5c2fa92c9c84531c55b5b73e2dd6
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20190529/74c5cd48/attachment-0001.html>


More information about the ghc-commits mailing list