Check for unconstrained superclass kind varswip/t17562

See Note [Unquantifiable kind variables] in TcTyClsDecls.

The actual fix for this is relatively short. Getting a good
error message printed takes much more code!

test cases: typecheck/should_compile/T17562
            typecheck/should_fail/T17562b

Closes #17562.

8 files changed, 107 insertions, 13 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 5635b2d7b7..cc46d9fc59 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -269,6 +269,7 @@ tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
 -- No validity checking or zonking
 -- Returns also a Bool indicating whether the type induced an insoluble constraint;
 -- True <=> constraint is insoluble
+-- See Note [Recipe for checking a signature]
 tc_hs_sig_type skol_info hs_sig_type ctxt_kind
   | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
   = do { (tc_lvl, (wanted, (spec_tkvs, ty)))
@@ -388,7 +389,7 @@ tcHsClsInstType user_ctxt hs_inst_ty
 ----------------------------------------------
 -- | Type-check a visible type application
 tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
--- See Note [Recipe for checking a signature] in TcHsType
+-- See Note [Recipe for checking a signature]
 tcHsTypeApp wc_ty kind
   | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
   = do { ty <- solveLocalEqualities "tcHsTypeApp" $
@@ -1746,8 +1747,10 @@ Note [Recipe for checking a signature]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Checking a user-written signature requires several steps:
 
- 1. Generate constraints.
- 2. Solve constraints.
+ With a bumped TcLevel {
+   1. Generate constraints.
+   2. Solve constraints.
+ }
  3. Promote tyvars and/or kind-generalize.
  4. Zonk.
  5. Check validity.
@@ -1761,11 +1764,11 @@ order: Implicit]). Additionally, solving is necessary in order to
 kind-generalize correctly: otherwise, we do not know which metavariables
 are left unsolved.
 
-Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to
-kindGeneralize{All,Some,None}. Here, we have to deal with the fact that
-metatyvars generated in the type may have a bumped TcLevel, because explicit
-foralls raise the TcLevel. To avoid these variables from ever being visible in
-the surrounding context, we must obey the following dictum:
+Step 3 is done by a call to kindGeneralize{All,Some,None}. Here, we have to
+deal with the fact that metatyvars generated in the type may have a bumped
+TcLevel, because explicit foralls raise the TcLevel. To avoid these variables
+from ever being visible in the surrounding context, we must obey the following
+dictum:
 
   Every metavariable in a type must either be
     (A) generalized, or
@@ -1775,9 +1778,9 @@ the surrounding context, we must obey the following dictum:
 The kindGeneralize functions do not require pre-zonking; they zonk as they
 go.
 
-If you are actually doing kind-generalization, you need to bump the level
-before generating constraints, as we will only generalize variables with
-a TcLevel higher than the ambient one.
+If you use kindGeneralizeNone, you can skip bumping the level in the recipe
+above. Only variables with a bumped level are generalized, so it's necessary
+to bump the level in other cases.
 
 After promoting/generalizing, we need to zonk again because both
 promoting and generalizing fill in metavariables.
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index d4cc7eea71..6db7b064a6 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -50,7 +50,7 @@ import Coercion
 import TcOrigin
 import Type
 import TyCoRep   -- for checkValidRoles
-import TyCoPpr( pprTyVars, pprWithExplicitKindsWhen )
+import TyCoPpr( pprTyVars, pprWithExplicitKindsWhen, pprTyConBinders )
 import Class
 import CoAxiom
 import TyCon
@@ -1724,6 +1724,30 @@ There's also a change in the renamer:
 For completeness, it was also necessary to make coerce work on
 unlifted types, resolving #13595.
 
+Note [Unquantifiable kind variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#17562):
+
+  class (forall a. a b ~ a c) => C b c
+
+After elaboration and solving, we get
+
+  class (forall (a :: k -> kappa). (~) kappa (a b) (a c)) => C @{k} b c
+
+Note that kappa is unconstrained. (The k comes from generaliseTcTyCon,
+which has happened earlier.) We cannot possibly quantify over kappa -- there's
+nowhere to put it. But instead, we try to quantify over it, failing if
+we find any variable to quantify. Without this step, the final zonker
+(in TcHsSyn) will zap kappa to Any. In the case here, we then get an
+inexplicable failure about the use of the Any type family in the head of
+a quantified constraint.
+
+If we have -XNoPolyKinds, then all is well: quantifyTyVars will default
+kappa to Type.
+
+When trying to quantify, we don't want to quantify over class variables,
+so we quantify the type (forall class_tvs. ctxt => ()).
+
 -}
 
 tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM (TyCon, [DerivInfo])
@@ -1824,6 +1848,16 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
                   ; at_stuff  <- tcClassATs class_name clas ats at_defs
                   ; return (ctxt, fds, sig_stuff, at_stuff) }
 
+       ; bad_kvs <- kindGeneralizeAll (mkForAllTys (tyConTyVarBinders binders) $
+                                       mkPhiTy ctxt unitTy)
+          -- See Note [Unquantifiable kind variables]
+          -- See also Note [Recipe for checking a signature] in TcHsType
+          -- We don't generalize here because we don't have anywhere
+          -- to put freshly-generalized variables
+
+       ; unless (null bad_kvs) $
+         unquantifiable_kind_vars binders bad_kvs ctxt
+
        -- The solveEqualities will report errors for any
        -- unsolved equalities, so these zonks should not encounter
        -- any unfilled coercion variables unless there is such an error
