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 <g...@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] -- ~~~~~~~~~~~~~~~~~~~~~ _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
