[project @ 2004-12-21 12:22:22 by simonpj]
[ghc-hetmet.git] / ghc / compiler / types / Unify.lhs
1 \begin{code}
2 module Unify ( 
3         -- Matching and unification
4         tcMatchTys, tcMatchTyX, tcMatchPreds, MatchEnv(..), 
5
6         tcUnifyTys, tcUnifyTysX,
7
8         gadtRefineTys, gadtMatchTys, coreRefineTys,
9
10         -- Re-export
11         MaybeErr(..)
12    ) where
13
14 #include "HsVersions.h"
15
16 import Type             ( pprParendType )
17 import Var              ( Var, TyVar, tyVarKind )
18 import VarEnv
19 import VarSet
20 import Kind             ( isSubKind )
21 import Type             ( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta, 
22                           TvSubstEnv, TvSubst(..), substTy, tcEqTypeX )
23 import TypeRep          ( Type(..), PredType(..), funTyCon )
24 import Util             ( snocView )
25 import ErrUtils         ( Message )
26 import Outputable
27 import Maybes
28 \end{code}
29
30
31 %************************************************************************
32 %*                                                                      *
33                 Matching
34 %*                                                                      *
35 %************************************************************************
36
37
38 Matching is much tricker than you might think.
39
40 1. The substitution we generate binds the *template type variables*
41    which are given to us explicitly.
42
43 2. We want to match in the presence of foralls; 
44         e.g     (forall a. t1) ~ (forall b. t2)
45
46    That is what the RnEnv2 is for; it does the alpha-renaming
47    that makes it as if a and b were the same variable.
48    Initialising the RnEnv2, so that it can generate a fresh
49    binder when necessary, entails knowing the free variables of
50    both types.
51
52 3. We must be careful not to bind a template type variable to a
53    locally bound variable.  E.g.
54         (forall a. x) ~ (forall b. b)
55    where x is the template type variable.  Then we do not want to
56    bind x to a/b!  This is a kind of occurs check.
57    The necessary locals accumulate in the RnEnv2.
58
59
60 \begin{code}
61 data MatchEnv
62   = ME  { me_tmpls :: VarSet    -- Template tyvars
63         , me_env   :: RnEnv2    -- Renaming envt for nested foralls
64         }                       --   In-scope set includes template tyvars
65
66 tcMatchTys :: TyVarSet          -- Template tyvars
67          -> [Type]              -- Template
68          -> [Type]              -- Target
69          -> Maybe TvSubstEnv    -- One-shot; in principle the template
70                                 -- variables could be free in the target
71
72 tcMatchTys tmpls tys1 tys2
73   = match_tys (ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope_tyvars})
74               emptyTvSubstEnv 
75               tys1 tys2
76   where
77     in_scope_tyvars = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
78         -- We're assuming that all the interesting 
79         -- tyvars in tys1 are in tmpls
80
81 tcMatchPreds
82         :: [TyVar]                      -- Bind these
83         -> [PredType] -> [PredType]
84         -> Maybe TvSubstEnv
85 tcMatchPreds tmpls ps1 ps2
86   = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
87   where
88     menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
89     in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
90
91 tcMatchTyX :: MatchEnv 
92          -> TvSubstEnv          -- Substitution to extend
93          -> Type                -- Template
94          -> Type                -- Target
95          -> Maybe TvSubstEnv
96
97 tcMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2        -- Rename for export
98 \end{code}
99
100 Now the internals of matching
101
102 \begin{code}
103 match :: MatchEnv       -- For the ost part this is pushed downwards
104       -> TvSubstEnv     -- Substitution so far:
105                         --   Domain is subset of template tyvars
106                         --   Free vars of range is subset of 
107                         --      in-scope set of the RnEnv2
108       -> Type -> Type   -- Template and target respectively
109       -> Maybe TvSubstEnv
110 -- This matcher works on source types; that is, 
111 -- it respects NewTypes and PredType
112
113 match menv subst (NoteTy _ ty1) ty2 = match menv subst ty1 ty2
114 match menv subst ty1 (NoteTy _ ty2) = match menv subst ty1 ty2
115
116 match menv subst (TyVarTy tv1) ty2
117   | tv1 `elemVarSet` me_tmpls menv
118   = case lookupVarEnv subst tv1' of
119         Nothing | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
120                 -> Nothing      -- Occurs check
121                 | otherwise
122                 -> Just (extendVarEnv subst tv1 ty2)
123
124         Just ty1' | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
125                 -- ty1 has no locally-bound variables, hence nukeRnEnvL
126                 -- Note tcEqType...we are doing source-type matching here
127                   -> Just subst
128
129         other -> Nothing
130
131    | otherwise  -- tv1 is not a template tyvar
132    = case ty2 of
133         TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
134         other                                   -> Nothing
135   where
136     rn_env = me_env menv
137     tv1' = rnOccL rn_env tv1
138
139 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2) 
140   = match menv' subst ty1 ty2
141   where         -- Use the magic of rnBndr2 to go under the binders
142     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
143
144 match menv subst (PredTy p1) (PredTy p2) 
145   = match_pred menv subst p1 p2
146 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
147   | tc1 == tc2 = match_tys menv subst tys1 tys2
148 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
149   = do { subst' <- match menv subst ty1a ty2a
150        ; match menv subst' ty1b ty2b }
151 match menv subst (AppTy ty1a ty1b) ty2
152   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
153   = do { subst' <- match menv subst ty1a ty2a
154        ; match menv subst' ty1b ty2b }
155
156 match menv subst ty1 ty2
157   = Nothing
158
159 --------------
160 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
161
162 --------------
163 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
164            -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
165 match_list fn subst []         []         = Just subst
166 match_list fn subst (ty1:tys1) (ty2:tys2) = do  { subst' <- fn subst ty1 ty2
167                                                 ; match_list fn subst' tys1 tys2 }
168 match_list fn subst tys1       tys2       = Nothing     
169
170 --------------
171 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
172   | c1 == c2 = match_tys menv subst tys1 tys2
173 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
174   | n1 == n2 = match menv subst t1 t2
175 match_pred menv subst p1 p2 = Nothing
176 \end{code}
177
178
179 %************************************************************************
180 %*                                                                      *
181                 The workhorse
182 %*                                                                      *
183 %************************************************************************
184
185 \begin{code}
186 gadtRefineTys, gadtMatchTys 
187         :: [TyVar]                      -- Try to unify these
188         -> TvSubstEnv                   -- Not idempotent
189         -> [Type] -> [Type]
190         -> MaybeErr Message TvSubstEnv  -- Not idempotent
191 -- This one is used by the type checker.  Neither the input nor result
192 -- substitition is idempotent
193 gadtRefineTys ex_tvs subst tys1 tys2
194   = initUM (tryToBind (mkVarSet ex_tvs)) (unify_tys subst tys1 tys2)
195
196 gadtMatchTys ex_tvs subst tys1 tys2
197   = initUM (bindOnly (mkVarSet ex_tvs)) (unify_tys subst tys1 tys2)
198
199 ----------------------------
200 coreRefineTys :: [TyVar]        -- Try to unify these
201               -> TvSubst        -- A full-blown apply-once substitition
202               -> Type           -- Both types should be a fixed point 
203               -> Type           --   of the incoming substitution
204               -> Maybe TvSubstEnv       -- In-scope set is unaffected
205 -- Used by Core Lint and the simplifier.  Takes a full apply-once substitution.
206 -- The incoming substitution's in-scope set should mention all the variables free 
207 -- in the incoming types
208 coreRefineTys ex_tvs subst@(TvSubst in_scope orig_env) ty1 ty2
209   = maybeErrToMaybe $ initUM (tryToBind (mkVarSet ex_tvs)) $
210     do  {       -- Run the unifier, starting with an empty env
211         ; extra_env <- unify emptyTvSubstEnv ty1 ty2
212
213                 -- Find the fixed point of the resulting non-idempotent
214                 -- substitution, and apply it to the incoming substitution
215         ; let extra_subst     = TvSubst in_scope extra_env_fixpt
216               extra_env_fixpt = mapVarEnv (substTy extra_subst) extra_env
217               orig_env'       = mapVarEnv (substTy extra_subst) orig_env
218         ; return (orig_env' `plusVarEnv` extra_env_fixpt) }
219
220 ----------------------------
221 tcUnifyTys :: TyVarSet -> [Type] -> [Type] -> Maybe TvSubstEnv
222 tcUnifyTys bind_these tys1 tys2
223   = maybeErrToMaybe $ initUM (bindOnly bind_these) $
224     unify_tys emptyTvSubstEnv tys1 tys2
225
226 tcUnifyTysX :: TyVarSet -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
227 tcUnifyTysX bind_these subst tys1 tys2
228   = maybeErrToMaybe $ initUM (bindOnly bind_these) $
229     unify_tys subst tys1 tys2
230
231 ----------------------------
232 tryToBind, bindOnly :: TyVarSet -> TyVar -> BindFlag
233 tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
234                     | otherwise              = AvoidMe
235
236 bindOnly tv_set tv | tv `elemVarSet` tv_set = BindMe
237                    | otherwise              = DontBindMe
238
239 emptyTvSubstEnv :: TvSubstEnv
240 emptyTvSubstEnv = emptyVarEnv
241 \end{code}
242
243
244 %************************************************************************
245 %*                                                                      *
246                 The workhorse
247 %*                                                                      *
248 %************************************************************************
249
250 \begin{code}
251 unify :: TvSubstEnv             -- An existing substitution to extend
252       -> Type -> Type           -- Types to be unified
253       -> UM TvSubstEnv          -- Just the extended substitution, 
254                                 -- Nothing if unification failed
255 -- We do not require the incoming substitution to be idempotent,
256 -- nor guarantee that the outgoing one is.  That's fixed up by
257 -- the wrappers.
258
259 -- Respects newtypes, PredTypes
260
261 unify subst ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $
262                       unify_ subst ty1 ty2
263
264 -- in unify_, any NewTcApps/Preds should be taken at face value
265 unify_ subst (TyVarTy tv1) ty2  = uVar False subst tv1 ty2
266 unify_ subst ty1 (TyVarTy tv2)  = uVar True  subst tv2 ty1
267
268 unify_ subst (NoteTy _ ty1) ty2  = unify subst ty1 ty2
269 unify_ subst ty1 (NoteTy _ ty2)  = unify subst ty1 ty2
270
271 unify_ subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
272
273 unify_ subst t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2) 
274   | tyc1 == tyc2 = unify_tys subst tys1 tys2
275
276 unify_ subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
277   = do { subst' <- unify subst ty1a ty2a
278        ; unify subst' ty1b ty2b }
279
280         -- Applications need a bit of care!
281         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
282         -- NB: we've already dealt with type variables and Notes,
283         -- so if one type is an App the other one jolly well better be too
284 unify_ subst (AppTy ty1a ty1b) ty2
285   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
286   = do  { subst' <- unify subst ty1a ty2a
287         ; unify subst' ty1b ty2b }
288
289 unify_ subst ty1 (AppTy ty2a ty2b)
290   | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
291   = do  { subst' <- unify subst ty1a ty2a
292         ; unify subst' ty1b ty2b }
293
294 unify_ subst ty1 ty2 = failWith (misMatch ty1 ty2)
295
296 ------------------------------
297 unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
298   | c1 == c2 = unify_tys subst tys1 tys2
299 unify_pred subst (IParam n1 t1) (IParam n2 t2)
300   | n1 == n2 = unify subst t1 t2
301 unify_pred subst p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
302  
303 ------------------------------
304 unify_tys = unifyList unify
305
306 unifyList :: Outputable a 
307           => (TvSubstEnv -> a -> a -> UM TvSubstEnv)
308           -> TvSubstEnv -> [a] -> [a] -> UM TvSubstEnv
309 unifyList unifier subst orig_xs orig_ys
310   = go subst orig_xs orig_ys
311   where
312     go subst []     []     = return subst
313     go subst (x:xs) (y:ys) = do { subst' <- unifier subst x y
314                                 ; go subst' xs ys }
315     go subst _      _      = failWith (lengthMisMatch orig_xs orig_ys)
316
317 ------------------------------
318 uVar :: Bool            -- Swapped
319      -> TvSubstEnv      -- An existing substitution to extend
320      -> TyVar           -- Type variable to be unified
321      -> Type            -- with this type
322      -> UM TvSubstEnv
323
324 uVar swap subst tv1 ty
325  = -- check to see whether tv1 is refined
326    case (lookupVarEnv subst tv1) of
327      -- yes, call back into unify'
328      Just ty' | swap      -> unify subst ty ty' 
329               | otherwise -> unify subst ty' ty
330      -- No, continue
331      Nothing          -> uUnrefined subst tv1 ty
332
333
334 uUnrefined :: TvSubstEnv          -- An existing substitution to extend
335            -> TyVar               -- Type variable to be unified
336            -> Type                -- with this type
337            -> UM TvSubstEnv
338
339 -- We know that tv1 isn't refined
340 uUnrefined subst tv1 ty2@(TyVarTy tv2)
341   | tv1 == tv2    -- Same, do nothing
342   = return subst
343
344     -- Check to see whether tv2 is refined
345   | Just ty' <- lookupVarEnv subst tv2
346   = uUnrefined subst tv1 ty'
347
348   -- So both are unrefined; next, see if the kinds force the direction
349   | k1 == k2    -- Can update either; so check the bind-flags
350   = do  { b1 <- tvBindFlag tv1
351         ; b2 <- tvBindFlag tv2
352         ; case (b1,b2) of
353             (DontBindMe, DontBindMe) -> failWith (misMatch ty1 ty2)
354             (DontBindMe, _)          -> bindTv subst tv2 ty1
355             (BindMe, _)              -> bindTv subst tv1 ty2
356             (AvoidMe, BindMe)        -> bindTv subst tv2 ty1
357             (AvoidMe, _)             -> bindTv subst tv1 ty2
358         }
359
360   | k1 `isSubKind` k2   -- Must update tv2
361   = do  { b2 <- tvBindFlag tv2
362         ; case b2 of
363             DontBindMe -> failWith (misMatch ty1 ty2)
364             other      -> bindTv subst tv2 ty1
365         }
366
367   | k2 `isSubKind` k1   -- Must update tv1
368   = do  { b1 <- tvBindFlag tv1
369         ; case b1 of
370             DontBindMe -> failWith (misMatch ty1 ty2)
371             other      -> bindTv subst tv1 ty2
372         }
373
374   | otherwise = failWith (kindMisMatch tv1 ty2)
375   where
376     ty1 = TyVarTy tv1
377     k1 = tyVarKind tv1
378     k2 = tyVarKind tv2
379
380 uUnrefined subst tv1 ty2        -- ty2 is not a type variable
381         -- Do occurs check...
382   | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2)
383   = failWith (occursCheck tv1 ty2)
384         -- And a kind check...
385   | k2 `isSubKind` k1
386   = do  { b1 <- tvBindFlag tv1
387         ; case b1 of            -- And  check that tv1 is bindable
388             DontBindMe -> failWith (misMatch ty1 ty2)
389             other      -> bindTv subst tv1 ty2
390         }
391   | otherwise
392   = pprTrace "kind" (ppr tv1 <+> ppr k1 $$ ppr ty2 <+> ppr k2) $
393     failWith (kindMisMatch tv1 ty2)
394   where
395     ty1 = TyVarTy tv1
396     k1 = tyVarKind tv1
397     k2 = typeKind ty2
398
399 substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
400 -- Apply the non-idempotent substitution to a set of type variables,
401 -- remembering that the substitution isn't necessarily idempotent
402 substTvSet subst tvs
403   = foldVarSet (unionVarSet . get) emptyVarSet tvs
404   where
405     get tv = case lookupVarEnv subst tv of
406                 Nothing -> unitVarSet tv
407                 Just ty -> substTvSet subst (tyVarsOfType ty)
408
409 bindTv subst tv ty = return (extendVarEnv subst tv ty)
410 \end{code}
411
412 %************************************************************************
413 %*                                                                      *
414                 Unification monad
415 %*                                                                      *
416 %************************************************************************
417
418 \begin{code}
419 data BindFlag = BindMe | AvoidMe | DontBindMe
420
421 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
422                          -> MaybeErr Message a }
423
424 instance Monad UM where
425   return a = UM (\tvs -> Succeeded a)
426   fail s   = UM (\tvs -> Failed (text s))
427   m >>= k  = UM (\tvs -> case unUM m tvs of
428                            Failed err -> Failed err
429                            Succeeded v  -> unUM (k v) tvs)
430
431 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
432 initUM badtvs um = unUM um badtvs
433
434 tvBindFlag :: TyVar -> UM BindFlag
435 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
436
437 failWith :: Message -> UM a
438 failWith msg = UM (\tv_fn -> Failed msg)
439
440 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
441 maybeErrToMaybe (Succeeded a) = Just a
442 maybeErrToMaybe (Failed m)    = Nothing
443
444 ------------------------------
445 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
446 -- Like Type.splitAppTy_maybe, but any coreView stuff is already done
447 repSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
448 repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
449 repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
450                                                 Just (tys', ty') -> Just (TyConApp tc tys', ty')
451                                                 Nothing          -> Nothing
452 repSplitAppTy_maybe other = Nothing
453 \end{code}
454
455
456 %************************************************************************
457 %*                                                                      *
458                 Error reporting
459         We go to a lot more trouble to tidy the types
460         in TcUnify.  Maybe we'll end up having to do that
461         here too, but I'll leave it for now.
462 %*                                                                      *
463 %************************************************************************
464
465 \begin{code}
466 misMatch t1 t2
467   = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+> 
468     ptext SLIT("and") <+> quotes (ppr t2)
469
470 lengthMisMatch tys1 tys2
471   = sep [ptext SLIT("Can't match unequal length lists"), 
472          nest 2 (ppr tys1), nest 2 (ppr tys2) ]
473
474 kindMisMatch tv1 t2
475   = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
476             ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
477           ptext SLIT("when matching") <+> quotes (ppr tv1) <+> 
478                 ptext SLIT("with") <+> quotes (ppr t2)]
479
480 occursCheck tv ty
481   = hang (ptext SLIT("Can't construct the infinite type"))
482        2 (ppr tv <+> equals <+> ppr ty)
483 \end{code}