substTyVar's definition is highly dubious

Currently, we have:

substTyVar :: TCvSubst -> TyVar -> Type
substTyVar (TCvSubst _ tenv _) tv
  = ASSERT( isTyVar tv )
    case lookupVarEnv tenv tv of
      Just ty -> ty
      Nothing -> TyVarTy tv

But as Richard pointed out to me, the Nothing case is flat-out wrong. If tv isn't in the substitution, we need to check if any of the variables in tv's kind are in the substitution, and if so, apply the substitution to them.

Fixing this might seem straightforward enough:

diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 5ac63e5..4f7d650 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -2191,11 +2191,11 @@ subst_ty subst ty
     go (CoercionTy co)   = CoercionTy $! (subst_co subst co)

 substTyVar :: TCvSubst -> TyVar -> Type
-substTyVar (TCvSubst _ tenv _) tv
+substTyVar subst@(TCvSubst _ tenv _) tv
   = ASSERT( isTyVar tv )
     case lookupVarEnv tenv tv of
       Just ty -> ty
-      Nothing -> TyVarTy tv
+      Nothing -> TyVarTy (updateTyVarKind (substTyUnchecked subst) tv)

 substTyVars :: TCvSubst -> [TyVar] -> [Type]
 substTyVars subst = map $ substTyVar subst

But note that I'm using substTyUnchecked, not substTy, since if you try using the latter, GHC will pretty quickly fall over on a ./validate --slow build, as substTy's assertions are violated all over the place.

I'm fairly certain I know why the assertions would be tripping up, however. To build most of the in-scope sets used for substTyVar's substitutions, the mkVarSet :: [Var] -> VarSet function is used. But mkVarSet only grabs the Uniques of the type variables themselves, not the variables in the kind of each type variable. This means the in-scope sets will frequently be too narrow to encompass the kind variables, which absolutely must be in the set if we want to change substTyVar as described above.

I'm not sure what the solution is here. Perhaps we should be using a variant of mkVarSet called mkTyVarSet that grabs the Uniques of the kind variables as well?

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire
Operating system
Architecture