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.

4 files changed, 15 insertions, 17 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 ()