[commit: ghc] ghc-kinds: fix double quantification in kind poly data types (58b1a1a)

[Julien Cretin]

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

On branch  : ghc-kinds

http://hackage.haskell.org/trac/ghc/changeset/58b1a1a0f44e3b1fdb7ccc336eaf993e8d2aa081

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

commit 58b1a1a0f44e3b1fdb7ccc336eaf993e8d2aa081
Author: Julien Cretin <ghc at ia0.eu>
Date:   Wed Sep 7 17:43:56 2011 +0200

    fix double quantification in kind poly data types

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

 compiler/typecheck/TcHsType.lhs     |   56 +++++++++++++++++++++++-----------
 compiler/typecheck/TcTyClsDecls.lhs |   10 ++++--
 compiler/types/Unify.lhs            |   11 +++----
 3 files changed, 49 insertions(+), 28 deletions(-)

diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index a76767a..a543d9c 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -20,7 +20,7 @@ module TcHsType (
 
                 -- Typechecking kinded types
 	tcHsKindedContext, tcHsKindedType, tcHsBangType,
-	tcTyVarBndrs, dsHsType, kcHsLPred, dsHsLPred,
+	tcTyVarBndrs, tcTyVarBndrsKindGen, dsHsType, kcHsLPred, dsHsLPred,
 	tcDataKindSig, ExpKind(..), EkCtxt(..),
 
 		-- Pattern type signatures
@@ -60,6 +60,7 @@ import Outputable
 import BuildTyCl ( buildPromotedDataTyCon )
 import FastString
 import Control.Monad ( unless, filterM )
+import Data.List ( mapAccumL )
 \end{code}
 
 
@@ -657,7 +658,7 @@ ds_type (HsSpliceTy _ _ kind)
 ds_type (HsQuasiQuoteTy {}) = panic "ds_type"	-- Eliminated by renamer
 ds_type (HsCoreTy ty)       = return ty
 
--- IA0: ds_type (HsLitTy _) = panic "IA0: ds_type"  -- IA0: UNDEFINED
+-- ds_type (HsLitTy _) = panic "IA0_UNDEFINED: ds_type"
 
 ds_type (HsExplicitListTy kind tys) = do
   kind' <- zonkTcKindToKind kind
@@ -783,24 +784,38 @@ tcTyVarBndrs bndrs thing_inside = do
     zonk (KindedTyVar name _ kind) = do { kind' <- zonkTcKindToKind kind
 				        ; return (mkTyVar name kind') }
 
+tcTyVarBndrsKindGen :: [LHsTyVarBndr Name] -> ([KindVar] -> [TyVar] -> TcM r) -> TcM r
+tcTyVarBndrsKindGen bndrs thing_inside = do
+    (kvs, kinds) <- kindGeneralizeKinds $ map (hsTyVarKind.unLoc) bndrs
+    let tyvars = zipWith mkTyVar (map hsLTyVarName bndrs) kinds
+    tcExtendTyVarEnv (kvs ++ tyvars) (thing_inside kvs tyvars)
+
+kindGeneralizeKinds :: [TcKind] -> TcM ([KindVar], [Kind])
+kindGeneralizeKinds kinds = do
+  kinds' <- mapM zonkTcKind kinds
+  flexis <- freeFlexisOfTypes kinds'
+  traceTc "generalizeKind 1" (ppr flexis <+> ppr kinds')
+  let (_, occs) = mapAccumL tidy_one emptyTidyOccEnv flexis
+      tidy_one env flexi = tidyOccName env (getOccName (tyVarName flexi))
+  kvs <- flip mapM (zip occs flexis) $ \(occ, flexi) -> do
+         span <- getSrcSpanM
+         uniq <- newUnique
+         let name = mkInternalName uniq occ span
+             kv = mkTcTyVar name (tyVarKind flexi) vanillaSkolemTv
+         writeMetaTyVar flexi (mkTyVarTy kv)
+         return kv
+  let flexiToKind kv = case lookup kv (zip flexis kvs) of
+                         Nothing -> return (mkTyVarTy kv)
+                         Just kv -> return (mkTyVarTy kv)
+  bodys <- mapM (zonkKind (mkZonkTcTyVar flexiToKind)) kinds'
+  traceTc "generalizeKind 2" (ppr kvs <+> ppr bodys)
+  return (kvs, bodys)
+
 kindGeneralizeKind :: TcKind -> TcM ( [KindVar]  -- these were flexi kind vars
-                                , Kind )     -- this is the old kind where flexis got zonked
+                                    , Kind )     -- this is the old kind where flexis got zonked
 kindGeneralizeKind kind = do
-  kind' <- zonkTcKind kind
-  flexis <- freeFlexisOfType kind'
-  kvs <- mapM zonkQuantifiedTyVar flexis
-  body <- zonkKind (mkZonkTcTyVar flexiToKind) kind'
-  traceTc "IA0_DEBUG generalizeKind" (ppr kvs <+> ppr body)
-  return (kvs, body)
-
-flexiToKind :: KindVar -> TcM Kind
-flexiToKind kv = do
-  isFlexi <- isFlexiMetaTyVar kv
-  if isFlexi
-    then do
-      kv' <- zonkQuantifiedTyVar kv
-      return (mkTyVarTy kv')
-    else return (mkTyVarTy kv)
+  (kvs, [kind']) <- kindGeneralizeKinds [kind]
+  return (kvs, kind')
 
 freeFlexisOfType :: Type -> TcM [Var]
 freeFlexisOfType ty = do
@@ -808,6 +823,11 @@ freeFlexisOfType ty = do
   -- IA0_TODO: remove in scope variables
   return fs
 
+freeFlexisOfTypes :: [Type] -> TcM [Var]
+freeFlexisOfTypes tys = do
+  fss <- mapM freeFlexisOfType tys
+  return $ varSetElems $ unionVarSets $ map mkVarSet fss
+
 -----------------------------------
 tcDataKindSig :: Maybe Kind -> TcM [TyVar]
 -- GADT decls can have a (perhaps partial) kind signature
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index ab9bb84..ac37e97 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -614,12 +614,12 @@ tcConDecl :: Bool		-- True <=> -XExistentialQuantificaton or -XGADTs
 tcConDecl existential_ok rep_tycon res_tmpl 	-- Data types
 	  con@(ConDecl {con_name = name, con_qvars = tvs, con_cxt = ctxt
                    , con_details = details, con_res = res_ty })
-  = addErrCtxt (dataConCtxt name)	$
-    tcTyVarBndrs tvs $ \ tvs' -> do
+  = addErrCtxt (dataConCtxt name) $
+    tcTyVarBndrsKindGen tvs $ \ kvs tvs' -> do
     { ctxt' <- tcHsKindedContext ctxt
     ; checkTc (existential_ok || conRepresentibleWithH98Syntax con)
 	      (badExistential name)
-    ; (univ_tvs, ex_tvs, eq_preds, res_ty') <- tcResultType res_tmpl tvs' res_ty
+    ; (univ_tvs, ex_tvs, eq_preds, res_ty') <- tcResultType res_tmpl (kvs ++ tvs') res_ty
     ; let 
 	tc_datacon is_infix field_lbls btys
 	  = do { (arg_tys, stricts) <- mapAndUnzipM tcConArg btys
@@ -936,10 +936,12 @@ checkValidDataCon tc con
               tc_kvs = fst $ splitForAllTys (tyConKind tc)
 	      res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys (tc_kvs ++ tc_tvs))
 	      actual_res_ty = dataConOrigResTy con
-	; checkTc (isJust (tcMatchTy (mkVarSet tc_tvs)
+	; checkTc (isJust (tcMatchTy (mkVarSet (tc_kvs ++ tc_tvs))
 				res_ty_tmpl
 				actual_res_ty))
 		  (badDataConTyCon con res_ty_tmpl actual_res_ty)
+             -- IA0_TODO: we should also check that kind variables
+             -- are only instantiated with kind variables
 	; checkValidMonoType (dataConOrigResTy con)
 		-- Disallow MkT :: T (forall a. a->a)
 		-- Reason: it's really the argument of an equality constraint
diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index 04f5e68..4c37cd2 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -34,8 +34,6 @@ import ErrUtils
 import Util
 import Maybes
 import FastString
-
-import Control.Monad (guard)
 \end{code}
 
 
@@ -168,7 +166,7 @@ match menv subst (TyVarTy tv1) ty2
   | tv1' `elemVarSet` me_tmpls menv
   = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
     then Nothing	-- Occurs check
-    else do { subst1 <- match_kind menv subst tv1 ty2
+    else do { subst1 <- match_kind menv subst (tyVarKind tv1) (typeKind ty2)
 			-- Note [Matching kinds]
 	    ; return (extendVarEnv subst1 tv1' ty2) }
 
@@ -202,11 +200,12 @@ match _ _ _ _
   = Nothing
 
 --------------
-match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
+match_kind :: MatchEnv -> TvSubstEnv -> Kind -> Kind -> Maybe TvSubstEnv
 -- Match the kind of the template tyvar with the kind of Type
 -- Note [Matching kinds]
-match_kind _ subst tv ty
-  = guard (typeKind ty `isSubKind` tyVarKind tv) >> return subst
+match_kind _ subst k1 k2
+  | k2 `isSubKind` k1 = return subst
+match_kind menv subst k1 k2 = match menv subst k1 k2
 
 -- Note [Matching kinds]
 -- ~~~~~~~~~~~~~~~~~~~~~