X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=63089b603e5e0af294996523edcbef8924d4db9d;hb=30c122df62ec75f9ed7f392f24c2925675bf1d06;hp=f99c56c0d4f1fcb1d45093cb5fc5294c6e29fb32;hpb=70918cf4a4d61d4752b18f29ce14c7d7f1fbce01;p=ghc-hetmet.git diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index f99c56c..63089b6 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -8,7 +8,9 @@ module Unify ( -- the "tc" prefix indicates that matching always -- respects newtypes (rather than looking through them) tcMatchTy, tcMatchTys, tcMatchTyX, - ruleMatchTyX, tcMatchPreds, MatchEnv(..) + ruleMatchTyX, tcMatchPreds, MatchEnv(..), + + dataConCannotMatch ) where #include "HsVersions.h" @@ -17,8 +19,12 @@ import Var import VarEnv import VarSet import Type +import Coercion +import TyCon +import DataCon import TypeRep import Outputable +import Util import Maybes \end{code} @@ -133,11 +139,12 @@ match :: MatchEnv -- For the most part this is pushed downwards -- in-scope set of the RnEnv2 -> Type -> Type -- Template and target respectively -> Maybe TvSubstEnv --- This matcher works on source types; that is, --- it respects NewTypes and PredType +-- This matcher works on core types; that is, it ignores PredTypes +-- Watch out if newtypes become transparent agin! +-- this matcher must respect newtypes -match menv subst ty1 ty2 | Just ty1' <- tcView ty1 = match menv subst ty1' ty2 - | Just ty2' <- tcView ty2 = match menv subst ty1 ty2' +match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2 + | Just ty2' <- coreView ty2 = match menv subst ty1 ty2' match menv subst (TyVarTy tv1) ty2 | tv1' `elemVarSet` me_tmpls menv @@ -145,10 +152,10 @@ match menv subst (TyVarTy tv1) ty2 Nothing -- No existing binding | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2)) -> Nothing -- Occurs check - | not (typeKind ty2 `isSubKind` tyVarKind tv1) - -> Nothing -- Kind mis-match - | otherwise - -> Just (extendVarEnv subst tv1' ty2) + | otherwise + -> do { subst1 <- match_kind menv subst tv1 ty2 + ; return (extendVarEnv subst1 tv1' ty2) } + -- Note [Matching kinds] Just ty1' -- There is an existing binding; check whether ty2 matches it | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2 @@ -161,7 +168,7 @@ match menv subst (TyVarTy tv1) ty2 | otherwise -- tv1 is not a template tyvar = case ty2 of TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst - other -> Nothing + _ -> Nothing where rn_env = me_env menv tv1' = rnOccL rn_env tv1 @@ -184,26 +191,177 @@ match menv subst (AppTy ty1a ty1b) ty2 = do { subst' <- match menv subst ty1a ty2a ; match menv subst' ty1b ty2b } -match menv subst ty1 ty2 +match _ _ _ _ = Nothing -------------- +match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv +-- Match the kind of the template tyvar with the kind of Type +-- Note [Matching kinds] +match_kind menv subst tv ty + | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv) + (ty3,ty4) = coercionKind ty + ; subst1 <- match menv subst ty1 ty3 + ; match menv subst1 ty2 ty4 } + | otherwise = if typeKind ty `isSubKind` tyVarKind tv + then Just subst + else Nothing + +-- Note [Matching kinds] +-- ~~~~~~~~~~~~~~~~~~~~~ +-- For ordinary type variables, we don't want (m a) to match (n b) +-- if say (a::*) and (b::*->*). This is just a yes/no issue. +-- +-- For coercion kinds matters are more complicated. If we have a +-- coercion template variable co::a~[b], where a,b are presumably also +-- template type variables, then we must match co's kind against the +-- kind of the actual argument, so as to give bindings to a,b. +-- +-- In fact I have no example in mind that *requires* this kind-matching +-- to instantiate template type variables, but it seems like the right +-- thing to do. C.f. Note [Matching variable types] in Rules.lhs + +-------------- +match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2 -------------- match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv) -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv -match_list fn subst [] [] = Just subst +match_list _ subst [] [] = Just subst match_list fn subst (ty1:tys1) (ty2:tys2) = do { subst' <- fn subst ty1 ty2 ; match_list fn subst' tys1 tys2 } -match_list fn subst tys1 tys2 = Nothing +match_list _ _ _ _ = Nothing -------------- +match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2) | c1 == c2 = match_tys menv subst tys1 tys2 match_pred menv subst (IParam n1 t1) (IParam n2 t2) | n1 == n2 = match menv subst t1 t2 -match_pred menv subst p1 p2 = Nothing +match_pred _ _ _ _ = Nothing \end{code} +%************************************************************************ +%* * + GADTs +%* * +%************************************************************************ + +Note [Pruning dead case alternatives] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider data T a where + T1 :: T Int + T2 :: T a + + newtype X = MkX Int + newtype Y = MkY Char + + type family F a + type instance F Bool = Int + +Now consider case x of { T1 -> e1; T2 -> e2 } + +The question before the house is this: if I know something about the type +of x, can I prune away the T1 alternative? + +Suppose x::T Char. It's impossible to construct a (T Char) using T1, + Answer = YES (clearly) + +Suppose x::T (F a), where 'a' is in scope. Then 'a' might be instantiated +to 'Bool', in which case x::T Int, so + ANSWER = NO (clearly) + +Suppose x::T X. Then *in Haskell* it's impossible to construct a (non-bottom) +value of type (T X) using T1. But *in FC* it's quite possible. The newtype +gives a coercion + CoX :: X ~ Int +So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value +of type (T X) constructed with T1. Hence + ANSWER = NO (surprisingly) + +Furthermore, this can even happen; see Trac #1251. GHC's newtype-deriving +mechanism uses a cast, just as above, to move from one dictionary to another, +in effect giving the programmer access to CoX. + +Finally, suppose x::T Y. Then *even in FC* we can't construct a +non-bottom value of type (T Y) using T1. That's because we can get +from Y to Char, but not to Int. + + +Here's a related question. data Eq a b where EQ :: Eq a a +Consider + case x of { EQ -> ... } + +Suppose x::Eq Int Char. Is the alternative dead? Clearly yes. + +What about x::Eq Int a, in a context where we have evidence that a~Char. +Then again the alternative is dead. + + + Summary + +We are really doing a test for unsatisfiability of the type +constraints implied by the match. And that is clearly, in general, a +hard thing to do. + +However, since we are simply dropping dead code, a conservative test +suffices. There is a continuum of tests, ranging from easy to hard, that +drop more and more dead code. + +For now we implement a very simple test: type variables match +anything, type functions (incl newtypes) match anything, and only +distinct data types fail to match. We can elaborate later. + +\begin{code} +dataConCannotMatch :: [Type] -> DataCon -> Bool +-- Returns True iff the data con *definitely cannot* match a +-- scrutinee of type (T tys) +-- where T is the type constructor for the data con +-- +dataConCannotMatch tys con + | null eq_spec = False -- Common + | all isTyVarTy tys = False -- Also common + | otherwise + = cant_match_s (map (substTyVar subst . fst) eq_spec) + (map snd eq_spec) + where + dc_tvs = dataConUnivTyVars con + eq_spec = dataConEqSpec con + subst = zipTopTvSubst dc_tvs tys + + cant_match_s :: [Type] -> [Type] -> Bool + cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 ) + or (zipWith cant_match tys1 tys2) + + cant_match :: Type -> Type -> Bool + cant_match t1 t2 + | Just t1' <- coreView t1 = cant_match t1' t2 + | Just t2' <- coreView t2 = cant_match t1 t2' + + cant_match (FunTy a1 r1) (FunTy a2 r2) + = cant_match a1 a2 || cant_match r1 r2 + + cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2) + | isDataTyCon tc1 && isDataTyCon tc2 + = tc1 /= tc2 || cant_match_s tys1 tys2 + + cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc + cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc + -- tc can't be FunTyCon by invariant + + cant_match (AppTy f1 a1) ty2 + | Just (f2, a2) <- repSplitAppTy_maybe ty2 + = cant_match f1 f2 || cant_match a1 a2 + cant_match ty1 (AppTy f2 a2) + | Just (f1, a1) <- repSplitAppTy_maybe ty1 + = cant_match f1 f2 || cant_match a1 a2 + + cant_match _ _ = False -- Safe! + +-- Things we could add; +-- foralls +-- look through newtypes +-- take account of tyvar bindings (EQ example above) +\end{code} \ No newline at end of file