Wrap an implication around class-sig kind errors

Ticket #17841 showed that we can get a kind error
in a class signature, but lack an enclosing implication
that binds its skolems.

This patch

* Adds the wrapping implication: the new call to
  checkTvConstraints in tcClassDecl1

* Simplifies the API to checkTvConstraints, which
  was not otherwise called at all.

* Simplifies TcErrors.report_unsolved by *not*
  initialising the TidyEnv from the typechecker lexical
  envt.  It's enough to do so from the free vars of the
  unsolved constraints; and we get silly renamings if
  we add variables twice: once from the lexical scope
  and once from the implication constraint.

8 files changed, 37 insertions, 18 deletions

diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index e111afc08a..2d0104f434 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -210,10 +210,9 @@ report_unsolved type_errors expr_holes
        ; traceTc "reportUnsolved (before zonking and tidying)" (ppr wanted)
 
        ; wanted <- zonkWC wanted   -- Zonk to reveal all information
-       ; env0 <- tcInitTidyEnv
             -- If we are deferring we are going to need /all/ evidence around,
             -- including the evidence produced by unflattening (zonkWC)
-       ; let tidy_env = tidyFreeTyCoVars env0 free_tvs
+       ; let tidy_env = tidyFreeTyCoVars emptyTidyEnv free_tvs
              free_tvs = tyCoVarsOfWCList wanted
 
        ; traceTc "reportUnsolved (after zonking):" $
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 89bf4149b7..e350ebeac6 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -442,8 +442,7 @@ use CoEvBindsVar (see newCoTcEvBinds) to signal that no term-level
 evidence bindings are allowed.  Notebly ():
 
   - Places in types where we are solving kind constraints (all of which
-    are equalities); see solveEqualities, solveLocalEqualities,
-    checkTvConstraints
+    are equalities); see solveEqualities, solveLocalEqualities
 
   - When unifying forall-types
 -}
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 7f4b7c6b6e..8d8f254a3e 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -39,7 +39,7 @@ import TcTyDecls
 import TcClassDcl
 import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
 import TcDeriv (DerivInfo(..))
-import TcUnify ( unifyKind )
+import TcUnify ( unifyKind, checkTvConstraints )
 import TcHsType
 import ClsInst( AssocInstInfo(..) )
 import TcMType
@@ -2026,6 +2026,9 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
        ; (ctxt, fds, sig_stuff, at_stuff)
             <- pushTcLevelM_   $
                solveEqualities $
+               checkTvConstraints skol_info (binderVars binders) $
+               -- The checkTvConstraints is needed bring into scope the
+               -- skolems bound by the class decl header (#17841)
                do { ctxt <- tcHsContext hs_ctxt
                   ; fds  <- mapM (addLocM tc_fundep) fundeps
                   ; sig_stuff <- tcClassSigs class_name sigs meths
@@ -2058,6 +2061,7 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
                                 ppr fds)
        ; return clas }
   where
+    skol_info = TyConSkol ClassFlavour class_name
     tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
                                 ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
                                 ; return (tvs1', tvs2') }
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 0832f80de4..4c1b18d89c 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1195,18 +1195,14 @@ checkConstraints skol_info skol_tvs given thing_inside
                  ; return (emptyTcEvBinds, res) } }
 
 checkTvConstraints :: SkolemInfo
-                   -> Maybe SDoc  -- User-written telescope, if present
-                   -> TcM ([TcTyVar], result)
-                   -> TcM ([TcTyVar], result)
-
-checkTvConstraints skol_info m_telescope thing_inside
-  = do { (tclvl, wanted, (skol_tvs, result))
-             <- pushLevelAndCaptureConstraints thing_inside
-
-       ; emitResidualTvConstraint skol_info m_telescope
-                                  skol_tvs tclvl wanted
-
-       ; return (skol_tvs, result) }
+                   -> [TcTyVar]          -- Skolem tyvars
+                   -> TcM result
+                   -> TcM result
+
+checkTvConstraints skol_info skol_tvs thing_inside
+  = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
+       ; emitResidualTvConstraint skol_info Nothing skol_tvs tclvl wanted
+       ; return result }
 
 emitResidualTvConstraint :: SkolemInfo -> Maybe SDoc -> [TcTyVar]
                          -> TcLevel -> WantedConstraints -> TcM ()
diff --git a/testsuite/tests/polykinds/T16902.stderr b/testsuite/tests/polykinds/T16902.stderr
index e265866119..2da3e41c36 100644
--- a/testsuite/tests/polykinds/T16902.stderr
+++ b/testsuite/tests/polykinds/T16902.stderr
@@ -1,6 +1,6 @@
 
 T16902.hs:11:10: error:
-    • Expected a type, but found something with kind ‘a1’
+    • Expected a type, but found something with kind ‘a’
     • In the type ‘F a’
       In the definition of data constructor ‘MkF’
       In the data declaration for ‘F’
diff --git a/testsuite/tests/polykinds/T17841.hs b/testsuite/tests/polykinds/T17841.hs
new file mode 100644
index 0000000000..c728a11f02
--- /dev/null
+++ b/testsuite/tests/polykinds/T17841.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+
+module T17841 where
+
+data Proxy a = Proxy
+
+class Foo (t :: k) where foo :: Proxy (a :: t)
diff --git a/testsuite/tests/polykinds/T17841.stderr b/testsuite/tests/polykinds/T17841.stderr
new file mode 100644
index 0000000000..975f5a11d0
--- /dev/null
+++ b/testsuite/tests/polykinds/T17841.stderr
@@ -0,0 +1,13 @@
+
+T17841.hs:7:40: error:
+    • Couldn't match kind ‘k’ with ‘*’
+      ‘k’ is a rigid type variable bound by
+        the class declaration for ‘Foo’
+        at T17841.hs:7:17
+      When matching kinds
+        k0 :: *
+        t :: k
+      Expected kind ‘t’, but ‘a’ has kind ‘k0’
+    • In the first argument of ‘Proxy’, namely ‘(a :: t)’
+      In the type signature: foo :: Proxy (a :: t)
+      In the class declaration for ‘Foo’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 4312691755..454be6fc62 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -215,3 +215,4 @@ test('T16342', normal, compile, [''])
 test('T16263', normal, compile_fail, [''])
 test('T16902', normal, compile_fail, [''])
 test('CuskFam', normal, compile, [''])
+test('T17841', normal, compile_fail, [''])