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