Commit 8c846f71 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix substitution but in liftCoSubst (Trac #7973)

Iavor uncovered this subtle omission in liftCoSubst.  The problem and its
solution are desribed in
    Note [Substituting kinds in liftCoSubst]
parent 4c497724
......@@ -1115,7 +1115,53 @@ lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
%* *
%************************************************************************
Note [Lifting coercions over types: liftCoSubst]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The KPUSH rule deals with this situation
data T a = MkK (a -> Maybe a)
g :: T t1 ~ K t2
x :: t1 -> Maybe t1
case (K @t1 x) |> g of
K (y:t2 -> Maybe t2) -> rhs
We want to push the coercion inside the constructor application.
So we do this
g' :: t1~t2 = Nth 0 g
case K @t2 (x |> g' -> Maybe g') of
K (y:t2 -> Maybe t2) -> rhs
The crucial operation is that we
* take the type of K's argument: a -> Maybe a
* and substitute g' for a
thus giving *coercion*. This is what liftCoSubst does.
Note [Substituting kinds in liftCoSubst]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to take care with kind polymorphism. Suppose
K :: forall k (a:k). (forall b:k. a -> b) -> T k a
Now given (K @kk1 @ty1 v) |> g) where
g :: T kk1 ty1 ~ T kk2 ty2
we want to compute
(forall b:k a->b) [ Nth 0 g/k, Nth 1 g/a ]
Notice that we MUST substitute for 'k'; this happens in
liftCoSubstTyVarBndr. But what should we substitute?
We need to take b's kind 'k' and return a Kind, not a Coercion!
Happily we can do this because we know that all kind coercions
((Nth 0 g) in this case) are Refl. So we need a special purpose
subst_kind: LiftCoSubst -> Kind -> Kind
that expects a Refl coercion (or something equivalent to Refl)
when it looks up a kind variable.
\begin{code}
-- ----------------------------------------------------
-- See Note [Lifting coercions over types: liftCoSubst]
-- ----------------------------------------------------
data LiftCoSubst = LCS InScopeSet LiftCoEnv
type LiftCoEnv = VarEnv Coercion
......@@ -1158,14 +1204,44 @@ liftCoSubstTyVar :: LiftCoSubst -> TyVar -> Maybe Coercion
liftCoSubstTyVar (LCS _ cenv) tv = lookupVarEnv cenv tv
liftCoSubstTyVarBndr :: LiftCoSubst -> TyVar -> (LiftCoSubst, TyVar)
liftCoSubstTyVarBndr (LCS in_scope cenv) old_var
liftCoSubstTyVarBndr subst@(LCS in_scope cenv) old_var
= (LCS (in_scope `extendInScopeSet` new_var) new_cenv, new_var)
where
new_cenv | no_change = delVarEnv cenv old_var
| otherwise = extendVarEnv cenv old_var (Refl (TyVarTy new_var))
no_change = new_var == old_var
new_var = uniqAway in_scope old_var
no_change = no_kind_change && (new_var == old_var)
new_var1 = uniqAway in_scope old_var
old_ki = tyVarKind old_var
no_kind_change = isEmptyVarSet (tyVarsOfType old_ki)
new_var | no_kind_change = new_var1
| otherwise = setTyVarKind new_var1 (subst_kind subst old_ki)
subst_kind :: LiftCoSubst -> Kind -> Kind
-- See Note [Substituting kinds in liftCoSubst]
subst_kind subst@(LCS _ cenv) kind
= go kind
where
go (LitTy n) = n `seq` LitTy n
go (TyVarTy kv) = subst_kv kv
go (TyConApp tc tys) = let args = map go tys
in args `seqList` TyConApp tc args
go (FunTy arg res) = (FunTy $! (go arg)) $! (go res)
go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
go (ForAllTy tv ty) = case liftCoSubstTyVarBndr subst tv of
(subst', tv') ->
ForAllTy tv' $! (subst_kind subst' ty)
subst_kv kv
| Just co <- lookupVarEnv cenv kv
, let co_kind = coercionKind co
= ASSERT2( pFst co_kind `eqKind` pSnd co_kind, ppr kv $$ ppr co )
pFst co_kind
| otherwise
= TyVarTy kv
\end{code}
\begin{code}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment