Refactoring around FunDeps
[ghc.git] / compiler / types / Unify.hs
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE CPP, DeriveFunctor #-}
4
5 module Unify (
6 -- Matching of types:
7 -- the "tc" prefix indicates that matching always
8 -- respects newtypes (rather than looking through them)
9 tcMatchTy, tcMatchTys, tcMatchTyX, tcMatchTysX,
10 ruleMatchTyX, tcMatchPreds,
11
12 MatchEnv(..), matchList,
13
14 typesCantMatch,
15
16 -- Side-effect free unification
17 tcUnifyTy, tcUnifyTys, BindFlag(..),
18
19 UnifyResultM(..), UnifyResult, tcUnifyTysFG
20
21 ) where
22
23 #include "HsVersions.h"
24
25 import Var
26 import VarEnv
27 import VarSet
28 import Kind
29 import Type
30 import TyCon
31 import TypeRep
32
33 import Control.Monad (liftM, ap)
34 #if __GLASGOW_HASKELL__ < 709
35 import Control.Applicative (Applicative(..))
36 #endif
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 data MatchEnv
69 = ME { me_tmpls :: VarSet -- Template variables
70 , me_env :: RnEnv2 -- Renaming envt for nested foralls
71 } -- In-scope set includes template variables
72 -- Nota Bene: MatchEnv isn't specific to Types. It is used
73 -- for matching terms and coercions as well as types
74
75 tcMatchTy :: TyVarSet -- Template tyvars
76 -> Type -- Template
77 -> Type -- Target
78 -> Maybe TvSubst -- One-shot; in principle the template
79 -- variables could be free in the target
80 tcMatchTy tmpls ty1 ty2
81 = tcMatchTyX tmpls init_subst ty1 ty2
82 where
83 init_subst = mkTvSubst in_scope emptyTvSubstEnv
84 in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
85 -- We're assuming that all the interesting
86 -- tyvars in ty1 are in tmpls
87
88 tcMatchTys :: TyVarSet -- Template tyvars
89 -> [Type] -- Template
90 -> [Type] -- Target
91 -> Maybe TvSubst -- One-shot; in principle the template
92 -- variables could be free in the target
93 tcMatchTys tmpls tys1 tys2
94 = tcMatchTysX tmpls init_subst tys1 tys2
95 where
96 init_subst = mkTvSubst in_scope emptyTvSubstEnv
97 in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
98
99 tcMatchTyX :: TyVarSet -- Template tyvars
100 -> TvSubst -- Substitution to extend
101 -> Type -- Template
102 -> Type -- Target
103 -> Maybe TvSubst
104 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
105 = case match menv subst_env ty1 ty2 of
106 Just subst_env' -> Just (TvSubst in_scope subst_env')
107 Nothing -> Nothing
108 where
109 menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
110
111 tcMatchTysX :: TyVarSet -- Template tyvars
112 -> TvSubst -- Substitution to extend
113 -> [Type] -- Template
114 -> [Type] -- Target
115 -> Maybe TvSubst -- One-shot; in principle the template
116 -- variables could be free in the target
117 tcMatchTysX tmpls (TvSubst in_scope subst_env) tys1 tys2
118 = case match_tys menv subst_env tys1 tys2 of
119 Just subst_env' -> Just (TvSubst in_scope subst_env')
120 Nothing -> Nothing
121 where
122 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
123
124 tcMatchPreds
125 :: [TyVar] -- Bind these
126 -> [PredType] -> [PredType]
127 -> Maybe TvSubstEnv
128 tcMatchPreds tmpls ps1 ps2
129 = matchList (match menv) emptyTvSubstEnv ps1 ps2
130 where
131 menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
132 in_scope_tyvars = mkInScopeSet (tyVarsOfTypes ps1 `unionVarSet` tyVarsOfTypes ps2)
133
134 -- This one is called from the expression matcher, which already has a MatchEnv in hand
135 ruleMatchTyX :: MatchEnv
136 -> TvSubstEnv -- Substitution to extend
137 -> Type -- Template
138 -> Type -- Target
139 -> Maybe TvSubstEnv
140
141 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2 -- Rename for export
142
143 -- Now the internals of matching
144
145 -- | Workhorse matching function. Our goal is to find a substitution
146 -- on all of the template variables (specified by @me_tmpls menv@) such
147 -- that @ty1@ and @ty2@ unify. This substitution is accumulated in @subst@.
148 -- If a variable is not a template variable, we don't attempt to find a
149 -- substitution for it; it must match exactly on both sides. Furthermore,
150 -- only @ty1@ can have template variables.
151 --
152 -- This function handles binders, see 'RnEnv2' for more details on
153 -- how that works.
154 match :: MatchEnv -- For the most part this is pushed downwards
155 -> TvSubstEnv -- Substitution so far:
156 -- Domain is subset of template tyvars
157 -- Free vars of range is subset of
158 -- in-scope set of the RnEnv2
159 -> Type -> Type -- Template and target respectively
160 -> Maybe TvSubstEnv
161
162 match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
163 | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
164
165 match menv subst (TyVarTy tv1) ty2
166 | Just ty1' <- lookupVarEnv subst tv1' -- tv1' is already bound
167 = if eqTypeX (nukeRnEnvL rn_env) ty1' ty2
168 -- ty1 has no locally-bound variables, hence nukeRnEnvL
169 then Just subst
170 else Nothing -- ty2 doesn't match
171
172 | tv1' `elemVarSet` me_tmpls menv
173 = if any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
174 then Nothing -- Occurs check
175 -- ezyang: Is this really an occurs check? It seems
176 -- to just reject matching \x. A against \x. x (maintaining
177 -- the invariant that the free vars of the range of @subst@
178 -- are a subset of the in-scope set in @me_env menv@.)
179 else do { subst1 <- match_kind menv subst (tyVarKind tv1) (typeKind ty2)
180 -- Note [Matching kinds]
181 ; return (extendVarEnv subst1 tv1' ty2) }
182
183 | otherwise -- tv1 is not a template tyvar
184 = case ty2 of
185 TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
186 _ -> Nothing
187 where
188 rn_env = me_env menv
189 tv1' = rnOccL rn_env tv1
190
191 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2)
192 = do { subst' <- match_kind menv subst (tyVarKind tv1) (tyVarKind tv2)
193 ; match menv' subst' ty1 ty2 }
194 where -- Use the magic of rnBndr2 to go under the binders
195 menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
196
197 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2)
198 | tc1 == tc2 = match_tys menv subst tys1 tys2
199 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
200 = do { subst' <- match menv subst ty1a ty2a
201 ; match menv subst' ty1b ty2b }
202 match menv subst (AppTy ty1a ty1b) ty2
203 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
204 -- 'repSplit' used because the tcView stuff is done above
205 = do { subst' <- match menv subst ty1a ty2a
206 ; match menv subst' ty1b ty2b }
207
208 match _ subst (LitTy x) (LitTy y) | x == y = return subst
209
210 match _ _ _ _
211 = Nothing
212
213
214
215 --------------
216 match_kind :: MatchEnv -> TvSubstEnv -> Kind -> Kind -> Maybe TvSubstEnv
217 -- Match the kind of the template tyvar with the kind of Type
218 -- Note [Matching kinds]
219 match_kind menv subst k1 k2
220 | k2 `isSubKind` k1
221 = return subst
222
223 | otherwise
224 = match menv subst k1 k2
225
226 -- Note [Matching kinds]
227 -- ~~~~~~~~~~~~~~~~~~~~~
228 -- For ordinary type variables, we don't want (m a) to match (n b)
229 -- if say (a::*) and (b::*->*). This is just a yes/no issue.
230 --
231 -- For coercion kinds matters are more complicated. If we have a
232 -- coercion template variable co::a~[b], where a,b are presumably also
233 -- template type variables, then we must match co's kind against the
234 -- kind of the actual argument, so as to give bindings to a,b.
235 --
236 -- In fact I have no example in mind that *requires* this kind-matching
237 -- to instantiate template type variables, but it seems like the right
238 -- thing to do. C.f. Note [Matching variable types] in Rules.hs
239
240 --------------
241 match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
242 match_tys menv subst tys1 tys2 = matchList (match menv) subst tys1 tys2
243
244 --------------
245 matchList :: (env -> a -> b -> Maybe env)
246 -> env -> [a] -> [b] -> Maybe env
247 matchList _ subst [] [] = Just subst
248 matchList fn subst (a:as) (b:bs) = do { subst' <- fn subst a b
249 ; matchList fn subst' as bs }
250 matchList _ _ _ _ = Nothing
251
252 {-
253 ************************************************************************
254 * *
255 GADTs
256 * *
257 ************************************************************************
258
259 Note [Pruning dead case alternatives]
260 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
261 Consider data T a where
262 T1 :: T Int
263 T2 :: T a
264
265 newtype X = MkX Int
266 newtype Y = MkY Char
267
268 type family F a
269 type instance F Bool = Int
270
271 Now consider case x of { T1 -> e1; T2 -> e2 }
272
273 The question before the house is this: if I know something about the type
274 of x, can I prune away the T1 alternative?
275
276 Suppose x::T Char. It's impossible to construct a (T Char) using T1,
277 Answer = YES we can prune the T1 branch (clearly)
278
279 Suppose x::T (F a), where 'a' is in scope. Then 'a' might be instantiated
280 to 'Bool', in which case x::T Int, so
281 ANSWER = NO (clearly)
282
283 We see here that we want precisely the apartness check implemented within
284 tcUnifyTysFG. So that's what we do! Two types cannot match if they are surely
285 apart. Note that since we are simply dropping dead code, a conservative test
286 suffices.
287 -}
288
289 -- | Given a list of pairs of types, are any two members of a pair surely
290 -- apart, even after arbitrary type function evaluation and substitution?
291 typesCantMatch :: [(Type,Type)] -> Bool
292 -- See Note [Pruning dead case alternatives]
293 typesCantMatch prs = any (\(s,t) -> cant_match s t) prs
294 where
295 cant_match :: Type -> Type -> Bool
296 cant_match t1 t2 = case tcUnifyTysFG (const BindMe) [t1] [t2] of
297 SurelyApart -> True
298 _ -> False
299
300 {-
301 ************************************************************************
302 * *
303 Unification
304 * *
305 ************************************************************************
306
307 Note [Fine-grained unification]
308 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
309 Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
310 no substitution to finite types makes these match. But, a substitution to
311 *infinite* types can unify these two types: [x |-> [[[...]]], y |-> [[[...]]] ].
312 Why do we care? Consider these two type family instances:
313
314 type instance F x x = Int
315 type instance F [y] y = Bool
316
317 If we also have
318
319 type instance Looper = [Looper]
320
321 then the instances potentially overlap. The solution is to use unification
322 over infinite terms. This is possible (see [1] for lots of gory details), but
323 a full algorithm is a little more power than we need. Instead, we make a
324 conservative approximation and just omit the occurs check.
325
326 [1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
327
328 tcUnifyTys considers an occurs-check problem as the same as general unification
329 failure.
330
331 tcUnifyTysFG ("fine-grained") returns one of three results: success, occurs-check
332 failure ("MaybeApart"), or general failure ("SurelyApart").
333
334 See also Trac #8162.
335
336 It's worth noting that unification in the presence of infinite types is not
337 complete. This means that, sometimes, a closed type family does not reduce
338 when it should. See test case indexed-types/should_fail/Overlap15 for an
339 example.
340
341 Note [The substitution in MaybeApart]
342 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
343 The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why?
344 Because consider unifying these:
345
346 (a, a, Int) ~ (b, [b], Bool)
347
348 If we go left-to-right, we start with [a |-> b]. Then, on the middle terms, we
349 apply the subst we have so far and discover that we need [b |-> [b]]. Because
350 this fails the occurs check, we say that the types are MaybeApart (see above
351 Note [Fine-grained unification]). But, we can't stop there! Because if we
352 continue, we discover that Int is SurelyApart from Bool, and therefore the
353 types are apart. This has practical consequences for the ability for closed
354 type family applications to reduce. See test case
355 indexed-types/should_compile/Overlap14.
356
357 Note [Unifying with skolems]
358 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
359 If we discover that two types unify if and only if a skolem variable is
360 substituted, we can't properly unify the types. But, that skolem variable
361 may later be instantiated with a unifyable type. So, we return maybeApart
362 in these cases.
363
364 Note [Lists of different lengths are MaybeApart]
365 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
366 It is unusual to call tcUnifyTys or tcUnifyTysFG with lists of different
367 lengths. The place where we know this can happen is from compatibleBranches in
368 FamInstEnv, when checking data family instances. Data family instances may be
369 eta-reduced; see Note [Eta reduction for data family axioms] in TcInstDcls.
370
371 We wish to say that
372
373 D :: * -> * -> *
374 axDF1 :: D Int ~ DFInst1
375 axDF2 :: D Int Bool ~ DFInst2
376
377 overlap. If we conclude that lists of different lengths are SurelyApart, then
378 it will look like these do *not* overlap, causing disaster. See Trac #9371.
379
380 In usages of tcUnifyTys outside of family instances, we always use tcUnifyTys,
381 which can't tell the difference between MaybeApart and SurelyApart, so those
382 usages won't notice this design choice.
383 -}
384
385 tcUnifyTy :: Type -> Type -- All tyvars are bindable
386 -> Maybe TvSubst -- A regular one-shot (idempotent) substitution
387 -- Simple unification of two types; all type variables are bindable
388 tcUnifyTy ty1 ty2
389 = case initUM (const BindMe) (unify ty1 ty2) of
390 Unifiable subst -> Just subst
391 _other -> Nothing
392
393 -----------------
394 tcUnifyTys :: (TyVar -> BindFlag)
395 -> [Type] -> [Type]
396 -> Maybe TvSubst -- A regular one-shot (idempotent) substitution
397 -- The two types may have common type variables, and indeed do so in the
398 -- second call to tcUnifyTys in FunDeps.checkClsFD
399 tcUnifyTys bind_fn tys1 tys2
400 = case tcUnifyTysFG bind_fn tys1 tys2 of
401 Unifiable subst -> Just subst
402 _ -> Nothing
403
404 -- This type does double-duty. It is used in the UM (unifier monad) and to
405 -- return the final result. See Note [Fine-grained unification]
406 type UnifyResult = UnifyResultM TvSubst
407 data UnifyResultM a = Unifiable a -- the subst that unifies the types
408 | MaybeApart a -- the subst has as much as we know
409 -- it must be part of an most general unifier
410 -- See Note [The substitution in MaybeApart]
411 | SurelyApart
412 deriving Functor
413
414 -- See Note [Fine-grained unification]
415 tcUnifyTysFG :: (TyVar -> BindFlag)
416 -> [Type] -> [Type]
417 -> UnifyResult
418 tcUnifyTysFG bind_fn tys1 tys2
419 = initUM bind_fn (unify_tys tys1 tys2)
420
421 {-
422 ************************************************************************
423 * *
424 Non-idempotent substitution
425 * *
426 ************************************************************************
427
428 Note [Non-idempotent substitution]
429 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
430 During unification we use a TvSubstEnv that is
431 (a) non-idempotent
432 (b) loop-free; ie repeatedly applying it yields a fixed point
433
434 Note [Finding the substitution fixpoint]
435 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
436 Finding the fixpoint of a non-idempotent substitution arising from a
437 unification is harder than it looks, because of kinds. Consider
438 T k (H k (f:k)) ~ T * (g:*)
439 If we unify, we get the substitution
440 [ k -> *
441 , g -> H k (f:k) ]
442 To make it idempotent we don't want to get just
443 [ k -> *
444 , g -> H * (f:k) ]
445 We also want to substitute inside f's kind, to get
446 [ k -> *
447 , g -> H k (f:*) ]
448 If we don't do this, we may apply the substitition to something,
449 and get an ill-formed type, i.e. one where typeKind will fail.
450 This happened, for example, in Trac #9106.
451
452 This is the reason for extending env with [f:k -> f:*], in the
453 definition of env' in niFixTvSubst
454 -}
455
456 niFixTvSubst :: TvSubstEnv -> TvSubst
457 -- Find the idempotent fixed point of the non-idempotent substitution
458 -- See Note [Finding the substitution fixpoint]
459 -- ToDo: use laziness instead of iteration?
460 niFixTvSubst env = f env
461 where
462 f env | not_fixpoint = f (mapVarEnv (substTy subst') env)
463 | otherwise = subst
464 where
465 not_fixpoint = foldVarSet ((||) . in_domain) False all_range_tvs
466 in_domain tv = tv `elemVarEnv` env
467
468 range_tvs = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet env
469 all_range_tvs = closeOverKinds range_tvs
470 subst = mkTvSubst (mkInScopeSet all_range_tvs) env
471
472 -- env' extends env by replacing any free type with
473 -- that same tyvar with a substituted kind
474 -- See note [Finding the substitution fixpoint]
475 env' = extendVarEnvList env [ (rtv, mkTyVarTy $ setTyVarKind rtv $
476 substTy subst $ tyVarKind rtv)
477 | rtv <- varSetElems range_tvs
478 , not (in_domain rtv) ]
479 subst' = mkTvSubst (mkInScopeSet all_range_tvs) env'
480
481 niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
482 -- Apply the non-idempotent substitution to a set of type variables,
483 -- remembering that the substitution isn't necessarily idempotent
484 -- This is used in the occurs check, before extending the substitution
485 niSubstTvSet subst tvs
486 = foldVarSet (unionVarSet . get) emptyVarSet tvs
487 where
488 get tv = case lookupVarEnv subst tv of
489 Nothing -> unitVarSet tv
490 Just ty -> niSubstTvSet subst (tyVarsOfType ty)
491
492 {-
493 ************************************************************************
494 * *
495 The workhorse
496 * *
497 ************************************************************************
498 -}
499
500 unify :: Type -> Type -> UM ()
501 -- Respects newtypes, PredTypes
502
503 -- in unify, any NewTcApps/Preds should be taken at face value
504 unify (TyVarTy tv1) ty2 = uVar tv1 ty2
505 unify ty1 (TyVarTy tv2) = uVar tv2 ty1
506
507 unify ty1 ty2 | Just ty1' <- tcView ty1 = unify ty1' ty2
508 unify ty1 ty2 | Just ty2' <- tcView ty2 = unify ty1 ty2'
509
510 unify ty1 ty2
511 | Just (tc1, tys1) <- splitTyConApp_maybe ty1
512 , Just (tc2, tys2) <- splitTyConApp_maybe ty2
513 = if tc1 == tc2
514 then if isInjectiveTyCon tc1 Nominal
515 then unify_tys tys1 tys2
516 else don'tBeSoSure $ unify_tys tys1 tys2
517 else -- tc1 /= tc2
518 if isGenerativeTyCon tc1 Nominal && isGenerativeTyCon tc2 Nominal
519 then surelyApart
520 else maybeApart
521
522 -- Applications need a bit of care!
523 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
524 -- NB: we've already dealt with type variables and Notes,
525 -- so if one type is an App the other one jolly well better be too
526 unify (AppTy ty1a ty1b) ty2
527 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
528 = do { unify ty1a ty2a
529 ; unify ty1b ty2b }
530
531 unify ty1 (AppTy ty2a ty2b)
532 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
533 = do { unify ty1a ty2a
534 ; unify ty1b ty2b }
535
536 unify (LitTy x) (LitTy y) | x == y = return ()
537
538 unify _ _ = surelyApart
539 -- ForAlls??
540
541 ------------------------------
542 unify_tys :: [Type] -> [Type] -> UM ()
543 unify_tys orig_xs orig_ys
544 = go orig_xs orig_ys
545 where
546 go [] [] = return ()
547 go (x:xs) (y:ys) = do { unify x y
548 ; go xs ys }
549 go _ _ = maybeApart -- See Note [Lists of different lengths are MaybeApart]
550
551 ---------------------------------
552 uVar :: TyVar -- Type variable to be unified
553 -> Type -- with this type
554 -> UM ()
555
556 uVar tv1 ty
557 = do { subst <- umGetTvSubstEnv
558 -- Check to see whether tv1 is refined by the substitution
559 ; case (lookupVarEnv subst tv1) of
560 Just ty' -> unify ty' ty -- Yes, call back into unify'
561 Nothing -> uUnrefined subst tv1 ty ty } -- No, continue
562
563 uUnrefined :: TvSubstEnv -- environment to extend (from the UM monad)
564 -> TyVar -- Type variable to be unified
565 -> Type -- with this type
566 -> Type -- (version w/ expanded synonyms)
567 -> UM ()
568
569 -- We know that tv1 isn't refined
570
571 uUnrefined subst tv1 ty2 ty2'
572 | Just ty2'' <- tcView ty2'
573 = uUnrefined subst tv1 ty2 ty2'' -- Unwrap synonyms
574 -- This is essential, in case we have
575 -- type Foo a = a
576 -- and then unify a ~ Foo a
577
578 uUnrefined subst tv1 ty2 (TyVarTy tv2)
579 | tv1 == tv2 -- Same type variable
580 = return ()
581
582 -- Check to see whether tv2 is refined
583 | Just ty' <- lookupVarEnv subst tv2
584 = uUnrefined subst tv1 ty' ty'
585
586 | otherwise
587
588 = do { -- So both are unrefined; unify the kinds
589 ; unify (tyVarKind tv1) (tyVarKind tv2)
590
591 -- And then bind one or the other,
592 -- depending on which is bindable
593 -- NB: unlike TcUnify we do not have an elaborate sub-kinding
594 -- story. That is relevant only during type inference, and
595 -- (I very much hope) is not relevant here.
596 ; b1 <- tvBindFlag tv1
597 ; b2 <- tvBindFlag tv2
598 ; let ty1 = TyVarTy tv1
599 ; case (b1, b2) of
600 (Skolem, Skolem) -> maybeApart -- See Note [Unification with skolems]
601 (BindMe, _) -> extendSubst tv1 ty2
602 (_, BindMe) -> extendSubst tv2 ty1 }
603
604 uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable
605 | tv1 `elemVarSet` niSubstTvSet subst (tyVarsOfType ty2')
606 = maybeApart -- Occurs check
607 -- See Note [Fine-grained unification]
608 | otherwise
609 = do { unify k1 k2
610 -- Note [Kinds Containing Only Literals]
611 ; bindTv tv1 ty2 } -- Bind tyvar to the synonym if poss
612 where
613 k1 = tyVarKind tv1
614 k2 = typeKind ty2'
615
616 bindTv :: TyVar -> Type -> UM ()
617 bindTv tv ty -- ty is not a type variable
618 = do { b <- tvBindFlag tv
619 ; case b of
620 Skolem -> maybeApart -- See Note [Unification with skolems]
621 BindMe -> extendSubst tv ty
622 }
623
624 {-
625 ************************************************************************
626 * *
627 Binding decisions
628 * *
629 ************************************************************************
630 -}
631
632 data BindFlag
633 = BindMe -- A regular type variable
634
635 | Skolem -- This type variable is a skolem constant
636 -- Don't bind it; it only matches itself
637
638 {-
639 ************************************************************************
640 * *
641 Unification monad
642 * *
643 ************************************************************************
644 -}
645
646 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
647 -> TvSubstEnv
648 -> UnifyResultM (a, TvSubstEnv) }
649
650 instance Functor UM where
651 fmap = liftM
652
653 instance Applicative UM where
654 pure = return
655 (<*>) = ap
656
657 instance Monad UM where
658 return a = UM (\_tvs subst -> Unifiable (a, subst))
659 fail _ = UM (\_tvs _subst -> SurelyApart) -- failed pattern match
660 m >>= k = UM (\tvs subst -> case unUM m tvs subst of
661 Unifiable (v, subst') -> unUM (k v) tvs subst'
662 MaybeApart (v, subst') ->
663 case unUM (k v) tvs subst' of
664 Unifiable (v', subst'') -> MaybeApart (v', subst'')
665 other -> other
666 SurelyApart -> SurelyApart)
667
668 -- returns an idempotent substitution
669 initUM :: (TyVar -> BindFlag) -> UM () -> UnifyResult
670 initUM badtvs um = fmap (niFixTvSubst . snd) $ unUM um badtvs emptyTvSubstEnv
671
672 tvBindFlag :: TyVar -> UM BindFlag
673 tvBindFlag tv = UM (\tv_fn subst -> Unifiable (tv_fn tv, subst))
674
675 -- | Extend the TvSubstEnv in the UM monad
676 extendSubst :: TyVar -> Type -> UM ()
677 extendSubst tv ty = UM (\_tv_fn subst -> Unifiable ((), extendVarEnv subst tv ty))
678
679 -- | Retrive the TvSubstEnv from the UM monad
680 umGetTvSubstEnv :: UM TvSubstEnv
681 umGetTvSubstEnv = UM $ \_tv_fn subst -> Unifiable (subst, subst)
682
683 -- | Converts any SurelyApart to a MaybeApart
684 don'tBeSoSure :: UM () -> UM ()
685 don'tBeSoSure um = UM $ \tv_fn subst -> case unUM um tv_fn subst of
686 SurelyApart -> MaybeApart ((), subst)
687 other -> other
688
689 maybeApart :: UM ()
690 maybeApart = UM (\_tv_fn subst -> MaybeApart ((), subst))
691
692 surelyApart :: UM a
693 surelyApart = UM (\_tv_fn _subst -> SurelyApart)