← Back to branch summary

~ubuntu-branches/ubuntu/precise/ghc/precise

« back to all changes in this revision

Viewing changes to compiler/types/Unify.lhs

  • Committer: Bazaar Package Importer
  • Author(s): Joachim Breitner
  • Date: 2011-01-17 12:49:24 UTC
  • Revision ID: james.westby@ubuntu.com-20110117124924-do1pym1jlf5o636m
Tags: upstream-7.0.1
Import upstream version 7.0.1

Show diffs side-by-side

added added

removed removed

Lines of Context:
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
 
 
15
        -- Side-effect free unification
 
16
        tcUnifyTys, BindFlag(..)
 
17
 
 
18
   ) where
 
19
 
 
20
#include "HsVersions.h"
 
21
 
 
22
import Var
 
23
import VarEnv
 
24
import VarSet
 
25
import Type
 
26
import Coercion
 
27
import TyCon
 
28
import DataCon
 
29
import TypeRep
 
30
import Outputable
 
31
import ErrUtils
 
32
import Util
 
33
import Maybes
 
34
import UniqFM
 
35
import FastString
 
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
  | Just ty1' <- lookupVarEnv subst tv1'        -- tv1' is already bound
 
158
  = if tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
 
159
        -- ty1 has no locally-bound variables, hence nukeRnEnvL
 
160
        -- Note tcEqType...we are doing source-type matching here
 
161
    then Just subst
 
162
    else Nothing        -- ty2 doesn't match
 
163
 
 
164
  | tv1' `elemVarSet` me_tmpls menv
 
165
  = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
 
166
    then Nothing        -- Occurs check
 
