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