Fix #17112wip/fix-T17112

The `mkOneConFull` function of the pattern match checker used to try to
guess the type arguments of the data type's type constructor by looking
at the ambient type of the match. This doesn't work well for Pattern
Synonyms, where the result type isn't even necessarily a TyCon
application, and it shows in #11336 and #17112.

Also the effort seems futile; why try to try hard when the type checker
has already done the hard lifting? After this patch, we instead supply
the type constructors arguments as an argument to the function and
lean on the type-annotated AST.

3 files changed, 54 insertions, 27 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 4a5d978..602c125 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -56,7 +56,6 @@ import TyCoRep
 import Type
 import UniqSupply
 import DsUtils       (isTrueLHsExpr)
-import Maybes        (expectJust)
 import qualified GHC.LanguageExtensions as LangExt
 
 import Data.List     (find)
@@ -853,7 +852,7 @@ inhabitationCandidates ty_cs ty = do
     alts_to_check :: Type -> Type -> [DataCon]
                   -> PmM (Either Type (TyCon, [InhabitationCandidate]))
     alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of
-      Just (tc, _)
+      Just (tc, tc_args)
         |  tc `elem` trivially_inhabited
         -> case dcs of
              []    -> return (Left src_ty)
@@ -869,7 +868,7 @@ inhabitationCandidates ty_cs ty = do
            -- them extremely misleading.
         -> liftD $ do
              var  <- mkPmId core_ty -- it would be wrong to unify x
-             alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
+             alts <- mapM (mkOneConFull var tc_args . RealDataCon) (tyConDataCons tc)
              return $ Right
                (tc, [ alt{ic_val_abs = build_tm (ic_val_abs alt) dcs}
                     | alt <- alts ])
@@ -1616,37 +1615,31 @@ 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
---  *  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
---       leads to
---            data TPair a b = T1 a b  -- The "representation" type
---       It is TPair, not T, that is given to mkOneConFull
+mkOneConFull :: Id -> [Type] -> ConLike -> DsM InhabitationCandidate
+--  * 'con' K is a conlike of algebraic data type 'T tys'
+
+--  * 'tc_args' are the type arguments of the 'con's TyCon T
 --
---  * 'con' K is a conlike of data type T
+--  *  'x' is the variable for which we encode an equality constraint
+--     in the term oracle
 --
--- After instantiating the universal tyvars of K we get
---          K tys :: forall bs. Q => s1 .. sn -> T tys
+-- After instantiating the universal tyvars of K to tc_args we get
+--          K @tys :: forall bs. Q => s1 .. sn -> T tys
 --
 -- Suppose y1 is a strict field. Then we get
 -- Results: ic_val_abs:        K (y1::s1) .. (yn::sn)
 --          ic_tm_ct:          x ~ K y1..yn
 --          ic_ty_cs:          Q
 --          ic_strict_arg_tys: [s1]
-mkOneConFull x con = do
-  let res_ty  = idType x
-      (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, con_res_ty)
+mkOneConFull x tc_args con = do
+  let (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, _con_res_ty)
         = conLikeFullSig con
       arg_is_banged = map isBanged $ conLikeImplBangs con
-      tc_args = tyConAppArgs res_ty
-      subst1  = case con of
-                  RealDataCon {} -> zipTvSubst univ_tvs tc_args
-                  PatSynCon {}   -> expectJust "mkOneConFull" (tcMatchTy con_res_ty res_ty)
-                                    -- See Note [Pattern synonym result type] in PatSyn
+      subst1  = zipTvSubst univ_tvs tc_args
 
   (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM
 
+  -- Field types
   let arg_tys' = substTys subst arg_tys
   -- Fresh term variables (VAs) as arguments to the constructor
   arguments <-  mapM mkPmVar arg_tys'
@@ -2094,7 +2087,7 @@ pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
           (PmVar x) (ValVec vva delta) = do
   (prov, complete_match) <- select =<< liftD (allCompleteMatches con tys)
 
-  cons_cs <- mapM (liftD . mkOneConFull x) complete_match
+  cons_cs <- mapM (liftD . mkOneConFull x tys) complete_match
 
   inst_vsa <- flip mapMaybeM cons_cs $
       \InhabitationCandidate{ ic_val_abs = va, ic_tm_ct = tm_ct
@@ -2201,11 +2194,11 @@ Where:
   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.
+K as well as a list of type arguments [t_1, ..., t_n] to substitute T's
+universally quantified type variables u_1, ..., u_n for. It's crucial to take
+these in as arguments, as it is non-trivial to derive them just from the result
+type of a pattern synonym and the ambient type of the match (#11336, #17112).
+The type checker already did the hard work, so we should just make use of it.
 
 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,
diff --git a/testsuite/tests/pmcheck/should_compile/T17112.hs b/testsuite/tests/pmcheck/should_compile/T17112.hs
new file mode 100644
index 0000000..a6755f7
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17112.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+
+import Data.Functor.Identity
+
+data HideArg f where
+  HideArg :: f a -> HideArg f
+
+data family App :: tF -> tF
+data instance App f x = App1 (f x)
+
+class WrappedIn s a | s -> a where
+  unwrap :: s -> a
+
+instance WrappedIn (App f a) (f a) where
+  unwrap (App1 fa) = fa
+
+pattern Unwrapped :: WrappedIn s a => a -> s
+pattern Unwrapped x <- (unwrap -> x)
+{-# COMPLETE Unwrapped :: App #-}
+
+boom :: HideArg (App Identity) -> Bool
+boom (HideArg (Unwrapped (Identity _))) = True
+
+main :: IO ()
+main = print ":("
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 5fe7d9e..87874f8 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -76,6 +76,8 @@ test('T15884', expect_broken(15884), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T16289', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17112', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
 test('pmc001', [], compile,