[commit: ghc] ghc-kinds: kind substitution in tcInstSkolTyVars and all friends (09495da)

[Julien Cretin]

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : ghc-kinds

http://hackage.haskell.org/trac/ghc/changeset/09495daf5b71fb9faea19ebd893a26b85911eaa3

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

commit 09495daf5b71fb9faea19ebd893a26b85911eaa3
Author: Julien Cretin <ghc at ia0.eu>
Date:   Wed Sep 14 18:11:54 2011 +0200

    kind substitution in tcInstSkolTyVars and all friends

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

 compiler/typecheck/TcMType.lhs |   61 +++++++++++++++++++++++-----------------
 compiler/types/Kind.lhs        |   13 ++++++--
 2 files changed, 44 insertions(+), 30 deletions(-)

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 034a812..8bd7ed6 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -204,16 +204,22 @@ tcSuperSkolTyVars :: [TyVar] -> [TcTyVar]
 -- Make skolem constants, but do *not* give them new names, as above
 -- Moreover, make them "super skolems"; see comments with superSkolemTv
 tcSuperSkolTyVars tyvars
-  = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv
-    | tv <- tyvars ]
+  = kvs' ++ tvs'
+  where
+    (kvs, tvs) = span (isSuperKind . tyVarKind) tyvars
+    kvs' = [ mkTcTyVar (tyVarName kv) (tyVarKind kv) superSkolemTv
+           | kv <- kvs ]
+    tvs' = [ mkTcTyVar (tyVarName tv) (substTy subst (tyVarKind tv)) superSkolemTv
+           | tv <- tvs ]
+    subst = zipTopTvSubst kvs (map mkTyVarTy kvs')
 
-tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar
+tcInstSkolTyVar :: Bool -> TvSubst -> TyVar -> TcM TcTyVar
 -- Instantiate the tyvar, using 
 --	* the occ-name and kind of the supplied tyvar, 
 --	* the unique from the monad,
 --	* the location either from the tyvar (skol_info = SigSkol)
 --                     or from the monad (otherwise)
-tcInstSkolTyVar overlappable tyvar
+tcInstSkolTyVar overlappable subst tyvar
   = do	{ uniq <- newUnique
         ; loc <-  getSrcSpanM
 	; let new_name = mkInternalName uniq occ loc
@@ -221,13 +227,21 @@ tcInstSkolTyVar overlappable tyvar
   where
     old_name = tyVarName tyvar
     occ      = nameOccName old_name
-    kind     = tyVarKind tyvar
+    kind     = substTy subst (tyVarKind tyvar)
 
 tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar]
-tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars
+tcInstSkolTyVars tyvars
+  = do { kvs' <- mapM (tcInstSkolTyVar False (mkTopTvSubst [])) kvs
+       ; tvs' <- mapM (tcInstSkolTyVar False (zipTopTvSubst kvs (map mkTyVarTy kvs'))) tvs
+       ; return (kvs' ++ tvs') }
+  where (kvs, tvs) = span (isSuperKind . tyVarKind) tyvars
 
 tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
-tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars
+tcInstSuperSkolTyVars tyvars
+  = do { kvs' <- mapM (tcInstSkolTyVar True (mkTopTvSubst [])) kvs
+       ; tvs' <- mapM (tcInstSkolTyVar True (zipTopTvSubst kvs (map mkTyVarTy kvs'))) tvs
+       ; return (kvs' ++ tvs') }
+  where (kvs, tvs) = span (isSuperKind . tyVarKind) tyvars
 
 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type with fresh skolem constants
@@ -242,25 +256,20 @@ tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
 -- should become
 --     [(?k1 :: BOX), (?k2 :: BOX), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
 tcInstSigTyVars tyvars
-  = do { kvs' <- mapM tcInstSigTyVar kvs
-       ; tvs' <- mapM tcInstSigTyVar tvs
-       ; let ks_tvs = map updateKind tvs'  -- kind substitued tvs
-             updateKind tv = setTyVarKind tv (substTy subst (tyVarKind tv))
-             subst = zipTopTvSubst kvs (map mkTyVarTy kvs')
-       ; return (kvs' ++ ks_tvs) }
-  where
-    (kvs, tvs) = span (isSuperKind . tyVarKind) tyvars
-    -- This function is local because we apply a substitution on the
-    -- kinds of the type variables
-    tcInstSigTyVar :: TyVar -> TcM TcTyVar
-    tcInstSigTyVar tyvar
-      = do { uniq <- newMetaUnique
-           ; ref <- newMutVar Flexi
-           ; let name = setNameUnique (tyVarName tyvar) uniq
-                        -- Use the same OccName so that the tidy-er
-                        -- doesn't rename 'a' to 'a0' etc
-                 kind = tyVarKind tyvar
-           ; return (mkTcTyVar name kind (MetaTv SigTv ref)) }
+  = do { kvs' <- mapM (tcInstSigTyVar (mkTopTvSubst [])) kvs
+       ; tvs' <- mapM (tcInstSigTyVar (zipTopTvSubst kvs (map mkTyVarTy kvs'))) tvs
+       ; return (kvs' ++ tvs') }
+  where (kvs, tvs) = span (isSuperKind . tyVarKind) tyvars
+
+tcInstSigTyVar :: TvSubst -> TyVar -> TcM TcTyVar
+tcInstSigTyVar subst tyvar
+  = do { uniq <- newMetaUnique
+       ; ref <- newMutVar Flexi
+       ; let name = setNameUnique (tyVarName tyvar) uniq
+                    -- Use the same OccName so that the tidy-er
+                    -- doesn't rename 'a' to 'a0' etc
+             kind = substTy subst (tyVarKind tyvar)
+       ; return (mkTcTyVar name kind (MetaTv SigTv ref)) }
 \end{code}
 
 
diff --git a/compiler/types/Kind.lhs b/compiler/types/Kind.lhs
index 56458a9..2ca79ac 100644
--- a/compiler/types/Kind.lhs
+++ b/compiler/types/Kind.lhs
@@ -183,18 +183,23 @@ isKind k = isSuperKind (typeKind k)
 
 isSubKind :: Kind -> Kind -> Bool
 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
-isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
+
+isSubKind (FunTy a1 r1) (FunTy a2 r2)
+  = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
+
 isSubKind (TyConApp kc1 k1s) (TyConApp kc2 k2s)
   | isSuperKindTyCon kc1 =  -- handles BOX
     isSuperKindTyCon kc2 && null k1s && null k2s
+
   | isSuperKind (tyConKind kc1) =  -- handles not promoted kinds (*, #, (#), etc.)
     ASSERT( isSuperKind (tyConKind kc2) && null k1s && null k2s )
     kc1 `isSubKindCon` kc2
+
   | otherwise =  -- handles promoted kinds (List *, Nat, etc.)
     kc1 == kc2 && length k1s == length k2s && all (uncurry eqKind) (zip k1s k2s)
-isSubKind (TyVarTy kv1) (TyVarTy kv2) = kv1 == kv2
-isSubKind (ForAllTy {}) (ForAllTy {}) = panic "IA0: isSubKind on ForAllTy"
-isSubKind _ _ = False
+
+isSubKind k1 k2 = eqKind k1 k2
+
 
 isSubKindCon :: TyCon -> TyCon -> Bool
 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@