167
    else do { subst1 <- match_kind menv subst tv1 ty2
 
168
                        -- Note [Matching kinds]
 
169
            ; return (extendVarEnv subst1 tv1' ty2) }
 
170
 
 
171
   | otherwise  -- tv1 is not a template tyvar
 
172
   = case ty2 of
 
173
        TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
 
174
        _                                       -> Nothing
 
175
  where
 
176
    rn_env = me_env menv
 
177
    tv1' = rnOccL rn_env tv1
 
178
 
 
179
match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2) 
 
180
  = match menv' subst ty1 ty2
 
181
  where         -- Use the magic of rnBndr2 to go under the binders
 
182
    menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
 
183
 
 
184
match menv subst (PredTy p1) (PredTy p2) 
 
185
  = match_pred menv subst p1 p2
 
186
match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
 
187
  | tc1 == tc2 = match_tys menv subst tys1 tys2
 
188
match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
 
189
  = do { subst' <- match menv subst ty1a ty2a
 
190
       ; match menv subst' ty1b ty2b }
 
191
match menv subst (AppTy ty1a ty1b) ty2
 
192
  | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 
193
        -- 'repSplit' used because the tcView stuff is done above
 
194
  = do { subst' <- match menv subst ty1a ty2a
 
195
       ; match menv subst' ty1b ty2b }
 
196
 
 
197
match _ _ _ _
 
198
  = Nothing
 
199
 
 
200
--------------
 
201
match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
 
202
-- Match the kind of the template tyvar with the kind of Type
 
203
-- Note [Matching kinds]
 
204
match_kind menv subst tv ty
 
205
  | isCoVar tv = do { let (ty1,ty2) = coVarKind tv
 
206
                          (ty3,ty4) = coercionKind ty
 
207
                    ; subst1 <- match menv subst ty1 ty3
 
208
                    ; match menv subst1 ty2 ty4 }
 
209
  | otherwise  = if typeKind ty `isSubKind` tyVarKind tv
 
210
                 then Just subst
 
211
                 else Nothing
 
212
 
 
213
-- Note [Matching kinds]
 
214
-- ~~~~~~~~~~~~~~~~~~~~~
 
215
-- For ordinary type variables, we don't want (m a) to match (n b) 
 
216
-- if say (a::*) and (b::*->*).  This is just a yes/no issue. 
 
217
--
 
218
-- For coercion kinds matters are more complicated.  If we have a 
 
219
-- coercion template variable co::a~[b], where a,b are presumably also
 
220
-- template type variables, then we must match co's kind against the 
 
221
-- kind of the actual argument, so as to give bindings to a,b.  
 
222
--
 
223
-- In fact I have no example in mind that *requires* this kind-matching
 
224
-- to instantiate template type variables, but it seems like the right
 
225
-- thing to do.  C.f. Note [Matching variable types] in Rules.lhs
 
226
 
 
227
--------------
 
228
match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
 
229
match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
 
230
 
 
231
--------------
 
232
match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
 
233
           -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
 
234
match_list _  subst []         []         = Just subst
 
235
match_list fn subst (ty1:tys1) (ty2:tys2) = do  { subst' <- fn subst ty1 ty2
 
236
                                                ; match_list fn subst' tys1 tys2 }
 
237
match_list _  _     _          _          = Nothing
 
238
 
 
239
--------------
 
240
match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv
 
241
match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
 
242
  | c1 == c2 = match_tys menv subst tys1 tys2
 
243
match_pred menv subst (IParam n1 t1) (IParam n2 t2)
 
244
  | n1 == n2 = match menv subst t1 t2
 
245
match_pred _    _     _ _ = Nothing
 
246
\end{code}
 
247
 
 
248
 
 
249
%************************************************************************
 
250
%*                                                                      *
 
251
                GADTs
 
252
%*                                                                      *
 
253
%************************************************************************
 
254
 
 
255
Note [Pruning dead case alternatives]
 
256
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
257
Consider        data T a where
 
258
                   T1 :: T Int
 
259
                   T2 :: T a
 
260
 
 
261
                newtype X = MkX Int
 
262
                newtype Y = MkY Char
 
263
 
 
264
                type family F a
 
265
                type instance F Bool = Int
 
266
 
 
267
Now consider    case x of { T1 -> e1; T2 -> e2 }
 
268
 
 
269
The question before the house is this: if I know something about the type
 
270
of x, can I prune away the T1 alternative?
 
271
 
 
272
Suppose x::T Char.  It's impossible to construct a (T Char) using T1, 
 
273
        Answer = YES (clearly)
 
274
 
 
275
Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
 
276
to 'Bool', in which case x::T Int, so
 
277
        ANSWER = NO (clearly)
 
278
 
 
279
Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom) 
 
280
value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
 
281
gives a coercion
 
282
        CoX :: X ~ Int
 
283
So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
 
284
of type (T X) constructed with T1.  Hence
 
285
        ANSWER = NO (surprisingly)
 
286
 
 
287
Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
 
288
mechanism uses a cast, just as above, to move from one dictionary to another,
 
289
in effect giving the programmer access to CoX.
 
290
 
 
291
Finally, suppose x::T Y.  Then *even in FC* we can't construct a
 
292
non-bottom value of type (T Y) using T1.  That's because we can get
 
293
from Y to Char, but not to Int.
 
294
 
 
295
 
 
296
Here's a related question.      data Eq a b where EQ :: Eq a a
 
297
Consider
 
298
        case x of { EQ -> ... }
 
299
 
 
300
Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
 
301
 
 
302
What about x::Eq Int a, in a context where we have evidence that a~Char.
 
303
Then again the alternative is dead.   
 
304
 
 
305
 
 
306
                        Summary
 
307
 
 
308
We are really doing a test for unsatisfiability of the type
 
309
constraints implied by the match. And that is clearly, in general, a
 
310
hard thing to do.  
 
311
 
 
312
However, since we are simply dropping dead code, a conservative test
 
313
suffices.  There is a continuum of tests, ranging from easy to hard, that
 
314
drop more and more dead code.
 
315
 
 
316
For now we implement a very simple test: type variables match
 
317
anything, type functions (incl newtypes) match anything, and only
 
318
distinct data types fail to match.  We can elaborate later.
 
319
 
 
320
\begin{code}
 
321
dataConCannotMatch :: [Type] -> DataCon -> Bool
 
322
-- Returns True iff the data con *definitely cannot* match a 
 
323
--                  scrutinee of type (T tys)
 
324
--                  where T is the type constructor for the data con
 
325
--
 
326
dataConCannotMatch tys con
 
327
  | null eq_spec      = False   -- Common
 
328
  | all isTyVarTy tys = False   -- Also common
 
329
  | otherwise
 
330
  = cant_match_s (map (substTyVar subst . fst) eq_spec)
 
331
                 (map snd eq_spec)
 
332
  where
 
333
    dc_tvs  = dataConUnivTyVars con
 
334
    eq_spec = dataConEqSpec con
 
335
    subst   = zipTopTvSubst dc_tvs tys
 
336
 
 
337
    cant_match_s :: [Type] -> [Type] -> Bool
 
338
    cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
 
339
                             or (zipWith cant_match tys1 tys2)
 
340
 
 
341
    cant_match :: Type -> Type -> Bool
 
342
    cant_match t1 t2
 
343
        | Just t1' <- coreView t1 = cant_match t1' t2
 
344
        | Just t2' <- coreView t2 = cant_match t1 t2'
 
345
 
 
346
    cant_match (FunTy a1 r1) (FunTy a2 r2)
 
347
        = cant_match a1 a2 || cant_match r1 r2
 
348
 
 
349
    cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 
350
        | isDataTyCon tc1 && isDataTyCon tc2
 
351
        = tc1 /= tc2 || cant_match_s tys1 tys2
 
352
 
 
353
    cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
 
354
    cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
 
355
        -- tc can't be FunTyCon by invariant
 
356
 
 
357
    cant_match (AppTy f1 a1) ty2
 
358
        | Just (f2, a2) <- repSplitAppTy_maybe ty2
 
359
        = cant_match f1 f2 || cant_match a1 a2
 
360
    cant_match ty1 (AppTy f2 a2)
 
361
        | Just (f1, a1) <- repSplitAppTy_maybe ty1
 
362
        = cant_match f1 f2 || cant_match a1 a2
 
363
 
 
364
    cant_match _ _ = False      -- Safe!
 
365
 
 
366
-- Things we could add;
 
367
--      foralls
 
368
--      look through newtypes
 
369
--      take account of tyvar bindings (EQ example above)
 
370
\end{code}
 
371
 
 
372
 
 
373
 
 
374
%************************************************************************
 
375
%*                                                                      *
 
376
                Unification
 
377
%*                                                                      *
 
378
%************************************************************************
 
379
 
 
380
\begin{code}
 
381
tcUnifyTys :: (TyVar -> BindFlag)
 
382
           -> [Type] -> [Type]
 
383
           -> Maybe TvSubst     -- A regular one-shot (idempotent) substitution
 
384
-- The two types may have common type variables, and indeed do so in the
 
385
-- second call to tcUnifyTys in FunDeps.checkClsFD
 
386
--
 
387
tcUnifyTys bind_fn tys1 tys2
 
388
  = maybeErrToMaybe $ initUM bind_fn $
 
389
    do { subst <- unifyList emptyTvSubstEnv tys1 tys2
 
390
 
 
391
        -- Find the fixed point of the resulting non-idempotent substitution
 
392
        ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
 
393
              tv_env   = fixTvSubstEnv in_scope subst
 
394
 
 
395
        ; return (mkTvSubst in_scope tv_env) }
 
396
  where
 
397
    tvs1 = tyVarsOfTypes tys1
 
398
    tvs2 = tyVarsOfTypes tys2
 
399
 
 
400
----------------------------
 
401
-- XXX Can we do this more nicely, by exploiting laziness?
 
402
-- Or avoid needing it in the first place?
 
403
fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
 
404
fixTvSubstEnv in_scope env = f env
 
405
  where
 
406
    f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e
 
407
          in if and $ eltsUFM $ intersectUFM_C tcEqType e e'
 
408
             then e
 
409
             else f e'
 
410
 
 
411
\end{code}
 
412
 
 
413
 
 
414
%************************************************************************
 
415
%*                                                                      *
 
416
                The workhorse
 
417
%*                                                                      *
 
418
%************************************************************************
 
419
 
 
420
\begin{code}
 
421
unify :: TvSubstEnv     -- An existing substitution to extend
 
422
      -> Type -> Type   -- Types to be unified, and witness of their equality
 
423
      -> UM TvSubstEnv          -- Just the extended substitution, 
 
424
                                -- Nothing if unification failed
 
425
-- We do not require the incoming substitution to be idempotent,
 
426
-- nor guarantee that the outgoing one is.  That's fixed up by
 
427
-- the wrappers.
 
428
 
 
429
-- Respects newtypes, PredTypes
 
430
 
 
431
-- in unify, any NewTcApps/Preds should be taken at face value
 
432
unify subst (TyVarTy tv1) ty2  = uVar subst tv1 ty2
 
433
unify subst ty1 (TyVarTy tv2)  = uVar subst tv2 ty1
 
434
 
 
435
unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
 
436
unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'
 
437
 
 
438
unify subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
 
439
 
 
440
unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2) 
 
441
  | tyc1 == tyc2 = unify_tys subst tys1 tys2
 
442
 
 
443
unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
 
444
  = do  { subst' <- unify subst ty1a ty2a
 
445
        ; unify subst' ty1b ty2b }
 
446
 
 
447
        -- Applications need a bit of care!
 
448
        -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 
449
        -- NB: we've already dealt with type variables and Notes,
 
450
        -- so if one type is an App the other one jolly well better be too
 
451
unify subst (AppTy ty1a ty1b) ty2
 
452
  | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
 
453
  = do  { subst' <- unify subst ty1a ty2a
 
454
        ; unify subst' ty1b ty2b }
 
455
 
 
456
unify subst ty1 (AppTy ty2a ty2b)
 
457
  | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
 
458
  = do  { subst' <- unify subst ty1a ty2a
 
459
        ; unify subst' ty1b ty2b }
 
460
 
 
461
unify _ ty1 ty2 = failWith (misMatch ty1 ty2)
 
462
        -- ForAlls??
 
463
 
 
464
------------------------------
 
465
unify_pred :: TvSubstEnv -> PredType -> PredType -> UM TvSubstEnv
 
466
unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
 
467
  | c1 == c2 = unify_tys subst tys1 tys2
 
468
unify_pred subst (IParam n1 t1) (IParam n2 t2)
 
469
  | n1 == n2 = unify subst t1 t2
 
470
unify_pred _ p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
 
471
 
 
472
------------------------------
 
473
unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 
474
unify_tys subst xs ys = unifyList subst xs ys
 
475
 
 
476
unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
 
477
unifyList subst orig_xs orig_ys
 
478
  = go subst orig_xs orig_ys
 
479
  where
 
480
    go subst []     []     = return subst
 
481
    go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
 
482
                                ; go subst' xs ys }
 
483
    go _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
 
484
 
 
485
---------------------------------
 
486
uVar :: TvSubstEnv      -- An existing substitution to extend
 
487
     -> TyVar           -- Type variable to be unified
 
488
     -> Type            -- with this type
 
489
     -> UM TvSubstEnv
 
490
 
 
491
-- PRE-CONDITION: in the call (uVar swap r tv1 ty), we know that
 
492
--      if swap=False   (tv1~ty)
 
493
--      if swap=True    (ty~tv1)
 
494
 
 
495
uVar subst tv1 ty
 
496
 = -- Check to see whether tv1 is refined by the substitution
 
497
   case (lookupVarEnv subst tv1) of
 
498
     Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
 
499
     Nothing  -> uUnrefined subst       -- No, continue
 
500
                            tv1 ty ty
 
501
 
 
502
uUnrefined :: TvSubstEnv          -- An existing substitution to extend
 
503
           -> TyVar               -- Type variable to be unified
 
504
           -> Type                -- with this type
 
505
           -> Type                -- (version w/ expanded synonyms)
 
506
           -> UM TvSubstEnv
 
507
 
 
508
-- We know that tv1 isn't refined
 
509
 
 
510
uUnrefined subst tv1 ty2 ty2'
 
511
  | Just ty2'' <- tcView ty2'
 
512
  = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
 
513
                -- This is essential, in case we have
 
514
                --      type Foo a = a
 
515
                -- and then unify a ~ Foo a
 
516
 
 
517
uUnrefined subst tv1 ty2 (TyVarTy tv2)
 
518
  | tv1 == tv2          -- Same type variable
 
519
  = return subst
 
520
 
 
521
    -- Check to see whether tv2 is refined
 
522
  | Just ty' <- lookupVarEnv subst tv2
 
523
  = uUnrefined subst tv1 ty' ty'
 
524
 
 
525
  -- So both are unrefined; next, see if the kinds force the direction
 
526
  | eqKind k1 k2        -- Can update either; so check the bind-flags
 
527
  = do  { b1 <- tvBindFlag tv1
 
528
        ; b2 <- tvBindFlag tv2
 
529
        ; case (b1,b2) of
 
530
            (BindMe, _)          -> bind tv1 ty2
 
531
            (Skolem, Skolem)     -> failWith (misMatch ty1 ty2)
 
532
            (Skolem, _)          -> bind tv2 ty1
 
533
        }
 
534
 
 
535
  | k1 `isSubKind` k2 = bindTv subst tv2 ty1  -- Must update tv2
 
536
  | k2 `isSubKind` k1 = bindTv subst tv1 ty2  -- Must update tv1
 
537
 
 
538
  | otherwise = failWith (kindMisMatch tv1 ty2)
 
539
  where
 
540
    ty1 = TyVarTy tv1
 
541
    k1 = tyVarKind tv1
 
542
    k2 = tyVarKind tv2
 
543
    bind tv ty = return $ extendVarEnv subst tv ty
 
544
 
 
545
uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
 
546
  | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
 
547
  = failWith (occursCheck tv1 ty2)      -- Occurs check
 
548
  | not (k2 `isSubKind` k1)
 
549
  = failWith (kindMisMatch tv1 ty2)     -- Kind check
 
550
  | otherwise
 
551
  = bindTv subst tv1 ty2                -- Bind tyvar to the synonym if poss
 
552
  where
 
553
    k1 = tyVarKind tv1
 
554
    k2 = typeKind ty2'
 
555
 
 
556
substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
 
557
-- Apply the non-idempotent substitution to a set of type variables,
 
558
-- remembering that the substitution isn't necessarily idempotent
 
559
substTvSet subst tvs
 
560
  = foldVarSet (unionVarSet . get) emptyVarSet tvs
 
561
  where
 
562
    get tv = case lookupVarEnv subst tv of
 
563
               Nothing -> unitVarSet tv
 
564
               Just ty -> substTvSet subst (tyVarsOfType ty)
 
565
 
 
566
bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
 
567
bindTv subst tv ty      -- ty is not a type variable
 
568
  = do  { b <- tvBindFlag tv
 
569
        ; case b of
 
570
            Skolem -> failWith (misMatch (TyVarTy tv) ty)
 
571
            BindMe -> return $ extendVarEnv subst tv ty
 
572
        }
 
573
\end{code}
 
574
 
 
575
%************************************************************************
 
576
%*                                                                      *
 
577
                Binding decisions
 
578
%*                                                                      *
 
579
%************************************************************************
 
580
 
 
581
\begin{code}
 
582
data BindFlag 
 
583
  = BindMe      -- A regular type variable
 
584
 
 
585
  | Skolem      -- This type variable is a skolem constant
 
586
                -- Don't bind it; it only matches itself
 
587
\end{code}
 
588
 
 
589
 
 
590
%************************************************************************
 
591
%*                                                                      *
 
592
                Unification monad
 
593
%*                                                                      *
 
594
%************************************************************************
 
595
 
 
596
\begin{code}
 
597
newtype UM a = UM { unUM :: (TyVar -> BindFlag)
 
598
                         -> MaybeErr Message a }
 
599
 
 
600
instance Monad UM where
 
601
  return a = UM (\_tvs -> Succeeded a)
 
602
  fail s   = UM (\_tvs -> Failed (text s))
 
603
  m >>= k  = UM (\tvs -> case unUM m tvs of
 
604
                           Failed err -> Failed err
 
605
                           Succeeded v  -> unUM (k v) tvs)
 
606
 
 
607
initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
 
608
initUM badtvs um = unUM um badtvs
 
609
 
 
610
tvBindFlag :: TyVar -> UM BindFlag
 
611
tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
 
612
 
 
613
failWith :: Message -> UM a
 
614
failWith msg = UM (\_tv_fn -> Failed msg)
 
615
 
 
616
maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
 
617
maybeErrToMaybe (Succeeded a) = Just a
 
618
maybeErrToMaybe (Failed _)    = Nothing
 
619
\end{code}
 
620
 
 
621
 
 
622
%************************************************************************
 
623
%*                                                                      *
 
624
                Error reporting
 
625
        We go to a lot more trouble to tidy the types
 
626
        in TcUnify.  Maybe we'll end up having to do that
 
627
        here too, but I'll leave it for now.
 
628
%*                                                                      *
 
629
%************************************************************************
 
630
 
 
631
\begin{code}
 
632
misMatch :: Type -> Type -> SDoc
 
633
misMatch t1 t2
 
634
  = ptext (sLit "Can't match types") <+> quotes (ppr t1) <+> 
 
635
    ptext (sLit "and") <+> quotes (ppr t2)
 
636
 
 
637
lengthMisMatch :: [Type] -> [Type] -> SDoc
 
638
lengthMisMatch tys1 tys2
 
639
  = sep [ptext (sLit "Can't match unequal length lists"), 
 
640
         nest 2 (ppr tys1), nest 2 (ppr tys2) ]
 
641
 
 
642
kindMisMatch :: TyVar -> Type -> SDoc
 
643
kindMisMatch tv1 t2
 
644
  = vcat [ptext (sLit "Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
 
645
            ptext (sLit "and") <+> quotes (ppr (typeKind t2)),
 
646
          ptext (sLit "when matching") <+> quotes (ppr tv1) <+> 
 
647
                ptext (sLit "with") <+> quotes (ppr t2)]
 
648
 
 
649
occursCheck :: TyVar -> Type -> SDoc
 
650
occursCheck tv ty
 
651
  = hang (ptext (sLit "Can't construct the infinite type"))
 
652
       2 (ppr tv <+> equals <+> ppr ty)
 
653
\end{code}