@@ -1854,6 +1888,21 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
                                 ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
                                 ; return (tvs1', tvs2') }
 
+    unquantifiable_kind_vars binders bad_kvs ctxt
+      = do { let (env1, binders') = tidyTyCoVarBinders emptyTidyEnv binders
+                 (env2, bad_kvs') = tidyVarBndrs env1 bad_kvs
+           ; (env3, ctxt') <- zonkTidyTcTypes env2 ctxt
+           ; let doc = pprWithExplicitKindsWhen True $ -- always print kinds in this message
+                       vcat [ sep [ text "Unconstrained kind variable" <> plural bad_kvs'
+                                  , pprTyVars bad_kvs'
+                                  , text "in superclass context:" ]
+                            , nest 2 (text "class" <+> sep
+                                          [ pprThetaArrowTy ctxt'
+                                          , ppr class_name <+> pprTyConBinders binders' ])
+                            , text "Perhaps add a kind signature to a local type variable." ]
+            ; failWithTcM (env3, doc) }
+
+
 
 {- Note [Associated type defaults]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/types/TyCoPpr.hs b/compiler/types/TyCoPpr.hs
index f7a768210b..86068ce539 100644
--- a/compiler/types/TyCoPpr.hs
+++ b/compiler/types/TyCoPpr.hs
@@ -7,6 +7,7 @@ module TyCoPpr
         -- * Pretty-printing types
         pprType, pprParendType, pprTidiedType, pprPrecType, pprPrecTypeX,
         pprTypeApp, pprTCvBndr, pprTCvBndrs,
+        pprTyConBinders,
         pprSigmaType,
         pprTheta, pprParendTheta, pprForAll, pprUserForAll,
         pprTyVar, pprTyVars,
@@ -49,7 +50,7 @@ import GHC.Iface.Type
 import VarSet
 import VarEnv
 
-import DynFlags   ( gopt_set,
+import DynFlags   ( gopt_set, gopt,
                     GeneralFlag(Opt_PrintExplicitKinds, Opt_PrintExplicitRuntimeReps) )
 import Outputable
 import BasicTypes ( PprPrec(..), topPrec, sigPrec, opPrec
@@ -195,6 +196,27 @@ pprTyVar tv
   where
     kind = tyVarKind tv
 
+-- | Print the binders as they might appear in a surface-level
+-- declaration.
+pprTyConBinders :: [TyConBinder] -> SDoc
+pprTyConBinders tcbs = sdocWithDynFlags $ \dflags ->
+  let print_kinds = gopt Opt_PrintExplicitKinds dflags
+      ppr_tcb (Bndr tv flag) = case flag of
+        NamedTCB Required                -> pprTyVar tv
+        NamedTCB Specified | print_kinds -> char '@' <> pprTyVar tv
+        NamedTCB Inferred  | print_kinds -> char '@' <>
+          braces (if isLiftedTypeKind kind  -- cf. pprTyVar
+                  then ppr tv
+                  else ppr tv <+> dcolon <+> ppr kind)
+          where kind = tyVarKind tv
+        AnonTCB VisArg                   -> pprTyVar tv
+        _                                -> empty
+         -- last case covers invisible arguments without
+         -- -fprint-explicit-kinds, and also AnonTCB InvisArg
+
+  in
+  sep (map ppr_tcb tcbs)
+
 -----------------
 debugPprType :: Type -> SDoc
 -- ^ debugPprType is a simple pretty printer that prints a type
diff --git a/testsuite/tests/typecheck/should_compile/T17562.hs b/testsuite/tests/typecheck/should_compile/T17562.hs
new file mode 100644
index 0000000000..51c1073828
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17562.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #-}
+
+module T17562 where
+
+class (forall a. a b ~ a c) => C b c
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 80b11ca851..9b474c1f41 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -692,3 +692,4 @@ test('T17202', expect_broken(17202), compile, [''])
 test('T15839a', normal, compile, [''])
 test('T15839b', normal, compile, [''])
 test('T17343', exit_code(1), compile_and_run, [''])
+test('T17562', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T17562b.hs b/testsuite/tests/typecheck/should_fail/T17562b.hs
new file mode 100644
index 0000000000..7434e03f38
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17562b.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses,
+             PolyKinds #-}
+
+module T17562b where
+
+class (forall a. a b ~ a c) => C b c
diff --git a/testsuite/tests/typecheck/should_fail/T17562b.stderr b/testsuite/tests/typecheck/should_fail/T17562b.stderr
new file mode 100644
index 0000000000..6838d910ba
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17562b.stderr
@@ -0,0 +1,7 @@
+
+T17562b.hs:6:1: error:
+    • Unconstrained kind variable k1 in superclass context:
+        class (forall (a :: k -> k1). (a b :: k1) ~ (a c :: k1)) =>
+              C @{k} (b :: k) (c :: k)
+      Perhaps add a kind signature to a local type variable.
+    • In the class declaration for ‘C’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index e11c239742..d7a561e40b 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -548,5 +548,6 @@ test('T16512b', normal, compile_fail, [''])
 test('T17213', [extra_files(['T17213a.hs'])], multimod_compile_fail, ['T17213', '-v0'])
 test('T17355', normal, compile_fail, [''])
 test('T17360', normal, compile_fail, [''])
+test('T17562b', normal, compile_fail, [''])
 test('T17563', normal, compile_fail, [''])
 test('T16946', normal, compile_fail, [''])