Fix another obscure pattern-synonym crash

This one, discovered by Iceland Jack (Trac #14507), shows
that a pattern-bound coercion can show up in the argument
type(s) of the matcher of a pattern synonym.

The error message isn't great, but at least we now rightly
reject the program.

4 files changed, 90 insertions, 7 deletions

diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 0086a83367..b89c4bed63 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -91,16 +91,26 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
              univ_tvs   = filterOut (`elemVarSet` ex_tv_set) qtvs
              req_theta  = map evVarPred req_dicts
 
+       ; prov_dicts <- mapM zonkId prov_dicts
+       ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
+             prov_theta = map evVarPred filtered_prov_dicts
+             -- Filtering: see Note [Remove redundant provided dicts]
+
+       -- Report bad universal type variables
        -- See Note [Type variables whose kind is captured]
        ; let bad_tvs    = [ tv | tv <- univ_tvs
                                , tyCoVarsOfType (tyVarKind tv)
                                  `intersectsVarSet` ex_tv_set ]
-       ; mapM_ (badUnivTv ex_tvs) bad_tvs
+       ; mapM_ (badUnivTvErr ex_tvs) bad_tvs
 
-       ; prov_dicts <- mapM zonkId prov_dicts
-       ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
-             prov_theta = map evVarPred filtered_prov_dicts
-             -- Filtering: see Note [Remove redundant provided dicts]
+       -- Report coercions that esacpe
+       -- See Note [Coercions that escape]
+       ; args <- mapM zonkId args
+       ; let bad_args = [ (arg, bad_cos) | arg <- args ++ prov_dicts
+                              , let bad_cos = filterDVarSet isId $
+                                              (tyCoVarsOfTypeDSet (idType arg))
+                              , not (isEmptyDVarSet bad_cos) ]
+       ; mapM_ dependentArgErr bad_args
 
        ; traceTc "tcInferPatSynDecl }" $ (ppr name $$ ppr ex_tvs)
        ; tc_patsyn_finish lname dir is_infix lpat'
@@ -111,8 +121,9 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
                           (map nlHsVar args, map idType args)
                           pat_ty rec_fields }
 
-badUnivTv :: [TyVar] -> TyVar -> TcM ()
-badUnivTv ex_tvs bad_tv
+badUnivTvErr :: [TyVar] -> TyVar -> TcM ()
+-- See Note [Type variables whose kind is captured]
+badUnivTvErr ex_tvs bad_tv
   = addErrTc $
     vcat [ text "Universal type variable" <+> quotes (ppr bad_tv)
                 <+> text "has existentially bound kind:"
@@ -124,6 +135,22 @@ badUnivTv ex_tvs bad_tv
   where
     ppr_with_kind tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
 
+dependentArgErr :: (Id, DTyCoVarSet) -> TcM ()
+-- See Note [Coercions that escape]
+dependentArgErr (arg, bad_cos)
+  = addErrTc $
+    vcat [ text "Iceland Jack!  Iceland Jack! Stop torturing me!"
+         , hang (text "Pattern-bound variable")
+              2 (ppr arg <+> dcolon <+> ppr (idType arg))
+         , nest 2 $
+           hang (text "has a type that mentions pattern-bound coercion"
+                 <> plural bad_co_list <> colon)
+              2 (pprWithCommas ppr bad_co_list)
+         , text "Hint: use -fprint-explicit-coercions to see the coercions"
+         , text "Probable fix: add a pattern signature" ]
+  where
+    bad_co_list = dVarSetElems bad_cos
+
 {- Note [Remove redundant provided dicts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Recall that
@@ -176,6 +203,34 @@ the problem, simplifyInfer has already skolemised 's'.)
 
 This stuff can only happen in the presence of view patterns, with
 TypeInType, so it's a bit of a corner case.
+
+Note [Coercions that escape]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Trac #14507 showed an example where the inferred type of the matcher
+for the pattern synonym was somethign like
+   $mSO :: forall (r :: TYPE rep) kk (a :: k).
+           TypeRep k a
+           -> ((Bool ~ k) => TypeRep Bool (a |> co_a2sv) -> r)
+           -> (Void# -> r)
+           -> r
+
+What is that co_a2sv :: Bool ~# *??  It was bound (via a superclass
+selection) by the pattern being matched; and indeed it is implicit in
+the context (Bool ~ k).  You could imagine trying to extract it like
+this:
+   $mSO :: forall (r :: TYPE rep) kk (a :: k).
+           TypeRep k a
+           -> ( co :: ((Bool :: *) ~ (k :: *)) =>
+                  let co_a2sv = sc_sel co
+                  in TypeRep Bool (a |> co_a2sv) -> r)
+           -> (Void# -> r)
+           -> r
+
+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.
 -}
 
 tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
diff --git a/testsuite/tests/patsyn/should_fail/T14507.hs b/testsuite/tests/patsyn/should_fail/T14507.hs
new file mode 100644
index 0000000000..84166d0286
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14507.hs
@@ -0,0 +1,19 @@
+{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies #-}
+
+module T14507 where
+
+import Type.Reflection
+import Data.Kind
+
+foo :: TypeRep a -> (Bool :~~: k, TypeRep a)
+foo rep = error "urk"
+
+type family SING :: k -> Type where
+  SING = (TypeRep :: Bool -> Type)
+
+pattern RepN :: forall (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk)
+pattern RepN tr <- (foo -> ( HRefl :: Bool:~~:kk
+                           , tr :: TypeRep (a::Bool)))
+
+pattern SO x <- RepN (id -> x)
+
diff --git a/testsuite/tests/patsyn/should_fail/T14507.stderr b/testsuite/tests/patsyn/should_fail/T14507.stderr
new file mode 100644
index 0000000000..2ed89cbac6
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14507.stderr
@@ -0,0 +1,8 @@
+
+T14507.hs:18:9: error:
+    • Iceland Jack!  Iceland Jack! Stop torturing me!
+      Pattern-bound variable x :: TypeRep a
+        has a type that mentions pattern-bound coercion: co_a2CF
+      Hint: use -fprint-explicit-coercions to see the coercions
+      Probable fix: add a pattern signature
+    • In the declaration for pattern synonym ‘SO’
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index d2985d5e14..2b3b85bf28 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -41,3 +41,4 @@ test('T14114', normal, compile_fail, [''])
 test('T14380', normal, compile_fail, [''])
 test('T14498', normal, compile_fail, [''])
 test('T14552', normal, compile_fail, [''])
+test('T14507', normal, compile_fail, [''])