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