Unify.lhs 27.6 KB
Newer Older
1
2
3
4
%
% (c) The University of Glasgow 2006
%

5
\begin{code}
6
{-# LANGUAGE CPP #-}
Ian Lynagh's avatar
Ian Lynagh committed
7

8
9
10
11
12
13
module Unify (
        -- Matching of types:
        --      the "tc" prefix indicates that matching always
        --      respects newtypes (rather than looking through them)
        tcMatchTy, tcMatchTys, tcMatchTyX,
        ruleMatchTyX, tcMatchPreds,
14

15
        MatchEnv(..), matchList,
16

17
        typesCantMatch,
18

19
        -- Side-effect free unification
20
        tcUnifyTy, tcUnifyTys, BindFlag(..),
21

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
22
        UnifyResultM(..), UnifyResult, tcUnifyTysFG
23

24
25
26
27
   ) where

#include "HsVersions.h"

28
import Var
29
30
import VarEnv
import VarSet
31
import Kind
32
import Type
33
import TyCon
34
import TypeRep
35
import Util
Austin Seipp's avatar
Austin Seipp committed
36

37
import Control.Monad (liftM, ap)
38
#if __GLASGOW_HASKELL__ < 709
Austin Seipp's avatar
Austin Seipp committed
39
import Control.Applicative (Applicative(..))
40
#endif
41
42
43
44
\end{code}


%************************************************************************
45
46
47
%*                                                                      *
                Matching
%*                                                                      *
48
49
50
51
52
53
54
55
%************************************************************************


Matching is much tricker than you might think.

1. The substitution we generate binds the *template type variables*
   which are given to us explicitly.

56
57
2. We want to match in the presence of foralls;
        e.g     (forall a. t1) ~ (forall b. t2)
58
59
60
61
62
63
64
65
66

   That is what the RnEnv2 is for; it does the alpha-renaming
   that makes it as if a and b were the same variable.
   Initialising the RnEnv2, so that it can generate a fresh
   binder when necessary, entails knowing the free variables of
   both types.

3. We must be careful not to bind a template type variable to a
   locally bound variable.  E.g.
67
        (forall a. x) ~ (forall b. b)
68
69
70
71
72
73
74
   where x is the template type variable.  Then we do not want to
   bind x to a/b!  This is a kind of occurs check.
   The necessary locals accumulate in the RnEnv2.


\begin{code}
data MatchEnv
75
76
77
  = ME  { me_tmpls :: VarSet    -- Template variables
        , me_env   :: RnEnv2    -- Renaming envt for nested foralls
        }                       --   In-scope set includes template variables
78
79
    -- Nota Bene: MatchEnv isn't specific to Types.  It is used
    --            for matching terms and coercions as well as types
80

81
82
83
84
85
tcMatchTy :: TyVarSet           -- Template tyvars
          -> Type               -- Template
          -> Type               -- Target
          -> Maybe TvSubst      -- One-shot; in principle the template
                                -- variables could be free in the target
86
87
88

tcMatchTy tmpls ty1 ty2
  = case match menv emptyTvSubstEnv ty1 ty2 of
89
90
        Just subst_env -> Just (TvSubst in_scope subst_env)
        Nothing        -> Nothing
91
92
93
  where
    menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
    in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
94
95
        -- We're assuming that all the interesting
        -- tyvars in tys1 are in tmpls
96

97
98
99
100
101
tcMatchTys :: TyVarSet          -- Template tyvars
           -> [Type]            -- Template
           -> [Type]            -- Target
           -> Maybe TvSubst     -- One-shot; in principle the template
                                -- variables could be free in the target
102

103
tcMatchTys tmpls tys1 tys2
104
  = case match_tys menv emptyTvSubstEnv tys1 tys2 of
105
106
        Just subst_env -> Just (TvSubst in_scope subst_env)
        Nothing        -> Nothing
107
  where
108
109
    menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
    in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
110
111
        -- We're assuming that all the interesting
        -- tyvars in tys1 are in tmpls
112

113
-- This is similar, but extends a substitution
114
115
116
117
118
tcMatchTyX :: TyVarSet          -- Template tyvars
           -> TvSubst           -- Substitution to extend
           -> Type              -- Template
           -> Type              -- Target
           -> Maybe TvSubst
119
120
tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
  = case match menv subst_env ty1 ty2 of
121
122
        Just subst_env -> Just (TvSubst in_scope subst_env)
        Nothing        -> Nothing
123
124
125
  where
    menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}

