X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcGadt.lhs;h=fd82201b763ca2fd00a65da9f463eaa8f3ab8e67;hb=bf1bf9fb07f1607aa66e7490b2df1ac1b62dd2d0;hp=e0725fb66ce6c102185af7c88975540829f1ec3e;hpb=143f4381d242e4a1c3174e8a0732a1e48f00a1aa;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcGadt.lhs b/compiler/typecheck/TcGadt.lhs index e0725fb..fd82201 100644 --- a/compiler/typecheck/TcGadt.lhs +++ b/compiler/typecheck/TcGadt.lhs @@ -1,4 +1,5 @@ % +% (c) The University of Glasgow 2006 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % @@ -10,33 +11,29 @@ \begin{code} module TcGadt ( - Refinement, emptyRefinement, gadtRefine, - refineType, refineResType, - dataConCanMatch, + Refinement, emptyRefinement, isEmptyRefinement, + matchRefine, + refineType, refinePred, refineResType, tcUnifyTys, BindFlag(..) ) where -import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion ) -import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion, - mkLeftCoercion, mkRightCoercion, - splitCoercionKind, decomposeCo ) -import TcType ( TvSubst(..), TvSubstEnv, substTy, mkTvSubst, - substTyVar, zipTopTvSubst, typeKind, - eqKind, isSubKind, repSplitAppTy_maybe, - tcView - ) -import Type ( Type, tyVarsOfType, tyVarsOfTypes ) -import TypeRep ( Type(..), PredType(..) ) -import DataCon ( DataCon, dataConUnivTyVars, dataConEqSpec ) -import Var ( CoVar, TyVar, tyVarKind ) +#include "HsVersions.h" + +import HsSyn +import Coercion +import Type + +import TypeRep +import Var import VarEnv import VarSet -import ErrUtils ( Message ) -import Maybes ( MaybeErr(..), isJust ) -import Control.Monad ( foldM ) +import ErrUtils +import Maybes +import Control.Monad import Outputable - -#include "HsVersions.h" +import TcType +import UniqFM +import FastString \end{code} @@ -47,122 +44,129 @@ 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 + +type InternalReft = TyVarEnv (Coercion, Type) +-- 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) +isEmptyRefinement :: Refinement -> Bool +isEmptyRefinement (Reft _ env) = isEmptyVarEnv env + +refineType :: Refinement -> Type -> Maybe (Coercion, 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)) - = (ExprCoFn (substTy co_subst ty), substTy tv_subst ty) +-- Nothing => the refinement does nothing to this type +refineType (Reft in_scope env) ty + | not (isEmptyVarEnv env), -- Common case + any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty)) + = Just (substTy co_subst ty, substTy tv_subst ty) | otherwise - = (idCoercion, ty) -- The type doesn't mention any refined type variables + = Nothing -- 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) +refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType) +refinePred (Reft in_scope env) pred + | not (isEmptyVarEnv env), -- Common case + any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred)) + = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred) + | otherwise + = Nothing -- The type doesn't mention any refined type variables + where + tv_subst = mkTvSubst in_scope (mapVarEnv snd env) + co_subst = mkTvSubst in_scope (mapVarEnv fst env) + +refineResType :: Refinement -> Type -> (HsWrapper, Type) -- Like refineType, but returns the 'sym' coercion -- If (refineResType r ty) = (co, ty') -- Then co :: ty':=:ty +-- It's convenient to return a HsWrapper here refineResType reft ty = case refineType reft ty of - (ExprCoFn co, ty1) -> (ExprCoFn (mkSymCoercion co), ty1) - (id_co, ty1) -> ASSERT( isIdCoercion id_co ) - (idCoercion, ty1) + Just (co, ty1) -> (WpCo (mkSymCoercion co), ty1) + Nothing -> (idHsWrapper, ty) \end{code} %************************************************************************ %* * - Generating a type refinement + Simple generation of a type refinement %* * %************************************************************************ \begin{code} -gadtRefine :: Refinement - -> [TyVar] -- Bind these by preference - -> [CoVar] - -> MaybeErr Message Refinement +matchRefine :: [CoVar] -> Refinement \end{code} -(gadtRefine cvs) takes a list of coercion variables, and returns a -list of coercions, obtained by unifying the types equated by the -incoming coercions. The returned coercions all have kinds of form -(a:=:ty), where a is a rigid type variable. - -Example: - gadtRefine [c :: (a,Int):=:(Bool,b)] - = [ right (left c) :: a:=:Bool, - sym (right c) :: b:=:Int ] - -That is, given evidence 'c' that (a,Int)=(Bool,b), it returns derived -evidence in easy-to-use form. In particular, given any e::ty, we know -that: - e `cast` ty[right (left c)/a, sym (right c)/b] - :: ty [Bool/a, Int/b] - -Two refinements: - -- It can fail, if the coercion is unsatisfiable. - -- It's biased, by being given a set of type variables to bind - when there is a choice. Example: - MkT :: forall a. a -> T [a] - f :: forall b. T [b] -> b - f x = let v = case x of { MkT y -> y } - in ... - Here we want to bind [a->b], not the other way round, because - in this example the return type is wobbly, and we want the - program to typecheck - - --- E.g. (a, Bool, right (left c)) --- INVARIANT: in the triple (tv, ty, co), we have (co :: tv:=:ty) --- The result is idempotent: the +Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2 +is a specialisation of ty1, produce a type refinement that maps the variables +of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg, + + matchRefine (co :: [(a, b)] ~ [(c, Maybe d)]) + = { right (left (right co)) :: a ~ c + , right (right co) :: b ~ Maybe d + } + +Precondition: The rhs types must indeed be a specialisation of the lhs types; + i.e., some free variables of the lhs are replaced with either distinct free + variables or proper type terms to obtain the rhs. (We don't perform full + unification or type matching here!) + +NB: matchRefine does *not* expand the type synonyms. \begin{code} -gadtRefine (Reft in_scope tv_env1 co_env1) - ex_tvs co_vars --- Precondition: fvs( co_vars ) # tv_env1 --- That is, the kinds of the co_vars are a --- fixed point of the incoming refinement - - = 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)) } +matchRefine co_vars + = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars)) where - tv_set = mkVarSet ex_tvs - in_scope' = foldr extend in_scope co_vars + in_scope = foldr extend emptyInScopeSet co_vars + + -- For each co_var, add it *and* the tyvars it mentions, to in_scope extend co_var in_scope - = extendInScopeSetSet (extendInScopeSet in_scope co_var) - (tyVarsOfType (tyVarKind co_var)) - - do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2 - where - (ty1,ty2) = splitCoercionKind (tyVarKind co_var) -\end{code} + = extendInScopeSetSet in_scope $ + extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var + + refineOne co_var = refine (TyVarTy co_var) ty1 ty2 + where + (ty1, ty2) = splitCoercionKind (tyVarKind co_var) + + refine co (TyVarTy tv) ty = unitVarEnv tv (co, ty) + refine co (TyConApp _ tys) (TyConApp _ tys') = refineArgs co tys tys' + refine co (NoteTy _ ty) ty' = refine co ty ty' + refine co ty (NoteTy _ ty') = refine co ty ty' + refine _ (PredTy _) (PredTy _) = + error "TcGadt.matchRefine: PredTy" + refine co (FunTy arg res) (FunTy arg' res') = + refine (mkRightCoercion (mkLeftCoercion co)) arg arg' + `plusVarEnv` + refine (mkRightCoercion co) res res' + refine co (AppTy fun arg) (AppTy fun' arg') = + refine (mkLeftCoercion co) fun fun' + `plusVarEnv` + refine (mkRightCoercion co) arg arg' + refine co (ForAllTy tv ty) (ForAllTy _tv ty') = + refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv + refine _ _ _ = error "RcGadt.matchRefine: mismatch" + + refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft + refineArgs co tys tys' = + fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys') + where + refineArg (ty, ty') (reft, coWrapper) + = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft, + mkLeftCoercion . coWrapper) +\end{code} + %************************************************************************ %* * @@ -196,33 +200,16 @@ tcUnifyTys bind_fn tys1 tys2 ---------------------------- +-- XXX Can we do this more nicely, by exploiting laziness? +-- Or avoid needing it in the first place? fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv - -- Find the fixed point of a TvSubstEnv - -- (assuming it has no loops!) -fixTvSubstEnv in_scope env - = fixpt - where - fixpt = mapVarEnv (substTy (mkTvSubst in_scope fixpt)) env - ----------------------------- -dataConCanMatch :: DataCon -> [Type] -> Bool --- Returns True iff the data con can match a scrutinee of type (T tys) --- where T is the type constructor for the data con --- --- Instantiate the equations and try to unify them -dataConCanMatch con tys - = isJust (tcUnifyTys (\tv -> BindMe) - (map (substTyVar subst . fst) eq_spec) - (map snd eq_spec)) +fixTvSubstEnv in_scope env = f env where - dc_tvs = dataConUnivTyVars con - eq_spec = dataConEqSpec con - subst = zipTopTvSubst dc_tvs tys + f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e + in if and $ eltsUFM $ intersectUFM_C tcEqType e e' + then e + else f e' ----------------------------- -tryToBind :: TyVarSet -> TyVar -> BindFlag -tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe - | otherwise = AvoidMe \end{code} @@ -233,11 +220,6 @@ tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe %************************************************************************ \begin{code} -type InternalReft = TyVarEnv (Coercion, Type) - --- INVARIANT: a->(co,ty) then co :: (a:=:ty) --- Not necessarily idemopotent - emptyInternalReft :: InternalReft emptyInternalReft = emptyVarEnv @@ -338,11 +320,12 @@ uVar swap subst co tv1 ty -> unify subst (mkTransCoercion (mkSymCoercion co') co) ty' ty -- No, continue - Nothing -> uUnrefined subst (if swap then mkSymCoercion co else co) + Nothing -> uUnrefined swap subst co tv1 ty ty -uUnrefined :: InternalReft -- An existing substitution to extend +uUnrefined :: Bool -- Whether the input is swapped + -> InternalReft -- An existing substitution to extend -> Coercion -> TyVar -- Type variable to be unified -> Type -- with this type @@ -350,60 +333,62 @@ 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 False r co tv1 ty2 ty2'), we know that +-- co :: tv1:=:ty2 +-- and if the first argument is True instead, we know +-- co :: ty2:=:tv1 -uUnrefined subst co tv1 ty2 ty2' +uUnrefined swap subst co tv1 ty2 ty2' | Just ty2'' <- tcView ty2' - = uUnrefined subst co tv1 ty2 ty2'' -- Unwrap synonyms + = uUnrefined swap subst co tv1 ty2 ty2'' -- Unwrap synonyms -- This is essential, in case we have -- type Foo a = a -- and then unify a :=: Foo a -uUnrefined subst co tv1 ty2 (TyVarTy tv2) +uUnrefined swap subst co tv1 ty2 (TyVarTy tv2) | tv1 == tv2 -- Same type variable = return subst -- Check to see whether tv2 is refined - | Just (co',ty') <- lookupVarEnv subst tv2 - = uUnrefined subst (mkTransCoercion co co') tv1 ty' ty' + | Just (co',ty') <- lookupVarEnv subst tv2 -- co' :: tv2:=:ty' + = uUnrefined False subst (mkTransCoercion (doSwap swap co) co') tv1 ty' ty' -- So both are unrefined; next, see if the kinds force the direction | eqKind k1 k2 -- Can update either; so check the bind-flags = do { b1 <- tvBindFlag tv1 ; b2 <- tvBindFlag tv2 ; case (b1,b2) of - (BindMe, _) -> bind tv1 ty2 + (BindMe, _) -> bind swap tv1 ty2 - (AvoidMe, BindMe) -> bind tv2 ty1 - (AvoidMe, _) -> bind tv1 ty2 + (AvoidMe, BindMe) -> bind (not swap) tv2 ty1 + (AvoidMe, _) -> bind swap tv1 ty2 (WildCard, WildCard) -> return subst (WildCard, Skolem) -> return subst - (WildCard, _) -> bind tv2 ty1 + (WildCard, _) -> bind (not swap) tv2 ty1 (Skolem, WildCard) -> return subst (Skolem, Skolem) -> failWith (misMatch ty1 ty2) - (Skolem, _) -> bind tv2 ty1 + (Skolem, _) -> bind (not swap) tv2 ty1 } - | k1 `isSubKind` k2 = bindTv subst co tv2 ty1 -- Must update tv2 - | k2 `isSubKind` k1 = bindTv subst co tv1 ty2 -- Must update tv1 + | k1 `isSubKind` k2 = bindTv (not swap) subst co tv2 ty1 -- Must update tv2 + | k2 `isSubKind` k1 = bindTv swap subst co tv1 ty2 -- Must update tv1 | otherwise = failWith (kindMisMatch tv1 ty2) where ty1 = TyVarTy tv1 k1 = tyVarKind tv1 k2 = tyVarKind tv2 - bind tv ty = return (extendVarEnv subst tv (co,ty)) + bind swap tv ty = extendReft swap subst tv co ty -uUnrefined subst co tv1 ty2 ty2' -- ty2 is not a type variable +uUnrefined swap subst co tv1 ty2 ty2' -- ty2 is not a type variable | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2') = failWith (occursCheck tv1 ty2) -- Occurs check | not (k2 `isSubKind` k1) = failWith (kindMisMatch tv1 ty2) -- Kind check | otherwise - = bindTv subst co tv1 ty2 -- Bind tyvar to the synonym if poss + = bindTv swap subst co tv1 ty2 -- Bind tyvar to the synonym if poss where k1 = tyVarKind tv1 k2 = typeKind ty2' @@ -418,13 +403,30 @@ substTvSet subst tvs Nothing -> unitVarSet tv Just (_,ty) -> substTvSet subst (tyVarsOfType ty) -bindTv subst co tv ty -- ty is not a type variable - = do { b <- tvBindFlag tv +bindTv swap subst co tv ty -- ty is not a type variable + = do { b <- tvBindFlag tv ; case b of Skolem -> failWith (misMatch (TyVarTy tv) ty) WildCard -> return subst - other -> return (extendVarEnv subst tv (co,ty)) + other -> extendReft swap subst tv co ty } + +doSwap :: Bool -> Coercion -> Coercion +doSwap swap co = if swap then mkSymCoercion co else co + +extendReft :: Bool + -> InternalReft + -> TyVar + -> Coercion + -> Type + -> UM InternalReft +extendReft swap subst tv co ty + = ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty), + (text "Refinement invariant failure: co = " <+> ppr co1 <+> ppr (coercionKindPredTy co1) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)) ) + return (extendVarEnv subst tv (co1, ty)) + where + co1 = doSwap swap co + \end{code} %************************************************************************ @@ -496,4 +498,4 @@ kindMisMatch tv1 t2 occursCheck tv ty = hang (ptext SLIT("Can't construct the infinite type")) 2 (ppr tv <+> equals <+> ppr ty) -\end{code} \ No newline at end of file +\end{code}