Fix the coverage checker's treatment of existential tyvars

Previously, the pattern-match coverage checker was far too
eager to freshen the names of existentially quantified type
variables, which led to incorrect sets of type constraints that
misled GHC into thinking that certain programs that involve nested
GADT pattern matches were non-exhaustive (when in fact they were).
Now, we generate extra equality constraints in the ConCon case of
the coverage algorithm to ensure that these fresh tyvars align
with existing existential tyvars. See
`Note [Coverage checking and existential tyvars]` for the full story.

Test Plan: make test TEST="T11984 T14098"

Reviewers: gkaracha, bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie, carter

GHC Trac Issues: #11984, #14098

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

4 files changed, 188 insertions, 6 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 7e52e469eb..22af2fb9d0 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -55,8 +55,8 @@ import DsGRHSs       (isTrueLHsExpr)
 import Maybes        (expectJust)
 
 import Data.List     (find)
-import Data.Maybe    (isJust, fromMaybe)
-import Control.Monad (forM, when, forM_)
+import Data.Maybe    (catMaybes, isJust, fromMaybe)
+import Control.Monad (forM, when, forM_, zipWithM)
 import Coercion
 import TcEvidence
 import IOEnv
@@ -1502,12 +1502,28 @@ pmcheckHd (PmVar x) ps guards va (ValVec vva delta)
   | otherwise = return mempty
 
 -- ConCon
-pmcheckHd ( p@(PmCon {pm_con_con = c1, pm_con_args = args1})) ps guards
-          (va@(PmCon {pm_con_con = c2, pm_con_args = args2})) (ValVec vva delta)
+pmcheckHd ( p@(PmCon { pm_con_con = c1, pm_con_tvs = ex_tvs1
+                     , pm_con_args = args1})) ps guards
+          (va@(PmCon { pm_con_con = c2, pm_con_tvs = ex_tvs2
+                     , pm_con_args = args2})) (ValVec vva delta)
   | c1 /= c2  =
     return (usimple [ValVec (va:vva) delta])
