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 Unique
s 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 Unique
s 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 |