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

3 files changed, 51 insertions, 0 deletions

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,