[GHC] #13959: substTyVar's definition is highly dubious

[GHC]

#13959: substTyVar's definition is highly dubious
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Currently, we have:

 {{{#!hs
 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
 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?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13959>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler