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