126
tcMatchPreds
127
128
129
        :: [TyVar]                      -- Bind these
        -> [PredType] -> [PredType]
        -> Maybe TvSubstEnv
130
tcMatchPreds tmpls ps1 ps2
batterseapower's avatar
batterseapower committed
131
  = matchList (match menv) emptyTvSubstEnv ps1 ps2
132
133
  where
    menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
batterseapower's avatar
batterseapower committed
134
    in_scope_tyvars = mkInScopeSet (tyVarsOfTypes ps1 `unionVarSet` tyVarsOfTypes ps2)
135

136
-- This one is called from the expression matcher, which already has a MatchEnv in hand
137
138
139
140
141
ruleMatchTyX :: MatchEnv
         -> TvSubstEnv          -- Substitution to extend
         -> Type                -- Template
         -> Type                -- Target
         -> Maybe TvSubstEnv
142

143
ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
144
145
146
147
148
\end{code}

Now the internals of matching

\begin{code}
149
150
151
152
153
154
match :: MatchEnv       -- For the most part this is pushed downwards
      -> TvSubstEnv     -- Substitution so far:
                        --   Domain is subset of template tyvars
                        --   Free vars of range is subset of
                        --      in-scope set of the RnEnv2
      -> Type -> Type   -- Template and target respectively
155
156
      -> Maybe TvSubstEnv

157
match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
158
                         | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
159
160

match menv subst (TyVarTy tv1) ty2
161
  | Just ty1' <- lookupVarEnv subst tv1'        -- tv1' is already bound
162
  = if eqTypeX (nukeRnEnvL rn_env) ty1' ty2
163
        -- ty1 has no locally-bound variables, hence nukeRnEnvL
164
    then Just subst
165
    else Nothing        -- ty2 doesn't match
166

167
  | tv1' `elemVarSet` me_tmpls menv
168
  = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
169
    then Nothing        -- Occurs check
