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