2 % (c) The University of Glasgow 2006
8 -- the "tc" prefix indicates that matching always
9 -- respects newtypes (rather than looking through them)
10 tcMatchTy, tcMatchTys, tcMatchTyX,
11 ruleMatchTyX, tcMatchPreds, MatchEnv(..),
16 -- XXX This define is a bit of a hack, and should be done more nicely
17 #define FAST_STRING_NOT_NEEDED 1
18 #include "HsVersions.h"
34 %************************************************************************
38 %************************************************************************
41 Matching is much tricker than you might think.
43 1. The substitution we generate binds the *template type variables*
44 which are given to us explicitly.
46 2. We want to match in the presence of foralls;
47 e.g (forall a. t1) ~ (forall b. t2)
49 That is what the RnEnv2 is for; it does the alpha-renaming
50 that makes it as if a and b were the same variable.
51 Initialising the RnEnv2, so that it can generate a fresh
52 binder when necessary, entails knowing the free variables of
55 3. We must be careful not to bind a template type variable to a
56 locally bound variable. E.g.
57 (forall a. x) ~ (forall b. b)
58 where x is the template type variable. Then we do not want to
59 bind x to a/b! This is a kind of occurs check.
60 The necessary locals accumulate in the RnEnv2.
65 = ME { me_tmpls :: VarSet -- Template tyvars
66 , me_env :: RnEnv2 -- Renaming envt for nested foralls
67 } -- In-scope set includes template tyvars
69 tcMatchTy :: TyVarSet -- Template tyvars
72 -> Maybe TvSubst -- One-shot; in principle the template
73 -- variables could be free in the target
75 tcMatchTy tmpls ty1 ty2
76 = case match menv emptyTvSubstEnv ty1 ty2 of
77 Just subst_env -> Just (TvSubst in_scope subst_env)
80 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
81 in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
82 -- We're assuming that all the interesting
83 -- tyvars in tys1 are in tmpls
85 tcMatchTys :: TyVarSet -- Template tyvars
88 -> Maybe TvSubst -- One-shot; in principle the template
89 -- variables could be free in the target
91 tcMatchTys tmpls tys1 tys2
92 = case match_tys menv emptyTvSubstEnv tys1 tys2 of
93 Just subst_env -> Just (TvSubst in_scope subst_env)
96 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
97 in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
98 -- We're assuming that all the interesting
99 -- tyvars in tys1 are in tmpls
101 -- This is similar, but extends a substitution
102 tcMatchTyX :: TyVarSet -- Template tyvars
103 -> TvSubst -- Substitution to extend
107 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
108 = case match menv subst_env ty1 ty2 of
109 Just subst_env -> Just (TvSubst in_scope subst_env)
112 menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
115 :: [TyVar] -- Bind these
116 -> [PredType] -> [PredType]
118 tcMatchPreds tmpls ps1 ps2
119 = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
121 menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
122 in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
124 -- This one is called from the expression matcher, which already has a MatchEnv in hand
125 ruleMatchTyX :: MatchEnv
126 -> TvSubstEnv -- Substitution to extend
131 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export
134 Now the internals of matching
137 match :: MatchEnv -- For the most part this is pushed downwards
138 -> TvSubstEnv -- Substitution so far:
139 -- Domain is subset of template tyvars
140 -- Free vars of range is subset of
141 -- in-scope set of the RnEnv2
142 -> Type -> Type -- Template and target respectively
144 -- This matcher works on core types; that is, it ignores PredTypes
145 -- Watch out if newtypes become transparent agin!
146 -- this matcher must respect newtypes
148 match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
149 | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
151 match menv subst (TyVarTy tv1) ty2
152 | tv1' `elemVarSet` me_tmpls menv
153 = case lookupVarEnv subst tv1' of
154 Nothing -- No existing binding
155 | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
156 -> Nothing -- Occurs check
158 -> do { subst1 <- match_kind menv subst tv1 ty2
159 ; return (extendVarEnv subst1 tv1' ty2) }
160 -- Note [Matching kinds]
162 Just ty1' -- There is an existing binding; check whether ty2 matches it
163 | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
164 -- ty1 has no locally-bound variables, hence nukeRnEnvL
165 -- Note tcEqType...we are doing source-type matching here
167 | otherwise -> Nothing -- ty2 doesn't match
170 | otherwise -- tv1 is not a template tyvar
172 TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
176 tv1' = rnOccL rn_env tv1
178 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2)
179 = match menv' subst ty1 ty2
180 where -- Use the magic of rnBndr2 to go under the binders
181 menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
183 match menv subst (PredTy p1) (PredTy p2)
184 = match_pred menv subst p1 p2
185 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2)
186 | tc1 == tc2 = match_tys menv subst tys1 tys2
187 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
188 = do { subst' <- match menv subst ty1a ty2a
189 ; match menv subst' ty1b ty2b }
190 match menv subst (AppTy ty1a ty1b) ty2
191 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
192 -- 'repSplit' used because the tcView stuff is done above
193 = do { subst' <- match menv subst ty1a ty2a
194 ; match menv subst' ty1b ty2b }
200 match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
201 -- Match the kind of the template tyvar with the kind of Type
202 -- Note [Matching kinds]
203 match_kind menv subst tv ty
204 | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
205 (ty3,ty4) = coercionKind ty
206 ; subst1 <- match menv subst ty1 ty3
207 ; match menv subst1 ty2 ty4 }
208 | otherwise = if typeKind ty `isSubKind` tyVarKind tv
212 -- Note [Matching kinds]
213 -- ~~~~~~~~~~~~~~~~~~~~~
214 -- For ordinary type variables, we don't want (m a) to match (n b)
215 -- if say (a::*) and (b::*->*). This is just a yes/no issue.
217 -- For coercion kinds matters are more complicated. If we have a
218 -- coercion template variable co::a~[b], where a,b are presumably also
219 -- template type variables, then we must match co's kind against the
220 -- kind of the actual argument, so as to give bindings to a,b.
222 -- In fact I have no example in mind that *requires* this kind-matching
223 -- to instantiate template type variables, but it seems like the right
224 -- thing to do. C.f. Note [Matching variable types] in Rules.lhs
227 match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
228 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
231 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
232 -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
233 match_list _ subst [] [] = Just subst
234 match_list fn subst (ty1:tys1) (ty2:tys2) = do { subst' <- fn subst ty1 ty2
235 ; match_list fn subst' tys1 tys2 }
236 match_list _ _ _ _ = Nothing
239 match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv
240 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
241 | c1 == c2 = match_tys menv subst tys1 tys2
242 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
243 | n1 == n2 = match menv subst t1 t2
244 match_pred _ _ _ _ = Nothing
248 %************************************************************************
252 %************************************************************************
254 Note [Pruning dead case alternatives]
255 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
256 Consider data T a where
264 type instance F Bool = Int
266 Now consider case x of { T1 -> e1; T2 -> e2 }
268 The question before the house is this: if I know something about the type
269 of x, can I prune away the T1 alternative?
271 Suppose x::T Char. It's impossible to construct a (T Char) using T1,
272 Answer = YES (clearly)
274 Suppose x::T (F a), where 'a' is in scope. Then 'a' might be instantiated
275 to 'Bool', in which case x::T Int, so
276 ANSWER = NO (clearly)
278 Suppose x::T X. Then *in Haskell* it's impossible to construct a (non-bottom)
279 value of type (T X) using T1. But *in FC* it's quite possible. The newtype
282 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
283 of type (T X) constructed with T1. Hence
284 ANSWER = NO (surprisingly)
286 Furthermore, this can even happen; see Trac #1251. GHC's newtype-deriving
287 mechanism uses a cast, just as above, to move from one dictionary to another,
288 in effect giving the programmer access to CoX.
290 Finally, suppose x::T Y. Then *even in FC* we can't construct a
291 non-bottom value of type (T Y) using T1. That's because we can get
292 from Y to Char, but not to Int.
295 Here's a related question. data Eq a b where EQ :: Eq a a
297 case x of { EQ -> ... }
299 Suppose x::Eq Int Char. Is the alternative dead? Clearly yes.
301 What about x::Eq Int a, in a context where we have evidence that a~Char.
302 Then again the alternative is dead.
307 We are really doing a test for unsatisfiability of the type
308 constraints implied by the match. And that is clearly, in general, a
311 However, since we are simply dropping dead code, a conservative test
312 suffices. There is a continuum of tests, ranging from easy to hard, that
313 drop more and more dead code.
315 For now we implement a very simple test: type variables match
316 anything, type functions (incl newtypes) match anything, and only
317 distinct data types fail to match. We can elaborate later.
320 dataConCannotMatch :: [Type] -> DataCon -> Bool
321 -- Returns True iff the data con *definitely cannot* match a
322 -- scrutinee of type (T tys)
323 -- where T is the type constructor for the data con
325 dataConCannotMatch tys con
326 | null eq_spec = False -- Common
327 | all isTyVarTy tys = False -- Also common
329 = cant_match_s (map (substTyVar subst . fst) eq_spec)
332 dc_tvs = dataConUnivTyVars con
333 eq_spec = dataConEqSpec con
334 subst = zipTopTvSubst dc_tvs tys
336 cant_match_s :: [Type] -> [Type] -> Bool
337 cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
338 or (zipWith cant_match tys1 tys2)
340 cant_match :: Type -> Type -> Bool
342 | Just t1' <- coreView t1 = cant_match t1' t2
343 | Just t2' <- coreView t2 = cant_match t1 t2'
345 cant_match (FunTy a1 r1) (FunTy a2 r2)
346 = cant_match a1 a2 || cant_match r1 r2
348 cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
349 | isDataTyCon tc1 && isDataTyCon tc2
350 = tc1 /= tc2 || cant_match_s tys1 tys2
352 cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
353 cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
354 -- tc can't be FunTyCon by invariant
356 cant_match (AppTy f1 a1) ty2
357 | Just (f2, a2) <- repSplitAppTy_maybe ty2
358 = cant_match f1 f2 || cant_match a1 a2
359 cant_match ty1 (AppTy f2 a2)
360 | Just (f1, a1) <- repSplitAppTy_maybe ty1
361 = cant_match f1 f2 || cant_match a1 a2
363 cant_match _ _ = False -- Safe!
365 -- Things we could add;
367 -- look through newtypes
368 -- take account of tyvar bindings (EQ example above)