Tidying could cause ill-kinded types

I found (Trac #14175) that the tidying we do when reporting
type error messages could cause a well-kinded type to become
ill-kinded. Reason: we initialised the tidy-env with a
completely un-zonked TidyEnv accumulated in the TcLclEnv
as we come across lexical type-varialbe bindings.

Solution: zonk them.

But I ended up refactoring a bit:

* Get rid of tcl_tidy :: TidyEnv altogether

* Instead use tcl_bndrs :: TcBinderStack
  This used to contain only Ids, but now I've added those
  lexically scoped TyVars too.

* Change names:
     TcIdBinderStack -> TcBinderStack
     TcIdBinder      -> TcBinder
     extendTcIdBndrs -> extendTcBinderStack

* Now tcInitTidyEnv can grab those TyVars from the
  tcl_bndrs, zonk, and tidy them.

The only annoyance is that I had to add TcEnv.hs-boot, to
break the recursion between the zonking code and the
TrRnMonad functions like addErrTc that call tcInitTidyEnv.
Tiresome, but in fact that file existed already.

compiler/typecheck/TcBinds.hs

@@ -408,7 +408,7 @@ tcValBinds top_lvl binds sigs thing_inside
 
                 -- Extend the envt right away with all the Ids
                 -- declared with complete type signatures
-                -- Do not extend the TcIdBinderStack; instead
+                -- Do not extend the TcBinderStack; instead
                 -- we extend it on a per-rhs basis in tcExtendForRhs
         ; tcExtendSigIds top_lvl poly_ids $ do
             { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do
@@ -702,7 +702,7 @@ tcPolyCheck prag_fn
 
        ; (ev_binds, (co_fn, matches'))
             <- checkConstraints skol_info skol_tvs ev_vars $
-               tcExtendIdBndrs [TcIdBndr mono_id NotTopLevel]  $
+               tcExtendBinderStack [TcIdBndr mono_id NotTopLevel]  $
                tcExtendTyVarEnv2 tv_prs $
                setSrcSpan loc           $
                tcMatchesFun (L nm_loc mono_name) matches (mkCheckExpType tau)
@@ -1282,7 +1282,7 @@ tcMonoBinds is_rec sig_fn no_gen
             <- tcInferInst $ \ exp_ty ->
                   -- tcInferInst: see TcUnify,
                   -- Note [Deep instantiation of InferResult]
-               tcExtendIdBndrs [TcIdBndr_ExpType name exp_ty NotTopLevel] $
+               tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $
                   -- We extend the error context even for a non-recursive
                   -- function so that in type error messages we show the
                   -- type of the thing whose rhs we are type checking
@@ -1470,7 +1470,7 @@ tcExtendTyVarEnvFromSig sig_inst thing_inside
     thing_inside
 
 tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
--- Extend the TcIdBinderStack for the RHS of the binding, with
+-- Extend the TcBinderStack for the RHS of the binding, with
 -- the monomorphic Id.  That way, if we have, say
 --     f = \x -> blah
 -- and something goes wrong in 'blah', we get a "relevant binding"
@@ -1479,10 +1479,10 @@ tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
 --    f :: forall a. [a] -> [a]
 --    f x = True
 -- We can't unify True with [a], and a relevant binding is f :: [a] -> [a]
--- If we had the *polymorphic* version of f in the TcIdBinderStack, it
+-- If we had the *polymorphic* version of f in the TcBinderStack, it
 -- would not be reported as relevant, because its type is closed
 tcExtendIdBinderStackForRhs infos thing_inside
-  = tcExtendIdBndrs [ TcIdBndr mono_id NotTopLevel
+  = tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel
                         | MBI { mbi_mono_id = mono_id } <- infos ]
                         thing_inside
     -- NotTopLevel: it's a monomorphic binding

compiler/typecheck/TcEnv.hs

@@ -30,7 +30,7 @@ module TcEnv(
         tcExtendTyVarEnv, tcExtendTyVarEnv2,
         tcExtendLetEnv, tcExtendSigIds, tcExtendRecIds,
         tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2,
-        tcExtendIdBndrs, tcExtendLocalTypeEnv,
+        tcExtendBinderStack, tcExtendLocalTypeEnv,
         isTypeClosedLetBndr,
 
         tcLookup, tcLookupLocated, tcLookupLocalIds,
@@ -43,6 +43,9 @@ module TcEnv(
         getTypeSigNames,
         tcExtendRecEnv,         -- For knot-tying
 
+        -- Tidying
+        tcInitTidyEnv, tcInitOpenTidyEnv,
+
         -- Instances
         tcLookupInstance, tcGetInstEnvs,
 
@@ -85,6 +88,7 @@ import DataCon ( DataCon )
 import PatSyn  ( PatSyn )
 import ConLike
 import TyCon
+import Type
 import CoAxiom
 import Class
 import Name
@@ -398,23 +402,11 @@ tcExtendTyVarEnv2 binds thing_inside
   -- thus, no coercion variables
   = do { tc_extend_local_env NotTopLevel
                     [(name, ATyVar name tv) | (name, tv) <- binds] $
-         do { env <- getLclEnv
-            ; let env' = env { tcl_tidy = add_tidy_tvs (tcl_tidy env) }
-            ; setLclEnv env' thing_inside }}
-  where
-    add_tidy_tvs env = foldl add env binds
-
-    -- We initialise the "tidy-env", used for tidying types before printing,
-    -- by building a reverse map from the in-scope type variables to the
-    -- OccName that the programmer originally used for them
-    add :: TidyEnv -> (Name, TcTyVar) -> TidyEnv
-    add (env,subst) (name, tyvar)
-        = ASSERT( isTyVar tyvar )
-          case tidyOccName env (nameOccName name) of
-            (env', occ') ->  (env', extendVarEnv subst tyvar tyvar')
+         tcExtendBinderStack tv_binds $
+         thing_inside }
   where
-                  tyvar' = setTyVarName tyvar name'
-                  name'  = tidyNameOcc name occ'
+    tv_binds :: [TcBinder]
+    tv_binds = [TcTvBndr name tv | (name,tv) <- binds]
 
 isTypeClosedLetBndr :: Id -> Bool
 -- See Note [Bindings with closed types] in TcRnTypes
@@ -423,7 +415,7 @@ isTypeClosedLetBndr = noFreeVarsOfType . idType
 tcExtendRecIds :: [(Name, TcId)] -> TcM a -> TcM a
 -- Used for binding the recurive uses of Ids in a binding
 -- both top-level value bindings and and nested let/where-bindings
--- Does not extend the TcIdBinderStack
+-- Does not extend the TcBinderStack
 tcExtendRecIds pairs thing_inside
   = tc_extend_local_env NotTopLevel
           [ (name, ATcId { tct_id   = let_id
@@ -433,7 +425,7 @@ tcExtendRecIds pairs thing_inside
 
 tcExtendSigIds :: TopLevelFlag -> [TcId] -> TcM a -> TcM a
 -- Used for binding the Ids that have a complete user type signature
--- Does not extend the TcIdBinderStack
+-- Does not extend the TcBinderStack
 tcExtendSigIds top_lvl sig_ids thing_inside
   = tc_extend_local_env top_lvl
           [ (idName id, ATcId { tct_id   = id
@@ -447,10 +439,10 @@ tcExtendSigIds top_lvl sig_ids thing_inside
 tcExtendLetEnv :: TopLevelFlag -> TcSigFun -> IsGroupClosed
                   -> [TcId] -> TcM a -> TcM a
 -- Used for both top-level value bindings and and nested let/where-bindings
--- Adds to the TcIdBinderStack too
+-- Adds to the TcBinderStack too
 tcExtendLetEnv top_lvl sig_fn (IsGroupClosed fvs fv_type_closed)
                ids thing_inside
-  = tcExtendIdBndrs [TcIdBndr id top_lvl | id <- ids] $
+  = tcExtendBinderStack [TcIdBndr id top_lvl | id <- ids] $
     tc_extend_local_env top_lvl
           [ (idName id, ATcId { tct_id   = id
                               , tct_info = mk_tct_info id })
@@ -468,7 +460,7 @@ tcExtendLetEnv top_lvl sig_fn (IsGroupClosed fvs fv_type_closed)
 
 tcExtendIdEnv :: [TcId] -> TcM a -> TcM a
 -- For lambda-bound and case-bound Ids
--- Extends the the TcIdBinderStack as well
+-- Extends the the TcBinderStack as well
 tcExtendIdEnv ids thing_inside
   = tcExtendIdEnv2 [(idName id, id) | id <- ids] thing_inside
 
@@ -479,7 +471,7 @@ tcExtendIdEnv1 name id thing_inside
 
 tcExtendIdEnv2 :: [(Name,TcId)] -> TcM a -> TcM a
 tcExtendIdEnv2 names_w_ids thing_inside
-  = tcExtendIdBndrs [ TcIdBndr mono_id NotTopLevel
+  = tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel
                         | (_,mono_id) <- names_w_ids ] $
     tc_extend_local_env NotTopLevel
             [ (name, ATcId { tct_id = id
@@ -560,15 +552,51 @@ tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things
         --
         -- Nor must we generalise g over any kind variables free in r's kind
 
--------------------------------------------------------------
--- Extending the TcIdBinderStack, used only for error messages
 
-tcExtendIdBndrs :: [TcIdBinder] -> TcM a -> TcM a
-tcExtendIdBndrs bndrs thing_inside
-  = do { traceTc "tcExtendIdBndrs" (ppr bndrs)
+{- *********************************************************************
+*                                                                      *
+             The TcBinderStack
+*                                                                      *
+********************************************************************* -}
+
+tcExtendBinderStack :: [TcBinder] -> TcM a -> TcM a
+tcExtendBinderStack bndrs thing_inside
+  = do { traceTc "tcExtendBinderStack" (ppr bndrs)
        ; updLclEnv (\env -> env { tcl_bndrs = bndrs ++ tcl_bndrs env })
                    thing_inside }
 
+tcInitTidyEnv :: TcM TidyEnv
+-- We initialise the "tidy-env", used for tidying types before printing,
+-- by building a reverse map from the in-scope type variables to the
+-- OccName that the programmer originally used for them
+tcInitTidyEnv
+  = do  { lcl_env <- getLclEnv
+        ; go emptyTidyEnv (tcl_bndrs lcl_env) }
+  where
+    go (env, subst) []
+      = return (env, subst)
+    go (env, subst) (b : bs)
+      | TcTvBndr name tyvar <- b
+       = do { let (env', occ') = tidyOccName env (nameOccName name)
+                  name'  = tidyNameOcc name occ'
+                  tyvar1 = setTyVarName tyvar name'
+            ; tyvar2 <- zonkTcTyVarToTyVar tyvar1
+              -- Be sure to zonk here!  Tidying applies to zonked
+              -- types, so if we don't zonk we may create an
+              -- ill-kinded type (Trac #14175)
+            ; go (env', extendVarEnv subst tyvar tyvar2) bs }
+      | otherwise
+      = go (env, subst) bs
+
+-- | Get a 'TidyEnv' that includes mappings for all vars free in the given
+-- type. Useful when tidying open types.
+tcInitOpenTidyEnv :: [TyCoVar] -> TcM TidyEnv
+tcInitOpenTidyEnv tvs
+  = do { env1 <- tcInitTidyEnv
+       ; let env2 = tidyFreeTyCoVars env1 tvs
+       ; return env2 }
+
+
 
 {- *********************************************************************
 *                                                                      *

compiler/typecheck/TcEnv.hs-boot

-{-
->module TcEnv where
->import TcRnTypes
->import HsExtension ( GhcTcId, IdP )
->
->tcExtendIdEnv :: [TcId] -> TcM a -> TcM a
--}
+module TcEnv where
+
+import TcRnTypes( TcM )
+import VarEnv( TidyEnv )
+
+-- Annoyingly, there's a recursion between tcInitTidyEnv
+-- (which does zonking and hence needs TcMType) and
+-- addErrTc etc which live in TcRnMonad.  Rats.
+tcInitTidyEnv :: TcM TidyEnv
+

compiler/typecheck/TcErrors.hs

@@ -13,6 +13,7 @@ import TcRnTypes
 import TcRnMonad
 import TcMType
 import TcUnify( occCheckForErrors, OccCheckResult(..) )
+import TcEnv( tcInitTidyEnv )
 import TcType
 import RnUnbound ( unknownNameSuggestions )
 import Type
@@ -196,6 +197,7 @@ report_unsolved mb_binds_var err_as_warn type_errors expr_holes
 
        ; traceTc "reportUnsolved (after zonking):" $
          vcat [ text "Free tyvars:" <+> pprTyVars free_tvs
+              , text "Tidy env:" <+> ppr tidy_env
               , text "Wanted:" <+> ppr wanted ]
 
        ; warn_redundant <- woptM Opt_WarnRedundantConstraints
@@ -442,6 +444,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
                                        , text "Insols =" <+> ppr insols
                                        , text "Suppress =" <+> ppr (cec_suppress ctxt)])
        ; let tidy_cts = bagToList (mapBag (tidyCt env) (insols `unionBags` simples))
+       ; traceTc "rw2" (ppr tidy_cts)
 
          -- First deal with things that are utterly wrong
          -- Like Int ~ Bool (incl nullary TyCons)
@@ -1147,11 +1150,13 @@ validSubstitutions ct | isExprHoleCt ct =
     localsFirst elts = lcl ++ gbl
       where (lcl, gbl) = partition gre_lcl elts
 
-    getBndrOcc :: TcIdBinder -> OccName
-    getBndrOcc (TcIdBndr id _) = occName $ getName id
-    getBndrOcc (TcIdBndr_ExpType name _ _) = occName $ getName name
+    is_id_bind :: TcBinder -> Bool
+    is_id_bind (TcIdBndr {})         = True
+    is_id_bind (TcIdBndr_ExpType {}) = True
+    is_id_bind (TcTvBndr {})         = False
 
-    relBindSet =  mkOccSet $ map getBndrOcc $ tcl_bndrs hole_env
+    relBindSet = mkOccSet $ [ occName b | b <- tcl_bndrs hole_env
+                                        , is_id_bind b ]
 
     shouldBeSkipped :: GlobalRdrElt -> Bool
     shouldBeSkipped el = (occName $ gre_name el) `elemOccSet` relBindSet
@@ -2912,7 +2917,7 @@ relevantBindings want_filtering ctxt ct
 
     ---- fixes #12177
     ---- builds up a list of bindings whose OccName has not been seen before
-    remove_shadowing :: [TcIdBinder] -> [TcIdBinder]
+    remove_shadowing :: [TcBinder] -> [TcBinder]
     remove_shadowing bindings = reverse $ fst $ foldl
       (\(bindingAcc, seenNames) binding ->
         if (occName binding) `elemOccSet` seenNames -- if we've seen it
@@ -2922,13 +2927,14 @@ relevantBindings want_filtering ctxt ct
 
     go :: DynFlags -> TidyEnv -> TcTyVarSet -> Maybe Int -> TcTyVarSet -> [SDoc]
        -> Bool                          -- True <=> some filtered out due to lack of fuel
-       -> [TcIdBinder]
+       -> [TcBinder]
        -> TcM (TidyEnv, [SDoc], Bool)   -- The bool says if we filtered any out
                                         -- because of lack of fuel
     go _ tidy_env _ _ _ docs discards []
       = return (tidy_env, reverse docs, discards)
     go dflags tidy_env ct_tvs n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
       = case tc_bndr of
+          TcTvBndr {} -> discard_it
           TcIdBndr id top_lvl -> go2 (idName id) (idType id) top_lvl
           TcIdBndr_ExpType name et top_lvl ->
             do { mb_ty <- readExpType_maybe et

compiler/typecheck/TcRnMonad.hs

@@ -85,7 +85,7 @@ module TcRnMonad(
   failIfTc, failIfTcM,
   warnIfFlag, warnIf, warnTc, warnTcM,
   addWarnTc, addWarnTcM, addWarn, addWarnAt, add_warn,
-  tcInitTidyEnv, tcInitOpenTidyEnv, mkErrInfo,
+  mkErrInfo,
 
   -- * Type constraints
   newTcEvBinds,
@@ -178,6 +178,8 @@ import Data.Set ( Set )
 import qualified Data.Set as Set
 
 import {-# SOURCE #-} TcSplice ( runRemoteModFinalizers )
+import {-# SOURCE #-} TcEnv    ( tcInitTidyEnv )
+
 import qualified Data.Map as Map
 
 {-
@@ -325,7 +327,6 @@ initTcWithGbl hsc_env gbl_env loc do_this
                 tcl_arrow_ctxt = NoArrowCtxt,
                 tcl_env        = emptyNameEnv,
                 tcl_bndrs      = [],
-                tcl_tidy       = emptyTidyEnv,
                 tcl_tyvars     = tvs_var,
                 tcl_lie        = lie_var,
                 tcl_tclvl      = topTcLevel
@@ -1299,19 +1300,6 @@ add_warn_at reason loc msg extra_info
                                     msg extra_info } ;
          reportWarning reason warn }
 
-tcInitTidyEnv :: TcM TidyEnv
-tcInitTidyEnv
-  = do  { lcl_env <- getLclEnv
-        ; return (tcl_tidy lcl_env) }
-
--- | Get a 'TidyEnv' that includes mappings for all vars free in the given
--- type. Useful when tidying open types.
-tcInitOpenTidyEnv :: [TyCoVar] -> TcM TidyEnv
-tcInitOpenTidyEnv tvs
-  = do { env1 <- tcInitTidyEnv
-       ; let env2 = tidyFreeTyCoVars env1 tvs
-       ; return env2 }
-
 
 {-
 -----------------------------------

compiler/typecheck/TcRnTypes.hs

@@ -38,7 +38,7 @@ module TcRnTypes(
         WhereFrom(..), mkModDeps, modDepsElts,
 
         -- Typechecker types
-        TcTypeEnv, TcIdBinderStack, TcIdBinder(..),
+        TcTypeEnv, TcBinderStack, TcBinder(..),
         TcTyThing(..), PromotionErr(..),
         IdBindingInfo(..), ClosedTypeId, RhsNames,
         IsGroupClosed(..),
@@ -828,10 +828,8 @@ data TcLclEnv           -- Changes as we move inside an expression
         tcl_env  :: TcTypeEnv,    -- The local type environment:
                                   -- Ids and TyVars defined in this module
 
-        tcl_bndrs :: TcIdBinderStack,   -- Used for reporting relevant bindings
-
-        tcl_tidy :: TidyEnv,      -- Used for tidying types; contains all
-                                  -- in-scope type variables (but not term variables)
+        tcl_bndrs :: TcBinderStack,   -- Used for reporting relevant bindings,
+                                      -- and for tidying types
 
         tcl_tyvars :: TcRef TcTyVarSet, -- The "global tyvars"
                         -- Namely, the in-scope TyVars bound in tcl_env,
@@ -885,34 +883,44 @@ type TcId        = Id
 type TcIdSet     = IdSet
 
 ---------------------------
--- The TcIdBinderStack
+-- The TcBinderStack
 ---------------------------
 
-type TcIdBinderStack = [TcIdBinder]
-   -- This is a stack of locally-bound ids, innermost on top
-   -- Used only in error reporting (relevantBindings in TcError)
+type TcBinderStack = [TcBinder]
+   -- This is a stack of locally-bound ids and tyvars,
+   --   innermost on top
+   -- Used only in error reporting (relevantBindings in TcError),
+   --   and in tidying
    -- We can't use the tcl_env type environment, because it doesn't
    --   keep track of the nesting order
 
-data TcIdBinder
+data TcBinder
   = TcIdBndr
        TcId
        TopLevelFlag    -- Tells whether the binding is syntactically top-level
                        -- (The monomorphic Ids for a recursive group count
                        --  as not-top-level for this purpose.)
+
   | TcIdBndr_ExpType  -- Variant that allows the type to be specified as
                       -- an ExpType
        Name
        ExpType
        TopLevelFlag
 
-instance Outputable TcIdBinder where
+  | TcTvBndr          -- e.g.   case x of P (y::a) -> blah
+       Name           -- We bind the lexical name "a" to the type of y,
+       TyVar          -- which might be an utterly different (perhaps
+                      -- existential) tyvar
+
+instance Outputable TcBinder where
    ppr (TcIdBndr id top_lvl)           = ppr id <> brackets (ppr top_lvl)
    ppr (TcIdBndr_ExpType id _ top_lvl) = ppr id <> brackets (ppr top_lvl)
+   ppr (TcTvBndr name tv)              = ppr name <+> ppr tv
 
-instance HasOccName TcIdBinder where
-    occName (TcIdBndr id _) = (occName (idName id))
-    occName (TcIdBndr_ExpType name _ _) = (occName name)
+instance HasOccName TcBinder where
+    occName (TcIdBndr id _)             = occName (idName id)
+    occName (TcIdBndr_ExpType name _ _) = occName name
+    occName (TcTvBndr name _)           = occName name
 
 ---------------------------
 -- Template Haskell stages and levels
@@ -2934,7 +2942,7 @@ data CtLoc = CtLoc { ctl_origin :: CtOrigin
   -- The TcLclEnv includes particularly
   --    source location:  tcl_loc   :: RealSrcSpan
   --    context:          tcl_ctxt  :: [ErrCtxt]
-  --    binder stack:     tcl_bndrs :: TcIdBinderStack
+  --    binder stack:     tcl_bndrs :: TcBinderStack
   --    level:            tcl_tclvl :: TcLevel
 
 mkKindLoc :: TcType -> TcType   -- original *types* being compared

compiler/typecheck/TcValidity.hs

@@ -39,7 +39,7 @@ import TyCon
 -- others:
 import HsSyn            -- HsType
 import TcRnMonad        -- TcType, amongst others
-import TcEnv       ( tcGetInstEnvs )
+import TcEnv       ( tcGetInstEnvs, tcInitTidyEnv, tcInitOpenTidyEnv )
 import FunDeps
 import InstEnv     ( InstMatch, lookupInstEnv )
 import FamInstEnv  ( isDominatedBy, injectiveBranches,

testsuite/tests/indexed-types/should_fail/T14175.hs

+{-# LANGUAGE TypeFamilies, PolyKinds, TypeInType #-}
+
+module T14175 where
+
+import Data.Kind
+
+type family PComp (k :: j -> Type) (x :: k) :: ()

testsuite/tests/indexed-types/should_fail/T14175.stderr

+
+T14175.hs:7:42: error:
+    • Expecting one more argument to ‘k’
+      Expected a type, but ‘k’ has kind ‘j -> *’
+    • In the kind ‘k’

testsuite/tests/indexed-types/should_fail/all.T

@@ -139,3 +139,4 @@ test('T13877', normal, compile_fail, [''])
 test('T13972', normal, compile_fail, [''])
 test('T14033', normal, compile_fail, [''])
 test('T14045a', normal, compile_fail, [''])
+test('T14175', normal, compile_fail, [''])