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