-  | otherwise = kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
-                <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta)
+  | otherwise = do
+    let to_evvar tv1 tv2 = nameType "pmConCon" $
+                           mkPrimEqPred (mkTyVarTy tv1) (mkTyVarTy tv2)
+        mb_to_evvar tv1 tv2
+            -- If we have identical constructors but different existential
+            -- tyvars, then generate extra equality constraints to ensure the
+            -- existential tyvars.
+            -- See Note [Coverage checking and existential tyvars].
+          | tv1 == tv2 = pure Nothing
+          | otherwise  = Just <$> to_evvar tv1 tv2
+    evvars <- (listToBag . catMaybes) <$>
+              ASSERT(ex_tvs1 `equalLength` ex_tvs2)
+              liftD (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')
 
 -- LitLit
 pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva =
@@ -1598,6 +1614,121 @@ pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
 -- Impossible: handled by pmcheck
 pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
 
+{-
+Note [Coverage checking and existential tyvars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC's implementation of the pattern-match coverage algorithm (as described in
+the GADTs Meet Their Match paper) must take some care to emit enough type
+constraints when handling data constructors with exisentially quantified type
+variables. To better explain what the challenge is, consider a constructor K
+of the form:
+
+  K @e_1 ... @e_m ev_1 ... ev_v ty_1 ... ty_n :: T u_1 ... u_p
+
+Where:
+
+* e_1, ..., e_m are the existentially bound type variables.
+* ev_1, ..., ev_v are evidence variables, which may inhabit a dictionary type
+  (e.g., Eq) or an equality constraint (e.g., e_1 ~ Int).
+* ty_1, ..., ty_n are the types of K's fields.
+* T u_1 ... u_p is the return type, where T is the data type constructor, and
+  u_1, ..., u_p are the universally quantified type variables.
+
+In the ConVar case, the coverage algorithm will have in hand the constructor
+K as well as a pattern variable (pv :: T PV_1 ... PV_p), where PV_1, ..., PV_p
+are some types that instantiate u_1, ... u_p. The idea is that we should
+substitute PV_1 for u_1, ..., and PV_p for u_p when forming a PmCon (the
+mkOneConFull function accomplishes this) and then hand this PmCon off to the
+ConCon case.
+
+The presence of existentially quantified type variables adds a significant
+wrinkle. We always grab e_1, ..., e_m from the definition of K to begin with,
+but we don't want them to appear in the final PmCon, because then
+calling (mkOneConFull K) for other pattern variables might reuse the same
+existential tyvars, which is certainly wrong.
+
+Previously, GHC's solution to this wrinkle was to always create fresh names
+for the existential tyvars and put them into the PmCon. This works well for
+many cases, but it can break down if you nest GADT pattern matches in just
+the right way. For instance, consider the following program:
+
+    data App f a where
+      App :: f a -> App f (Maybe a)
+
+    data Ty a where
+      TBool :: Ty Bool
+      TInt  :: Ty Int
+
+    data T f a where
+      C :: T Ty (Maybe Bool)
+
+    foo :: T f a -> App f a -> ()
+    foo C (App TBool) = ()
+
+foo is a total program, but with the previous approach to handling existential
+tyvars, GHC would mark foo's patterns as non-exhaustive.
+
+When foo is desugared to Core, it looks roughly like so:
+
+    foo @f @a (C co1 _co2) (App @a1 _co3 (TBool |> co1)) = ()
+
+(Where `a1` is an existential tyvar.)
+
+That, in turn, is processed by the coverage checker to become:
+
+    foo @f @a (C co1 _co2) (App @a1 _co3 (pmvar123 :: f a1))
+      | TBool <- pmvar123 |> co1
+      = ()
+
+Note that the type of pmvar123 is `f a1`—this will be important later.
+
+Now, we proceed with coverage-checking as usual. When we come to the
+ConVar case for App, we create a fresh variable `a2` to represent its
+existential tyvar. At this point, we have the equality constraints
+`(a ~ Maybe a2, a ~ Maybe Bool, f ~ Ty)` in scope.
+
+However, when we check the guard, it will use the type of pmvar123, which is
+`f a1`. Thus, when considering if pmvar123 can match the constructor TInt,
+it will generate the constraint `a1 ~ Int`. This means our final set of
+equality constraints would be:
+
+    f  ~ Ty
+    a  ~ Maybe Bool
+    a  ~ Maybe a2
+    a1 ~ Int
+
+Which is satisfiable! Freshening the existential tyvar `a` to `a2` doomed us,
+because GHC is unable to relate `a2` to `a1`, which really should be the same
+tyvar.
+
+Luckily, we can avoid this pitfall. Recall that the ConVar case was where we
+generated a PmCon with too-fresh existentials. But after ConVar, we have the
+ConCon case, which considers whether each constructor of a particular data type
+can be matched on in a particular spot.
+
+In the case of App, when we get to the ConCon case, we will compare our
+original App PmCon (from the source program) to the App PmCon created from the
+ConVar case. In the former PmCon, we have `a1` in hand, which is exactly the
+existential tyvar we want! Thus, we can force `a1` to be the same as `a2` here
+by emitting an additional `a1 ~ a2` constraint. Now our final set of equality
+constraints will be:
+
+    f  ~ Ty
+    a  ~ Maybe Bool
+    a  ~ Maybe a2
+    a1 ~ Int
+    a1 ~ a2
+
+Which is unsatisfiable, as we desired, since we now have that
+Int ~ a1 ~ a2 ~ Bool.
+
+In general, App might have more than one constructor, in which case we
+couldn't reuse the existential tyvar for App for a different constructor. This
+means that we can only use this trick in ConCon when the constructors are the
+same. But this is fine, since this is the only scenario where this situation
+arises in the first place!
+-}
+
 -- ----------------------------------------------------------------------------
 -- * Utilities for main checking
 
diff --git a/testsuite/tests/pmcheck/should_compile/T11984.hs b/testsuite/tests/pmcheck/should_compile/T11984.hs
new file mode 100644
index 0000000000..b655df0efe
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T11984.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE PolyKinds, TypeOperators, DataKinds, TypeFamilies, GADTs #-}
+
+module T11984 where
+
+data family Sing (a :: k)
+
+data Schema = Sch [Bool]
+
+data instance Sing (x :: Schema) where
+  SSch :: Sing x -> Sing ('Sch x)
+
+data instance Sing (x :: [k]) where
+  SNil :: Sing '[]
+  SCons :: Sing a -> Sing b -> Sing (a ': b)
+
+data G a where
+  GCons :: G ('Sch (a ': b))
+
+eval :: G s -> Sing s -> ()
+eval GCons s =
+        case s of
+          -- SSch SNil -> undefined
+          SSch (SCons _ _) -> undefined
diff --git a/testsuite/tests/pmcheck/should_compile/T14098.hs b/testsuite/tests/pmcheck/should_compile/T14098.hs
new file mode 100644
index 0000000000..ecb01029eb
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T14098.hs
@@ -0,0 +1,24 @@
+{-# Language GADTs #-}
+module T14098 where
+
+data App f a where
+  App :: f a -> App f (Maybe a)
+
+data Ty a where
+  TBool :: Ty Bool
+  TInt  :: Ty Int
+
+data T f a where
+  C :: T Ty (Maybe Bool)
+
+f1 :: T f a -> App f a -> ()
+f1 C (App TBool) = ()
+
+f2 :: T f a -> App f a -> ()
+f2 C (App x)
+  | TBool <- x
+  = ()
+
+g :: T f a -> App f a -> ()
+g C (App x) = case x of
+                TBool -> ()
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index cabe23950b..db6e7267e0 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -41,8 +41,12 @@ test('T11276', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-pa
 test('T11303b', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
 test('T11374', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
 test('T11195', compile_timeout_multiplier(0.60), compile, ['-package ghc -fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M2G -RTS'])
+test('T11984', normal, compile,
+    ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14086', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T14098', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
 test('pmc001', [], compile,