X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcGadt.lhs;h=75d5c5461d8f912c2f4499a5fc5870cefe010cf6;hb=4ea5fe11fbc339a7a1bce13cbb2a2301772b493a;hp=e0725fb66ce6c102185af7c88975540829f1ec3e;hpb=143f4381d242e4a1c3174e8a0732a1e48f00a1aa;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcGadt.lhs b/compiler/typecheck/TcGadt.lhs index e0725fb..75d5c54 100644 --- a/compiler/typecheck/TcGadt.lhs +++ b/compiler/typecheck/TcGadt.lhs @@ -18,23 +18,25 @@ module TcGadt ( import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion ) import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion, - mkLeftCoercion, mkRightCoercion, - splitCoercionKind, decomposeCo ) + mkLeftCoercion, mkRightCoercion, mkCoKind, coercionKindPredTy, + splitCoercionKind, decomposeCo, coercionKind ) import TcType ( TvSubst(..), TvSubstEnv, substTy, mkTvSubst, substTyVar, zipTopTvSubst, typeKind, eqKind, isSubKind, repSplitAppTy_maybe, - tcView + tcView, tcGetTyVar_maybe ) -import Type ( Type, tyVarsOfType, tyVarsOfTypes ) +import Type ( Type, tyVarsOfType, tyVarsOfTypes, tcEqType, mkTyVarTy ) import TypeRep ( Type(..), PredType(..) ) import DataCon ( DataCon, dataConUnivTyVars, dataConEqSpec ) -import Var ( CoVar, TyVar, tyVarKind ) +import Var ( CoVar, TyVar, tyVarKind, varUnique ) import VarEnv import VarSet import ErrUtils ( Message ) import Maybes ( MaybeErr(..), isJust ) import Control.Monad ( foldM ) import Outputable +import Unique ( Unique ) +import UniqFM ( ufmToList ) #include "HsVersions.h" \end{code} @@ -47,32 +49,32 @@ import Outputable %************************************************************************ \begin{code} -data Refinement = Reft InScopeSet TvSubstEnv CoSubstEnv -type CoSubstEnv = TvSubstEnv -- Maps type variables to *coercions* --- INVARIANT: in the refinement (tsub, csub) --- forall a. (csub(a) :: a:=:tsub(a)) +data Refinement = Reft InScopeSet InternalReft +-- INVARIANT: a->(co,ty) then co :: (a:=:ty) +-- Not necessarily idemopotent instance Outputable Refinement where - ppr (Reft in_scope tv_env co_env) - = ptext SLIT("Refinment") <+> - braces (ppr tv_env $$ ppr co_env) + ppr (Reft in_scope env) + = ptext SLIT("Refinement") <+> + braces (ppr env) emptyRefinement :: Refinement -emptyRefinement = Reft emptyInScopeSet emptyVarEnv emptyVarEnv +emptyRefinement = (Reft emptyInScopeSet emptyVarEnv) + refineType :: Refinement -> Type -> (ExprCoFn, Type) -- Apply the refinement to the type. -- If (refineType r ty) = (co, ty') -- Then co :: ty:=:ty' -refineType (Reft in_scope tv_env co_env) ty - | not (isEmptyVarEnv tv_env), -- Common case - any (`elemVarEnv` tv_env) (varSetElems (tyVarsOfType ty)) +refineType (Reft in_scope env) ty + | not (isEmptyVarEnv env), -- Common case + any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty)) = (ExprCoFn (substTy co_subst ty), substTy tv_subst ty) | otherwise = (idCoercion, ty) -- The type doesn't mention any refined type variables where - tv_subst = mkTvSubst in_scope tv_env - co_subst = mkTvSubst in_scope co_env + tv_subst = mkTvSubst in_scope (mapVarEnv snd env) + co_subst = mkTvSubst in_scope (mapVarEnv fst env) refineResType :: Refinement -> Type -> (ExprCoFn, Type) -- Like refineType, but returns the 'sym' coercion @@ -135,23 +137,25 @@ Two refinements: -- The result is idempotent: the \begin{code} -gadtRefine (Reft in_scope tv_env1 co_env1) +gadtRefine (Reft in_scope env1) ex_tvs co_vars --- Precondition: fvs( co_vars ) # tv_env1 +-- Precondition: fvs( co_vars ) # env1 -- That is, the kinds of the co_vars are a -- fixed point of the incoming refinement - = initUM (tryToBind tv_set) $ + = ASSERT2( not $ any (`elemVarEnv` env1) (varSetElems $ tyVarsOfTypes $ map tyVarKind co_vars), + ppr env1 $$ ppr co_vars $$ ppr (map tyVarKind co_vars) ) + initUM (tryToBind tv_set) $ do { -- Run the unifier, starting with an empty env ; env2 <- foldM do_one emptyInternalReft co_vars -- Find the fixed point of the resulting -- non-idempotent substitution - ; let tv_env2 = tv_env1 `plusVarEnv` mapVarEnv snd env2 - co_env2 = co_env1 `plusVarEnv` mapVarEnv fst env2 - - ; return (Reft in_scope' (fixTvSubstEnv in_scope' tv_env2) - (fixTvSubstEnv in_scope' co_env2)) } + ; let tmp_env = env1 `plusVarEnv` env2 + out_env = fixTvCoEnv in_scope' tmp_env + ; WARN( not (null (badReftElts tmp_env)), ppr (badReftElts tmp_env) $$ ppr tmp_env ) + WARN( not (null (badReftElts out_env)), ppr (badReftElts out_env) $$ ppr out_env ) + return (Reft in_scope' out_env) } where tv_set = mkVarSet ex_tvs in_scope' = foldr extend in_scope co_vars @@ -196,9 +200,26 @@ tcUnifyTys bind_fn tys1 tys2 ---------------------------- -fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv - -- Find the fixed point of a TvSubstEnv +fixTvCoEnv :: InScopeSet -> InternalReft -> InternalReft + -- Find the fixed point of a Refinement -- (assuming it has no loops!) +fixTvCoEnv in_scope env + = fixpt + where + fixpt = mapVarEnv step env + + step (co, ty) = (co1, ty') + -- Apply fixpt one step: + -- Use refineType to get a substituted type, ty', and a coercion, co_fn, + -- which justifies the substitution. If the coercion is not the identity + -- then use transitivity with the original coercion + where + (co_fn, ty') = refineType (Reft in_scope fixpt) ty + co1 | ExprCoFn co'' <- co_fn = mkTransCoercion co co'' + | otherwise = ASSERT( isIdCoercion co_fn ) co + +----------------------------- +fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv fixTvSubstEnv in_scope env = fixpt where @@ -223,6 +244,8 @@ dataConCanMatch con tys tryToBind :: TyVarSet -> TyVar -> BindFlag tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe | otherwise = AvoidMe + + \end{code} @@ -238,6 +261,19 @@ type InternalReft = TyVarEnv (Coercion, Type) -- INVARIANT: a->(co,ty) then co :: (a:=:ty) -- Not necessarily idemopotent +badReftElts :: InternalReft -> [(Unique, (Coercion,Type))] +-- Return the BAD elements of the refinement +-- Should be empty; used in asserions only +badReftElts env + = filter (not . ok) (ufmToList env) + where + ok :: (Unique, (Coercion, Type)) -> Bool + ok (u, (co, ty)) | Just tv <- tcGetTyVar_maybe ty1 + = varUnique tv == u && ty `tcEqType` ty2 + | otherwise = False + where + (ty1,ty2) = coercionKind co + emptyInternalReft :: InternalReft emptyInternalReft = emptyVarEnv @@ -350,8 +386,8 @@ uUnrefined :: InternalReft -- An existing substitution to extend -> UM InternalReft -- We know that tv1 isn't refined --- PRE-CONDITION: in the call (uUnrefined r co tv ty ty'), we know that --- co :: tv:=:ty +-- PRE-CONDITION: in the call (uUnrefined r co tv1 ty2 ty2'), we know that +-- co :: tv1:=:ty2 uUnrefined subst co tv1 ty2 ty2' | Just ty2'' <- tcView ty2' @@ -365,7 +401,7 @@ uUnrefined subst co tv1 ty2 (TyVarTy tv2) = return subst -- Check to see whether tv2 is refined - | Just (co',ty') <- lookupVarEnv subst tv2 + | Just (co',ty') <- lookupVarEnv subst tv2 -- co' :: tv2:=:ty' = uUnrefined subst (mkTransCoercion co co') tv1 ty' ty' -- So both are unrefined; next, see if the kinds force the direction @@ -373,21 +409,21 @@ uUnrefined subst co tv1 ty2 (TyVarTy tv2) = do { b1 <- tvBindFlag tv1 ; b2 <- tvBindFlag tv2 ; case (b1,b2) of - (BindMe, _) -> bind tv1 ty2 + (BindMe, _) -> bind False tv1 ty2 - (AvoidMe, BindMe) -> bind tv2 ty1 - (AvoidMe, _) -> bind tv1 ty2 + (AvoidMe, BindMe) -> bind True tv2 ty1 + (AvoidMe, _) -> bind False tv1 ty2 (WildCard, WildCard) -> return subst (WildCard, Skolem) -> return subst - (WildCard, _) -> bind tv2 ty1 + (WildCard, _) -> bind True tv2 ty1 (Skolem, WildCard) -> return subst (Skolem, Skolem) -> failWith (misMatch ty1 ty2) - (Skolem, _) -> bind tv2 ty1 + (Skolem, _) -> bind True tv2 ty1 } - | k1 `isSubKind` k2 = bindTv subst co tv2 ty1 -- Must update tv2 + | k1 `isSubKind` k2 = bindTv subst (mkSymCoercion co) tv2 ty1 -- Must update tv2 | k2 `isSubKind` k1 = bindTv subst co tv1 ty2 -- Must update tv1 | otherwise = failWith (kindMisMatch tv1 ty2) @@ -395,7 +431,12 @@ uUnrefined subst co tv1 ty2 (TyVarTy tv2) ty1 = TyVarTy tv1 k1 = tyVarKind tv1 k2 = tyVarKind tv2 - bind tv ty = return (extendVarEnv subst tv (co,ty)) + bind swap tv ty = + ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty) + , (text "Refinement invariant failure: co = " <+> ppr co <+> ppr (coercionKindPredTy co) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty))) + return (extendVarEnv subst tv (co1,ty)) + where + co1 = if swap then mkSymCoercion co else co uUnrefined subst co tv1 ty2 ty2' -- ty2 is not a type variable | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2') @@ -419,7 +460,9 @@ substTvSet subst tvs Just (_,ty) -> substTvSet subst (tyVarsOfType ty) bindTv subst co tv ty -- ty is not a type variable - = do { b <- tvBindFlag tv + = ASSERT2( (coercionKindPredTy co `tcEqType` mkCoKind (mkTyVarTy tv) ty), + (text "Refinement invariant failure: co = " <+> ppr co <+> ppr (coercionKindPredTy co) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)) ) + do { b <- tvBindFlag tv ; case b of Skolem -> failWith (misMatch (TyVarTy tv) ty) WildCard -> return subst