[commit: ghc] master: Fix substitution but in liftCoSubst (Trac #7973) (8c846f7)

[Simon Peyton Jones]

Repository : http://darcs.haskell.org/ghc.git/

On branch  : master

https://github.com/ghc/ghc/commit/8c846f714223c33adef76e6072ba94d3e33b7e97

>---------------------------------------------------------------

commit 8c846f714223c33adef76e6072ba94d3e33b7e97
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Mon Jun 10 11:04:09 2013 +0100

    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]

>---------------------------------------------------------------

 compiler/types/Coercion.lhs | 82 +++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 79 insertions(+), 3 deletions(-)

diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 02e2783..59b0102 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -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}