Comments only
[ghc.git] / compiler / types / Unify.hs
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE ScopedTypeVariables #-}
4 {-# LANGUAGE CPP #-}
5 {-# LANGUAGE DeriveFunctor #-}
6
7 module Unify (
8 tcMatchTy, tcMatchTyKi,
9 tcMatchTys, tcMatchTyKis,
10 tcMatchTyX, tcMatchTysX, tcMatchTyKisX,
11 ruleMatchTyKiX,
12
13 -- * Rough matching
14 roughMatchTcs, instanceCantMatch,
15 typesCantMatch,
16
17 -- Side-effect free unification
18 tcUnifyTy, tcUnifyTyKi, tcUnifyTys, tcUnifyTyKis,
19 tcUnifyTysFG, tcUnifyTyWithTFs,
20 BindFlag(..),
21 UnifyResult, UnifyResultM(..),
22
23 -- Matching a type against a lifted type (coercion)
24 liftCoMatch
25 ) where
26
27 #include "HsVersions.h"
28
29 import GhcPrelude
30
31 import Var
32 import VarEnv
33 import VarSet
34 import Kind
35 import Name( Name )
36 import Type hiding ( getTvSubstEnv )
37 import Coercion hiding ( getCvSubstEnv )
38 import TyCon
39 import TyCoRep hiding ( getTvSubstEnv, getCvSubstEnv )
40 import Util
41 import Pair
42 import Outputable
43 import UniqFM
44 import UniqSet
45
46 import Control.Monad
47 import qualified Control.Monad.Fail as MonadFail
48 import Control.Applicative hiding ( empty )
49 import qualified Control.Applicative
50
51 {-
52
53 Unification is much tricker than you might think.
54
55 1. The substitution we generate binds the *template type variables*
56 which are given to us explicitly.
57
58 2. We want to match in the presence of foralls;
59 e.g (forall a. t1) ~ (forall b. t2)
60
61 That is what the RnEnv2 is for; it does the alpha-renaming
62 that makes it as if a and b were the same variable.
63 Initialising the RnEnv2, so that it can generate a fresh
64 binder when necessary, entails knowing the free variables of
65 both types.
66
67 3. We must be careful not to bind a template type variable to a
68 locally bound variable. E.g.
69 (forall a. x) ~ (forall b. b)
70 where x is the template type variable. Then we do not want to
71 bind x to a/b! This is a kind of occurs check.
72 The necessary locals accumulate in the RnEnv2.
73
74 Note [tcMatchTy vs tcMatchTyKi]
75 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
76 This module offers two variants of matching: with kinds and without.
77 The TyKi variant takes two types, of potentially different kinds,
78 and matches them. Along the way, it necessarily also matches their
79 kinds. The Ty variant instead assumes that the kinds are already
80 eqType and so skips matching up the kinds.
81
82 How do you choose between them?
83
84 1. If you know that the kinds of the two types are eqType, use
85 the Ty variant. It is more efficient, as it does less work.
86
87 2. If the kinds of variables in the template type might mention type families,
88 use the Ty variant (and do other work to make sure the kinds
89 work out). These pure unification functions do a straightforward
90 syntactic unification and do no complex reasoning about type
91 families. Note that the types of the variables in instances can indeed
92 mention type families, so instance lookup must use the Ty variant.
93
94 (Nothing goes terribly wrong -- no panics -- if there might be type
95 families in kinds in the TyKi variant. You just might get match
96 failure even though a reducing a type family would lead to success.)
97
98 3. Otherwise, if you're sure that the variable kinds to not mention
99 type families and you're not already sure that the kind of the template
100 equals the kind of the target, then use the TyKi versio.n
101 -}
102
103 -- | @tcMatchTy t1 t2@ produces a substitution (over fvs(t1))
104 -- @s@ such that @s(t1)@ equals @t2@.
105 -- The returned substitution might bind coercion variables,
106 -- if the variable is an argument to a GADT constructor.
107 --
108 -- Precondition: typeKind ty1 `eqType` typeKind ty2
109 --
110 -- We don't pass in a set of "template variables" to be bound
111 -- by the match, because tcMatchTy (and similar functions) are
112 -- always used on top-level types, so we can bind any of the
113 -- free variables of the LHS.
114 -- See also Note [tcMatchTy vs tcMatchTyKi]
115 tcMatchTy :: Type -> Type -> Maybe TCvSubst
116 tcMatchTy ty1 ty2 = tcMatchTys [ty1] [ty2]
117
118 -- | Like 'tcMatchTy', but allows the kinds of the types to differ,
119 -- and thus matches them as well.
120 -- See also Note [tcMatchTy vs tcMatchTyKi]
121 tcMatchTyKi :: Type -> Type -> Maybe TCvSubst
122 tcMatchTyKi ty1 ty2 = tcMatchTyKis [ty1] [ty2]
123
124 -- | This is similar to 'tcMatchTy', but extends a substitution
125 -- See also Note [tcMatchTy vs tcMatchTyKi]
126 tcMatchTyX :: TCvSubst -- ^ Substitution to extend
127 -> Type -- ^ Template
128 -> Type -- ^ Target
129 -> Maybe TCvSubst
130 tcMatchTyX subst ty1 ty2 = tcMatchTysX subst [ty1] [ty2]
131
132 -- | Like 'tcMatchTy' but over a list of types.
133 -- See also Note [tcMatchTy vs tcMatchTyKi]
134 tcMatchTys :: [Type] -- ^ Template
135 -> [Type] -- ^ Target
136 -> Maybe TCvSubst -- ^ One-shot; in principle the template
137 -- variables could be free in the target
138 tcMatchTys tys1 tys2
139 = tcMatchTysX (mkEmptyTCvSubst in_scope) tys1 tys2
140 where
141 in_scope = mkInScopeSet (tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2)
142
143 -- | Like 'tcMatchTyKi' but over a list of types.
144 -- See also Note [tcMatchTy vs tcMatchTyKi]
145 tcMatchTyKis :: [Type] -- ^ Template
146 -> [Type] -- ^ Target
147 -> Maybe TCvSubst -- ^ One-shot substitution
148 tcMatchTyKis tys1 tys2
149 = tcMatchTyKisX (mkEmptyTCvSubst in_scope) tys1 tys2
150 where
151 in_scope = mkInScopeSet (tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2)
152
153 -- | Like 'tcMatchTys', but extending a substitution
154 -- See also Note [tcMatchTy vs tcMatchTyKi]
155 tcMatchTysX :: TCvSubst -- ^ Substitution to extend
156 -> [Type] -- ^ Template
157 -> [Type] -- ^ Target
158 -> Maybe TCvSubst -- ^ One-shot substitution
159 tcMatchTysX subst tys1 tys2
160 = tc_match_tys_x False subst tys1 tys2
161
162 -- | Like 'tcMatchTyKis', but extending a substitution
163 -- See also Note [tcMatchTy vs tcMatchTyKi]
164 tcMatchTyKisX :: TCvSubst -- ^ Substitution to extend
165 -> [Type] -- ^ Template
166 -> [Type] -- ^ Target
167 -> Maybe TCvSubst -- ^ One-shot substitution
168 tcMatchTyKisX subst tys1 tys2
169 = tc_match_tys_x True subst tys1 tys2
170
171 -- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX'
172 tc_match_tys_x :: Bool -- ^ match kinds?
173 -> TCvSubst
174 -> [Type]
175 -> [Type]
176 -> Maybe TCvSubst
177 tc_match_tys_x match_kis (TCvSubst in_scope tv_env cv_env) tys1 tys2
178 = case tc_unify_tys (const BindMe)
179 False -- Matching, not unifying
180 False -- Not an injectivity check
181 match_kis
182 (mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of
183 Unifiable (tv_env', cv_env')
184 -> Just $ TCvSubst in_scope tv_env' cv_env'
185 _ -> Nothing
186
187 -- | This one is called from the expression matcher,
188 -- which already has a MatchEnv in hand
189 ruleMatchTyKiX
190 :: TyCoVarSet -- ^ template variables
191 -> RnEnv2
192 -> TvSubstEnv -- ^ type substitution to extend
193 -> Type -- ^ Template
194 -> Type -- ^ Target
195 -> Maybe TvSubstEnv
196 ruleMatchTyKiX tmpl_tvs rn_env tenv tmpl target
197 -- See Note [Kind coercions in Unify]
198 = case tc_unify_tys (matchBindFun tmpl_tvs) False False
199 True -- <-- this means to match the kinds
200 rn_env tenv emptyCvSubstEnv [tmpl] [target] of
201 Unifiable (tenv', _) -> Just tenv'
202 _ -> Nothing
203
204 matchBindFun :: TyCoVarSet -> TyVar -> BindFlag
205 matchBindFun tvs tv = if tv `elemVarSet` tvs then BindMe else Skolem
206
207
208 {- *********************************************************************
209 * *
210 Rough matching
211 * *
212 ********************************************************************* -}
213
214 -- See Note [Rough match] field in InstEnv
215
216 roughMatchTcs :: [Type] -> [Maybe Name]
217 roughMatchTcs tys = map rough tys
218 where
219 rough ty
220 | Just (ty', _) <- splitCastTy_maybe ty = rough ty'
221 | Just (tc,_) <- splitTyConApp_maybe ty = Just (tyConName tc)
222 | otherwise = Nothing
223
224 instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
225 -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot
226 -- possibly be instantiated to actual, nor vice versa;
227 -- False is non-committal
228 instanceCantMatch (mt : ts) (ma : as) = itemCantMatch mt ma || instanceCantMatch ts as
229 instanceCantMatch _ _ = False -- Safe
230
231 itemCantMatch :: Maybe Name -> Maybe Name -> Bool
232 itemCantMatch (Just t) (Just a) = t /= a
233 itemCantMatch _ _ = False
234
235
236 {-
237 ************************************************************************
238 * *
239 GADTs
240 * *
241 ************************************************************************
242
243 Note [Pruning dead case alternatives]
244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
245 Consider data T a where
246 T1 :: T Int
247 T2 :: T a
248
249 newtype X = MkX Int
250 newtype Y = MkY Char
251
252 type family F a
253 type instance F Bool = Int
254
255 Now consider case x of { T1 -> e1; T2 -> e2 }
256
257 The question before the house is this: if I know something about the type
258 of x, can I prune away the T1 alternative?
259
260 Suppose x::T Char. It's impossible to construct a (T Char) using T1,
261 Answer = YES we can prune the T1 branch (clearly)
262
263 Suppose x::T (F a), where 'a' is in scope. Then 'a' might be instantiated
264 to 'Bool', in which case x::T Int, so
265 ANSWER = NO (clearly)
266
267 We see here that we want precisely the apartness check implemented within
268 tcUnifyTysFG. So that's what we do! Two types cannot match if they are surely
269 apart. Note that since we are simply dropping dead code, a conservative test
270 suffices.
271 -}
272
273 -- | Given a list of pairs of types, are any two members of a pair surely
274 -- apart, even after arbitrary type function evaluation and substitution?
275 typesCantMatch :: [(Type,Type)] -> Bool
276 -- See Note [Pruning dead case alternatives]
277 typesCantMatch prs = any (uncurry cant_match) prs
278 where
279 cant_match :: Type -> Type -> Bool
280 cant_match t1 t2 = case tcUnifyTysFG (const BindMe) [t1] [t2] of
281 SurelyApart -> True
282 _ -> False
283
284 {-
285 ************************************************************************
286 * *
287 Unification
288 * *
289 ************************************************************************
290
291 Note [Fine-grained unification]
292 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
293 Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
294 no substitution to finite types makes these match. But, a substitution to
295 *infinite* types can unify these two types: [x |-> [[[...]]], y |-> [[[...]]] ].
296 Why do we care? Consider these two type family instances:
297
298 type instance F x x = Int
299 type instance F [y] y = Bool
300
301 If we also have
302
303 type instance Looper = [Looper]
304
305 then the instances potentially overlap. The solution is to use unification
306 over infinite terms. This is possible (see [1] for lots of gory details), but
307 a full algorithm is a little more power than we need. Instead, we make a
308 conservative approximation and just omit the occurs check.
309
310 [1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
311
312 tcUnifyTys considers an occurs-check problem as the same as general unification
313 failure.
314
315 tcUnifyTysFG ("fine-grained") returns one of three results: success, occurs-check
316 failure ("MaybeApart"), or general failure ("SurelyApart").
317
318 See also Trac #8162.
319
320 It's worth noting that unification in the presence of infinite types is not
321 complete. This means that, sometimes, a closed type family does not reduce
322 when it should. See test case indexed-types/should_fail/Overlap15 for an
323 example.
324
325 Note [The substitution in MaybeApart]
326 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
327 The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why?
328 Because consider unifying these:
329
330 (a, a, Int) ~ (b, [b], Bool)
331
332 If we go left-to-right, we start with [a |-> b]. Then, on the middle terms, we
333 apply the subst we have so far and discover that we need [b |-> [b]]. Because
334 this fails the occurs check, we say that the types are MaybeApart (see above
335 Note [Fine-grained unification]). But, we can't stop there! Because if we
336 continue, we discover that Int is SurelyApart from Bool, and therefore the
337 types are apart. This has practical consequences for the ability for closed
338 type family applications to reduce. See test case
339 indexed-types/should_compile/Overlap14.
340
341 Note [Unifying with skolems]
342 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
343 If we discover that two types unify if and only if a skolem variable is
344 substituted, we can't properly unify the types. But, that skolem variable
345 may later be instantiated with a unifyable type. So, we return maybeApart
346 in these cases.
347
348 Note [Lists of different lengths are MaybeApart]
349 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
350 It is unusual to call tcUnifyTys or tcUnifyTysFG with lists of different
351 lengths. The place where we know this can happen is from compatibleBranches in
352 FamInstEnv, when checking data family instances. Data family instances may be
353 eta-reduced; see Note [Eta reduction for data family axioms] in TcInstDcls.
354
355 We wish to say that
356
357 D :: * -> * -> *
358 axDF1 :: D Int ~ DFInst1
359 axDF2 :: D Int Bool ~ DFInst2
360
361 overlap. If we conclude that lists of different lengths are SurelyApart, then
362 it will look like these do *not* overlap, causing disaster. See Trac #9371.
363
364 In usages of tcUnifyTys outside of family instances, we always use tcUnifyTys,
365 which can't tell the difference between MaybeApart and SurelyApart, so those
366 usages won't notice this design choice.
367 -}
368
369 -- | Simple unification of two types; all type variables are bindable
370 -- Precondition: the kinds are already equal
371 tcUnifyTy :: Type -> Type -- All tyvars are bindable
372 -> Maybe TCvSubst
373 -- A regular one-shot (idempotent) substitution
374 tcUnifyTy t1 t2 = tcUnifyTys (const BindMe) [t1] [t2]
375
376 -- | Like 'tcUnifyTy', but also unifies the kinds
377 tcUnifyTyKi :: Type -> Type -> Maybe TCvSubst
378 tcUnifyTyKi t1 t2 = tcUnifyTyKis (const BindMe) [t1] [t2]
379
380 -- | Unify two types, treating type family applications as possibly unifying
381 -- with anything and looking through injective type family applications.
382 -- Precondition: kinds are the same
383 tcUnifyTyWithTFs :: Bool -- ^ True <=> do two-way unification;
384 -- False <=> do one-way matching.
385 -- See end of sec 5.2 from the paper
386 -> Type -> Type -> Maybe TCvSubst
387 -- This algorithm is an implementation of the "Algorithm U" presented in
388 -- the paper "Injective type families for Haskell", Figures 2 and 3.
389 -- The code is incorporated with the standard unifier for convenience, but
390 -- its operation should match the specification in the paper.
391 tcUnifyTyWithTFs twoWay t1 t2
392 = case tc_unify_tys (const BindMe) twoWay True False
393 rn_env emptyTvSubstEnv emptyCvSubstEnv
394 [t1] [t2] of
395 Unifiable (subst, _) -> Just $ niFixTCvSubst subst
396 MaybeApart (subst, _) -> Just $ niFixTCvSubst subst
397 -- we want to *succeed* in questionable cases. This is a
398 -- pre-unification algorithm.
399 SurelyApart -> Nothing
400 where
401 rn_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [t1, t2]
402
403 -----------------
404 tcUnifyTys :: (TyCoVar -> BindFlag)
405 -> [Type] -> [Type]
406 -> Maybe TCvSubst
407 -- ^ A regular one-shot (idempotent) substitution
408 -- that unifies the erased types. See comments
409 -- for 'tcUnifyTysFG'
410
411 -- The two types may have common type variables, and indeed do so in the
412 -- second call to tcUnifyTys in FunDeps.checkClsFD
413 tcUnifyTys bind_fn tys1 tys2
414 = case tcUnifyTysFG bind_fn tys1 tys2 of
415 Unifiable result -> Just result
416 _ -> Nothing
417
418 -- | Like 'tcUnifyTys' but also unifies the kinds
419 tcUnifyTyKis :: (TyCoVar -> BindFlag)
420 -> [Type] -> [Type]
421 -> Maybe TCvSubst
422 tcUnifyTyKis bind_fn tys1 tys2
423 = case tcUnifyTyKisFG bind_fn tys1 tys2 of
424 Unifiable result -> Just result
425 _ -> Nothing
426
427 -- This type does double-duty. It is used in the UM (unifier monad) and to
428 -- return the final result. See Note [Fine-grained unification]
429 type UnifyResult = UnifyResultM TCvSubst
430 data UnifyResultM a = Unifiable a -- the subst that unifies the types
431 | MaybeApart a -- the subst has as much as we know
432 -- it must be part of a most general unifier
433 -- See Note [The substitution in MaybeApart]
434 | SurelyApart
435 deriving Functor
436
437 instance Applicative UnifyResultM where
438 pure = Unifiable
439 (<*>) = ap
440
441 instance Monad UnifyResultM where
442
443 SurelyApart >>= _ = SurelyApart
444 MaybeApart x >>= f = case f x of
445 Unifiable y -> MaybeApart y
446 other -> other
447 Unifiable x >>= f = f x
448
449 instance Alternative UnifyResultM where
450 empty = SurelyApart
451
452 a@(Unifiable {}) <|> _ = a
453 _ <|> b@(Unifiable {}) = b
454 a@(MaybeApart {}) <|> _ = a
455 _ <|> b@(MaybeApart {}) = b
456 SurelyApart <|> SurelyApart = SurelyApart
457
458 instance MonadPlus UnifyResultM
459
460 -- | @tcUnifyTysFG bind_tv tys1 tys2@ attepts to find a substitution @s@ (whose
461 -- domain elements all respond 'BindMe' to @bind_tv@) such that
462 -- @s(tys1)@ and that of @s(tys2)@ are equal, as witnessed by the returned
463 -- Coercions. This version requires that the kinds of the types are the same,
464 -- if you unify left-to-right.
465 tcUnifyTysFG :: (TyVar -> BindFlag)
466 -> [Type] -> [Type]
467 -> UnifyResult
468 tcUnifyTysFG bind_fn tys1 tys2
469 = tc_unify_tys_fg False bind_fn tys1 tys2
470
471 tcUnifyTyKisFG :: (TyVar -> BindFlag)
472 -> [Type] -> [Type]
473 -> UnifyResult
474 tcUnifyTyKisFG bind_fn tys1 tys2
475 = tc_unify_tys_fg True bind_fn tys1 tys2
476
477 tc_unify_tys_fg :: Bool
478 -> (TyVar -> BindFlag)
479 -> [Type] -> [Type]
480 -> UnifyResult
481 tc_unify_tys_fg match_kis bind_fn tys1 tys2
482 = do { (env, _) <- tc_unify_tys bind_fn True False match_kis env
483 emptyTvSubstEnv emptyCvSubstEnv
484 tys1 tys2
485 ; return $ niFixTCvSubst env }
486 where
487 vars = tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2
488 env = mkRnEnv2 $ mkInScopeSet vars
489
490 -- | This function is actually the one to call the unifier -- a little
491 -- too general for outside clients, though.
492 tc_unify_tys :: (TyVar -> BindFlag)
493 -> AmIUnifying -- ^ True <=> unify; False <=> match
494 -> Bool -- ^ True <=> doing an injectivity check
495 -> Bool -- ^ True <=> treat the kinds as well
496 -> RnEnv2
497 -> TvSubstEnv -- ^ substitution to extend
498 -> CvSubstEnv
499 -> [Type] -> [Type]
500 -> UnifyResultM (TvSubstEnv, CvSubstEnv)
501 -- NB: It's tempting to ASSERT here that, if we're not matching kinds, then
502 -- the kinds of the types should be the same. However, this doesn't work,
503 -- as the types may be a dependent telescope, where later types have kinds
504 -- that mention variables occuring earlier in the list of types. Here's an
505 -- example (from typecheck/should_fail/T12709):
506 -- template: [rep :: RuntimeRep, a :: TYPE rep]
507 -- target: [LiftedRep :: RuntimeRep, Int :: TYPE LiftedRep]
508 -- We can see that matching the first pair will make the kinds of the second
509 -- pair equal. Yet, we still don't need a separate pass to unify the kinds
510 -- of these types, so it's appropriate to use the Ty variant of unification.
511 -- See also Note [tcMatchTy vs tcMatchTyKi].
512 tc_unify_tys bind_fn unif inj_check match_kis rn_env tv_env cv_env tys1 tys2
513 = initUM tv_env cv_env $
514 do { when match_kis $
515 unify_tys env kis1 kis2
516 ; unify_tys env tys1 tys2
517 ; (,) <$> getTvSubstEnv <*> getCvSubstEnv }
518 where
519 env = UMEnv { um_bind_fun = bind_fn
520 , um_unif = unif
521 , um_inj_tf = inj_check
522 , um_rn_env = rn_env }
523
524 kis1 = map typeKind tys1
525 kis2 = map typeKind tys2
526
527 instance Outputable a => Outputable (UnifyResultM a) where
528 ppr SurelyApart = text "SurelyApart"
529 ppr (Unifiable x) = text "Unifiable" <+> ppr x
530 ppr (MaybeApart x) = text "MaybeApart" <+> ppr x
531
532 {-
533 ************************************************************************
534 * *
535 Non-idempotent substitution
536 * *
537 ************************************************************************
538
539 Note [Non-idempotent substitution]
540 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
541 During unification we use a TvSubstEnv/CvSubstEnv pair that is
542 (a) non-idempotent
543 (b) loop-free; ie repeatedly applying it yields a fixed point
544
545 Note [Finding the substitution fixpoint]
546 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
547 Finding the fixpoint of a non-idempotent substitution arising from a
548 unification is harder than it looks, because of kinds. Consider
549 T k (H k (f:k)) ~ T * (g:*)
550 If we unify, we get the substitution
551 [ k -> *
552 , g -> H k (f:k) ]
553 To make it idempotent we don't want to get just
554 [ k -> *
555 , g -> H * (f:k) ]
556 We also want to substitute inside f's kind, to get
557 [ k -> *
558 , g -> H k (f:*) ]
559 If we don't do this, we may apply the substitution to something,
560 and get an ill-formed type, i.e. one where typeKind will fail.
561 This happened, for example, in Trac #9106.
562
563 This is the reason for extending env with [f:k -> f:*], in the
564 definition of env' in niFixTvSubst
565 -}
566
567 niFixTCvSubst :: TvSubstEnv -> TCvSubst
568 -- Find the idempotent fixed point of the non-idempotent substitution
569 -- See Note [Finding the substitution fixpoint]
570 -- ToDo: use laziness instead of iteration?
571 niFixTCvSubst tenv = f tenv
572 where
573 f tenv
574 | not_fixpoint = f (mapVarEnv (substTy subst') tenv)
575 | otherwise = subst
576 where
577 not_fixpoint = anyVarSet in_domain range_tvs
578 in_domain tv = tv `elemVarEnv` tenv
579
580 range_tvs = nonDetFoldUFM (unionVarSet . tyCoVarsOfType) emptyVarSet tenv
581 -- It's OK to use nonDetFoldUFM here because we
582 -- forget the order immediately by creating a set
583 subst = mkTvSubst (mkInScopeSet range_tvs) tenv
584
585 -- env' extends env by replacing any free type with
586 -- that same tyvar with a substituted kind
587 -- See note [Finding the substitution fixpoint]
588 tenv' = extendVarEnvList tenv [ (rtv, mkTyVarTy $
589 setTyVarKind rtv $
590 substTy subst $
591 tyVarKind rtv)
592 | rtv <- nonDetEltsUniqSet range_tvs
593 -- It's OK to use nonDetEltsUniqSet here
594 -- because we forget the order
595 -- immediatedly by putting it in VarEnv
596 , not (in_domain rtv) ]
597 subst' = mkTvSubst (mkInScopeSet range_tvs) tenv'
598
599 niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
600 -- Apply the non-idempotent substitution to a set of type variables,
601 -- remembering that the substitution isn't necessarily idempotent
602 -- This is used in the occurs check, before extending the substitution
603 niSubstTvSet tsubst tvs
604 = nonDetFoldUniqSet (unionVarSet . get) emptyVarSet tvs
605 -- It's OK to nonDetFoldUFM here because we immediately forget the
606 -- ordering by creating a set.
607 where
608 get tv
609 | Just ty <- lookupVarEnv tsubst tv
610 = niSubstTvSet tsubst (tyCoVarsOfType ty)
611
612 | otherwise
613 = unitVarSet tv
614
615 {-
616 ************************************************************************
617 * *
618 unify_ty: the main workhorse
619 * *
620 ************************************************************************
621
622 Note [Specification of unification]
623 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
624 The pure unifier, unify_ty, defined in this module, tries to work out
625 a substitution to make two types say True to eqType. NB: eqType is
626 itself not purely syntactic; it accounts for CastTys;
627 see Note [Non-trivial definitional equality] in TyCoRep
628
629 Unlike the "impure unifiers" in the typechecker (the eager unifier in
630 TcUnify, and the constraint solver itself in TcCanonical), the pure
631 unifier It does /not/ work up to ~.
632
633 The algorithm implemented here is rather delicate, and we depend on it
634 to uphold certain properties. This is a summary of these required
635 properties. Any reference to "flattening" refers to the flattening
636 algorithm in FamInstEnv (See Note [Flattening] in FamInstEnv), not
637 the flattening algorithm in the solver.
638
639 Notation:
640 θ,φ substitutions
641 ξ type-function-free types
642 τ,σ other types
643 τ♭ type τ, flattened
644
645 ≡ eqType
646
647 (U1) Soundness.
648 If (unify τ₁ τ₂) = Unifiable θ, then θ(τ₁) ≡ θ(τ₂).
649 θ is a most general unifier for τ₁ and τ₂.
650
651 (U2) Completeness.
652 If (unify ξ₁ ξ₂) = SurelyApart,
653 then there exists no substitution θ such that θ(ξ₁) ≡ θ(ξ₂).
654
655 These two properties are stated as Property 11 in the "Closed Type Families"
656 paper (POPL'14). Below, this paper is called [CTF].
657
658 (U3) Apartness under substitution.
659 If (unify ξ τ♭) = SurelyApart, then (unify ξ θ(τ)♭) = SurelyApart,
660 for any θ. (Property 12 from [CTF])
661
662 (U4) Apart types do not unify.
663 If (unify ξ τ♭) = SurelyApart, then there exists no θ
664 such that θ(ξ) = θ(τ). (Property 13 from [CTF])
665
666 THEOREM. Completeness w.r.t ~
667 If (unify τ₁♭ τ₂♭) = SurelyApart,
668 then there exists no proof that (τ₁ ~ τ₂).
669
670 PROOF. See appendix of [CTF].
671
672
673 The unification algorithm is used for type family injectivity, as described
674 in the "Injective Type Families" paper (Haskell'15), called [ITF]. When run
675 in this mode, it has the following properties.
676
677 (I1) If (unify σ τ) = SurelyApart, then σ and τ are not unifiable, even
678 after arbitrary type family reductions. Note that σ and τ are
679 not flattened here.
680
681 (I2) If (unify σ τ) = MaybeApart θ, and if some
682 φ exists such that φ(σ) ~ φ(τ), then φ extends θ.
683
684
685 Furthermore, the RULES matching algorithm requires this property,
686 but only when using this algorithm for matching:
687
688 (M1) If (match σ τ) succeeds with θ, then all matchable tyvars
689 in σ are bound in θ.
690
691 Property M1 means that we must extend the substitution with,
692 say (a ↦ a) when appropriate during matching.
693 See also Note [Self-substitution when matching].
694
695 (M2) Completeness of matching.
696 If θ(σ) = τ, then (match σ τ) = Unifiable φ,
697 where θ is an extension of φ.
698
699 Sadly, property M2 and I2 conflict. Consider
700
701 type family F1 a b where
702 F1 Int Bool = Char
703 F1 Double String = Char
704
705 Consider now two matching problems:
706
707 P1. match (F1 a Bool) (F1 Int Bool)
708 P2. match (F1 a Bool) (F1 Double String)
709
710 In case P1, we must find (a ↦ Int) to satisfy M2.
711 In case P2, we must /not/ find (a ↦ Double), in order to satisfy I2. (Note
712 that the correct mapping for I2 is (a ↦ Int). There is no way to discover
713 this, but we musn't map a to anything else!)
714
715 We thus must parameterize the algorithm over whether it's being used
716 for an injectivity check (refrain from looking at non-injective arguments
717 to type families) or not (do indeed look at those arguments). This is
718 implemented by the uf_inj_tf field of UmEnv.
719
720 (It's all a question of whether or not to include equation (7) from Fig. 2
721 of [ITF].)
722
723 This extra parameter is a bit fiddly, perhaps, but seemingly less so than
724 having two separate, almost-identical algorithms.
725
726 Note [Self-substitution when matching]
727 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
728 What should happen when we're *matching* (not unifying) a1 with a1? We
729 should get a substitution [a1 |-> a1]. A successful match should map all
730 the template variables (except ones that disappear when expanding synonyms).
731 But when unifying, we don't want to do this, because we'll then fall into
732 a loop.
733
734 This arrangement affects the code in three places:
735 - If we're matching a refined template variable, don't recur. Instead, just
736 check for equality. That is, if we know [a |-> Maybe a] and are matching
737 (a ~? Maybe Int), we want to just fail.
738
739 - Skip the occurs check when matching. This comes up in two places, because
740 matching against variables is handled separately from matching against
741 full-on types.
742
743 Note that this arrangement was provoked by a real failure, where the same
744 unique ended up in the template as in the target. (It was a rule firing when
745 compiling Data.List.NonEmpty.)
746
747 Note [Matching coercion variables]
748 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
749 Consider this:
750
751 type family F a
752
753 data G a where
754 MkG :: F a ~ Bool => G a
755
756 type family Foo (x :: G a) :: F a
757 type instance Foo MkG = False
758
759 We would like that to be accepted. For that to work, we need to introduce
760 a coercion variable on the left and then use it on the right. Accordingly,
761 at use sites of Foo, we need to be able to use matching to figure out the
762 value for the coercion. (See the desugared version:
763
764 axFoo :: [a :: *, c :: F a ~ Bool]. Foo (MkG c) = False |> (sym c)
765
766 ) We never want this action to happen during *unification* though, when
767 all bets are off.
768
769 Note [Kind coercions in Unify]
770 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
771 We wish to match/unify while ignoring casts. But, we can't just ignore
772 them completely, or we'll end up with ill-kinded substitutions. For example,
773 say we're matching `a` with `ty |> co`. If we just drop the cast, we'll
774 return [a |-> ty], but `a` and `ty` might have different kinds. We can't
775 just match/unify their kinds, either, because this might gratuitously
776 fail. After all, `co` is the witness that the kinds are the same -- they
777 may look nothing alike.
778
779 So, we pass a kind coercion to the match/unify worker. This coercion witnesses
780 the equality between the substed kind of the left-hand type and the substed
781 kind of the right-hand type. Note that we do not unify kinds at the leaves
782 (as we did previously). We thus have
783
784 INVARIANT: In the call
785 unify_ty ty1 ty2 kco
786 it must be that subst(kco) :: subst(kind(ty1)) ~N subst(kind(ty2)), where
787 `subst` is the ambient substitution in the UM monad.
788
789 To get this coercion, we first have to match/unify
790 the kinds before looking at the types. Happily, we need look only one level
791 up, as all kinds are guaranteed to have kind *.
792
793 When we're working with type applications (either TyConApp or AppTy) we
794 need to worry about establishing INVARIANT, as the kinds of the function
795 & arguments aren't (necessarily) included in the kind of the result.
796 When unifying two TyConApps, this is easy, because the two TyCons are
797 the same. Their kinds are thus the same. As long as we unify left-to-right,
798 we'll be sure to unify types' kinds before the types themselves. (For example,
799 think about Proxy :: forall k. k -> *. Unifying the first args matches up
800 the kinds of the second args.)
801
802 For AppTy, we must unify the kinds of the functions, but once these are
803 unified, we can continue unifying arguments without worrying further about
804 kinds.
805
806 The interface to this module includes both "...Ty" functions and
807 "...TyKi" functions. The former assume that INVARIANT is already
808 established, either because the kinds are the same or because the
809 list of types being passed in are the well-typed arguments to some
810 type constructor (see two paragraphs above). The latter take a separate
811 pre-pass over the kinds to establish INVARIANT. Sometimes, it's important
812 not to take the second pass, as it caused #12442.
813
814 We thought, at one point, that this was all unnecessary: why should
815 casts be in types in the first place? But they are sometimes. In
816 dependent/should_compile/KindEqualities2, we see, for example the
817 constraint Num (Int |> (blah ; sym blah)). We naturally want to find
818 a dictionary for that constraint, which requires dealing with
819 coercions in this manner.
820
821 Note [Matching in the presence of casts]
822 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
823 When matching, it is crucial that no variables from the template
824 end up in the range of the matching substitution (obviously!).
825 When unifying, that's not a constraint; instead we take the fixpoint
826 of the substitution at the end.
827
828 So what should we do with this, when matching?
829 unify_ty (tmpl |> co) tgt kco
830
831 Previously, wrongly, we pushed 'co' in the (horrid) accumulating
832 'kco' argument like this:
833 unify_ty (tmpl |> co) tgt kco
834 = unify_ty tmpl tgt (kco ; co)
835
836 But that is obviously wrong because 'co' (from the template) ends
837 up in 'kco', which in turn ends up in the range of the substitution.
838
839 This all came up in Trac #13910. Because we match tycon arguments
840 left-to-right, the ambient substitution will already have a matching
841 substitution for any kinds; so there is an easy fix: just apply
842 the substitution-so-far to the coercion from the LHS.
843
844 Note that
845
846 * When matching, the first arg of unify_ty is always the template;
847 we never swap round.
848
849 * The above argument is distressingly indirect. We seek a
850 better way.
851
852 * One better way is to ensure that type patterns (the template
853 in the matching process) have no casts. See Trac #14119.
854
855 -}
856
857 -------------- unify_ty: the main workhorse -----------
858
859 type AmIUnifying = Bool -- True <=> Unifying
860 -- False <=> Matching
861
862 unify_ty :: UMEnv
863 -> Type -> Type -- Types to be unified and a co
864 -> Coercion -- A coercion between their kinds
865 -- See Note [Kind coercions in Unify]
866 -> UM ()
867 -- See Note [Specification of unification]
868 -- Respects newtypes, PredTypes
869
870 unify_ty env ty1 ty2 kco
871 -- TODO: More commentary needed here
872 | Just ty1' <- tcView ty1 = unify_ty env ty1' ty2 kco
873 | Just ty2' <- tcView ty2 = unify_ty env ty1 ty2' kco
874 | CastTy ty1' co <- ty1 = if um_unif env
875 then unify_ty env ty1' ty2 (co `mkTransCo` kco)
876 else -- See Note [Matching in the presence of casts]
877 do { subst <- getSubst env
878 ; let co' = substCo subst co
879 ; unify_ty env ty1' ty2 (co' `mkTransCo` kco) }
880 | CastTy ty2' co <- ty2 = unify_ty env ty1 ty2' (kco `mkTransCo` mkSymCo co)
881
882 unify_ty env (TyVarTy tv1) ty2 kco
883 = uVar env tv1 ty2 kco
884 unify_ty env ty1 (TyVarTy tv2) kco
885 | um_unif env -- If unifying, can swap args
886 = uVar (umSwapRn env) tv2 ty1 (mkSymCo kco)
887
888 unify_ty env ty1 ty2 _kco
889 | Just (tc1, tys1) <- mb_tc_app1
890 , Just (tc2, tys2) <- mb_tc_app2
891 , tc1 == tc2 || (tcIsStarKind ty1 && tcIsStarKind ty2)
892 = if isInjectiveTyCon tc1 Nominal
893 then unify_tys env tys1 tys2
894 else do { let inj | isTypeFamilyTyCon tc1
895 = case tyConInjectivityInfo tc1 of
896 NotInjective -> repeat False
897 Injective bs -> bs
898 | otherwise
899 = repeat False
900
901 (inj_tys1, noninj_tys1) = partitionByList inj tys1
902 (inj_tys2, noninj_tys2) = partitionByList inj tys2
903
904 ; unify_tys env inj_tys1 inj_tys2
905 ; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
906 don'tBeSoSure $ unify_tys env noninj_tys1 noninj_tys2 }
907
908 | Just (tc1, _) <- mb_tc_app1
909 , not (isGenerativeTyCon tc1 Nominal)
910 -- E.g. unify_ty (F ty1) b = MaybeApart
911 -- because the (F ty1) behaves like a variable
912 -- NB: if unifying, we have already dealt
913 -- with the 'ty2 = variable' case
914 = maybeApart
915
916 | Just (tc2, _) <- mb_tc_app2
917 , not (isGenerativeTyCon tc2 Nominal)
918 , um_unif env
919 -- E.g. unify_ty [a] (F ty2) = MaybeApart, when unifying (only)
920 -- because the (F ty2) behaves like a variable
921 -- NB: we have already dealt with the 'ty1 = variable' case
922 = maybeApart
923
924 where
925 mb_tc_app1 = tcSplitTyConApp_maybe ty1
926 mb_tc_app2 = tcSplitTyConApp_maybe ty2
927
928 -- Applications need a bit of care!
929 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
930 -- NB: we've already dealt with type variables,
931 -- so if one type is an App the other one jolly well better be too
932 unify_ty env (AppTy ty1a ty1b) ty2 _kco
933 | Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
934 = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
935
936 unify_ty env ty1 (AppTy ty2a ty2b) _kco
937 | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
938 = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
939
940 unify_ty _ (LitTy x) (LitTy y) _kco | x == y = return ()
941
942 unify_ty env (ForAllTy (TvBndr tv1 _) ty1) (ForAllTy (TvBndr tv2 _) ty2) kco
943 = do { unify_ty env (tyVarKind tv1) (tyVarKind tv2) (mkNomReflCo liftedTypeKind)
944 ; let env' = umRnBndr2 env tv1 tv2
945 ; unify_ty env' ty1 ty2 kco }
946
947 -- See Note [Matching coercion variables]
948 unify_ty env (CoercionTy co1) (CoercionTy co2) kco
949 = do { c_subst <- getCvSubstEnv
950 ; case co1 of
951 CoVarCo cv
952 | not (um_unif env)
953 , not (cv `elemVarEnv` c_subst)
954 , BindMe <- tvBindFlagL env cv
955 -> do { checkRnEnvRCo env co2
956 ; let (co_l, co_r) = decomposeFunCo kco
957 -- cv :: t1 ~ t2
958 -- co2 :: s1 ~ s2
959 -- co_l :: t1 ~ s1
960 -- co_r :: t2 ~ s2
961 ; extendCvEnv cv (co_l `mkTransCo`
962 co2 `mkTransCo`
963 mkSymCo co_r) }
964 _ -> return () }
965
966 unify_ty _ _ _ _ = surelyApart
967
968 unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
969 unify_ty_app env ty1 ty1args ty2 ty2args
970 | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
971 , Just (ty2', ty2a) <- repSplitAppTy_maybe ty2
972 = unify_ty_app env ty1' (ty1a : ty1args) ty2' (ty2a : ty2args)
973
974 | otherwise
975 = do { let ki1 = typeKind ty1
976 ki2 = typeKind ty2
977 -- See Note [Kind coercions in Unify]
978 ; unify_ty env ki1 ki2 (mkNomReflCo liftedTypeKind)
979 ; unify_ty env ty1 ty2 (mkNomReflCo ki1)
980 ; unify_tys env ty1args ty2args }
981
982 unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
983 unify_tys env orig_xs orig_ys
984 = go orig_xs orig_ys
985 where
986 go [] [] = return ()
987 go (x:xs) (y:ys)
988 -- See Note [Kind coercions in Unify]
989 = do { unify_ty env x y (mkNomReflCo $ typeKind x)
990 ; go xs ys }
991 go _ _ = maybeApart -- See Note [Lists of different lengths are MaybeApart]
992
993 ---------------------------------
994 uVar :: UMEnv
995 -> TyVar -- Variable to be unified
996 -> Type -- with this Type
997 -> Coercion -- :: kind tv ~N kind ty
998 -> UM ()
999
1000 uVar env tv1 ty kco
1001 = do { -- Check to see whether tv1 is refined by the substitution
1002 subst <- getTvSubstEnv
1003 ; case (lookupVarEnv subst tv1) of
1004 Just ty' | um_unif env -- Unifying, so call
1005 -> unify_ty env ty' ty kco -- back into unify
1006 | otherwise
1007 -> -- Matching, we don't want to just recur here.
1008 -- this is because the range of the subst is the target
1009 -- type, not the template type. So, just check for
1010 -- normal type equality.
1011 guard ((ty' `mkCastTy` kco) `eqType` ty)
1012 Nothing -> uUnrefined env tv1 ty ty kco } -- No, continue
1013
1014 uUnrefined :: UMEnv
1015 -> TyVar -- variable to be unified
1016 -> Type -- with this Type
1017 -> Type -- (version w/ expanded synonyms)
1018 -> Coercion -- :: kind tv ~N kind ty
1019 -> UM ()
1020
1021 -- We know that tv1 isn't refined
1022
1023 uUnrefined env tv1 ty2 ty2' kco
1024 | Just ty2'' <- coreView ty2'
1025 = uUnrefined env tv1 ty2 ty2'' kco -- Unwrap synonyms
1026 -- This is essential, in case we have
1027 -- type Foo a = a
1028 -- and then unify a ~ Foo a
1029
1030 | TyVarTy tv2 <- ty2'
1031 = do { let tv1' = umRnOccL env tv1
1032 tv2' = umRnOccR env tv2
1033 ; unless (tv1' == tv2' && um_unif env) $ do
1034 -- If we are unifying a ~ a, just return immediately
1035 -- Do not extend the substitution
1036 -- See Note [Self-substitution when matching]
1037
1038 -- Check to see whether tv2 is refined
1039 { subst <- getTvSubstEnv
1040 ; case lookupVarEnv subst tv2 of
1041 { Just ty' | um_unif env -> uUnrefined env tv1 ty' ty' kco
1042 ; _ ->
1043
1044 do { -- So both are unrefined
1045 -- Bind one or the other, depending on which is bindable
1046 ; let b1 = tvBindFlagL env tv1
1047 b2 = tvBindFlagR env tv2
1048 ty1 = mkTyVarTy tv1
1049 ; case (b1, b2) of
1050 (BindMe, _) -> bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco)
1051 (_, BindMe) | um_unif env
1052 -> bindTv (umSwapRn env) tv2 (ty1 `mkCastTy` kco)
1053
1054 _ | tv1' == tv2' -> return ()
1055 -- How could this happen? If we're only matching and if
1056 -- we're comparing forall-bound variables.
1057
1058 _ -> maybeApart -- See Note [Unification with skolems]
1059 }}}}
1060
1061 uUnrefined env tv1 ty2 _ kco -- ty2 is not a type variable
1062 = case tvBindFlagL env tv1 of
1063 Skolem -> maybeApart -- See Note [Unification with skolems]
1064 BindMe -> bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco)
1065
1066 bindTv :: UMEnv -> TyVar -> Type -> UM ()
1067 -- OK, so we want to extend the substitution with tv := ty
1068 -- But first, we must do a couple of checks
1069 bindTv env tv1 ty2
1070 = do { let free_tvs2 = tyCoVarsOfType ty2
1071
1072 -- Make sure tys mentions no local variables
1073 -- E.g. (forall a. b) ~ (forall a. [a])
1074 -- We should not unify b := [a]!
1075 ; checkRnEnvR env free_tvs2
1076
1077 -- Occurs check, see Note [Fine-grained unification]
1078 -- Make sure you include 'kco' (which ty2 does) Trac #14846
1079 ; occurs <- occursCheck env tv1 free_tvs2
1080
1081 ; if occurs then maybeApart
1082 else extendTvEnv tv1 ty2 }
1083
1084 occursCheck :: UMEnv -> TyVar -> VarSet -> UM Bool
1085 occursCheck env tv free_tvs
1086 | um_unif env
1087 = do { tsubst <- getTvSubstEnv
1088 ; return (tv `elemVarSet` niSubstTvSet tsubst free_tvs) }
1089
1090 | otherwise -- Matching; no occurs check
1091 = return False -- See Note [Self-substitution when matching]
1092
1093 {-
1094 %************************************************************************
1095 %* *
1096 Binding decisions
1097 * *
1098 ************************************************************************
1099 -}
1100
1101 data BindFlag
1102 = BindMe -- A regular type variable
1103
1104 | Skolem -- This type variable is a skolem constant
1105 -- Don't bind it; it only matches itself
1106 deriving Eq
1107
1108 {-
1109 ************************************************************************
1110 * *
1111 Unification monad
1112 * *
1113 ************************************************************************
1114 -}
1115
1116 data UMEnv = UMEnv { um_bind_fun :: TyVar -> BindFlag
1117 -- User-supplied BindFlag function
1118 , um_unif :: AmIUnifying
1119 , um_inj_tf :: Bool -- Checking for injectivity?
1120 -- See (end of) Note [Specification of unification]
1121 , um_rn_env :: RnEnv2 }
1122
1123 data UMState = UMState
1124 { um_tv_env :: TvSubstEnv
1125 , um_cv_env :: CvSubstEnv }
1126
1127 newtype UM a = UM { unUM :: UMState -> UnifyResultM (UMState, a) }
1128
1129 instance Functor UM where
1130 fmap = liftM
1131
1132 instance Applicative UM where
1133 pure a = UM (\s -> pure (s, a))
1134 (<*>) = ap
1135
1136 instance Monad UM where
1137 fail = MonadFail.fail
1138 m >>= k = UM (\state ->
1139 do { (state', v) <- unUM m state
1140 ; unUM (k v) state' })
1141
1142 -- need this instance because of a use of 'guard' above
1143 instance Alternative UM where
1144 empty = UM (\_ -> Control.Applicative.empty)
1145 m1 <|> m2 = UM (\state ->
1146 unUM m1 state <|>
1147 unUM m2 state)
1148
1149 instance MonadPlus UM
1150
1151 instance MonadFail.MonadFail UM where
1152 fail _ = UM (\_ -> SurelyApart) -- failed pattern match
1153
1154 initUM :: TvSubstEnv -- subst to extend
1155 -> CvSubstEnv
1156 -> UM a -> UnifyResultM a
1157 initUM subst_env cv_subst_env um
1158 = case unUM um state of
1159 Unifiable (_, subst) -> Unifiable subst
1160 MaybeApart (_, subst) -> MaybeApart subst
1161 SurelyApart -> SurelyApart
1162 where
1163 state = UMState { um_tv_env = subst_env
1164 , um_cv_env = cv_subst_env }
1165
1166 tvBindFlagL :: UMEnv -> TyVar -> BindFlag
1167 tvBindFlagL env tv
1168 | inRnEnvL (um_rn_env env) tv = Skolem
1169 | otherwise = um_bind_fun env tv
1170
1171 tvBindFlagR :: UMEnv -> TyVar -> BindFlag
1172 tvBindFlagR env tv
1173 | inRnEnvR (um_rn_env env) tv = Skolem
1174 | otherwise = um_bind_fun env tv
1175
1176 getTvSubstEnv :: UM TvSubstEnv
1177 getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state)
1178
1179 getCvSubstEnv :: UM CvSubstEnv
1180 getCvSubstEnv = UM $ \state -> Unifiable (state, um_cv_env state)
1181
1182 getSubst :: UMEnv -> UM TCvSubst
1183 getSubst env = do { tv_env <- getTvSubstEnv
1184 ; cv_env <- getCvSubstEnv
1185 ; let in_scope = rnInScopeSet (um_rn_env env)
1186 ; return (mkTCvSubst in_scope (tv_env, cv_env)) }
1187
1188 extendTvEnv :: TyVar -> Type -> UM ()
1189 extendTvEnv tv ty = UM $ \state ->
1190 Unifiable (state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())
1191
1192 extendCvEnv :: CoVar -> Coercion -> UM ()
1193 extendCvEnv cv co = UM $ \state ->
1194 Unifiable (state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())
1195
1196 umRnBndr2 :: UMEnv -> TyCoVar -> TyCoVar -> UMEnv
1197 umRnBndr2 env v1 v2
1198 = env { um_rn_env = rnBndr2 (um_rn_env env) v1 v2 }
1199
1200 checkRnEnv :: (RnEnv2 -> VarEnv Var) -> UMEnv -> VarSet -> UM ()
1201 checkRnEnv get_set env varset = UM $ \ state ->
1202 let env_vars = get_set (um_rn_env env) in
1203 if isEmptyVarEnv env_vars || (getUniqSet varset `disjointVarEnv` env_vars)
1204 -- NB: That isEmptyVarSet is a critical optimization; it
1205 -- means we don't have to calculate the free vars of
1206 -- the type, often saving quite a bit of allocation.
1207 then Unifiable (state, ())
1208 else MaybeApart (state, ()) -- ToDo: why MaybeApart
1209 -- I think SurelyApart would be right
1210
1211 -- | Converts any SurelyApart to a MaybeApart
1212 don'tBeSoSure :: UM () -> UM ()
1213 don'tBeSoSure um = UM $ \ state ->
1214 case unUM um state of
1215 SurelyApart -> MaybeApart (state, ())
1216 other -> other
1217
1218 checkRnEnvR :: UMEnv -> VarSet -> UM ()
1219 checkRnEnvR env fvs = checkRnEnv rnEnvR env fvs
1220
1221 checkRnEnvRCo :: UMEnv -> Coercion -> UM ()
1222 checkRnEnvRCo env co = checkRnEnv rnEnvR env (tyCoVarsOfCo co)
1223
1224 umRnOccL :: UMEnv -> TyVar -> TyVar
1225 umRnOccL env v = rnOccL (um_rn_env env) v
1226
1227 umRnOccR :: UMEnv -> TyVar -> TyVar
1228 umRnOccR env v = rnOccR (um_rn_env env) v
1229
1230 umSwapRn :: UMEnv -> UMEnv
1231 umSwapRn env = env { um_rn_env = rnSwap (um_rn_env env) }
1232
1233 maybeApart :: UM ()
1234 maybeApart = UM (\state -> MaybeApart (state, ()))
1235
1236 surelyApart :: UM a
1237 surelyApart = UM (\_ -> SurelyApart)
1238
1239 {-
1240 %************************************************************************
1241 %* *
1242 Matching a (lifted) type against a coercion
1243 %* *
1244 %************************************************************************
1245
1246 This section defines essentially an inverse to liftCoSubst. It is defined
1247 here to avoid a dependency from Coercion on this module.
1248
1249 -}
1250
1251 data MatchEnv = ME { me_tmpls :: TyVarSet
1252 , me_env :: RnEnv2 }
1253
1254 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
1255 -- @liftCoMatch vars ty co == Just s@, then @listCoSubst s ty == co@,
1256 -- where @==@ there means that the result of 'liftCoSubst' has the same
1257 -- type as the original co; but may be different under the hood.
1258 -- That is, it matches a type against a coercion of the same
1259 -- "shape", and returns a lifting substitution which could have been
1260 -- used to produce the given coercion from the given type.
1261 -- Note that this function is incomplete -- it might return Nothing
1262 -- when there does indeed exist a possible lifting context.
1263 --
1264 -- This function is incomplete in that it doesn't respect the equality
1265 -- in `eqType`. That is, it's possible that this will succeed for t1 and
1266 -- fail for t2, even when t1 `eqType` t2. That's because it depends on
1267 -- there being a very similar structure between the type and the coercion.
1268 -- This incompleteness shouldn't be all that surprising, especially because
1269 -- it depends on the structure of the coercion, which is a silly thing to do.
1270 --
1271 -- The lifting context produced doesn't have to be exacting in the roles
1272 -- of the mappings. This is because any use of the lifting context will
1273 -- also require a desired role. Thus, this algorithm prefers mapping to
1274 -- nominal coercions where it can do so.
1275 liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
1276 liftCoMatch tmpls ty co
1277 = do { cenv1 <- ty_co_match menv emptyVarEnv ki ki_co ki_ki_co ki_ki_co
1278 ; cenv2 <- ty_co_match menv cenv1 ty co
1279 (mkNomReflCo co_lkind) (mkNomReflCo co_rkind)
1280 ; return (LC (mkEmptyTCvSubst in_scope) cenv2) }
1281 where
1282 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
1283 in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
1284 -- Like tcMatchTy, assume all the interesting variables
1285 -- in ty are in tmpls
1286
1287 ki = typeKind ty
1288 ki_co = promoteCoercion co
1289 ki_ki_co = mkNomReflCo liftedTypeKind
1290
1291 Pair co_lkind co_rkind = coercionKind ki_co
1292
1293 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
1294 ty_co_match :: MatchEnv -- ^ ambient helpful info
1295 -> LiftCoEnv -- ^ incoming subst
1296 -> Type -- ^ ty, type to match
1297 -> Coercion -- ^ co, coercion to match against
1298 -> Coercion -- ^ :: kind of L type of substed ty ~N L kind of co
1299 -> Coercion -- ^ :: kind of R type of substed ty ~N R kind of co
1300 -> Maybe LiftCoEnv
1301 ty_co_match menv subst ty co lkco rkco
1302 | Just ty' <- coreView ty = ty_co_match menv subst ty' co lkco rkco
1303
1304 -- handle Refl case:
1305 | tyCoVarsOfType ty `isNotInDomainOf` subst
1306 , Just (ty', _) <- isReflCo_maybe co
1307 , ty `eqType` ty'
1308 = Just subst
1309
1310 where
1311 isNotInDomainOf :: VarSet -> VarEnv a -> Bool
1312 isNotInDomainOf set env
1313 = noneSet (\v -> elemVarEnv v env) set
1314
1315 noneSet :: (Var -> Bool) -> VarSet -> Bool
1316 noneSet f = allVarSet (not . f)
1317
1318 ty_co_match menv subst ty co lkco rkco
1319 | CastTy ty' co' <- ty
1320 = ty_co_match menv subst ty' co (co' `mkTransCo` lkco) (co' `mkTransCo` rkco)
1321
1322 | CoherenceCo co1 co2 <- co
1323 = ty_co_match menv subst ty co1 (lkco `mkTransCo` mkSymCo co2) rkco
1324
1325 | SymCo co' <- co
1326 = swapLiftCoEnv <$> ty_co_match menv (swapLiftCoEnv subst) ty co' rkco lkco
1327
1328 -- Match a type variable against a non-refl coercion
1329 ty_co_match menv subst (TyVarTy tv1) co lkco rkco
1330 | Just co1' <- lookupVarEnv subst tv1' -- tv1' is already bound to co1
1331 = if eqCoercionX (nukeRnEnvL rn_env) co1' co
1332 then Just subst
1333 else Nothing -- no match since tv1 matches two different coercions
1334
1335 | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
1336 = if any (inRnEnvR rn_env) (tyCoVarsOfCoList co)
1337 then Nothing -- occurs check failed
1338 else Just $ extendVarEnv subst tv1' $
1339 castCoercionKind co (mkSymCo lkco) (mkSymCo rkco)
1340
1341 | otherwise
1342 = Nothing
1343
1344 where
1345 rn_env = me_env menv
1346 tv1' = rnOccL rn_env tv1
1347
1348 -- just look through SubCo's. We don't really care about roles here.
1349 ty_co_match menv subst ty (SubCo co) lkco rkco
1350 = ty_co_match menv subst ty co lkco rkco
1351
1352 ty_co_match menv subst (AppTy ty1a ty1b) co _lkco _rkco
1353 | Just (co2, arg2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy
1354 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1355 ty_co_match menv subst ty1 (AppCo co2 arg2) _lkco _rkco
1356 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
1357 -- yes, the one from Type, not TcType; this is for coercion optimization
1358 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1359
1360 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos) _lkco _rkco
1361 = ty_co_match_tc menv subst tc1 tys tc2 cos
1362 ty_co_match menv subst (FunTy ty1 ty2) co _lkco _rkco
1363 -- Despite the fact that (->) is polymorphic in four type variables (two
1364 -- runtime rep and two types), we shouldn't need to explicitly unify the
1365 -- runtime reps here; unifying the types themselves should be sufficient.
1366 -- See Note [Representation of function types].
1367 | Just (tc, [_,_,co1,co2]) <- splitTyConAppCo_maybe co
1368 , tc == funTyCon
1369 = let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) [co1,co2]
1370 in ty_co_match_args menv subst [ty1, ty2] [co1, co2] lkcos rkcos
1371
1372 ty_co_match menv subst (ForAllTy (TvBndr tv1 _) ty1)
1373 (ForAllCo tv2 kind_co2 co2)
1374 lkco rkco
1375 = do { subst1 <- ty_co_match menv subst (tyVarKind tv1) kind_co2
1376 ki_ki_co ki_ki_co
1377 ; let rn_env0 = me_env menv
1378 rn_env1 = rnBndr2 rn_env0 tv1 tv2
1379 menv' = menv { me_env = rn_env1 }
1380 ; ty_co_match menv' subst1 ty1 co2 lkco rkco }
1381 where
1382 ki_ki_co = mkNomReflCo liftedTypeKind
1383
1384 ty_co_match _ subst (CoercionTy {}) _ _ _
1385 = Just subst -- don't inspect coercions
1386
1387 ty_co_match menv subst ty co lkco rkco
1388 | Just co' <- pushRefl co = ty_co_match menv subst ty co' lkco rkco
1389 | otherwise = Nothing
1390
1391 ty_co_match_tc :: MatchEnv -> LiftCoEnv
1392 -> TyCon -> [Type]
1393 -> TyCon -> [Coercion]
1394 -> Maybe LiftCoEnv
1395 ty_co_match_tc menv subst tc1 tys1 tc2 cos2
1396 = do { guard (tc1 == tc2)
1397 ; ty_co_match_args menv subst tys1 cos2 lkcos rkcos }
1398 where
1399 Pair lkcos rkcos
1400 = traverse (fmap mkNomReflCo . coercionKind) cos2
1401
1402 ty_co_match_app :: MatchEnv -> LiftCoEnv
1403 -> Type -> [Type] -> Coercion -> [Coercion]
1404 -> Maybe LiftCoEnv
1405 ty_co_match_app menv subst ty1 ty1args co2 co2args
1406 | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
1407 , Just (co2', co2a) <- splitAppCo_maybe co2
1408 = ty_co_match_app menv subst ty1' (ty1a : ty1args) co2' (co2a : co2args)
1409
1410 | otherwise
1411 = do { subst1 <- ty_co_match menv subst ki1 ki2 ki_ki_co ki_ki_co
1412 ; let Pair lkco rkco = mkNomReflCo <$> coercionKind ki2
1413 ; subst2 <- ty_co_match menv subst1 ty1 co2 lkco rkco
1414 ; let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) co2args
1415 ; ty_co_match_args menv subst2 ty1args co2args lkcos rkcos }
1416 where
1417 ki1 = typeKind ty1
1418 ki2 = promoteCoercion co2
1419 ki_ki_co = mkNomReflCo liftedTypeKind
1420
1421 ty_co_match_args :: MatchEnv -> LiftCoEnv -> [Type]
1422 -> [Coercion] -> [Coercion] -> [Coercion]
1423 -> Maybe LiftCoEnv
1424 ty_co_match_args _ subst [] [] _ _ = Just subst
1425 ty_co_match_args menv subst (ty:tys) (arg:args) (lkco:lkcos) (rkco:rkcos)
1426 = do { subst' <- ty_co_match menv subst ty arg lkco rkco
1427 ; ty_co_match_args menv subst' tys args lkcos rkcos }
1428 ty_co_match_args _ _ _ _ _ _ = Nothing
1429
1430 pushRefl :: Coercion -> Maybe Coercion
1431 pushRefl (Refl Nominal (AppTy ty1 ty2))
1432 = Just (AppCo (Refl Nominal ty1) (mkNomReflCo ty2))
1433 pushRefl (Refl r (FunTy ty1 ty2))
1434 | Just rep1 <- getRuntimeRep_maybe ty1
1435 , Just rep2 <- getRuntimeRep_maybe ty2
1436 = Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2
1437 , mkReflCo r ty1, mkReflCo r ty2 ])
1438 pushRefl (Refl r (TyConApp tc tys))
1439 = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
1440 pushRefl (Refl r (ForAllTy (TvBndr tv _) ty))
1441 = Just (mkHomoForAllCos_NoRefl [tv] (Refl r ty))
1442 -- NB: NoRefl variant. Otherwise, we get a loop!
1443 pushRefl (Refl r (CastTy ty co)) = Just (castCoercionKind (Refl r ty) co co)
1444 pushRefl _ = Nothing