Check for uninferrable variables in tcInferPatSynDeclwip/T21479

This fixes #21479

See Note [Unquantified tyvars in a pattern synonym]

While doing this, I found that some error messages pointed at the
pattern synonym /name/, rather than the /declaration/ so I widened the
SrcSpan to encompass the declaration.

12 files changed, 88 insertions, 43 deletions

diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 4c5fa5aaa8..14f7bbf6b5 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -429,9 +429,9 @@ tc_single :: forall thing.
           -> LHsBind GhcRn -> IsGroupClosed -> TcM thing
           -> TcM (LHsBinds GhcTc, thing)
 tc_single _top_lvl sig_fn prag_fn
-          (L _ (PatSynBind _ psb@PSB{ psb_id = L _ name }))
+          (L loc (PatSynBind _ psb))
           _ thing_inside
-  = do { (aux_binds, tcg_env) <- tcPatSynDecl psb (sig_fn name) prag_fn
+  = do { (aux_binds, tcg_env) <- tcPatSynDecl (L loc psb) sig_fn prag_fn
        ; thing <- setGblEnv tcg_env thing_inside
        ; return (aux_binds, thing)
        }
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index ce3025bafa..45810f5d9f 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -76,13 +76,16 @@ import Data.List( partition, mapAccumL )
 ************************************************************************
 -}
 
-tcPatSynDecl :: PatSynBind GhcRn GhcRn
-             -> Maybe TcSigInfo
+tcPatSynDecl :: LocatedA (PatSynBind GhcRn GhcRn)
+             -> TcSigFun
              -> TcPragEnv -- See Note [Pragmas for pattern synonyms]
              -> TcM (LHsBinds GhcTc, TcGblEnv)
-tcPatSynDecl psb mb_sig prag_fn
-  = recoverM (recoverPSB psb) $
-    case mb_sig of
+tcPatSynDecl (L loc psb@(PSB { psb_id = L _ name })) sig_fn prag_fn
+  = setSrcSpanA loc $
+    addErrCtxt (text "In the declaration for pattern synonym"
+                <+> quotes (ppr name)) $
+    recoverM (recoverPSB psb) $
+    case (sig_fn name) of
       Nothing                 -> tcInferPatSynDecl psb prag_fn
       Just (TcPatSynSig tpsi) -> tcCheckPatSynDecl psb tpsi prag_fn
       _                       -> panic "tcPatSynDecl"
@@ -145,8 +148,7 @@ tcInferPatSynDecl :: PatSynBind GhcRn GhcRn
 tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
                        , psb_def = lpat, psb_dir = dir })
                   prag_fn
