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