The Core type-matcher should look through PredTypes
[ghc.git] / compiler / types / Unify.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 \begin{code}
6 {-# OPTIONS -w #-}
7 -- The above warning supression flag is a temporary kludge.
8 -- While working on this module you are encouraged to remove it and fix
9 -- any warnings in the module. See
10 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
11 -- for details
12
13 module Unify ( 
14         -- Matching of types: 
15         --      the "tc" prefix indicates that matching always
16         --      respects newtypes (rather than looking through them)
17         tcMatchTy, tcMatchTys, tcMatchTyX, 
18         ruleMatchTyX, tcMatchPreds, MatchEnv(..),
19         
20         dataConCannotMatch
21    ) where
22
23 #include "HsVersions.h"
24
25 import Var
26 import VarEnv
27 import VarSet
28 import Type
29 import Coercion
30 import TyCon
31 import DataCon
32 import TypeRep
33 import Outputable
34 import Util
35 import Maybes
36 \end{code}
37
38
39 %************************************************************************
40 %*                                                                      *
41                 Matching
42 %*                                                                      *
43 %************************************************************************
44
45
46 Matching is much tricker than you might think.
47
48 1. The substitution we generate binds the *template type variables*
49    which are given to us explicitly.
50
51 2. We want to match in the presence of foralls; 
52         e.g     (forall a. t1) ~ (forall b. t2)
53
54    That is what the RnEnv2 is for; it does the alpha-renaming
55    that makes it as if a and b were the same variable.
56    Initialising the RnEnv2, so that it can generate a fresh
57    binder when necessary, entails knowing the free variables of
58    both types.
59
60 3. We must be careful not to bind a template type variable to a
61    locally bound variable.  E.g.
62         (forall a. x) ~ (forall b. b)
63    where x is the template type variable.  Then we do not want to
64    bind x to a/b!  This is a kind of occurs check.
65    The necessary locals accumulate in the RnEnv2.
66
67
68 \begin{code}
69 data MatchEnv
70   = ME  { me_tmpls :: VarSet    -- Template tyvars
71         , me_env   :: RnEnv2    -- Renaming envt for nested foralls
72         }                       --   In-scope set includes template tyvars
73
74 tcMatchTy :: TyVarSet           -- Template tyvars
75           -> Type               -- Template
76           -> Type               -- Target
77           -> Maybe TvSubst      -- One-shot; in principle the template
78                                 -- variables could be free in the target
79
80 tcMatchTy tmpls ty1 ty2
81   = case match menv emptyTvSubstEnv ty1 ty2 of
82         Just subst_env -> Just (TvSubst in_scope subst_env)
83         Nothing        -> Nothing
84   where
85     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
86     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
87         -- We're assuming that all the interesting 
88         -- tyvars in tys1 are in tmpls
89
90 tcMatchTys :: TyVarSet          -- Template tyvars
91            -> [Type]            -- Template
92            -> [Type]            -- Target
93            -> Maybe TvSubst     -- One-shot; in principle the template
94                                 -- variables could be free in the target
95
96 tcMatchTys tmpls tys1 tys2
97   = case match_tys menv emptyTvSubstEnv tys1 tys2 of
98         Just subst_env -> Just (TvSubst in_scope subst_env)
99         Nothing        -> Nothing
100   where
101     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
102     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
103         -- We're assuming that all the interesting 
104         -- tyvars in tys1 are in tmpls
105
106 -- This is similar, but extends a substitution
107 tcMatchTyX :: TyVarSet          -- Template tyvars
108            -> TvSubst           -- Substitution to extend
109            -> Type              -- Template
110            -> Type              -- Target
111            -> Maybe TvSubst
112 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
113   = case match menv subst_env ty1 ty2 of
114         Just subst_env -> Just (TvSubst in_scope subst_env)
115         Nothing        -> Nothing
116   where
117     menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
118
119 tcMatchPreds
120         :: [TyVar]                      -- Bind these
121         -> [PredType] -> [PredType]
122         -> Maybe TvSubstEnv
123 tcMatchPreds tmpls ps1 ps2
124   = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
125   where
126     menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
127     in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
128
129 -- This one is called from the expression matcher, which already has a MatchEnv in hand
130 ruleMatchTyX :: MatchEnv 
131          -> TvSubstEnv          -- Substitution to extend
132          -> Type                -- Template
133          -> Type                -- Target
134          -> Maybe TvSubstEnv
135
136 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
137 \end{code}
138
139 Now the internals of matching
140
141 \begin{code}
142 match :: MatchEnv       -- For the most part this is pushed downwards
143       -> TvSubstEnv     -- Substitution so far:
144                         --   Domain is subset of template tyvars
145                         --   Free vars of range is subset of 
146                         --      in-scope set of the RnEnv2
147       -> Type -> Type   -- Template and target respectively
148       -> Maybe TvSubstEnv
149 -- This matcher works on core types; that is, it ignores PredTypes
150 -- Watch out if newtypes become transparent agin!
151 --      this matcher must respect newtypes
152
153 match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
154                          | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
155
156 match menv subst (TyVarTy tv1) ty2
157   | tv1' `elemVarSet` me_tmpls menv
158   = case lookupVarEnv subst tv1' of
159         Nothing         -- No existing binding
160             | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
161             -> Nothing  -- Occurs check
162             | otherwise 
163             -> do { subst1 <- match_kind menv subst tv1 ty2
164                   ; return (extendVarEnv subst tv1' ty2) }
165
166         Just ty1'       -- There is an existing binding; check whether ty2 matches it
167             | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
168                 -- ty1 has no locally-bound variables, hence nukeRnEnvL
169                 -- Note tcEqType...we are doing source-type matching here
170             -> Just subst
171             | otherwise -> Nothing      -- ty2 doesn't match
172             
173
174    | otherwise  -- tv1 is not a template tyvar
175    = case ty2 of
176         TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
177         other                                   -> Nothing
178   where
179     rn_env = me_env menv
180     tv1' = rnOccL rn_env tv1
181
182 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2) 
183   = match menv' subst ty1 ty2
184   where         -- Use the magic of rnBndr2 to go under the binders
185     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
186
187 match menv subst (PredTy p1) (PredTy p2) 
188   = match_pred menv subst p1 p2
189 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
190   | tc1 == tc2 = match_tys menv subst tys1 tys2
191 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
192   = do { subst' <- match menv subst ty1a ty2a
193        ; match menv subst' ty1b ty2b }
194 match menv subst (AppTy ty1a ty1b) ty2
195   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
196         -- 'repSplit' used because the tcView stuff is done above
197   = do { subst' <- match menv subst ty1a ty2a
198        ; match menv subst' ty1b ty2b }
199
200 match menv subst ty1 ty2
201   = Nothing
202
203 --------------
204 match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
205 -- Match the kind of the template tyvar with the kind of Type
206 -- Note [Matching kinds]
207 match_kind menv subst tv ty
208   | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
209                           (ty3,ty4) = coercionKind ty
210                     ; subst1 <- match menv subst ty1 ty3
211                     ; match menv subst1 ty2 ty4 }
212   | otherwise  = if typeKind ty `isSubKind` tyVarKind tv
213                  then Just subst
214                  else Nothing
215
216 -- Note [Matching kinds]
217 -- ~~~~~~~~~~~~~~~~~~~~~
218 -- For ordinary type variables, we don't want (m a) to match (n b) 
219 -- if say (a::*) and (b::*->*).  This is just a yes/no issue. 
220 --
221 -- For coercion kinds matters are more complicated.  If we have a 
222 -- coercion template variable co::a~[b], where a,b are presumably also
223 -- template type variables, then we must match co's kind against the 
224 -- kind of the actual argument, so as to give bindings to a,b.  
225 --
226 -- In fact I have no example in mind that *requires* this kind-matching
227 -- to instantiate template type variables, but it seems like the right
228 -- thing to do.  C.f. Note [Matching variable types] in Rules.lhs
229
230 --------------
231 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
232
233 --------------
234 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
235            -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
236 match_list fn subst []         []         = Just subst
237 match_list fn subst (ty1:tys1) (ty2:tys2) = do  { subst' <- fn subst ty1 ty2
238                                                 ; match_list fn subst' tys1 tys2 }
239 match_list fn subst tys1       tys2       = Nothing     
240
241 --------------
242 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
243   | c1 == c2 = match_tys menv subst tys1 tys2
244 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
245   | n1 == n2 = match menv subst t1 t2
246 match_pred menv subst p1 p2 = Nothing
247 \end{code}
248
249
250 %************************************************************************
251 %*                                                                      *
252                 GADTs
253 %*                                                                      *
254 %************************************************************************
255
256 Note [Pruning dead case alternatives]
257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
258 Consider        data T a where
259                    T1 :: T Int
260                    T2 :: T a
261
262                 newtype X = MkX Int
263                 newtype Y = MkY Char
264
265                 type family F a
266                 type instance F Bool = Int
267
268 Now consider    case x of { T1 -> e1; T2 -> e2 }
269
270 The question before the house is this: if I know something about the type
271 of x, can I prune away the T1 alternative?
272
273 Suppose x::T Char.  It's impossible to construct a (T Char) using T1, 
274         Answer = YES (clearly)
275
276 Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
277 to 'Bool', in which case x::T Int, so
278         ANSWER = NO (clearly)
279
280 Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom) 
281 value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
282 gives a coercion
283         CoX :: X ~ Int
284 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
285 of type (T X) constructed with T1.  Hence
286         ANSWER = NO (surprisingly)
287
288 Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
289 mechanism uses a cast, just as above, to move from one dictionary to another,
290 in effect giving the programmer access to CoX.
291
292 Finally, suppose x::T Y.  Then *even in FC* we can't construct a
293 non-bottom value of type (T Y) using T1.  That's because we can get
294 from Y to Char, but not to Int.
295
296
297 Here's a related question.      data Eq a b where EQ :: Eq a a
298 Consider
299         case x of { EQ -> ... }
300
301 Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
302
303 What about x::Eq Int a, in a context where we have evidence that a~Char.
304 Then again the alternative is dead.   
305
306
307                         Summary
308
309 We are really doing a test for unsatisfiability of the type
310 constraints implied by the match. And that is clearly, in general, a
311 hard thing to do.  
312
313 However, since we are simply dropping dead code, a conservative test
314 suffices.  There is a continuum of tests, ranging from easy to hard, that
315 drop more and more dead code.
316
317 For now we implement a very simple test: type variables match
318 anything, type functions (incl newtypes) match anything, and only
319 distinct data types fail to match.  We can elaborate later.
320
321 \begin{code}
322 dataConCannotMatch :: [Type] -> DataCon -> Bool
323 -- Returns True iff the data con *definitely cannot* match a 
324 --                  scrutinee of type (T tys)
325 --                  where T is the type constructor for the data con
326 --
327 dataConCannotMatch tys con
328   | null eq_spec      = False   -- Common
329   | all isTyVarTy tys = False   -- Also common
330   | otherwise
331   = cant_match_s (map (substTyVar subst . fst) eq_spec)
332                  (map snd eq_spec)
333   where
334     dc_tvs  = dataConUnivTyVars con
335     eq_spec = dataConEqSpec con
336     subst   = zipTopTvSubst dc_tvs tys
337
338     cant_match_s :: [Type] -> [Type] -> Bool
339     cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
340                              or (zipWith cant_match tys1 tys2)
341
342     cant_match :: Type -> Type -> Bool
343     cant_match t1 t2
344         | Just t1' <- coreView t1 = cant_match t1' t2
345         | Just t2' <- coreView t2 = cant_match t1 t2'
346
347     cant_match (FunTy a1 r1) (FunTy a2 r2)
348         = cant_match a1 a2 || cant_match r1 r2
349
350     cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
351         | isDataTyCon tc1 && isDataTyCon tc2
352         = tc1 /= tc2 || cant_match_s tys1 tys2
353
354     cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
355     cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
356         -- tc can't be FunTyCon by invariant
357
358     cant_match (AppTy f1 a1) ty2
359         | Just (f2, a2) <- repSplitAppTy_maybe ty2
360         = cant_match f1 f2 || cant_match a1 a2
361     cant_match ty1 (AppTy f2 a2)
362         | Just (f1, a1) <- repSplitAppTy_maybe ty1
363         = cant_match f1 f2 || cant_match a1 a2
364
365     cant_match ty1 ty2 = False  -- Safe!
366
367 -- Things we could add;
368 --      foralls
369 --      look through newtypes
370 --      take account of tyvar bindings (EQ example above)
371 \end{code}