Comments in Unify, fixing #12442
[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, _) -> do { checkRnEnvR env ty2 -- make sure ty2 is not a local
1051 ; extendTvEnv tv1 (ty2 `mkCastTy` mkSymCo kco) }
1052 (_, BindMe) | um_unif env
1053 -> do { checkRnEnvL env ty1 -- ditto for ty1
1054 ; extendTvEnv tv2 (ty1 `mkCastTy` kco) }
1055
1056 _ | tv1' == tv2' -> return ()
1057 -- How could this happen? If we're only matching and if
1058 -- we're comparing forall-bound variables.
1059
1060 _ -> maybeApart -- See Note [Unification with skolems]
1061 }}}}
1062
1063 uUnrefined env tv1 ty2 ty2' kco -- ty2 is not a type variable
1064 = do { occurs <- elemNiSubstSet tv1 (tyCoVarsOfType ty2')
1065 ; if um_unif env && occurs -- See Note [Self-substitution when matching]
1066 then maybeApart -- Occurs check, see Note [Fine-grained unification]
1067 else bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco) }
1068 -- Bind tyvar to the synonym if poss
1069
1070 elemNiSubstSet :: TyVar -> TyCoVarSet -> UM Bool
1071 elemNiSubstSet v set
1072 = do { tsubst <- getTvSubstEnv
1073 ; return $ v `elemVarSet` niSubstTvSet tsubst set }
1074
1075 bindTv :: UMEnv -> TyVar -> Type -> UM ()
1076 bindTv env tv ty -- ty is not a variable
1077 = do { checkRnEnvR env ty -- make sure ty mentions no local variables
1078 ; case tvBindFlagL env tv of
1079 Skolem -> maybeApart -- See Note [Unification with skolems]
1080 BindMe -> extendTvEnv tv ty
1081 }
1082
1083 {-
1084 %************************************************************************
1085 %* *
1086 Binding decisions
1087 * *
1088 ************************************************************************
1089 -}
1090
1091 data BindFlag
1092 = BindMe -- A regular type variable
1093
1094 | Skolem -- This type variable is a skolem constant
1095 -- Don't bind it; it only matches itself
1096 deriving Eq
1097
1098 {-
1099 ************************************************************************
1100 * *
1101 Unification monad
1102 * *
1103 ************************************************************************
1104 -}
1105
1106 data UMEnv = UMEnv { um_bind_fun :: TyVar -> BindFlag
1107 -- User-supplied BindFlag function
1108 , um_unif :: AmIUnifying
1109 , um_inj_tf :: Bool -- Checking for injectivity?
1110 -- See (end of) Note [Specification of unification]
1111 , um_rn_env :: RnEnv2 }
1112
1113 data UMState = UMState
1114 { um_tv_env :: TvSubstEnv
1115 , um_cv_env :: CvSubstEnv }
1116
1117 newtype UM a = UM { unUM :: UMState -> UnifyResultM (UMState, a) }
1118
1119 instance Functor UM where
1120 fmap = liftM
1121
1122 instance Applicative UM where
1123 pure a = UM (\s -> pure (s, a))
1124 (<*>) = ap
1125
1126 instance Monad UM where
1127 fail = MonadFail.fail
1128 m >>= k = UM (\state ->
1129 do { (state', v) <- unUM m state
1130 ; unUM (k v) state' })
1131
1132 -- need this instance because of a use of 'guard' above
1133 instance Alternative UM where
1134 empty = UM (\_ -> Control.Applicative.empty)
1135 m1 <|> m2 = UM (\state ->
1136 unUM m1 state <|>
1137 unUM m2 state)
1138
1139 instance MonadPlus UM
1140
1141 instance MonadFail.MonadFail UM where
1142 fail _ = UM (\_ -> SurelyApart) -- failed pattern match
1143
1144 initUM :: TvSubstEnv -- subst to extend
1145 -> CvSubstEnv
1146 -> UM a -> UnifyResultM a
1147 initUM subst_env cv_subst_env um
1148 = case unUM um state of
1149 Unifiable (_, subst) -> Unifiable subst
1150 MaybeApart (_, subst) -> MaybeApart subst
1151 SurelyApart -> SurelyApart
1152 where
1153 state = UMState { um_tv_env = subst_env
1154 , um_cv_env = cv_subst_env }
1155
1156 tvBindFlagL :: UMEnv -> TyVar -> BindFlag
1157 tvBindFlagL env tv
1158 | inRnEnvL (um_rn_env env) tv = Skolem
1159 | otherwise = um_bind_fun env tv
1160
1161 tvBindFlagR :: UMEnv -> TyVar -> BindFlag
1162 tvBindFlagR env tv
1163 | inRnEnvR (um_rn_env env) tv = Skolem
1164 | otherwise = um_bind_fun env tv
1165
1166 getTvSubstEnv :: UM TvSubstEnv
1167 getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state)
1168
1169 getCvSubstEnv :: UM CvSubstEnv
1170 getCvSubstEnv = UM $ \state -> Unifiable (state, um_cv_env state)
1171
1172 getSubst :: UMEnv -> UM TCvSubst
1173 getSubst env = do { tv_env <- getTvSubstEnv
1174 ; cv_env <- getCvSubstEnv
1175 ; let in_scope = rnInScopeSet (um_rn_env env)
1176 ; return (mkTCvSubst in_scope (tv_env, cv_env)) }
1177
1178 extendTvEnv :: TyVar -> Type -> UM ()
1179 extendTvEnv tv ty = UM $ \state ->
1180 Unifiable (state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())
1181
1182 extendCvEnv :: CoVar -> Coercion -> UM ()
1183 extendCvEnv cv co = UM $ \state ->
1184 Unifiable (state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())
1185
1186 umRnBndr2 :: UMEnv -> TyCoVar -> TyCoVar -> UMEnv
1187 umRnBndr2 env v1 v2
1188 = env { um_rn_env = rnBndr2 (um_rn_env env) v1 v2 }
1189
1190 checkRnEnv :: (RnEnv2 -> VarEnv Var) -> UMEnv -> VarSet -> UM ()
1191 checkRnEnv get_set env varset = UM $ \ state ->
1192 let env_vars = get_set (um_rn_env env) in
1193 if isEmptyVarEnv env_vars || (getUniqSet varset `disjointVarEnv` env_vars)
1194 -- NB: That isEmptyVarSet is a critical optimization; it
1195 -- means we don't have to calculate the free vars of
1196 -- the type, often saving quite a bit of allocation.
1197 then Unifiable (state, ())
1198 else MaybeApart (state, ())
1199
1200 -- | Converts any SurelyApart to a MaybeApart
1201 don'tBeSoSure :: UM () -> UM ()
1202 don'tBeSoSure um = UM $ \ state ->
1203 case unUM um state of
1204 SurelyApart -> MaybeApart (state, ())
1205 other -> other
1206
1207 checkRnEnvR :: UMEnv -> Type -> UM ()
1208 checkRnEnvR env ty = checkRnEnv rnEnvR env (tyCoVarsOfType ty)
1209
1210 checkRnEnvL :: UMEnv -> Type -> UM ()
1211 checkRnEnvL env ty = checkRnEnv rnEnvL env (tyCoVarsOfType ty)
1212
1213 checkRnEnvRCo :: UMEnv -> Coercion -> UM ()
1214 checkRnEnvRCo env co = checkRnEnv rnEnvR env (tyCoVarsOfCo co)
1215
1216 umRnOccL :: UMEnv -> TyVar -> TyVar
1217 umRnOccL env v = rnOccL (um_rn_env env) v
1218
1219 umRnOccR :: UMEnv -> TyVar -> TyVar
1220 umRnOccR env v = rnOccR (um_rn_env env) v
1221
1222 umSwapRn :: UMEnv -> UMEnv
1223 umSwapRn env = env { um_rn_env = rnSwap (um_rn_env env) }
1224
1225 maybeApart :: UM ()
1226 maybeApart = UM (\state -> MaybeApart (state, ()))
1227
1228 surelyApart :: UM a
1229 surelyApart = UM (\_ -> SurelyApart)
1230
1231 {-
1232 %************************************************************************
1233 %* *
1234 Matching a (lifted) type against a coercion
1235 %* *
1236 %************************************************************************
1237
1238 This section defines essentially an inverse to liftCoSubst. It is defined
1239 here to avoid a dependency from Coercion on this module.
1240
1241 -}
1242
1243 data MatchEnv = ME { me_tmpls :: TyVarSet
1244 , me_env :: RnEnv2 }
1245
1246 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
1247 -- @liftCoMatch vars ty co == Just s@, then @listCoSubst s ty == co@,
1248 -- where @==@ there means that the result of 'liftCoSubst' has the same
1249 -- type as the original co; but may be different under the hood.
1250 -- That is, it matches a type against a coercion of the same
1251 -- "shape", and returns a lifting substitution which could have been
1252 -- used to produce the given coercion from the given type.
1253 -- Note that this function is incomplete -- it might return Nothing
1254 -- when there does indeed exist a possible lifting context.
1255 --
1256 -- This function is incomplete in that it doesn't respect the equality
1257 -- in `eqType`. That is, it's possible that this will succeed for t1 and
1258 -- fail for t2, even when t1 `eqType` t2. That's because it depends on
1259 -- there being a very similar structure between the type and the coercion.
1260 -- This incompleteness shouldn't be all that surprising, especially because
1261 -- it depends on the structure of the coercion, which is a silly thing to do.
1262 --
1263 -- The lifting context produced doesn't have to be exacting in the roles
1264 -- of the mappings. This is because any use of the lifting context will
1265 -- also require a desired role. Thus, this algorithm prefers mapping to
1266 -- nominal coercions where it can do so.
1267 liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
1268 liftCoMatch tmpls ty co
1269 = do { cenv1 <- ty_co_match menv emptyVarEnv ki ki_co ki_ki_co ki_ki_co
1270 ; cenv2 <- ty_co_match menv cenv1 ty co
1271 (mkNomReflCo co_lkind) (mkNomReflCo co_rkind)
1272 ; return (LC (mkEmptyTCvSubst in_scope) cenv2) }
1273 where
1274 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
1275 in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
1276 -- Like tcMatchTy, assume all the interesting variables
1277 -- in ty are in tmpls
1278
1279 ki = typeKind ty
1280 ki_co = promoteCoercion co
1281 ki_ki_co = mkNomReflCo liftedTypeKind
1282
1283 Pair co_lkind co_rkind = coercionKind ki_co
1284
1285 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
1286 ty_co_match :: MatchEnv -- ^ ambient helpful info
1287 -> LiftCoEnv -- ^ incoming subst
1288 -> Type -- ^ ty, type to match
1289 -> Coercion -- ^ co, coercion to match against
1290 -> Coercion -- ^ :: kind of L type of substed ty ~N L kind of co
1291 -> Coercion -- ^ :: kind of R type of substed ty ~N R kind of co
1292 -> Maybe LiftCoEnv
1293 ty_co_match menv subst ty co lkco rkco
1294 | Just ty' <- coreView ty = ty_co_match menv subst ty' co lkco rkco
1295
1296 -- handle Refl case:
1297 | tyCoVarsOfType ty `isNotInDomainOf` subst
1298 , Just (ty', _) <- isReflCo_maybe co
1299 , ty `eqType` ty'
1300 = Just subst
1301
1302 where
1303 isNotInDomainOf :: VarSet -> VarEnv a -> Bool
1304 isNotInDomainOf set env
1305 = noneSet (\v -> elemVarEnv v env) set
1306
1307 noneSet :: (Var -> Bool) -> VarSet -> Bool
1308 noneSet f = allVarSet (not . f)
1309
1310 ty_co_match menv subst ty co lkco rkco
1311 | CastTy ty' co' <- ty
1312 = ty_co_match menv subst ty' co (co' `mkTransCo` lkco) (co' `mkTransCo` rkco)
1313
1314 | CoherenceCo co1 co2 <- co
1315 = ty_co_match menv subst ty co1 (lkco `mkTransCo` mkSymCo co2) rkco
1316
1317 | SymCo co' <- co
1318 = swapLiftCoEnv <$> ty_co_match menv (swapLiftCoEnv subst) ty co' rkco lkco
1319
1320 -- Match a type variable against a non-refl coercion
1321 ty_co_match menv subst (TyVarTy tv1) co lkco rkco
1322 | Just co1' <- lookupVarEnv subst tv1' -- tv1' is already bound to co1
1323 = if eqCoercionX (nukeRnEnvL rn_env) co1' co
1324 then Just subst
1325 else Nothing -- no match since tv1 matches two different coercions
1326
1327 | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
1328 = if any (inRnEnvR rn_env) (tyCoVarsOfCoList co)
1329 then Nothing -- occurs check failed
1330 else Just $ extendVarEnv subst tv1' $
1331 castCoercionKind co (mkSymCo lkco) (mkSymCo rkco)
1332
1333 | otherwise
1334 = Nothing
1335
1336 where
1337 rn_env = me_env menv
1338 tv1' = rnOccL rn_env tv1
1339
1340 -- just look through SubCo's. We don't really care about roles here.
1341 ty_co_match menv subst ty (SubCo co) lkco rkco
1342 = ty_co_match menv subst ty co lkco rkco
1343
1344 ty_co_match menv subst (AppTy ty1a ty1b) co _lkco _rkco
1345 | Just (co2, arg2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy
1346 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1347 ty_co_match menv subst ty1 (AppCo co2 arg2) _lkco _rkco
1348 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
1349 -- yes, the one from Type, not TcType; this is for coercion optimization
1350 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1351
1352 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos) _lkco _rkco
1353 = ty_co_match_tc menv subst tc1 tys tc2 cos
1354 ty_co_match menv subst (FunTy ty1 ty2) co _lkco _rkco
1355 -- Despite the fact that (->) is polymorphic in four type variables (two
1356 -- runtime rep and two types), we shouldn't need to explicitly unify the
1357 -- runtime reps here; unifying the types themselves should be sufficient.
1358 -- See Note [Representation of function types].
1359 | Just (tc, [_,_,co1,co2]) <- splitTyConAppCo_maybe co
1360 , tc == funTyCon
1361 = let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) [co1,co2]
1362 in ty_co_match_args menv subst [ty1, ty2] [co1, co2] lkcos rkcos
1363
1364 ty_co_match menv subst (ForAllTy (TvBndr tv1 _) ty1)
1365 (ForAllCo tv2 kind_co2 co2)
1366 lkco rkco
1367 = do { subst1 <- ty_co_match menv subst (tyVarKind tv1) kind_co2
1368 ki_ki_co ki_ki_co
1369 ; let rn_env0 = me_env menv
1370 rn_env1 = rnBndr2 rn_env0 tv1 tv2
1371 menv' = menv { me_env = rn_env1 }
1372 ; ty_co_match menv' subst1 ty1 co2 lkco rkco }
1373 where
1374 ki_ki_co = mkNomReflCo liftedTypeKind
1375
1376 ty_co_match _ subst (CoercionTy {}) _ _ _
1377 = Just subst -- don't inspect coercions
1378
1379 ty_co_match menv subst ty co lkco rkco
1380 | Just co' <- pushRefl co = ty_co_match menv subst ty co' lkco rkco
1381 | otherwise = Nothing
1382
1383 ty_co_match_tc :: MatchEnv -> LiftCoEnv
1384 -> TyCon -> [Type]
1385 -> TyCon -> [Coercion]
1386 -> Maybe LiftCoEnv
1387 ty_co_match_tc menv subst tc1 tys1 tc2 cos2
1388 = do { guard (tc1 == tc2)
1389 ; ty_co_match_args menv subst tys1 cos2 lkcos rkcos }
1390 where
1391 Pair lkcos rkcos
1392 = traverse (fmap mkNomReflCo . coercionKind) cos2
1393
1394 ty_co_match_app :: MatchEnv -> LiftCoEnv
1395 -> Type -> [Type] -> Coercion -> [Coercion]
1396 -> Maybe LiftCoEnv
1397 ty_co_match_app menv subst ty1 ty1args co2 co2args
1398 | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
1399 , Just (co2', co2a) <- splitAppCo_maybe co2
1400 = ty_co_match_app menv subst ty1' (ty1a : ty1args) co2' (co2a : co2args)
1401
1402 | otherwise
1403 = do { subst1 <- ty_co_match menv subst ki1 ki2 ki_ki_co ki_ki_co
1404 ; let Pair lkco rkco = mkNomReflCo <$> coercionKind ki2
1405 ; subst2 <- ty_co_match menv subst1 ty1 co2 lkco rkco
1406 ; let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) co2args
1407 ; ty_co_match_args menv subst2 ty1args co2args lkcos rkcos }
1408 where
1409 ki1 = typeKind ty1
1410 ki2 = promoteCoercion co2
1411 ki_ki_co = mkNomReflCo liftedTypeKind
1412
1413 ty_co_match_args :: MatchEnv -> LiftCoEnv -> [Type]
1414 -> [Coercion] -> [Coercion] -> [Coercion]
1415 -> Maybe LiftCoEnv
1416 ty_co_match_args _ subst [] [] _ _ = Just subst
1417 ty_co_match_args menv subst (ty:tys) (arg:args) (lkco:lkcos) (rkco:rkcos)
1418 = do { subst' <- ty_co_match menv subst ty arg lkco rkco
1419 ; ty_co_match_args menv subst' tys args lkcos rkcos }
1420 ty_co_match_args _ _ _ _ _ _ = Nothing
1421
1422 pushRefl :: Coercion -> Maybe Coercion
1423 pushRefl (Refl Nominal (AppTy ty1 ty2))
1424 = Just (AppCo (Refl Nominal ty1) (mkNomReflCo ty2))
1425 pushRefl (Refl r (FunTy ty1 ty2))
1426 | Just rep1 <- getRuntimeRep_maybe ty1
1427 , Just rep2 <- getRuntimeRep_maybe ty2
1428 = Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2
1429 , mkReflCo r ty1, mkReflCo r ty2 ])
1430 pushRefl (Refl r (TyConApp tc tys))
1431 = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
1432 pushRefl (Refl r (ForAllTy (TvBndr tv _) ty))
1433 = Just (mkHomoForAllCos_NoRefl [tv] (Refl r ty))
1434 -- NB: NoRefl variant. Otherwise, we get a loop!
1435 pushRefl (Refl r (CastTy ty co)) = Just (castCoercionKind (Refl r ty) co co)
1436 pushRefl _ = Nothing