A crucial wibble in checking 98 constructors

This is a long standing bug actually, exposed by the new invariant
checking on Implications. We had too many variables in the skolems of
the reportUnsolvedEqualities call in the H98 case of tcConDecl.

compiler/GHC/Core/TyCo/Tidy.hs

@@ -56,7 +56,7 @@ tidyVarBndr tidy_env@(occ_env, subst) var
 
 avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv
 -- Seed the occ_env with clashes among the names, see
--- Note [Tidying multiple names at once] in GHC.Types.Names.Occurrence
+-- Note [Tidying multiple names at once] in GHC.Types.Name.Occurrence
 avoidNameClashes tvs (occ_env, subst)
   = (avoidClashesOccEnv occ_env occs, subst)
   where

compiler/GHC/Tc/Gen/HsType.hs

@@ -2591,7 +2591,7 @@ kcCheckDeclHeader_sig sig_kind name flav
         ; checkForDuplicateScopedTyVars implicit_prs
 
         -- Swizzle the Names so that the TyCon uses the user-declared implicit names
-        -- E.g  type T :: k -> Tye
+        -- E.g  type T :: k -> Type
         --      data T (a :: j) = ....
         -- We want the TyConBinders of T to be [j, a::j], not [k, a::k]
         -- Why? So that the TyConBinders of the TyCon will lexically scope over the
@@ -3485,12 +3485,12 @@ When we /must/ clone.
 --------------------------------------
 
 bindTyClTyVars :: Name -> ([TcTyConBinder] -> TcKind -> TcM a) -> TcM a
--- ^ Used for the type variables of a type or class decl
+-- ^ Bring into scope the binders of a PolyTcTyCon
+-- Used for the type variables of a type or class decl
 -- in the "kind checking" and "type checking" pass,
 -- but not in the initial-kind run.
 bindTyClTyVars tycon_name thing_inside
-  = do { tycon <- tcLookupTcTyCon tycon_name
-         -- The tycon is a PolyTcTyCon
+  = do { tycon <- tcLookupTcTyCon tycon_name     -- The tycon is a PolyTcTyCon
        ; let res_kind   = tyConResKind tycon
              binders    = tyConBinders tycon
        ; traceTc "bindTyClTyVars" (ppr tycon_name $$ ppr binders)
@@ -3498,6 +3498,8 @@ bindTyClTyVars tycon_name thing_inside
          thing_inside binders res_kind }
 
 bindTyClTyVarsAndZonk :: Name -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
+-- Like bindTyClTyVars, but in addition
+-- zonk the skolem TcTyVars of a PolyTcTyCon to TyVars
 bindTyClTyVarsAndZonk tycon_name thing_inside
   = bindTyClTyVars tycon_name $ \ tc_bndrs tc_kind ->
     do { ze          <- mkEmptyZonkEnv NoFlexi
@@ -3505,6 +3507,7 @@ bindTyClTyVarsAndZonk tycon_name thing_inside
        ; kind        <- zonkTcTypeToTypeX ze tc_kind
        ; thing_inside bndrs kind }
 
+
 {- *********************************************************************
 *                                                                      *
              Kind generalisation

compiler/GHC/Tc/TyCl.hs

@@ -3385,7 +3385,9 @@ tcConDecl new_or_data dd_info rep_tycon tc_bndrs res_kind tag_map
          --      hs_qvars = HsQTvs { hsq_implicit = {k}
          --                        , hsq_explicit = {f,b} }
 
-       ; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ])
+       ; traceTc "tcConDecl 1" (vcat [ ppr name
+                                     , text "explicit_tkv_nms" <+> ppr explicit_tkv_nms
+                                     , text "tc_bndrs" <+> ppr tc_bndrs ])
        ; skol_info <- mkSkolemInfo (DataConSkol name)
 
        ; (tclvl, wanted, (exp_tvbndrs, (ctxt, arg_tys, field_lbls, stricts)))
@@ -3419,7 +3421,7 @@ tcConDecl new_or_data dd_info rep_tycon tc_bndrs res_kind tag_map
 
        ; kvs <- kindGeneralizeAll skol_info fake_ty
 
-       ; let all_skol_tvs = tc_tvs ++ kvs ++ binderVars exp_tvbndrs
+       ; let all_skol_tvs = tc_tvs ++ kvs
        ; reportUnsolvedEqualities skol_info all_skol_tvs tclvl wanted
              -- The skol_info claims that all the variables are bound
              -- by the data constructor decl, whereas actually the

compiler/GHC/Tc/Types/Constraint.hs

@@ -1312,7 +1312,8 @@ data Implication
 
       ic_skols :: [TcTyVar],     -- Introduced skolems; always skolem TcTyVars
                                  -- Their level numbers should be precisely ic_tclvl
-                                 -- Their SkolemInfo should be precisely ic_info
+                                 -- Their SkolemInfo should be precisely ic_info (almost)
+                                 --       See Note [Implication invariants]
 
       ic_given  :: [EvVar],      -- Given evidence variables
                                  --   (order does not matter)
@@ -1624,7 +1625,25 @@ never see it.
 *                                                                      *
             Invariant checking (debug only)
 *                                                                      *
-********************************************************************* -}
+************************************************************************ 
+
+Note [Implication invariants]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The skolems of an implication have the following invariants, which are checked
+by checkImplicationInvariants:
+
+a) They are all SkolemTv TcTyVars; no TyVars, no unification variables
+b) Their TcLevel matches the ic_lvl for the implication
+c) Their SkolemInfo matches the implication.
+
+Actually (c) is not quite true.  Consider
+   data T a = forall b. MkT a b
+
+In tcConDecl for MkT we'll create an implication with ic_info of
+DataConSkol; but the type variable 'a' will have a SkolemInfo of
+TyConSkol.  So we allow the tyvar to have a SkolemInfo of TyConFlav if
+the implication SkolemInfo is DataConSkol.
+-}
 
 checkImplicationInvariants, check_implic :: (HasCallStack, Applicative m) => Implication -> m ()
 {-# INLINE checkImplicationInvariants #-}