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