Fix deep, dark corner of pattern synonyms

Trac #14552 showed a very obscure case where we can't infer a
good pattern-synonym type.

The error message is horrible, but at least we no longer crash
and burn.

4 files changed, 103 insertions, 0 deletions

diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 7e21af5faa..0086a83367 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -91,6 +91,12 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
              univ_tvs   = filterOut (`elemVarSet` ex_tv_set) qtvs
              req_theta  = map evVarPred req_dicts
 
+       -- 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
+
        ; prov_dicts <- mapM zonkId prov_dicts
        ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
              prov_theta = map evVarPred filtered_prov_dicts
@@ -105,6 +111,19 @@ 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
+  = addErrTc $
+    vcat [ text "Universal type variable" <+> quotes (ppr bad_tv)
+                <+> text "has existentially bound kind:"
+         , nest 2 (ppr_with_kind bad_tv)
+         , hang (text "Existentially-bound variables:")
+              2 (vcat (map ppr_with_kind ex_tvs))
+         , text "Probable fix: give the pattern synoym a type signature"
+         ]
+  where
+    ppr_with_kind tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
+
 {- Note [Remove redundant provided dicts]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Recall that
@@ -126,6 +145,37 @@ Similarly consider
 
 The pattern (Bam x y) binds two (Ord a) dictionaries, but we only
 need one.  Agian mkMimimalWithSCs removes the redundant one.
+
+Note [Type variables whose kind is captured]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  data AST a = Sym [a]
+  class Prj s where { prj :: [a] -> Maybe (s a)
+  pattern P x <= Sym (prj -> Just x)
+
+Here we get a matcher with this type
+  $mP :: forall s a. Prj s => AST a -> (s a -> r) -> r -> r
+
+No problem.  But note that 's' is not fixed by the type of the
+pattern (AST a), nor is it existentially bound.  It's really only
+fixed by the type of the continuation.
+
+Trac #14552 showed that this can go wrong if the kind of 's' mentions
+existentially bound variables.  We obviously can't make a type like
+  $mP :: forall (s::k->*) a. Prj s => AST a -> (forall k. s a -> r)
+                                   -> r -> r
+But neither is 's' itself existentially bound, so the forall (s::k->*)
+can't go in the inner forall either.  (What would the matcher apply
+the continuation to?)
+
+So we just fail in this case, with a pretty terrible error message.
+Maybe we could do better, but I can't see how.  (It'd be possible to
+default 's' to (Any k), but that probably isn't what the user wanted,
+and it not straightforward to implement, because by the time we see
+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.
 -}
 
 tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
diff --git a/testsuite/tests/patsyn/should_fail/T14552.hs b/testsuite/tests/patsyn/should_fail/T14552.hs
new file mode 100644
index 0000000000..77f08575b1
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14552.hs
@@ -0,0 +1,43 @@
+{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, ScopedTypeVariables,
+             KindSignatures, PolyKinds, DataKinds, TypeFamilies, TypeInType, GADTs #-}
+
+module T14552 where
+
+import Data.Kind
+import Data.Proxy
+
+data family Sing a
+
+type a --> b = (a, b) -> Type
+
+type family F (f::a --> b) (x::a) :: b
+
+newtype Limit :: (k --> Type) -> Type where
+  Limit :: (forall xx. Proxy xx -> F f xx) -> Limit f
+
+data Exp :: [Type] -> Type -> Type where
+  TLam :: (forall aa. Proxy aa -> Exp xs (F w aa))
+        -> Exp xs (Limit w)
+
+pattern FOO f <- TLam (($ Proxy) -> f)
+
+
+{-
+TLam :: forall (xs::[Type]) (b::Type).   -- Universal
+         forall k (w :: k --> Type).      -- Existential
+         (b ~ Limit w) =>
+         => (forall (aa :: k). Proxy aa -> Exp xs (F w aa))
+         -> Exp xs b
+
+-}
+
+{-
+mfoo :: Exp xs b
+     -> (forall k (w :: k --> Type).
+         (b ~ Limit w)
+         => Exp xs (F w aa)
+         -> r)
+     -> r
+mfoo scrut k = case srcut of
+                 TLam g -> k (g Proxy)
+-}
diff --git a/testsuite/tests/patsyn/should_fail/T14552.stderr b/testsuite/tests/patsyn/should_fail/T14552.stderr
new file mode 100644
index 0000000000..1ead6443b4
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14552.stderr
@@ -0,0 +1,9 @@
+
+T14552.hs:22:9: error:
+    • Universal type variable ‘aa’ has existentially bound kind:
+        aa :: k
+      Existentially-bound variables:
+        k :: *
+        w :: k --> *
+      Probable fix: give the pattern synoym a type signature
+    • In the declaration for pattern synonym ‘FOO’
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 4bf631f982..d2985d5e14 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -40,3 +40,4 @@ test('T14112', normal, compile_fail, [''])
 test('T14114', normal, compile_fail, [''])
 test('T14380', normal, compile_fail, [''])
 test('T14498', normal, compile_fail, [''])
+test('T14552', normal, compile_fail, [''])