dreixel's avatar
dreixel committed
170
    else do { subst1 <- match_kind menv subst (tyVarKind tv1) (typeKind ty2)
171
172
                        -- Note [Matching kinds]
            ; return (extendVarEnv subst1 tv1' ty2) }
173

174
   | otherwise  -- tv1 is not a template tyvar
175
   = case ty2 of
176
177
        TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
        _                                       -> Nothing
178
179
180
181
  where
    rn_env = me_env menv
    tv1' = rnOccL rn_env tv1

182
match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2)
dreixel's avatar
dreixel committed
183
184
  = do { subst' <- match_kind menv subst (tyVarKind tv1) (tyVarKind tv2)
       ; match menv' subst' ty1 ty2 }
185
  where         -- Use the magic of rnBndr2 to go under the binders
186
187
    menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }

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
192
193
194
  = do { subst' <- match menv subst ty1a ty2a
       ; match menv subst' ty1b ty2b }
match menv subst (AppTy ty1a ty1b) ty2
  | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
195
        -- 'repSplit' used because the tcView stuff is done above
196
197
198
  = do { subst' <- match menv subst ty1a ty2a
       ; match menv subst' ty1b ty2b }

199
200
match _ subst (LitTy x) (LitTy y) | x == y  = return subst

twanvl's avatar
twanvl committed
201
match _ _ _ _
202
203
  = Nothing

204
205


206
--------------
dreixel's avatar
dreixel committed
207
match_kind :: MatchEnv -> TvSubstEnv -> Kind -> Kind -> Maybe TvSubstEnv
208
209
-- Match the kind of the template tyvar with the kind of Type
-- Note [Matching kinds]
dreixel's avatar
dreixel committed
210
211
212
213
214
215
match_kind menv subst k1 k2
  | k2 `isSubKind` k1
  = return subst

  | otherwise
  = match menv subst k1 k2
216
217
218

-- Note [Matching kinds]
-- ~~~~~~~~~~~~~~~~~~~~~
219
220
-- For ordinary type variables, we don't want (m a) to match (n b)
-- if say (a::*) and (b::*->*).  This is just a yes/no issue.
221
--
222
-- For coercion kinds matters are more complicated.  If we have a
223
-- coercion template variable co::a~[b], where a,b are presumably also
224
225
-- template type variables, then we must match co's kind against the
-- kind of the actual argument, so as to give bindings to a,b.
226
227
228
229
230
--
-- In fact I have no example in mind that *requires* this kind-matching
-- to instantiate template type variables, but it seems like the right
-- thing to do.  C.f. Note [Matching variable types] in Rules.lhs

231
--------------
twanvl's avatar
twanvl committed
232
match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
233
match_tys menv subst tys1 tys2 = matchList (match menv) subst tys1 tys2
234
235

--------------
236
matchList :: (env -> a -> b -> Maybe env)
237
           -> env -> [a] -> [b] -> Maybe env
238
239
matchList _  subst []     []     = Just subst
matchList fn subst (a:as) (b:bs) = do { subst' <- fn subst a b
240
                                      ; matchList fn subst' as bs }
241
matchList _  _     _      _      = Nothing
242
243
244
\end{code}


245
%************************************************************************
246
247
248
%*                                                                      *
                GADTs
%*                                                                      *
249
250
251
252
%************************************************************************

Note [Pruning dead case alternatives]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
253
254
255
Consider        data T a where
                   T1 :: T Int
                   T2 :: T a
256

257
258
                newtype X = MkX Int
                newtype Y = MkY Char
259

260
261
                type family F a
                type instance F Bool = Int
262

263
Now consider    case x of { T1 -> e1; T2 -> e2 }
264
265
266
267

The question before the house is this: if I know something about the type
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,
        Answer = YES we can prune the T1 branch (clearly)
270
271
272

Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
to 'Bool', in which case x::T Int, so
273
        ANSWER = NO (clearly)
274

275
Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom)
276
277
value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
gives a coercion
278
        CoX :: X ~ Int
279
280
So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
of type (T X) constructed with T1.  Hence
281
        ANSWER = NO we can't prune the T1 branch (surprisingly)
282
283
284
285
286
287
288
289
290
291

Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
mechanism uses a cast, just as above, to move from one dictionary to another,
in effect giving the programmer access to CoX.

Finally, suppose x::T Y.  Then *even in FC* we can't construct a
non-bottom value of type (T Y) using T1.  That's because we can get
from Y to Char, but not to Int.


292
Here's a related question.      data Eq a b where EQ :: Eq a a
293
Consider
294
        case x of { EQ -> ... }
295
296
297
298

Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.

What about x::Eq Int a, in a context where we have evidence that a~Char.
299
Then again the alternative is dead.
300
301


302
                        Summary
303
304
305

We are really doing a test for unsatisfiability of the type
constraints implied by the match. And that is clearly, in general, a
306
hard thing to do.
307
308
309
310
311
312
313
314
315
316

However, since we are simply dropping dead code, a conservative test
suffices.  There is a continuum of tests, ranging from easy to hard, that
drop more and more dead code.

For now we implement a very simple test: type variables match
anything, type functions (incl newtypes) match anything, and only
distinct data types fail to match.  We can elaborate later.

\begin{code}
317
318
typesCantMatch :: [(Type,Type)] -> Bool
typesCantMatch prs = any (\(s,t) -> cant_match s t) prs
319
320
321
  where
    cant_match :: Type -> Type -> Bool
    cant_match t1 t2
322
323
        | Just t1' <- coreView t1 = cant_match t1' t2
        | Just t2' <- coreView t2 = cant_match t1 t2'
324
325

    cant_match (FunTy a1 r1) (FunTy a2 r2)
326
        = cant_match a1 a2 || cant_match r1 r2
327
328

    cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
329
330
        | isDistinctTyCon tc1 && isDistinctTyCon tc2
        = tc1 /= tc2 || typesCantMatch (zipEqual "typesCantMatch" tys1 tys2)
331

332
333
    cant_match (FunTy {}) (TyConApp tc _) = isDistinctTyCon tc
    cant_match (TyConApp tc _) (FunTy {}) = isDistinctTyCon tc
334
        -- tc can't be FunTyCon by invariant
335
336

    cant_match (AppTy f1 a1) ty2
337
338
        | Just (f2, a2) <- repSplitAppTy_maybe ty2
        = cant_match f1 f2 || cant_match a1 a2
339
    cant_match ty1 (AppTy f2 a2)
340
341
        | Just (f1, a1) <- repSplitAppTy_maybe ty1
        = cant_match f1 f2 || cant_match a1 a2
342

343
344
    cant_match (LitTy x) (LitTy y) = x /= y

twanvl's avatar
twanvl committed
345
    cant_match _ _ = False      -- Safe!
346
347

-- Things we could add;
348
349
350
--      foralls
--      look through newtypes
--      take account of tyvar bindings (EQ example above)
351
352
353
354
\end{code}


%************************************************************************
355
%*                                                                      *
356
357
             Unification
%*                                                                      *
358
359
%************************************************************************

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
360
361
362
363
364
365
Note [Fine-grained unification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
no substitution to finite types makes these match. But, a substitution to
*infinite* types can unify these two types: [x |-> [[[...]]], y |-> [[[...]]] ].
Why do we care? Consider these two type family instances:
366

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
367
368
type instance F x x   = Int
type instance F [y] y = Bool
369

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
370
If we also have
371

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
372
type instance Looper = [Looper]
373

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
374
375
376
377
then the instances potentially overlap. The solution is to use unification
over infinite terms. This is possible (see [1] for lots of gory details), but
a full algorithm is a little more power than we need. Instead, we make a
conservative approximation and just omit the occurs check.
378

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
379
[1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
380

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
381
382
tcUnifyTys considers an occurs-check problem as the same as general unification
failure.
383

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
384
385
tcUnifyTysFG ("fine-grained") returns one of three results: success, occurs-check
failure ("MaybeApart"), or general failure ("SurelyApart").
386

387
388
389
390
391
392
393
See also Trac #8162.

It's worth noting that unification in the presence of infinite types is not
complete. This means that, sometimes, a closed type family does not reduce
when it should. See test case indexed-types/should_fail/Overlap15 for an
example.

394
395
396
397
398
Note [The substitution in MaybeApart]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why?
Because consider unifying these:

399
(a, a, Int) ~ (b, [b], Bool)
400

401
402
403
404
405
406
407
408
If we go left-to-right, we start with [a |-> b]. Then, on the middle terms, we
apply the subst we have so far and discover that we need [b |-> [b]]. Because
this fails the occurs check, we say that the types are MaybeApart (see above
Note [Fine-grained unification]). But, we can't stop there! Because if we
continue, we discover that Int is SurelyApart from Bool, and therefore the
types are apart. This has practical consequences for the ability for closed
type family applications to reduce. See test case
indexed-types/should_compile/Overlap14.
409

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
410
411
412
413
414
415
Note [Unifying with skolems]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we discover that two types unify if and only if a skolem variable is
substituted, we can't properly unify the types. But, that skolem variable
may later be instantiated with a unifyable type. So, we return maybeApart
in these cases.
416

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
Note [Lists of different lengths are MaybeApart]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It is unusual to call tcUnifyTys or tcUnifyTysFG with lists of different
lengths. The place where we know this can happen is from compatibleBranches in
FamInstEnv, when checking data family instances. Data family instances may be
eta-reduced; see Note [Eta reduction for data family axioms] in TcInstDcls.

We wish to say that

  D :: * -> * -> *
  axDF1 :: D Int ~ DFInst1
  axDF2 :: D Int Bool ~ DFInst2

overlap. If we conclude that lists of different lengths are SurelyApart, then
it will look like these do *not* overlap, causing disaster. See Trac #9371.

In usages of tcUnifyTys outside of family instances, we always use tcUnifyTys,
which can't tell the difference between MaybeApart and SurelyApart, so those
usages won't notice this design choice.

437
\begin{code}
438
tcUnifyTy :: Type -> Type       -- All tyvars are bindable
439
          -> Maybe TvSubst      -- A regular one-shot (idempotent) substitution
440
441
442
443
444
445
446
-- Simple unification of two types; all type variables are bindable
tcUnifyTy ty1 ty2
  = case initUM (const BindMe) (unify emptyTvSubstEnv ty1 ty2) of
      Unifiable subst_env -> Just (niFixTvSubst subst_env)
      _other              -> Nothing

-----------------
447
tcUnifyTys :: (TyVar -> BindFlag)
448
449
           -> [Type] -> [Type]
           -> Maybe TvSubst     -- A regular one-shot (idempotent) substitution
450
451
452
-- The two types may have common type variables, and indeed do so in the
-- second call to tcUnifyTys in FunDeps.checkClsFD
tcUnifyTys bind_fn tys1 tys2
453
454
455
  = case tcUnifyTysFG bind_fn tys1 tys2 of
      Unifiable subst -> Just subst
      _               -> Nothing
456

457
-- This type does double-duty. It is used in the UM (unifier monad) and to
458
-- return the final result. See Note [Fine-grained unification]
459
460
461
462
463
464
type UnifyResult = UnifyResultM TvSubst
data UnifyResultM a = Unifiable a        -- the subst that unifies the types
                    | MaybeApart a       -- the subst has as much as we know
                                         -- it must be part of an most general unifier
                                         -- See Note [The substitution in MaybeApart]
                    | SurelyApart
465

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
466
467
468
469
470
-- See Note [Fine-grained unification]
tcUnifyTysFG :: (TyVar -> BindFlag)
             -> [Type] -> [Type]
             -> UnifyResult
tcUnifyTysFG bind_fn tys1 tys2
471
  = initUM bind_fn $
472
473
    do { subst <- unifyList emptyTvSubstEnv tys1 tys2

474
        -- Find the fixed point of the resulting non-idempotent substitution
475
476
477
478
479
        ; return (niFixTvSubst subst) }
\end{code}


%************************************************************************
480
%*                                                                      *
481
                Non-idempotent substitution
482
%*                                                                      *
483
484
485
486
487
488
489
%************************************************************************

Note [Non-idempotent substitution]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
During unification we use a TvSubstEnv that is
  (a) non-idempotent
  (b) loop-free; ie repeatedly applying it yields a fixed point
490

491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
Note [Finding the substitution fixpoint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Finding the fixpoint of a non-idempotent substitution arising from a
unification is harder than it looks, because of kinds.  Consider
   T k (H k (f:k)) ~ T * (g:*)
If we unify, we get the substitution
   [ k -> *
   , g -> H k (f:k) ]
To make it idempotent we don't want to get just
   [ k -> *
   , g -> H * (f:k) ]
We also want to substitute inside f's kind, to get
   [ k -> *
   , g -> H k (f:*) ]
If we don't do this, we may apply the substitition to something,
and get an ill-formed type, i.e. one where typeKind will fail.
This happened, for example, in Trac #9106.

This is the reason for extending env with [f:k -> f:*], in the
definition of env' in niFixTvSubst

512
513
514
\begin{code}
niFixTvSubst :: TvSubstEnv -> TvSubst
-- Find the idempotent fixed point of the non-idempotent substitution
515
-- See Note [Finding the substitution fixpoint]
516
517
-- ToDo: use laziness instead of iteration?
niFixTvSubst env = f env
518
  where
519
520
    f env | not_fixpoint = f (mapVarEnv (substTy subst') env)
          | otherwise    = subst
521
        where
522
523
524
525
526
527
528
          not_fixpoint  = foldVarSet ((||) . in_domain) False all_range_tvs
          in_domain tv  = tv `elemVarEnv` env

          range_tvs     = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet env
          all_range_tvs = closeOverKinds range_tvs
          subst         = mkTvSubst (mkInScopeSet all_range_tvs) env

529
             -- env' extends env by replacing any free type with
530
531
532
533
534
535
536
             -- that same tyvar with a substituted kind
             -- See note [Finding the substitution fixpoint]
          env'          = extendVarEnvList env [ (rtv, mkTyVarTy $ setTyVarKind rtv $
                                                       substTy subst $ tyVarKind rtv)
                                               | rtv <- varSetElems range_tvs
                                               , not (in_domain rtv) ]
          subst'        = mkTvSubst (mkInScopeSet all_range_tvs) env'
537
538
539
540
541
542
543

niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
-- Apply the non-idempotent substitution to a set of type variables,
-- remembering that the substitution isn't necessarily idempotent
-- This is used in the occurs check, before extending the substitution
niSubstTvSet subst tvs
  = foldVarSet (unionVarSet . get) emptyVarSet tvs
544
  where
545
    get tv = case lookupVarEnv subst tv of
546
               Nothing -> unitVarSet tv
547
               Just ty -> niSubstTvSet subst (tyVarsOfType ty)
548
549
550
\end{code}

%************************************************************************
551
552
553
%*                                                                      *
                The workhorse
%*                                                                      *
554
555
556
%************************************************************************

\begin{code}
557
558
559
560
unify :: TvSubstEnv     -- An existing substitution to extend
      -> Type -> Type   -- Types to be unified, and witness of their equality
      -> UM TvSubstEnv          -- Just the extended substitution,
                                -- Nothing if unification failed
561
562
563
564
565
566
567
568
569
570
571
572
573
-- We do not require the incoming substitution to be idempotent,
-- nor guarantee that the outgoing one is.  That's fixed up by
-- the wrappers.

-- Respects newtypes, PredTypes

-- in unify, any NewTcApps/Preds should be taken at face value
unify subst (TyVarTy tv1) ty2  = uVar subst tv1 ty2
unify subst ty1 (TyVarTy tv2)  = uVar subst tv2 ty1

unify subst ty1 ty2 | Just ty1' <- tcView ty1 = unify subst ty1' ty2
unify subst ty1 ty2 | Just ty2' <- tcView ty2 = unify subst ty1 ty2'

574
575
unify subst (TyConApp tyc1 tys1) (TyConApp tyc2 tys2)
  | tyc1 == tyc2
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
576
  = unify_tys subst tys1 tys2
577

578
579
580
unify subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
  = do  { subst' <- unify subst ty1a ty2a
        ; unify subst' ty1b ty2b }
581

582
583
584
585
        -- Applications need a bit of care!
        -- They can match FunTy and TyConApp, so use splitAppTy_maybe
        -- NB: we've already dealt with type variables and Notes,
        -- so if one type is an App the other one jolly well better be too
586
587
unify subst (AppTy ty1a ty1b) ty2
  | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
588
  = do  { subst' <- unify subst ty1a ty2a
589
590
591
592
        ; unify subst' ty1b ty2b }

unify subst ty1 (AppTy ty2a ty2b)
  | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
593
  = do  { subst' <- unify subst ty1a ty2a
594
595
        ; unify subst' ty1b ty2b }

596
597
unify subst (LitTy x) (LitTy y) | x == y = return subst

598
unify _ _ _ = surelyApart
599
        -- ForAlls??
600
601
602
603
604
605
606
607
608
609
610

------------------------------
unify_tys :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
unify_tys subst xs ys = unifyList subst xs ys

unifyList :: TvSubstEnv -> [Type] -> [Type] -> UM TvSubstEnv
unifyList subst orig_xs orig_ys
  = go subst orig_xs orig_ys
  where
    go subst []     []     = return subst
    go subst (x:xs) (y:ys) = do { subst' <- unify subst x y
611
                                ; go subst' xs ys }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
612
    go subst _ _ = maybeApart subst  -- See Note [Lists of different lengths are MaybeApart]
613
614

---------------------------------
615
uVar :: TvSubstEnv      -- An existing substitution to extend
616
617
618
619
620
621
622
623
624
     -> TyVar           -- Type variable to be unified
     -> Type            -- with this type
     -> UM TvSubstEnv

uVar subst tv1 ty
 = -- Check to see whether tv1 is refined by the substitution
   case (lookupVarEnv subst tv1) of
     Just ty' -> unify subst ty' ty     -- Yes, call back into unify'
     Nothing  -> uUnrefined subst       -- No, continue
625
                            tv1 ty ty
626
627
628
629
630
631
632
633
634
635
636

uUnrefined :: TvSubstEnv          -- An existing substitution to extend
           -> TyVar               -- Type variable to be unified
           -> Type                -- with this type
           -> Type                -- (version w/ expanded synonyms)
           -> UM TvSubstEnv

-- We know that tv1 isn't refined

uUnrefined subst tv1 ty2 ty2'
  | Just ty2'' <- tcView ty2'
637
638
639
640
  = uUnrefined subst tv1 ty2 ty2''      -- Unwrap synonyms
                -- This is essential, in case we have
                --      type Foo a = a
                -- and then unify a ~ Foo a
641
642

uUnrefined subst tv1 ty2 (TyVarTy tv2)
643
  | tv1 == tv2          -- Same type variable
644
645
646
647
648
649
  = return subst

    -- Check to see whether tv2 is refined
  | Just ty' <- lookupVarEnv subst tv2
  = uUnrefined subst tv1 ty' ty'

dreixel's avatar
dreixel committed
650
  | otherwise
651
652
653
654

  = do {   -- So both are unrefined; unify the kinds
       ; subst' <- unify subst (tyVarKind tv1) (tyVarKind tv2)

655
           -- And then bind one or the other,
656
           -- depending on which is bindable
657
658
           -- NB: unlike TcUnify we do not have an elaborate sub-kinding
           --     story.  That is relevant only during type inference, and
659
660
661
662
663
           --     (I very much hope) is not relevant here.
       ; b1 <- tvBindFlag tv1
       ; b2 <- tvBindFlag tv2
       ; let ty1 = TyVarTy tv1
       ; case (b1, b2) of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
664
           (Skolem, Skolem) -> maybeApart subst' -- See Note [Unification with skolems]
665
666
           (BindMe, _)      -> return (extendVarEnv subst' tv1 ty2)
           (_, BindMe)      -> return (extendVarEnv subst' tv2 ty1) }
667

668
uUnrefined subst tv1 ty2 ty2'   -- ty2 is not a type variable
669
  | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
670
  = maybeApart subst                    -- Occurs check
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
671
                                        -- See Note [Fine-grained unification]
672
  | otherwise
673
  = do { subst' <- unify subst k1 k2
674
       -- Note [Kinds Containing Only Literals]
675
       ; bindTv subst' tv1 ty2 }        -- Bind tyvar to the synonym if poss
676
677
678
679
680
  where
    k1 = tyVarKind tv1
    k2 = typeKind ty2'

bindTv :: TvSubstEnv -> TyVar -> Type -> UM TvSubstEnv
681
bindTv subst tv ty      -- ty is not a type variable
682
  = do  { b <- tvBindFlag tv
683
684
685
686
        ; case b of
            Skolem -> maybeApart subst -- See Note [Unification with skolems]
            BindMe -> return $ extendVarEnv subst tv ty
        }
687
688
689
\end{code}

%************************************************************************
690
691
692
%*                                                                      *
                Binding decisions
%*                                                                      *
693
694
695
%************************************************************************

\begin{code}
696
697
data BindFlag
  = BindMe      -- A regular type variable
698

699
700
  | Skolem      -- This type variable is a skolem constant
                -- Don't bind it; it only matches itself
701
702
\end{code}

703

704
%************************************************************************
705
706
707
%*                                                                      *
                Unification monad
%*                                                                      *
708
%************************************************************************
709

710
\begin{code}
711
newtype UM a = UM { unUM :: (TyVar -> BindFlag)
712
                         -> UnifyResultM a }
713

Austin Seipp's avatar
Austin Seipp committed
714
715
716
717
718
719
720
instance Functor UM where
      fmap = liftM

instance Applicative UM where
      pure = return
      (<*>) = ap

721
instance Monad UM where
722
723
  return a = UM (\_tvs -> Unifiable a)
  fail _   = UM (\_tvs -> SurelyApart) -- failed pattern match
724
  m >>= k  = UM (\tvs -> case unUM m tvs of
725
                           Unifiable v -> unUM (k v) tvs
726
727
728
729
730
731
                           MaybeApart v ->
                             case unUM (k v) tvs of
                               Unifiable v' -> MaybeApart v'
                               other        -> other
                           SurelyApart -> SurelyApart)

732
initUM :: (TyVar -> BindFlag) -> UM a -> UnifyResultM a
733
initUM badtvs um = unUM um badtvs
734

735
tvBindFlag :: TyVar -> UM BindFlag
736
tvBindFlag tv = UM (\tv_fn -> Unifiable (tv_fn tv))
737

738
739
maybeApart :: TvSubstEnv -> UM TvSubstEnv
maybeApart subst = UM (\_tv_fn -> MaybeApart subst)
740

741
surelyApart :: UM a
742
surelyApart = UM (\_tv_fn -> SurelyApart)
743
\end{code}