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