-  = addPatSynCtxt lname $
-    do { traceTc "tcInferPatSynDecl {" $ ppr name
+  = do { traceTc "tcInferPatSynDecl {" $ ppr name
 
        ; let (arg_names, is_infix) = collectPatSynArgInfo details
        ; (tclvl, wanted, ((lpat', args), pat_ty))
@@ -188,6 +190,16 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
                               , not (isEmptyDVarSet bad_cos) ]
        ; mapM_ dependentArgErr bad_args
 
+       -- Report un-quantifiable type variables:
+       -- see Note [Unquantified tyvars in a pattern synonym]
+       ; dvs <- candidateQTyVarsOfTypes prov_theta
+       ; let mk_doc tidy_env
+               = do { (tidy_env2, theta) <- zonkTidyTcTypes tidy_env prov_theta
+                    ; return ( tidy_env2
+                             , sep [ text "the provided context:"
+                                   , pprTheta theta ] ) }
+       ; doNotQuantifyTyVars dvs mk_doc
+
        ; traceTc "tcInferPatSynDecl }" $ (ppr name $$ ppr ex_tvs)
        ; rec_fields <- lookupConstructorFields name
        ; tc_patsyn_finish lname dir is_infix lpat' prag_fn
@@ -345,6 +357,27 @@ But we simply don't allow that in types.  Maybe one day but not now.
 How to detect this situation?  We just look for free coercion variables
 in the types of any of the arguments to the matcher.  The error message
 is not very helpful, but at least we don't get a Lint error.
+
+Note [Unquantified tyvars in a pattern synonym]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#21479)
+
+   data T a where MkT :: Int -> T Char   -- A GADT
+   foo :: forall b. Bool -> T b          -- Somewhat strange type
+
+   pattern T1 <- (foo -> MkT)
+
+In the view pattern, foo is instantiated, let's say b :-> b0
+where b0 is a unification variable.  Then matching the GADT
+MkT will add the "provided" constraint b0~Char, so we might infer
+   pattern T1 :: () => (b0~Char) => Int -> Bool
+
+Nothing constrains that `b0`. We don't want to quantify over it.
+We don't want to to zonk to Any (we don't like Any showing up in
+user-visible types).  So we want to error here. See
+Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
+
+Hence the call to doNotQuantifyTyVars here.
 -}
 
 tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
@@ -358,8 +391,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
                       , patsig_ex_bndrs   = explicit_ex_bndrs,   patsig_prov = prov_theta
                       , patsig_body_ty    = sig_body_ty }
                   prag_fn
-  = addPatSynCtxt lname $
-    do { traceTc "tcCheckPatSynDecl" $
+  = do { traceTc "tcCheckPatSynDecl" $
          vcat [ ppr implicit_bndrs, ppr explicit_univ_bndrs, ppr req_theta
               , ppr explicit_ex_bndrs, ppr prov_theta, ppr sig_body_ty ]
 
@@ -646,13 +678,6 @@ collectPatSynArgInfo details =
     InfixCon name1 name2 -> (map unLoc [name1, name2], True)
     RecCon names         -> (map (unLoc . recordPatSynPatVar) names, False)
 
-addPatSynCtxt :: LocatedN Name -> TcM a -> TcM a
-addPatSynCtxt (L loc name) thing_inside
-  = setSrcSpanA loc $
-    addErrCtxt (text "In the declaration for pattern synonym"
-                <+> quotes (ppr name)) $
-    thing_inside
-
 wrongNumberOfParmsErr :: Name -> Arity -> Arity -> TcM a
 wrongNumberOfParmsErr name decl_arity missing
   = failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs-boot b/compiler/GHC/Tc/TyCl/PatSyn.hs-boot
index 844a4c394d..5a16a55cd7 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs-boot
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs-boot
@@ -1,14 +1,14 @@
 module GHC.Tc.TyCl.PatSyn where
 
 import GHC.Hs    ( PatSynBind, LHsBinds )
-import GHC.Tc.Types ( TcM, TcSigInfo )
+import GHC.Tc.Types ( TcM )
 import GHC.Tc.Utils.Monad ( TcGblEnv)
 import GHC.Hs.Extension ( GhcRn, GhcTc )
-import Data.Maybe  ( Maybe )
-import GHC.Tc.Gen.Sig ( TcPragEnv )
+import GHC.Tc.Gen.Sig ( TcPragEnv, TcSigFun )
+import GHC.Parser.Annotation( LocatedA )
 
-tcPatSynDecl :: PatSynBind GhcRn GhcRn
-             -> Maybe TcSigInfo
+tcPatSynDecl :: LocatedA (PatSynBind GhcRn GhcRn)
+             -> TcSigFun
              -> TcPragEnv
              -> TcM (LHsBinds GhcTc, TcGblEnv)
 
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 21954240d6..5561e9064e 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1947,35 +1947,34 @@ skolemiseUnboundMetaTyVar skol_info tv
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
 
-  type C :: Type -> Type -> Constraint
+* type C :: Type -> Type -> Constraint
   class (forall a. a b ~ a c) => C b c
 
-or
+* type T = forall a. Proxy a
 
-  type T = forall a. Proxy a
+* data (forall a. a b ~ a c) => T b c
 
-or
+* type instance F Int = Proxy Any
+  where Any :: forall k. k
 
-  data (forall a. a b ~ a c) => T b c
-
-We will infer a :: Type -> kappa... but then we get no further information
-on kappa. What to do?
+In the first three cases we will infer a :: Type -> kappa, but then
+we get no further information on kappa. In the last, we will get
+  Proxy kappa Any
+but again will get no further info on kappa.
 
+What do do?
  A. We could choose kappa := Type. But this only works when the kind of kappa
     is Type (true in this example, but not always).
  B. We could default to Any.
  C. We could quantify.
  D. We could error.
 
-We choose (D), as described in #17567. Discussion of alternatives is below.
+We choose (D), as described in #17567, and implement this choice in
+doNotQuantifyTyVars.  Dicsussion of alternativs A-C is below.
 
 NB: this is all rather similar to, but sadly not the same as
     Note [Naughty quantification candidates]
 
-(One last example: type instance F Int = Proxy Any, where the unconstrained
-kind variable is the inferred kind of Any. The four examples here illustrate
-all cases in which this Note applies.)
-
 To do this, we must take an extra step before doing the final zonk to create
 e.g. a TyCon. (There is no problem in the final term-level zonk. See the
 section on alternative (B) below.) This extra step is needed only for
@@ -1990,7 +1989,7 @@ RuntimeRep and Multiplicity variables.)
 Because no meta-variables remain after quantifying or erroring, we perform
 the zonk with NoFlexi, which panics upon seeing a meta-variable.
 
-Alternatives not implemented:
+Alternatives A-C, not implemented:
 
 A. As stated above, this works only sometimes. We might have a free
    meta-variable of kind Nat, for example.
@@ -2067,7 +2066,9 @@ doNotQuantifyTyVars dvs where_found
        ; unless (null leftover_metas) $
          do { let (tidy_env1, tidied_tvs) = tidyOpenTyCoVars emptyTidyEnv leftover_metas
             ; (tidy_env2, where_doc) <- where_found tidy_env1
-            ; let msg = TcRnUnknownMessage $ mkPlainError noHints $ pprWithExplicitKindsWhen True $
+            ; let msg = TcRnUnknownMessage            $
+                        mkPlainError noHints          $
+                        pprWithExplicitKindsWhen True $
                     vcat [ text "Uninferrable type variable"
                            <> plural tidied_tvs
                            <+> pprWithCommas pprTyVar tidied_tvs
diff --git a/testsuite/tests/linear/should_fail/LinearPatSyn2.stderr b/testsuite/tests/linear/should_fail/LinearPatSyn2.stderr
index 1360983907..78b3ee52f6 100644
--- a/testsuite/tests/linear/should_fail/LinearPatSyn2.stderr
+++ b/testsuite/tests/linear/should_fail/LinearPatSyn2.stderr
@@ -1,5 +1,5 @@
 
-LinearPatSyn2.hs:6:9: error:
+LinearPatSyn2.hs:6:1: error:
     • Pattern synonyms do not support linear fields (GHC #18806):
         x %1 -> Maybe x
     • In the declaration for pattern synonym ‘J’
diff --git a/testsuite/tests/patsyn/should_fail/T11667.stderr b/testsuite/tests/patsyn/should_fail/T11667.stderr
index f4dafc0f28..e08299b235 100644
--- a/testsuite/tests/patsyn/should_fail/T11667.stderr
+++ b/testsuite/tests/patsyn/should_fail/T11667.stderr
@@ -3,7 +3,7 @@ T11667.hs:12:22: error:
     • Could not deduce (Num a) arising from the literal ‘42’
       from the context: Eq a
         bound by the signature for pattern synonym ‘Pat1’
-        at T11667.hs:12:9-12
+        at T11667.hs:12:1-23
       Possible fix:
         add (Num a) to the "required" context of
           the signature for pattern synonym ‘Pat1’
diff --git a/testsuite/tests/patsyn/should_fail/T14507.stderr b/testsuite/tests/patsyn/should_fail/T14507.stderr
index beeb4de685..d3dfa0a04f 100644
--- a/testsuite/tests/patsyn/should_fail/T14507.stderr
+++ b/testsuite/tests/patsyn/should_fail/T14507.stderr
@@ -1,5 +1,5 @@
 
-T14507.hs:21:9: error:
+T14507.hs:21:1: error:
     • Iceland Jack!  Iceland Jack! Stop torturing me!
       Pattern-bound variable x :: TypeRep a
         has a type that mentions pattern-bound coercion: co
diff --git a/testsuite/tests/patsyn/should_fail/T14552.stderr b/testsuite/tests/patsyn/should_fail/T14552.stderr
index 34ee266cdd..92c1adb57b 100644
--- a/testsuite/tests/patsyn/should_fail/T14552.stderr
+++ b/testsuite/tests/patsyn/should_fail/T14552.stderr
@@ -1,5 +1,5 @@
 
-T14552.hs:22:9: error:
+T14552.hs:22:1: error:
     • Cannot generalise type; skolem ‘k’ would escape its scope
       if I tried to quantify (t0 :: k) in this type:
         forall k (w :: k --> *). Exp a0 (F @k @(*) w t0)
diff --git a/testsuite/tests/patsyn/should_fail/T15685.stderr b/testsuite/tests/patsyn/should_fail/T15685.stderr
index afc6d45de4..204260a9e4 100644
--- a/testsuite/tests/patsyn/should_fail/T15685.stderr
+++ b/testsuite/tests/patsyn/should_fail/T15685.stderr
@@ -9,7 +9,7 @@ T15685.hs:13:24: error:
         at T15685.hs:13:19-26
       ‘k’ is a rigid type variable bound by
         the inferred type of HereNil :: NS f as
-        at T15685.hs:13:9-15
+        at T15685.hs:13:1-26
     • In the pattern: Nil
       In the pattern: Here Nil
       In the declaration for pattern synonym ‘HereNil’
diff --git a/testsuite/tests/patsyn/should_fail/T21479.hs b/testsuite/tests/patsyn/should_fail/T21479.hs
new file mode 100644
index 0000000000..889e811e88
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T21479.hs
@@ -0,0 +1,13 @@
+{-# Language PatternSynonyms #-}
+{-# Language ViewPatterns #-}
+{-# Language GADTs #-}
+
+module T21479 where
+
+data T a where
+  MkT :: T Int
+
+foo :: () -> T a
+foo = foo
+
+pattern T1 <- (foo -> MkT)
\ No newline at end of file
diff --git a/testsuite/tests/patsyn/should_fail/T21479.stderr b/testsuite/tests/patsyn/should_fail/T21479.stderr
new file mode 100644
index 0000000000..07601492a8
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T21479.stderr
@@ -0,0 +1,5 @@
+
+T21479.hs:13:1: error:
+    • Uninferrable type variable a0 in
+      the provided context: (a0 :: *) ~ (Int :: *)
+    • In the declaration for pattern synonym ‘T1’
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 8993e5c4bf..2db852a35b 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -48,3 +48,4 @@ test('T15694', normal, compile_fail, [''])
 test('T16900', normal, compile_fail, ['-fdiagnostics-show-caret'])
 test('T14552', normal, compile_fail, [''])
 test('T18856', normal, compile_fail, ['-fdiagnostics-show-caret'])
+test('T21479', normal, compile_fail, [''])