Fix exponential algorithm in pure unifier.
[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 = mkTvSubst (mkInScopeSet range_tvs) tenv
486
487 -- env' extends env by replacing any free type with
488 -- that same tyvar with a substituted kind
489 -- See note [Finding the substitution fixpoint]
490 tenv' = extendVarEnvList tenv [ (rtv, mkTyVarTy $
491 setTyVarKind rtv $
492 substTy subst $
493 tyVarKind rtv)
494 | rtv <- varSetElems range_tvs
495 , not (in_domain rtv) ]
496 subst' = mkTvSubst (mkInScopeSet range_tvs) tenv'
497
498 niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
499 -- Apply the non-idempotent substitution to a set of type variables,
500 -- remembering that the substitution isn't necessarily idempotent
501 -- This is used in the occurs check, before extending the substitution
502 niSubstTvSet tsubst tvs
503 = foldVarSet (unionVarSet . get) emptyVarSet tvs
504 where
505 get tv
506 | Just ty <- lookupVarEnv tsubst tv
507 = niSubstTvSet tsubst (tyCoVarsOfType ty)
508
509 | otherwise
510 = unitVarSet tv
511
512 {-
513 ************************************************************************
514 * *
515 The workhorse
516 * *
517 ************************************************************************
518
519 Note [Specification of unification]
520 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
521 The algorithm implemented here is rather delicate, and we depend on it
522 to uphold certain properties. This is a summary of these required
523 properties. Any reference to "flattening" refers to the flattening
524 algorithm in FamInstEnv (See Note [Flattening] in FamInstEnv), not
525 the flattening algorithm in the solver.
526
527 Notation:
528 θ,φ substitutions
529 ξ type-function-free types
530 τ,σ other types
531 τ♭ type τ, flattened
532
533 ≡ eqType
534
535 (U1) Soundness.
536 If (unify τ₁ τ₂) = Unifiable θ, then θ(τ₁) ≡ θ(τ₂). θ is a most general
537 unifier for τ₁ and τ₂.
538
539 (U2) Completeness.
540 If (unify ξ₁ ξ₂) = SurelyApart,
541 then there exists no substitution θ such that θ(ξ₁) ≡ θ(ξ₂).
542
543 These two properties are stated as Property 11 in the "Closed Type Families"
544 paper (POPL'14). Below, this paper is called [CTF].
545
546 (U3) Apartness under substitution.
547 If (unify ξ τ♭) = SurelyApart, then (unify ξ θ(τ)♭) = SurelyApart, for
548 any θ. (Property 12 from [CTF])
549
550 (U4) Apart types do not unify.
551 If (unify ξ τ♭) = SurelyApart, then there exists no θ such that
552 θ(ξ) = θ(τ). (Property 13 from [CTF])
553
554 THEOREM. Completeness w.r.t ~
555 If (unify τ₁♭ τ₂♭) = SurelyApart, then there exists no proof that (τ₁ ~ τ₂).
556
557 PROOF. See appendix of [CTF].
558
559
560 The unification algorithm is used for type family injectivity, as described
561 in the "Injective Type Families" paper (Haskell'15), called [ITF]. When run
562 in this mode, it has the following properties.
563
564 (I1) If (unify σ τ) = SurelyApart, then σ and τ are not unifiable, even
565 after arbitrary type family reductions. Note that σ and τ are not flattened
566 here.
567
568 (I2) If (unify σ τ) = MaybeApart θ, and if some
569 φ exists such that φ(σ) ~ φ(τ), then φ extends θ.
570
571
572 Furthermore, the RULES matching algorithm requires this property,
573 but only when using this algorithm for matching:
574
575 (M1) If (match σ τ) succeeds with θ, then all matchable tyvars in σ
576 are bound in θ.
577
578 Property M1 means that we must extend the substitution with, say
579 (a ↦ a) when appropriate during matching.
580 See also Note [Self-substitution when matching].
581
582 (M2) Completeness of matching.
583 If θ(σ) = τ, then (match σ τ) = Unifiable φ, where θ is an extension of φ.
584
585 Sadly, property M2 and I2 conflict. Consider
586
587 type family F1 a b where
588 F1 Int Bool = Char
589 F1 Double String = Char
590
591 Consider now two matching problems:
592
593 P1. match (F1 a Bool) (F1 Int Bool)
594 P2. match (F1 a Bool) (F1 Double String)
595
596 In case P1, we must find (a ↦ Int) to satisfy M2.
597 In case P2, we must /not/ find (a ↦ Double), in order to satisfy I2. (Note
598 that the correct mapping for I2 is (a ↦ Int). There is no way to discover
599 this, but we musn't map a to anything else!)
600
601 We thus must parameterize the algorithm over whether it's being used
602 for an injectivity check (refrain from looking at non-injective arguments
603 to type families) or not (do indeed look at those arguments).
604
605 (It's all a question of whether or not to include equation (7) from Fig. 2
606 of [ITF].)
607
608 This extra parameter is a bit fiddly, perhaps, but seemingly less so than
609 having two separate, almost-identical algorithms.
610
611 Note [Self-substitution when matching]
612 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
613 What should happen when we're *matching* (not unifying) a1 with a1? We
614 should get a substitution [a1 |-> a1]. A successful match should map all
615 the template variables (except ones that disappear when expanding synonyms).
616 But when unifying, we don't want to do this, because we'll then fall into
617 a loop.
618
619 This arrangement affects the code in three places:
620 - If we're matching a refined template variable, don't recur. Instead, just
621 check for equality. That is, if we know [a |-> Maybe a] and are matching
622 (a ~? Maybe Int), we want to just fail.
623
624 - Skip the occurs check when matching. This comes up in two places, because
625 matching against variables is handled separately from matching against
626 full-on types.
627
628 Note that this arrangement was provoked by a real failure, where the same
629 unique ended up in the template as in the target. (It was a rule firing when
630 compiling Data.List.NonEmpty.)
631
632 Note [Matching coercion variables]
633 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
634 Consider this:
635
636 type family F a
637
638 data G a where
639 MkG :: F a ~ Bool => G a
640
641 type family Foo (x :: G a) :: F a
642 type instance Foo MkG = False
643
644 We would like that to be accepted. For that to work, we need to introduce
645 a coercion variable on the left an then use it on the right. Accordingly,
646 at use sites of Foo, we need to be able to use matching to figure out the
647 value for the coercion. (See the desugared version:
648
649 axFoo :: [a :: *, c :: F a ~ Bool]. Foo (MkG c) = False |> (sym c)
650
651 ) We never want this action to happen during *unification* though, when
652 all bets are off.
653
654 -}
655
656 -- See Note [Specification of unification]
657 unify_ty :: Type -> Type -> Coercion -- Types to be unified and a co
658 -- between their kinds
659 -- See Note [Kind coercions in Unify]
660 -> UM ()
661 -- Respects newtypes, PredTypes
662
663 unify_ty ty1 ty2 kco
664 | Just ty1' <- coreView ty1 = unify_ty ty1' ty2 kco
665 | Just ty2' <- coreView ty2 = unify_ty ty1 ty2' kco
666 | CastTy ty1' co <- ty1 = unify_ty ty1' ty2 (co `mkTransCo` kco)
667 | CastTy ty2' co <- ty2 = unify_ty ty1 ty2' (kco `mkTransCo` mkSymCo co)
668
669 unify_ty (TyVarTy tv1) ty2 kco = uVar tv1 ty2 kco
670 unify_ty ty1 (TyVarTy tv2) kco
671 = do { unif <- amIUnifying
672 ; if unif
673 then umSwapRn $ uVar tv2 ty1 (mkSymCo kco)
674 else surelyApart } -- non-tv on left; tv on right: can't match.
675
676 unify_ty ty1 ty2 _kco
677 | Just (tc1, tys1) <- splitTyConApp_maybe ty1
678 , Just (tc2, tys2) <- splitTyConApp_maybe ty2
679 = if tc1 == tc2 || (isStarKind ty1 && isStarKind ty2)
680 then if isInjectiveTyCon tc1 Nominal
681 then unify_tys tys1 tys2
682 else do { let inj | isTypeFamilyTyCon tc1
683 = case familyTyConInjectivityInfo tc1 of
684 NotInjective -> repeat False
685 Injective bs -> bs
686 | otherwise
687 = repeat False
688
689 (inj_tys1, noninj_tys1) = partitionByList inj tys1
690 (inj_tys2, noninj_tys2) = partitionByList inj tys2
691
692 ; unify_tys inj_tys1 inj_tys2
693 ; inj_tf <- checkingInjectivity
694 ; unless inj_tf $ -- See (end of) Note [Specification of unification]
695 don'tBeSoSure $ unify_tys noninj_tys1 noninj_tys2 }
696 else -- tc1 /= tc2
697 if isGenerativeTyCon tc1 Nominal && isGenerativeTyCon tc2 Nominal
698 then surelyApart
699 else maybeApart
700
701 -- Applications need a bit of care!
702 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
703 -- NB: we've already dealt with type variables,
704 -- so if one type is an App the other one jolly well better be too
705 unify_ty (AppTy ty1a ty1b) ty2 _kco
706 | Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
707 = unify_ty_app ty1a [ty1b] ty2a [ty2b]
708
709 unify_ty ty1 (AppTy ty2a ty2b) _kco
710 | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
711 = unify_ty_app ty1a [ty1b] ty2a [ty2b]
712
713 unify_ty (LitTy x) (LitTy y) _kco | x == y = return ()
714
715 unify_ty (ForAllTy (Named tv1 _) ty1) (ForAllTy (Named tv2 _) ty2) kco
716 = do { unify_ty (tyVarKind tv1) (tyVarKind tv2) (mkNomReflCo liftedTypeKind)
717 ; umRnBndr2 tv1 tv2 $ unify_ty ty1 ty2 kco }
718
719 -- See Note [Matching coercion variables]
720 unify_ty (CoercionTy co1) (CoercionTy co2) kco
721 = do { unif <- amIUnifying
722 ; c_subst <- getCvSubstEnv
723 ; case co1 of
724 CoVarCo cv
725 | not unif
726 , not (cv `elemVarEnv` c_subst)
727 -> do { b <- tvBindFlagL cv
728 ; if b == BindMe
729 then do { checkRnEnvRCo co2
730 ; let [_, _, co_l, co_r] = decomposeCo 4 kco
731 -- cv :: t1 ~ t2
732 -- co2 :: s1 ~ s2
733 -- co_l :: t1 ~ s1
734 -- co_r :: t2 ~ s2
735 ; extendCvEnv cv (co_l `mkTransCo`
736 co2 `mkTransCo`
737 mkSymCo co_r) }
738 else return () }
739 _ -> return () }
740
741 unify_ty ty1 _ _
742 | Just (tc1, _) <- splitTyConApp_maybe ty1
743 , not (isGenerativeTyCon tc1 Nominal)
744 = maybeApart
745
746 unify_ty _ ty2 _
747 | Just (tc2, _) <- splitTyConApp_maybe ty2
748 , not (isGenerativeTyCon tc2 Nominal)
749 = do { unif <- amIUnifying
750 ; if unif then maybeApart else surelyApart }
751
752 unify_ty _ _ _ = surelyApart
753
754 unify_ty_app :: Type -> [Type] -> Type -> [Type] -> UM ()
755 unify_ty_app ty1 ty1args ty2 ty2args
756 | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
757 , Just (ty2', ty2a) <- repSplitAppTy_maybe ty2
758 = unify_ty_app ty1' (ty1a : ty1args) ty2' (ty2a : ty2args)
759
760 | otherwise
761 = do { let ki1 = typeKind ty1
762 ki2 = typeKind ty2
763 ; unify_ty ki1 ki2 (mkNomReflCo liftedTypeKind)
764 ; unify_ty ty1 ty2 (mkNomReflCo ki1)
765 ; unify_tys ty1args ty2args }
766
767 unify_tys :: [Type] -> [Type] -> UM ()
768 unify_tys orig_xs orig_ys
769 = go orig_xs orig_ys
770 where
771 go [] [] = return ()
772 go (x:xs) (y:ys)
773 = do { unify_ty x y (mkNomReflCo $ typeKind x)
774 ; go xs ys }
775 go _ _ = maybeApart -- See Note [Lists of different lengths are MaybeApart]
776
777 ---------------------------------
778 uVar :: TyVar -- Variable to be unified
779 -> Type -- with this Type
780 -> Coercion -- :: kind tv ~N kind ty
781 -> UM ()
782
783 uVar tv1 ty kco
784 = do { -- Check to see whether tv1 is refined by the substitution
785 subst <- getTvSubstEnv
786 ; case (lookupVarEnv subst tv1) of
787 Just ty' -> do { unif <- amIUnifying
788 ; if unif
789 then unify_ty ty' ty kco -- Yes, call back into unify
790 else -- when *matching*, we don't want to just recur here.
791 -- this is because the range of the subst is the target
792 -- type, not the template type. So, just check for
793 -- normal type equality.
794 guard ((ty' `mkCastTy` kco) `eqType` ty) }
795 Nothing -> uUnrefined tv1 ty ty kco } -- No, continue
796
797 uUnrefined :: TyVar -- variable to be unified
798 -> Type -- with this Type
799 -> Type -- (version w/ expanded synonyms)
800 -> Coercion -- :: kind tv ~N kind ty
801 -> UM ()
802
803 -- We know that tv1 isn't refined
804
805 uUnrefined tv1 ty2 ty2' kco
806 | Just ty2'' <- coreView ty2'
807 = uUnrefined tv1 ty2 ty2'' kco -- Unwrap synonyms
808 -- This is essential, in case we have
809 -- type Foo a = a
810 -- and then unify a ~ Foo a
811
812 | TyVarTy tv2 <- ty2'
813 = do { tv1' <- umRnOccL tv1
814 ; tv2' <- umRnOccR tv2
815 ; unif <- amIUnifying
816 -- See Note [Self-substitution when matching]
817 ; when (tv1' /= tv2' || not unif) $ do
818 { subst <- getTvSubstEnv
819 -- Check to see whether tv2 is refined
820 ; case lookupVarEnv subst tv2 of
821 { Just ty' | unif -> uUnrefined tv1 ty' ty' kco
822 ; _ -> do
823 { -- So both are unrefined
824
825 -- And then bind one or the other,
826 -- depending on which is bindable
827 ; b1 <- tvBindFlagL tv1
828 ; b2 <- tvBindFlagR tv2
829 ; let ty1 = mkTyVarTy tv1
830 ; case (b1, b2) of
831 (BindMe, _) -> do { checkRnEnvR ty2 -- make sure ty2 is not a local
832 ; extendTvEnv tv1 (ty2 `mkCastTy` mkSymCo kco) }
833 (_, BindMe) | unif -> do { checkRnEnvL ty1 -- ditto for ty1
834 ; extendTvEnv tv2 (ty1 `mkCastTy` kco) }
835
836 _ | tv1' == tv2' -> return ()
837 -- How could this happen? If we're only matching and if
838 -- we're comparing forall-bound variables.
839
840 _ -> maybeApart -- See Note [Unification with skolems]
841 }}}}
842
843 uUnrefined tv1 ty2 ty2' kco -- ty2 is not a type variable
844 = do { occurs <- elemNiSubstSet tv1 (tyCoVarsOfType ty2')
845 ; unif <- amIUnifying
846 ; if unif && occurs -- See Note [Self-substitution when matching]
847 then maybeApart -- Occurs check, see Note [Fine-grained unification]
848 else do bindTv tv1 (ty2 `mkCastTy` mkSymCo kco) }
849 -- Bind tyvar to the synonym if poss
850
851 elemNiSubstSet :: TyVar -> TyCoVarSet -> UM Bool
852 elemNiSubstSet v set
853 = do { tsubst <- getTvSubstEnv
854 ; return $ v `elemVarSet` niSubstTvSet tsubst set }
855
856 bindTv :: TyVar -> Type -> UM ()
857 bindTv tv ty -- ty is not a variable
858 = do { checkRnEnvR ty -- make sure ty mentions no local variables
859 ; b <- tvBindFlagL tv
860 ; case b of
861 Skolem -> maybeApart -- See Note [Unification with skolems]
862 BindMe -> extendTvEnv tv ty
863 }
864
865 {-
866 %************************************************************************
867 %* *
868 Binding decisions
869 * *
870 ************************************************************************
871 -}
872
873 data BindFlag
874 = BindMe -- A regular type variable
875
876 | Skolem -- This type variable is a skolem constant
877 -- Don't bind it; it only matches itself
878 deriving Eq
879
880 {-
881 ************************************************************************
882 * *
883 Unification monad
884 * *
885 ************************************************************************
886 -}
887
888 data UMEnv = UMEnv { um_bind_fun :: TyVar -> BindFlag
889 -- the user-supplied BindFlag function
890 , um_unif :: Bool -- unification (True) or matching?
891 , um_inj_tf :: Bool -- checking for injectivity?
892 -- See (end of) Note [Specification of unification]
893 , um_rn_env :: RnEnv2 }
894
895 data UMState = UMState
896 { um_tv_env :: TvSubstEnv
897 , um_cv_env :: CvSubstEnv }
898
899 newtype UM a = UM { unUM :: UMEnv -> UMState
900 -> UnifyResultM (UMState, a) }
901
902 instance Functor UM where
903 fmap = liftM
904
905 instance Applicative UM where
906 pure a = UM (\_ s -> pure (s, a))
907 (<*>) = ap
908
909 instance Monad UM where
910 fail _ = UM (\_ _ -> SurelyApart) -- failed pattern match
911 m >>= k = UM (\env state ->
912 do { (state', v) <- unUM m env state
913 ; unUM (k v) env state' })
914
915 -- need this instance because of a use of 'guard' above
916 instance Alternative UM where
917 empty = UM (\_ _ -> Control.Applicative.empty)
918 m1 <|> m2 = UM (\env state ->
919 unUM m1 env state <|>
920 unUM m2 env state)
921
922 instance MonadPlus UM
923
924 #if __GLASGOW_HASKELL__ > 710
925 instance MonadFail.MonadFail UM where
926 fail _ = UM (\_tvs _subst -> SurelyApart) -- failed pattern match
927 #endif
928
929 initUM :: (TyVar -> BindFlag)
930 -> Bool -- True <=> unify; False <=> match
931 -> Bool -- True <=> doing an injectivity check
932 -> RnEnv2
933 -> TvSubstEnv -- subst to extend
934 -> CvSubstEnv
935 -> UM a -> UnifyResultM a
936 initUM badtvs unif inj_tf rn_env subst_env cv_subst_env um
937 = case unUM um env state of
938 Unifiable (_, subst) -> Unifiable subst
939 MaybeApart (_, subst) -> MaybeApart subst
940 SurelyApart -> SurelyApart
941 where
942 env = UMEnv { um_bind_fun = badtvs
943 , um_unif = unif
944 , um_inj_tf = inj_tf
945 , um_rn_env = rn_env }
946 state = UMState { um_tv_env = subst_env
947 , um_cv_env = cv_subst_env }
948
949 tvBindFlagL :: TyVar -> UM BindFlag
950 tvBindFlagL tv = UM $ \env state ->
951 Unifiable (state, if inRnEnvL (um_rn_env env) tv
952 then Skolem
953 else um_bind_fun env tv)
954
955 tvBindFlagR :: TyVar -> UM BindFlag
956 tvBindFlagR tv = UM $ \env state ->
957 Unifiable (state, if inRnEnvR (um_rn_env env) tv
958 then Skolem
959 else um_bind_fun env tv)
960
961 getTvSubstEnv :: UM TvSubstEnv
962 getTvSubstEnv = UM $ \_ state -> Unifiable (state, um_tv_env state)
963
964 getCvSubstEnv :: UM CvSubstEnv
965 getCvSubstEnv = UM $ \_ state -> Unifiable (state, um_cv_env state)
966
967 extendTvEnv :: TyVar -> Type -> UM ()
968 extendTvEnv tv ty = UM $ \_ state ->
969 Unifiable (state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())
970
971 extendCvEnv :: CoVar -> Coercion -> UM ()
972 extendCvEnv cv co = UM $ \_ state ->
973 Unifiable (state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())
974
975 umRnBndr2 :: TyCoVar -> TyCoVar -> UM a -> UM a
976 umRnBndr2 v1 v2 thing = UM $ \env state ->
977 let rn_env' = rnBndr2 (um_rn_env env) v1 v2 in
978 unUM thing (env { um_rn_env = rn_env' }) state
979
980 checkRnEnv :: (RnEnv2 -> Var -> Bool) -> VarSet -> UM ()
981 checkRnEnv inRnEnv varset = UM $ \env state ->
982 if any (inRnEnv (um_rn_env env)) (varSetElems varset)
983 then MaybeApart (state, ())
984 else Unifiable (state, ())
985
986 -- | Converts any SurelyApart to a MaybeApart
987 don'tBeSoSure :: UM () -> UM ()
988 don'tBeSoSure um = UM $ \env state ->
989 case unUM um env state of
990 SurelyApart -> MaybeApart (state, ())
991 other -> other
992
993 checkRnEnvR :: Type -> UM ()
994 checkRnEnvR ty = checkRnEnv inRnEnvR (tyCoVarsOfType ty)
995
996 checkRnEnvL :: Type -> UM ()
997 checkRnEnvL ty = checkRnEnv inRnEnvL (tyCoVarsOfType ty)
998
999 checkRnEnvRCo :: Coercion -> UM ()
1000 checkRnEnvRCo co = checkRnEnv inRnEnvR (tyCoVarsOfCo co)
1001
1002 umRnOccL :: TyVar -> UM TyVar
1003 umRnOccL v = UM $ \env state ->
1004 Unifiable (state, rnOccL (um_rn_env env) v)
1005
1006 umRnOccR :: TyVar -> UM TyVar
1007 umRnOccR v = UM $ \env state ->
1008 Unifiable (state, rnOccR (um_rn_env env) v)
1009
1010 umSwapRn :: UM a -> UM a
1011 umSwapRn thing = UM $ \env state ->
1012 let rn_env' = rnSwap (um_rn_env env) in
1013 unUM thing (env { um_rn_env = rn_env' }) state
1014
1015 amIUnifying :: UM Bool
1016 amIUnifying = UM $ \env state -> Unifiable (state, um_unif env)
1017
1018 checkingInjectivity :: UM Bool
1019 checkingInjectivity = UM $ \env state -> Unifiable (state, um_inj_tf env)
1020
1021 maybeApart :: UM ()
1022 maybeApart = UM (\_ state -> MaybeApart (state, ()))
1023
1024 surelyApart :: UM a
1025 surelyApart = UM (\_ _ -> SurelyApart)
1026
1027 {-
1028 %************************************************************************
1029 %* *
1030 Matching a (lifted) type against a coercion
1031 %* *
1032 %************************************************************************
1033
1034 This section defines essentially an inverse to liftCoSubst. It is defined
1035 here to avoid a dependency from Coercion on this module.
1036
1037 -}
1038
1039 data MatchEnv = ME { me_tmpls :: TyVarSet
1040 , me_env :: RnEnv2 }
1041
1042 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
1043 -- @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@,
1044 -- where @==@ there means that the result of tyCoSubst has the same
1045 -- type as the original co; but may be different under the hood.
1046 -- That is, it matches a type against a coercion of the same
1047 -- "shape", and returns a lifting substitution which could have been
1048 -- used to produce the given coercion from the given type.
1049 -- Note that this function is incomplete -- it might return Nothing
1050 -- when there does indeed exist a possible lifting context.
1051 --
1052 -- This function is incomplete in that it doesn't respect the equality
1053 -- in `eqType`. That is, it's possible that this will succeed for t1 and
1054 -- fail for t2, even when t1 `eqType` t2. That's because it depends on
1055 -- there being a very similar structure between the type and the coercion.
1056 -- This incompleteness shouldn't be all that surprising, especially because
1057 -- it depends on the structure of the coercion, which is a silly thing to do.
1058 --
1059 -- The lifting context produced doesn't have to be exacting in the roles
1060 -- of the mappings. This is because any use of the lifting context will
1061 -- also require a desired role. Thus, this algorithm prefers mapping to
1062 -- nominal coercions where it can do so.
1063 liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
1064 liftCoMatch tmpls ty co
1065 = do { cenv1 <- ty_co_match menv emptyVarEnv ki ki_co ki_ki_co ki_ki_co
1066 ; cenv2 <- ty_co_match menv cenv1 ty co
1067 (mkNomReflCo co_lkind) (mkNomReflCo co_rkind)
1068 ; return (LC (mkEmptyTCvSubst in_scope) cenv2) }
1069 where
1070 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
1071 in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
1072 -- Like tcMatchTy, assume all the interesting variables
1073 -- in ty are in tmpls
1074
1075 ki = typeKind ty
1076 ki_co = promoteCoercion co
1077 ki_ki_co = mkNomReflCo liftedTypeKind
1078
1079 Pair co_lkind co_rkind = coercionKind ki_co
1080
1081 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
1082 ty_co_match :: MatchEnv -- ^ ambient helpful info
1083 -> LiftCoEnv -- ^ incoming subst
1084 -> Type -- ^ ty, type to match
1085 -> Coercion -- ^ co, coercion to match against
1086 -> Coercion -- ^ :: kind of L type of substed ty ~N L kind of co
1087 -> Coercion -- ^ :: kind of R type of substed ty ~N R kind of co
1088 -> Maybe LiftCoEnv
1089 ty_co_match menv subst ty co lkco rkco
1090 | Just ty' <- coreViewOneStarKind ty = ty_co_match menv subst ty' co lkco rkco
1091
1092 -- handle Refl case:
1093 | tyCoVarsOfType ty `isNotInDomainOf` subst
1094 , Just (ty', _) <- isReflCo_maybe co
1095 , ty `eqType` ty'
1096 = Just subst
1097
1098 where
1099 isNotInDomainOf :: VarSet -> VarEnv a -> Bool
1100 isNotInDomainOf set env
1101 = noneSet (\v -> elemVarEnv v env) set
1102
1103 noneSet :: (Var -> Bool) -> VarSet -> Bool
1104 noneSet f = foldVarSet (\v rest -> rest && (not $ f v)) True
1105
1106 ty_co_match menv subst ty co lkco rkco
1107 | CastTy ty' co' <- ty
1108 = ty_co_match menv subst ty' co (co' `mkTransCo` lkco) (co' `mkTransCo` rkco)
1109
1110 | CoherenceCo co1 co2 <- co
1111 = ty_co_match menv subst ty co1 (lkco `mkTransCo` mkSymCo co2) rkco
1112
1113 | SymCo co' <- co
1114 = swapLiftCoEnv <$> ty_co_match menv (swapLiftCoEnv subst) ty co' rkco lkco
1115
1116 -- Match a type variable against a non-refl coercion
1117 ty_co_match menv subst (TyVarTy tv1) co lkco rkco
1118 | Just co1' <- lookupVarEnv subst tv1' -- tv1' is already bound to co1
1119 = if eqCoercionX (nukeRnEnvL rn_env) co1' co
1120 then Just subst
1121 else Nothing -- no match since tv1 matches two different coercions
1122
1123 | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
1124 = if any (inRnEnvR rn_env) (tyCoVarsOfCoList co)
1125 then Nothing -- occurs check failed
1126 else Just $ extendVarEnv subst tv1' $
1127 castCoercionKind co (mkSymCo lkco) (mkSymCo rkco)
1128
1129 | otherwise
1130 = Nothing
1131
1132 where
1133 rn_env = me_env menv
1134 tv1' = rnOccL rn_env tv1
1135
1136 -- just look through SubCo's. We don't really care about roles here.
1137 ty_co_match menv subst ty (SubCo co) lkco rkco
1138 = ty_co_match menv subst ty co lkco rkco
1139
1140 ty_co_match menv subst (AppTy ty1a ty1b) co _lkco _rkco
1141 | Just (co2, arg2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy
1142 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1143 ty_co_match menv subst ty1 (AppCo co2 arg2) _lkco _rkco
1144 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
1145 -- yes, the one from Type, not TcType; this is for coercion optimization
1146 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1147
1148 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos) _lkco _rkco
1149 = ty_co_match_tc menv subst tc1 tys tc2 cos
1150 ty_co_match menv subst (ForAllTy (Anon ty1) ty2) (TyConAppCo _ tc cos) _lkco _rkco
1151 = ty_co_match_tc menv subst funTyCon [ty1, ty2] tc cos
1152
1153 ty_co_match menv subst (ForAllTy (Named tv1 _) ty1)
1154 (ForAllCo tv2 kind_co2 co2)
1155 lkco rkco
1156 = do { subst1 <- ty_co_match menv subst (tyVarKind tv1) kind_co2
1157 ki_ki_co ki_ki_co
1158 ; let rn_env0 = me_env menv
1159 rn_env1 = rnBndr2 rn_env0 tv1 tv2
1160 menv' = menv { me_env = rn_env1 }
1161 ; ty_co_match menv' subst1 ty1 co2 lkco rkco }
1162 where
1163 ki_ki_co = mkNomReflCo liftedTypeKind
1164
1165 ty_co_match _ subst (CoercionTy {}) _ _ _
1166 = Just subst -- don't inspect coercions
1167
1168 ty_co_match menv subst ty co lkco rkco
1169 | Just co' <- pushRefl co = ty_co_match menv subst ty co' lkco rkco
1170 | otherwise = Nothing
1171
1172 ty_co_match_tc :: MatchEnv -> LiftCoEnv
1173 -> TyCon -> [Type]
1174 -> TyCon -> [Coercion]
1175 -> Maybe LiftCoEnv
1176 ty_co_match_tc menv subst tc1 tys1 tc2 cos2
1177 = do { guard (tc1 == tc2)
1178 ; ty_co_match_args menv subst tys1 cos2 lkcos rkcos }
1179 where
1180 Pair lkcos rkcos
1181 = traverse (fmap mkNomReflCo . coercionKind) cos2
1182
1183 ty_co_match_app :: MatchEnv -> LiftCoEnv
1184 -> Type -> [Type] -> Coercion -> [Coercion]
1185 -> Maybe LiftCoEnv
1186 ty_co_match_app menv subst ty1 ty1args co2 co2args
1187 | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
1188 , Just (co2', co2a) <- splitAppCo_maybe co2
1189 = ty_co_match_app menv subst ty1' (ty1a : ty1args) co2' (co2a : co2args)
1190
1191 | otherwise
1192 = do { subst1 <- ty_co_match menv subst ki1 ki2 ki_ki_co ki_ki_co
1193 ; let Pair lkco rkco = mkNomReflCo <$> coercionKind ki2
1194 ; subst2 <- ty_co_match menv subst1 ty1 co2 lkco rkco
1195 ; let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) co2args
1196 ; ty_co_match_args menv subst2 ty1args co2args lkcos rkcos }
1197 where
1198 ki1 = typeKind ty1
1199 ki2 = promoteCoercion co2
1200 ki_ki_co = mkNomReflCo liftedTypeKind
1201
1202 ty_co_match_args :: MatchEnv -> LiftCoEnv -> [Type]
1203 -> [Coercion] -> [Coercion] -> [Coercion]
1204 -> Maybe LiftCoEnv
1205 ty_co_match_args _ subst [] [] _ _ = Just subst
1206 ty_co_match_args menv subst (ty:tys) (arg:args) (lkco:lkcos) (rkco:rkcos)
1207 = do { subst' <- ty_co_match menv subst ty arg lkco rkco
1208 ; ty_co_match_args menv subst' tys args lkcos rkcos }
1209 ty_co_match_args _ _ _ _ _ _ = Nothing
1210
1211 pushRefl :: Coercion -> Maybe Coercion
1212 pushRefl (Refl Nominal (AppTy ty1 ty2))
1213 = Just (AppCo (Refl Nominal ty1) (mkNomReflCo ty2))
1214 pushRefl (Refl r (ForAllTy (Anon ty1) ty2))
1215 = Just (TyConAppCo r funTyCon [mkReflCo r ty1, mkReflCo r ty2])
1216 pushRefl (Refl r (TyConApp tc tys))
1217 = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
1218 pushRefl (Refl r (ForAllTy (Named tv _) ty))
1219 = Just (mkHomoForAllCos_NoRefl [tv] (Refl r ty))
1220 -- NB: NoRefl variant. Otherwise, we get a loop!
1221 pushRefl (Refl r (CastTy ty co)) = Just (castCoercionKind (Refl r ty) co co)
1222 pushRefl _ = Nothing