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