Fixed warnings in types/Unify
[ghc.git] / compiler / types / Unify.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 \begin{code}
6 module Unify ( 
7         -- Matching of types: 
8         --      the "tc" prefix indicates that matching always
9         --      respects newtypes (rather than looking through them)
10         tcMatchTy, tcMatchTys, tcMatchTyX, 
11         ruleMatchTyX, tcMatchPreds, MatchEnv(..),
12         
13         dataConCannotMatch
14    ) where
15
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"
19
20 import Var
21 import VarEnv
22 import VarSet
23 import Type
24 import Coercion
25 import TyCon
26 import DataCon
27 import TypeRep
28 import Outputable
29 import Util
30 import Maybes
31 \end{code}
32
33
34 %************************************************************************
35 %*                                                                      *
36                 Matching
37 %*                                                                      *
38 %************************************************************************
39
40
41 Matching is much tricker than you might think.
42
43 1. The substitution we generate binds the *template type variables*
44    which are given to us explicitly.
45
46 2. We want to match in the presence of foralls; 
47         e.g     (forall a. t1) ~ (forall b. t2)
48
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
53    both types.
54
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.
61
62
63 \begin{code}
64 data MatchEnv
65   = ME  { me_tmpls :: VarSet    -- Template tyvars
66         , me_env   :: RnEnv2    -- Renaming envt for nested foralls
67         }                       --   In-scope set includes template tyvars
68
69 tcMatchTy :: TyVarSet           -- Template tyvars
70           -> Type               -- Template
71           -> Type               -- Target
72           -> Maybe TvSubst      -- One-shot; in principle the template
73                                 -- variables could be free in the target
74
75 tcMatchTy tmpls ty1 ty2
76   = case match menv emptyTvSubstEnv ty1 ty2 of
77         Just subst_env -> Just (TvSubst in_scope subst_env)
78         Nothing        -> Nothing
79   where
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
84
85 tcMatchTys :: TyVarSet          -- Template tyvars
86            -> [Type]            -- Template
87            -> [Type]            -- Target
88            -> Maybe TvSubst     -- One-shot; in principle the template
89                                 -- variables could be free in the target
90
91 tcMatchTys tmpls tys1 tys2
92   = case match_tys menv emptyTvSubstEnv tys1 tys2 of
93         Just subst_env -> Just (TvSubst in_scope subst_env)
94         Nothing        -> Nothing
95   where
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
100
101 -- This is similar, but extends a substitution
102 tcMatchTyX :: TyVarSet          -- Template tyvars
103            -> TvSubst           -- Substitution to extend
104            -> Type              -- Template
105            -> Type              -- Target
106            -> Maybe TvSubst
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)
110         Nothing        -> Nothing
111   where
112     menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
113
114 tcMatchPreds
115         :: [TyVar]                      -- Bind these
116         -> [PredType] -> [PredType]
117         -> Maybe TvSubstEnv
118 tcMatchPreds tmpls ps1 ps2
119   = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
120   where
121     menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
122     in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
123
124 -- This one is called from the expression matcher, which already has a MatchEnv in hand
125 ruleMatchTyX :: MatchEnv 
126          -> TvSubstEnv          -- Substitution to extend
127          -> Type                -- Template
128          -> Type                -- Target
129          -> Maybe TvSubstEnv
130
131 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
132 \end{code}
133
134 Now the internals of matching
135
136 \begin{code}
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
143       -> Maybe TvSubstEnv
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
147
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'
150
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
157             | otherwise 
158             -> do { subst1 <- match_kind menv subst tv1 ty2
159                   ; return (extendVarEnv subst1 tv1' ty2) }
160                         -- Note [Matching kinds]
161
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
166             -> Just subst
167             | otherwise -> Nothing      -- ty2 doesn't match
168             
169
170    | otherwise  -- tv1 is not a template tyvar
171    = case ty2 of
172         TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
173         _                                       -> Nothing
174   where
175     rn_env = me_env menv
176     tv1' = rnOccL rn_env tv1
177
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 }
182
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 }
195
196 match _ _ _ _
197   = Nothing
198
199 --------------
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
209                  then Just subst
210                  else Nothing
211
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. 
216 --
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.  
221 --
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
225
226 --------------
227 match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
228 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
229
230 --------------
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
237
238 --------------
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
245 \end{code}
246
247
248 %************************************************************************
249 %*                                                                      *
250                 GADTs
251 %*                                                                      *
252 %************************************************************************
253
254 Note [Pruning dead case alternatives]
255 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
256 Consider        data T a where
257                    T1 :: T Int
258                    T2 :: T a
259
260                 newtype X = MkX Int
261                 newtype Y = MkY Char
262
263                 type family F a
264                 type instance F Bool = Int
265
266 Now consider    case x of { T1 -> e1; T2 -> e2 }
267
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?
270
271 Suppose x::T Char.  It's impossible to construct a (T Char) using T1, 
272         Answer = YES (clearly)
273
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)
277
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
280 gives a coercion
281         CoX :: X ~ Int
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)
285
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.
289
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.
293
294
295 Here's a related question.      data Eq a b where EQ :: Eq a a
296 Consider
297         case x of { EQ -> ... }
298
299 Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
300
301 What about x::Eq Int a, in a context where we have evidence that a~Char.
302 Then again the alternative is dead.   
303
304
305                         Summary
306
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
309 hard thing to do.  
310
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.
314
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.
318
319 \begin{code}
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
324 --
325 dataConCannotMatch tys con
326   | null eq_spec      = False   -- Common
327   | all isTyVarTy tys = False   -- Also common
328   | otherwise
329   = cant_match_s (map (substTyVar subst . fst) eq_spec)
330                  (map snd eq_spec)
331   where
332     dc_tvs  = dataConUnivTyVars con
333     eq_spec = dataConEqSpec con
334     subst   = zipTopTvSubst dc_tvs tys
335
336     cant_match_s :: [Type] -> [Type] -> Bool
337     cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
338                              or (zipWith cant_match tys1 tys2)
339
340     cant_match :: Type -> Type -> Bool
341     cant_match t1 t2
342         | Just t1' <- coreView t1 = cant_match t1' t2
343         | Just t2' <- coreView t2 = cant_match t1 t2'
344
345     cant_match (FunTy a1 r1) (FunTy a2 r2)
346         = cant_match a1 a2 || cant_match r1 r2
347
348     cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
349         | isDataTyCon tc1 && isDataTyCon tc2
350         = tc1 /= tc2 || cant_match_s tys1 tys2
351
352     cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
353     cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
354         -- tc can't be FunTyCon by invariant
355
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
362
363     cant_match _ _ = False      -- Safe!
364
365 -- Things we could add;
366 --      foralls
367 --      look through newtypes
368 --      take account of tyvar bindings (EQ example above)
369 \end{code}