Fix Uncovered set of literal patterns

Issues #16289 and #15713 are proof that the pattern match checker did
an unsound job of estimating the value set abstraction corresponding to
the uncovered set.

The reason is that the fix from #11303 introducing `NLit` was
incomplete: The `LitCon` case desugared to `Var` rather than `LitVar`,
which would have done the necessary case splitting analogous to the
`ConVar` case.

This patch rectifies that by introducing the fresh unification variable
in `LitCon` in value abstraction position rather than pattern postition,
recording a constraint equating it to the constructor expression rather
than the literal. Fixes #16289 and #15713.

2 files changed, 14 insertions, 5 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 0c653da2b2..1495280f94 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -2118,15 +2118,22 @@ pmcheckHd (p@(PmLit l)) ps guards
 -- no information is lost
 
 -- LitCon
-pmcheckHd (PmLit l) ps guards (va@(PmCon {})) (ValVec vva delta)
+pmcheckHd p@PmLit{} ps guards va@PmCon{} (ValVec vva delta)
   = do y <- liftD $ mkPmId (pmPatType va)
-       let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
+       -- 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
+       -- care of the case split by resorting to NLit.
+       let tm_state = extendSubst y (vaToPmExpr va) (delta_tm_cs delta)
            delta'   = delta { delta_tm_cs = tm_state }
-       pmcheckHdI (PmVar y) ps guards va (ValVec vva delta')
+       pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
 
 -- ConLit
-pmcheckHd (p@(PmCon {})) ps guards (PmLit l) (ValVec vva delta)
+pmcheckHd p@PmCon{} ps guards (PmLit l) (ValVec vva delta)
   = do y <- liftD $ 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.
        let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
            delta'   = delta { delta_tm_cs = tm_state }
        pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs
index d6364bef52..87e5f0a268 100644
--- a/compiler/deSugar/TmOracle.hs
+++ b/compiler/deSugar/TmOracle.hs
@@ -33,6 +33,7 @@ import HsLit
 import TcHsSyn
 import MonadUtils
 import Util
+import Outputable
 
 import NameEnv
 
@@ -134,7 +135,8 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
 
   (PmExprEq _ _, PmExprEq _ _) -> Just (eq:standby, (unhandled, env))
 
-  _ -> Just (standby, (True, env)) -- I HATE CATCH-ALLS
+  _ -> WARN( True, text "solveComplexEq: Catch all" <+> ppr eq )
+       Just (standby, (True, env)) -- I HATE CATCH-ALLS
 
 -- | Extend the substitution and solve the (possibly updated) constraints.
 extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState