Fix instantiation of pattern synonyms

In Check.hs (pattern match ovelap checking) we to figure out the
instantiation of a pattern synonym from the type of the pattern. We
were doing this utterly wrongly.  Trac #13768 demonstrated this
bogosity.

The fix is easy; and is described in PatSyn.hs
  Note [Pattern synonym result type]

4 files changed, 89 insertions, 16 deletions

diff --git a/compiler/basicTypes/PatSyn.hs b/compiler/basicTypes/PatSyn.hs
index 0e218a39c1..176bb9f590 100644
--- a/compiler/basicTypes/PatSyn.hs
+++ b/compiler/basicTypes/PatSyn.hs
@@ -63,7 +63,7 @@ data PatSyn
                                        -- record pat syn or same length as
                                        -- psArgs
 
-        -- Universially-quantified type variables
+        -- Universally-quantified type variables
         psUnivTyVars  :: [TyVarBinder],
 
         -- Required dictionaries (may mention psUnivTyVars)
@@ -76,7 +76,8 @@ data PatSyn
         psProvTheta   :: ThetaType,
 
         -- Result type
-        psOrigResTy   :: Type,         -- Mentions only psUnivTyVars
+        psResultTy   :: Type,  -- Mentions only psUnivTyVars
+                                -- See Note [Pattern synonym result type]
 
         -- See Note [Matchers and builders for pattern synonyms]
         psMatcher     :: (Id, Bool),
@@ -145,6 +146,43 @@ Example 3:
    You can see it's existential because it doesn't appear in the
    result type (T3 b).
 
+Note [Pattern synonym result type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   data T a b = MkT b a
+
+   pattern P :: a -> T [a] Bool
+   pattern P x = MkT True [x]
+
+P's psResultTy is (T a Bool), and it really only matches values of
+type (T [a] Bool).  For example, this is ill-typed
+
+   f :: T p q -> String
+   f (P x) = "urk"
+
+This is differnet to the situation with GADTs:
+
+   data S a where
+     MkS :: Int -> S Bool
+
+Now MkS (and pattern synonyms coming from MkS) can match a
+value of type (S a), not just (S Bool); we get type refinement.
+
+That in turn means that if you have a pattern
+
+   P x :: T [ty] Bool
+
+it's not entirely straightforward to work out the instantiation of
+P's universal tyvars. You have to /match/
+  the type of the pattern, (T [ty] Bool)
+against
+  the psResultTy for the pattern synonym, T [a] Bool
+to get the insantiation a := ty.
+
+This is very unlike DataCons, where univ tyvars match 1-1 the
+arguments of the TyCon.
+
+
 Note [Pattern synonym representation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider the following pattern synonym declaration
@@ -174,7 +212,7 @@ In this case, the fields of MkPatSyn will be set as follows:
   psExTyVars   = [b]
   psProvTheta  = (Show (Maybe t), Ord b)
   psReqTheta   = (Eq t, Num t)
-  psOrigResTy  = T (Maybe t)
+  psResultTy  = T (Maybe t)
 
 Note [Matchers and builders for pattern synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -325,7 +363,7 @@ mkPatSyn name declared_infix
                 psInfix = declared_infix,
                 psArgs = orig_args,
                 psArity = length orig_args,
-                psOrigResTy = orig_res_ty,
+                psResultTy = orig_res_ty,
                 psMatcher = matcher,
                 psBuilder = builder,
                 psFieldLabels = field_labels
@@ -368,7 +406,7 @@ patSynExTyVarBinders = psExTyVars
 patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Type], Type)
 patSynSig (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs
                     , psProvTheta = prov, psReqTheta = req
-                    , psArgs = arg_tys, psOrigResTy = res_ty })
+                    , psArgs = arg_tys, psResultTy = res_ty })
   = (binderVars univ_tvs, req, binderVars ex_tvs, prov, arg_tys, res_ty)
 
 patSynMatcher :: PatSyn -> (Id,Bool)
@@ -405,9 +443,9 @@ patSynInstResTy :: PatSyn -> [Type] -> Type
 -- E.g.  pattern P x y = Just (x,x,y)
 --         P :: a -> b -> Just (a,a,b)
 --         (patSynInstResTy P [Int,Bool] = Maybe (Int,Int,Bool)
--- NB: unlikepatSynInstArgTys, the inst_tys should be just the *universal* tyvars
+-- NB: unlike patSynInstArgTys, the inst_tys should be just the *universal* tyvars
 patSynInstResTy (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
-                          , psOrigResTy = res_ty })
+                          , psResultTy = res_ty })
                 inst_tys
   = ASSERT2( univ_tvs `equalLength` inst_tys
            , text "patSynInstResTy" <+> ppr name $$ ppr univ_tvs $$ ppr inst_tys )
@@ -417,7 +455,7 @@ patSynInstResTy (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
 pprPatSynType :: PatSyn -> SDoc
 pprPatSynType (MkPatSyn { psUnivTyVars = univ_tvs,  psReqTheta  = req_theta
                         , psExTyVars   = ex_tvs,    psProvTheta = prov_theta
-                        , psArgs       = orig_args, psOrigResTy = orig_res_ty })
+                        , psArgs       = orig_args, psResultTy = orig_res_ty })
   = sep [ pprForAll univ_tvs
         , pprThetaArrowTy req_theta
         , ppWhen insert_empty_ctxt $ parens empty <+> darrow
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index cb9837ed0c..ce114e727b 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -18,7 +18,7 @@ module Check (
 #include "HsVersions.h"
 
 import TmOracle
-
+import Unify( tcMatchTy )
 import BasicTypes
 import DynFlags
 import HsSyn
@@ -45,6 +45,7 @@ import Var           (EvVar)
 import Type
 import UniqSupply
 import DsGRHSs       (isTrueLHsExpr)
+import Maybes        ( expectJust )
 
 import Data.List     (find)
 import Data.Maybe    (isJust, fromMaybe)
@@ -971,14 +972,14 @@ mkOneConFull :: Id -> ConLike -> DsM (ValAbs, ComplexEq, Bag EvVar)
 --          ComplexEq:       x ~ K y1..yn
 --          [EvVar]:         Q
 mkOneConFull x con = do
-  let -- res_ty == TyConApp (ConLikeTyCon cabs_con) cabs_arg_tys
-      res_ty  = idType x
-      (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, _)
+  let res_ty  = idType x
+      (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, con_res_ty)
         = conLikeFullSig con
-      tc_args = case splitTyConApp_maybe res_ty of
-                  Just (_, tys) -> tys
-                  Nothing -> pprPanic "mkOneConFull: Not TyConApp:" (ppr res_ty)
-      subst1  = zipTvSubst univ_tvs tc_args
+      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
 
   (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM
 
diff --git a/testsuite/tests/patsyn/should_compile/T13768.hs b/testsuite/tests/patsyn/should_compile/T13768.hs
new file mode 100644
index 0000000000..c4510bd20a
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13768.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+module T13768 where
+
+data NS (f :: k -> *) (xs :: [k]) = NS Int
+
+data IsNS (f :: k -> *) (xs :: [k]) where
+  IsZ :: f x -> IsNS f (x ': xs)
+  IsS :: NS f xs -> IsNS f (x ': xs)
+
+isNS :: NS f xs -> IsNS f xs
+isNS = undefined
+
+pattern Z :: () => (xs' ~ (x ': xs)) => f x -> NS f xs'
+pattern Z x <- (isNS -> IsZ x)
+
+pattern S :: () => (xs' ~ (x ': xs)) => NS f xs -> NS f xs'
+pattern S p <- (isNS -> IsS p)
+
+{-# COMPLETE Z, S #-}
+
+data SList :: [k] -> * where
+  SNil  :: SList '[]
+  SCons :: SList (x ': xs)
+
+go :: SList ys -> NS f ys -> Int
+go SCons (Z _) = 0
+go SCons (S _) = 1
+go SNil  _     = error "inaccessible"
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 30319c7050..286f735ac6 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -70,3 +70,4 @@ test('T13441b', normal, compile_fail, [''])
 test('T13454', normal, compile, [''])
 test('T13752', normal, compile, [''])
 test('T13752a', normal, compile, [''])
+test('T13768', normal, compile, [''])