Merge commit '5229c43ccf77bcbffeced01dccb27398d017fa34'
[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 GhcPrelude
30
31 import Var
32 import VarEnv
33 import VarSet
34 import Kind
35 import Name( Name )
36 import Type hiding ( getTvSubstEnv )
37 import Coercion hiding ( getCvSubstEnv )
38 import TyCon
39 import TyCoRep hiding ( getTvSubstEnv, getCvSubstEnv )
40 import Util
41 import Pair
42 import Outputable
43 import UniqFM
44 import UniqSet
45
46 import Control.Monad
47 import qualified Control.Monad.Fail as MonadFail
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 a 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 -> AmIUnifying -- ^ 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 tv_env cv_env $
468 do { when match_kis $
469 unify_tys env kis1 kis2
470 ; unify_tys env tys1 tys2
471 ; (,) <$> getTvSubstEnv <*> getCvSubstEnv }
472 where
473 env = UMEnv { um_bind_fun = bind_fn
474 , um_unif = unif
475 , um_inj_tf = inj_check
476 , um_rn_env = rn_env }
477
478 kis1 = map typeKind tys1
479 kis2 = map typeKind tys2
480
481 instance Outputable a => Outputable (UnifyResultM a) where
482 ppr SurelyApart = text "SurelyApart"
483 ppr (Unifiable x) = text "Unifiable" <+> ppr x
484 ppr (MaybeApart x) = text "MaybeApart" <+> ppr x
485
486 {-
487 ************************************************************************
488 * *
489 Non-idempotent substitution
490 * *
491 ************************************************************************
492
493 Note [Non-idempotent substitution]
494 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
495 During unification we use a TvSubstEnv/CvSubstEnv pair that is
496 (a) non-idempotent
497 (b) loop-free; ie repeatedly applying it yields a fixed point
498
499 Note [Finding the substitution fixpoint]
500 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
501 Finding the fixpoint of a non-idempotent substitution arising from a
502 unification is harder than it looks, because of kinds. Consider
503 T k (H k (f:k)) ~ T * (g:*)
504 If we unify, we get the substitution
505 [ k -> *
506 , g -> H k (f:k) ]
507 To make it idempotent we don't want to get just
508 [ k -> *
509 , g -> H * (f:k) ]
510 We also want to substitute inside f's kind, to get
511 [ k -> *
512 , g -> H k (f:*) ]
513 If we don't do this, we may apply the substitution to something,
514 and get an ill-formed type, i.e. one where typeKind will fail.
515 This happened, for example, in Trac #9106.
516
517 This is the reason for extending env with [f:k -> f:*], in the
518 definition of env' in niFixTvSubst
519 -}
520
521 niFixTCvSubst :: TvSubstEnv -> TCvSubst
522 -- Find the idempotent fixed point of the non-idempotent substitution
523 -- See Note [Finding the substitution fixpoint]
524 -- ToDo: use laziness instead of iteration?
525 niFixTCvSubst tenv = f tenv
526 where
527 f tenv
528 | not_fixpoint = f (mapVarEnv (substTy subst') tenv)
529 | otherwise = subst
530 where
531 not_fixpoint = anyVarSet in_domain range_tvs
532 in_domain tv = tv `elemVarEnv` tenv
533
534 range_tvs = nonDetFoldUFM (unionVarSet . tyCoVarsOfType) emptyVarSet tenv
535 -- It's OK to use nonDetFoldUFM here because we
536 -- forget the order immediately by creating a set
537 subst = mkTvSubst (mkInScopeSet range_tvs) tenv
538
539 -- env' extends env by replacing any free type with
540 -- that same tyvar with a substituted kind
541 -- See note [Finding the substitution fixpoint]
542 tenv' = extendVarEnvList tenv [ (rtv, mkTyVarTy $
543 setTyVarKind rtv $
544 substTy subst $
545 tyVarKind rtv)
546 | rtv <- nonDetEltsUniqSet range_tvs
547 -- It's OK to use nonDetEltsUniqSet here
548 -- because we forget the order
549 -- immediatedly by putting it in VarEnv
550 , not (in_domain rtv) ]
551 subst' = mkTvSubst (mkInScopeSet range_tvs) tenv'
552
553 niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
554 -- Apply the non-idempotent substitution to a set of type variables,
555 -- remembering that the substitution isn't necessarily idempotent
556 -- This is used in the occurs check, before extending the substitution
557 niSubstTvSet tsubst tvs
558 = nonDetFoldUniqSet (unionVarSet . get) emptyVarSet tvs
559 -- It's OK to nonDetFoldUFM here because we immediately forget the
560 -- ordering by creating a set.
561 where
562 get tv
563 | Just ty <- lookupVarEnv tsubst tv
564 = niSubstTvSet tsubst (tyCoVarsOfType ty)
565
566 | otherwise
567 = unitVarSet tv
568
569 {-
570 ************************************************************************
571 * *
572 unify_ty: the main workhorse
573 * *
574 ************************************************************************
575
576 Note [Specification of unification]
577 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
578 The pure unifier, unify_ty, defined in this module, tries to work out
579 a substitution to make two types say True to eqType. NB: eqType is
580 itself not purely syntactic; it accounts for CastTys;
581 see Note [Non-trivial definitional equality] in TyCoRep
582
583 Unlike the "impure unifiers" in the typechecker (the eager unifier in
584 TcUnify, and the constraint solver itself in TcCanonical), the pure
585 unifier It does /not/ work up to ~.
586
587 The algorithm implemented here is rather delicate, and we depend on it
588 to uphold certain properties. This is a summary of these required
589 properties. Any reference to "flattening" refers to the flattening
590 algorithm in FamInstEnv (See Note [Flattening] in FamInstEnv), not
591 the flattening algorithm in the solver.
592
593 Notation:
594 θ,φ substitutions
595 ξ type-function-free types
596 τ,σ other types
597 τ♭ type τ, flattened
598
599 ≡ eqType
600
601 (U1) Soundness.
602 If (unify τ₁ τ₂) = Unifiable θ, then θ(τ₁) ≡ θ(τ₂).
603 θ is a most general unifier for τ₁ and τ₂.
604
605 (U2) Completeness.
606 If (unify ξ₁ ξ₂) = SurelyApart,
607 then there exists no substitution θ such that θ(ξ₁) ≡ θ(ξ₂).
608
609 These two properties are stated as Property 11 in the "Closed Type Families"
610 paper (POPL'14). Below, this paper is called [CTF].
611
612 (U3) Apartness under substitution.
613 If (unify ξ τ♭) = SurelyApart, then (unify ξ θ(τ)♭) = SurelyApart,
614 for any θ. (Property 12 from [CTF])
615
616 (U4) Apart types do not unify.
617 If (unify ξ τ♭) = SurelyApart, then there exists no θ
618 such that θ(ξ) = θ(τ). (Property 13 from [CTF])
619
620 THEOREM. Completeness w.r.t ~
621 If (unify τ₁♭ τ₂♭) = SurelyApart,
622 then there exists no proof that (τ₁ ~ τ₂).
623
624 PROOF. See appendix of [CTF].
625
626
627 The unification algorithm is used for type family injectivity, as described
628 in the "Injective Type Families" paper (Haskell'15), called [ITF]. When run
629 in this mode, it has the following properties.
630
631 (I1) If (unify σ τ) = SurelyApart, then σ and τ are not unifiable, even
632 after arbitrary type family reductions. Note that σ and τ are
633 not flattened here.
634
635 (I2) If (unify σ τ) = MaybeApart θ, and if some
636 φ exists such that φ(σ) ~ φ(τ), then φ extends θ.
637
638
639 Furthermore, the RULES matching algorithm requires this property,
640 but only when using this algorithm for matching:
641
642 (M1) If (match σ τ) succeeds with θ, then all matchable tyvars
643 in σ are bound in θ.
644
645 Property M1 means that we must extend the substitution with,
646 say (a ↦ a) when appropriate during matching.
647 See also Note [Self-substitution when matching].
648
649 (M2) Completeness of matching.
650 If θ(σ) = τ, then (match σ τ) = Unifiable φ,
651 where θ is an extension of φ.
652
653 Sadly, property M2 and I2 conflict. Consider
654
655 type family F1 a b where
656 F1 Int Bool = Char
657 F1 Double String = Char
658
659 Consider now two matching problems:
660
661 P1. match (F1 a Bool) (F1 Int Bool)
662 P2. match (F1 a Bool) (F1 Double String)
663
664 In case P1, we must find (a ↦ Int) to satisfy M2.
665 In case P2, we must /not/ find (a ↦ Double), in order to satisfy I2. (Note
666 that the correct mapping for I2 is (a ↦ Int). There is no way to discover
667 this, but we musn't map a to anything else!)
668
669 We thus must parameterize the algorithm over whether it's being used
670 for an injectivity check (refrain from looking at non-injective arguments
671 to type families) or not (do indeed look at those arguments). This is
672 implemented by the uf_inj_tf field of UmEnv.
673
674 (It's all a question of whether or not to include equation (7) from Fig. 2
675 of [ITF].)
676
677 This extra parameter is a bit fiddly, perhaps, but seemingly less so than
678 having two separate, almost-identical algorithms.
679
680 Note [Self-substitution when matching]
681 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
682 What should happen when we're *matching* (not unifying) a1 with a1? We
683 should get a substitution [a1 |-> a1]. A successful match should map all
684 the template variables (except ones that disappear when expanding synonyms).
685 But when unifying, we don't want to do this, because we'll then fall into
686 a loop.
687
688 This arrangement affects the code in three places:
689 - If we're matching a refined template variable, don't recur. Instead, just
690 check for equality. That is, if we know [a |-> Maybe a] and are matching
691 (a ~? Maybe Int), we want to just fail.
692
693 - Skip the occurs check when matching. This comes up in two places, because
694 matching against variables is handled separately from matching against
695 full-on types.
696
697 Note that this arrangement was provoked by a real failure, where the same
698 unique ended up in the template as in the target. (It was a rule firing when
699 compiling Data.List.NonEmpty.)
700
701 Note [Matching coercion variables]
702 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
703 Consider this:
704
705 type family F a
706
707 data G a where
708 MkG :: F a ~ Bool => G a
709
710 type family Foo (x :: G a) :: F a
711 type instance Foo MkG = False
712
713 We would like that to be accepted. For that to work, we need to introduce
714 a coercion variable on the left and then use it on the right. Accordingly,
715 at use sites of Foo, we need to be able to use matching to figure out the
716 value for the coercion. (See the desugared version:
717
718 axFoo :: [a :: *, c :: F a ~ Bool]. Foo (MkG c) = False |> (sym c)
719
720 ) We never want this action to happen during *unification* though, when
721 all bets are off.
722
723 Note [Kind coercions in Unify]
724 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
725 We wish to match/unify while ignoring casts. But, we can't just ignore
726 them completely, or we'll end up with ill-kinded substitutions. For example,
727 say we're matching `a` with `ty |> co`. If we just drop the cast, we'll
728 return [a |-> ty], but `a` and `ty` might have different kinds. We can't
729 just match/unify their kinds, either, because this might gratuitously
730 fail. After all, `co` is the witness that the kinds are the same -- they
731 may look nothing alike.
732
733 So, we pass a kind coercion to the match/unify worker. This coercion witnesses
734 the equality between the substed kind of the left-hand type and the substed
735 kind of the right-hand type. Note that we do not unify kinds at the leaves
736 (as we did previously). We thus have
737
738 INVARIANT: In the call
739 unify_ty ty1 ty2 kco
740 it must be that subst(kco) :: subst(kind(ty1)) ~N subst(kind(ty2)), where
741 `subst` is the ambient substitution in the UM monad.
742
743 To get this coercion, we first have to match/unify
744 the kinds before looking at the types. Happily, we need look only one level
745 up, as all kinds are guaranteed to have kind *.
746
747 When we're working with type applications (either TyConApp or AppTy) we
748 need to worry about establishing INVARIANT, as the kinds of the function
749 & arguments aren't (necessarily) included in the kind of the result.
750 When unifying two TyConApps, this is easy, because the two TyCons are
751 the same. Their kinds are thus the same. As long as we unify left-to-right,
752 we'll be sure to unify types' kinds before the types themselves. (For example,
753 think about Proxy :: forall k. k -> *. Unifying the first args matches up
754 the kinds of the second args.)
755
756 For AppTy, we must unify the kinds of the functions, but once these are
757 unified, we can continue unifying arguments without worrying further about
758 kinds.
759
760 The interface to this module includes both "...Ty" functions and
761 "...TyKi" functions. The former assume that INVARIANT is already
762 established, either because the kinds are the same or because the
763 list of types being passed in are the well-typed arguments to some
764 type constructor (see two paragraphs above). The latter take a separate
765 pre-pass over the kinds to establish INVARIANT. Sometimes, it's important
766 not to take the second pass, as it caused #12442.
767
768 We thought, at one point, that this was all unnecessary: why should
769 casts be in types in the first place? But they are sometimes. In
770 dependent/should_compile/KindEqualities2, we see, for example the
771 constraint Num (Int |> (blah ; sym blah)). We naturally want to find
772 a dictionary for that constraint, which requires dealing with
773 coercions in this manner.
774
775 Note [Matching in the presence of casts]
776 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
777 When matching, it is crucial that no variables from the template
778 end up in the range of the matching substitution (obviously!).
779 When unifying, that's not a constraint; instead we take the fixpoint
780 of the substitution at the end.
781
782 So what should we do with this, when matching?
783 unify_ty (tmpl |> co) tgt kco
784
785 Previously, wrongly, we pushed 'co' in the (horrid) accumulating
786 'kco' argument like this:
787 unify_ty (tmpl |> co) tgt kco
788 = unify_ty tmpl tgt (kco ; co)
789
790 But that is obviously wrong because 'co' (from the template) ends
791 up in 'kco', which in turn ends up in the range of the substitution.
792
793 This all came up in Trac #13910. Because we match tycon arguments
794 left-to-right, the ambient substitution will already have a matching
795 substitution for any kinds; so there is an easy fix: just apply
796 the substitution-so-far to the coercion from the LHS.
797
798 Note that
799
800 * When matching, the first arg of unify_ty is always the template;
801 we never swap round.
802
803 * The above argument is distressingly indirect. We seek a
804 better way.
805
806 * One better way is to ensure that type patterns (the template
807 in the matching process) have no casts. See Trac #14119.
808
809 -}
810
811 -------------- unify_ty: the main workhorse -----------
812
813 type AmIUnifying = Bool -- True <=> Unifying
814 -- False <=> Matching
815
816 unify_ty :: UMEnv
817 -> Type -> Type -- Types to be unified and a co
818 -> Coercion -- A coercion between their kinds
819 -- See Note [Kind coercions in Unify]
820 -> UM ()
821 -- See Note [Specification of unification]
822 -- Respects newtypes, PredTypes
823
824 unify_ty env ty1 ty2 kco
825 -- TODO: More commentary needed here
826 | Just ty1' <- tcView ty1 = unify_ty env ty1' ty2 kco
827 | Just ty2' <- tcView ty2 = unify_ty env ty1 ty2' kco
828 | CastTy ty1' co <- ty1 = if um_unif env
829 then unify_ty env ty1' ty2 (co `mkTransCo` kco)
830 else -- See Note [Matching in the presence of casts]
831 do { subst <- getSubst env
832 ; let co' = substCo subst co
833 ; unify_ty env ty1' ty2 (co' `mkTransCo` kco) }
834 | CastTy ty2' co <- ty2 = unify_ty env ty1 ty2' (kco `mkTransCo` mkSymCo co)
835
836 unify_ty env (TyVarTy tv1) ty2 kco
837 = uVar env tv1 ty2 kco
838 unify_ty env ty1 (TyVarTy tv2) kco
839 | um_unif env -- If unifying, can swap args
840 = uVar (umSwapRn env) tv2 ty1 (mkSymCo kco)
841
842 unify_ty env ty1 ty2 _kco
843 | Just (tc1, tys1) <- mb_tc_app1
844 , Just (tc2, tys2) <- mb_tc_app2
845 , tc1 == tc2 || (tcIsStarKind ty1 && tcIsStarKind ty2)
846 = if isInjectiveTyCon tc1 Nominal
847 then unify_tys env tys1 tys2
848 else do { let inj | isTypeFamilyTyCon tc1
849 = case tyConInjectivityInfo tc1 of
850 NotInjective -> repeat False
851 Injective bs -> bs
852 | otherwise
853 = repeat False
854
855 (inj_tys1, noninj_tys1) = partitionByList inj tys1
856 (inj_tys2, noninj_tys2) = partitionByList inj tys2
857
858 ; unify_tys env inj_tys1 inj_tys2
859 ; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
860 don'tBeSoSure $ unify_tys env noninj_tys1 noninj_tys2 }
861
862 | Just (tc1, _) <- mb_tc_app1
863 , not (isGenerativeTyCon tc1 Nominal)
864 -- E.g. unify_ty (F ty1) b = MaybeApart
865 -- because the (F ty1) behaves like a variable
866 -- NB: if unifying, we have already dealt
867 -- with the 'ty2 = variable' case
868 = maybeApart
869
870 | Just (tc2, _) <- mb_tc_app2
871 , not (isGenerativeTyCon tc2 Nominal)
872 , um_unif env
873 -- E.g. unify_ty [a] (F ty2) = MaybeApart, when unifying (only)
874 -- because the (F ty2) behaves like a variable
875 -- NB: we have already dealt with the 'ty1 = variable' case
876 = maybeApart
877
878 where
879 mb_tc_app1 = tcSplitTyConApp_maybe ty1
880 mb_tc_app2 = tcSplitTyConApp_maybe ty2
881
882 -- Applications need a bit of care!
883 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
884 -- NB: we've already dealt with type variables,
885 -- so if one type is an App the other one jolly well better be too
886 unify_ty env (AppTy ty1a ty1b) ty2 _kco
887 | Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
888 = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
889
890 unify_ty env ty1 (AppTy ty2a ty2b) _kco
891 | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
892 = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
893
894 unify_ty _ (LitTy x) (LitTy y) _kco | x == y = return ()
895
896 unify_ty env (ForAllTy (TvBndr tv1 _) ty1) (ForAllTy (TvBndr tv2 _) ty2) kco
897 = do { unify_ty env (tyVarKind tv1) (tyVarKind tv2) (mkNomReflCo liftedTypeKind)
898 ; let env' = umRnBndr2 env tv1 tv2
899 ; unify_ty env' ty1 ty2 kco }
900
901 -- See Note [Matching coercion variables]
902 unify_ty env (CoercionTy co1) (CoercionTy co2) kco
903 = do { c_subst <- getCvSubstEnv
904 ; case co1 of
905 CoVarCo cv
906 | not (um_unif env)
907 , not (cv `elemVarEnv` c_subst)
908 , BindMe <- tvBindFlagL env cv
909 -> do { checkRnEnvRCo env co2
910 ; let (co_l, co_r) = decomposeFunCo kco
911 -- cv :: t1 ~ t2
912 -- co2 :: s1 ~ s2
913 -- co_l :: t1 ~ s1
914 -- co_r :: t2 ~ s2
915 ; extendCvEnv cv (co_l `mkTransCo`
916 co2 `mkTransCo`
917 mkSymCo co_r) }
918 _ -> return () }
919
920 unify_ty _ _ _ _ = surelyApart
921
922 unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
923 unify_ty_app env ty1 ty1args ty2 ty2args
924 | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
925 , Just (ty2', ty2a) <- repSplitAppTy_maybe ty2
926 = unify_ty_app env ty1' (ty1a : ty1args) ty2' (ty2a : ty2args)
927
928 | otherwise
929 = do { let ki1 = typeKind ty1
930 ki2 = typeKind ty2
931 -- See Note [Kind coercions in Unify]
932 ; unify_ty env ki1 ki2 (mkNomReflCo liftedTypeKind)
933 ; unify_ty env ty1 ty2 (mkNomReflCo ki1)
934 ; unify_tys env ty1args ty2args }
935
936 unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
937 unify_tys env orig_xs orig_ys
938 = go orig_xs orig_ys
939 where
940 go [] [] = return ()
941 go (x:xs) (y:ys)
942 -- See Note [Kind coercions in Unify]
943 = do { unify_ty env x y (mkNomReflCo $ typeKind x)
944 ; go xs ys }
945 go _ _ = maybeApart -- See Note [Lists of different lengths are MaybeApart]
946
947 ---------------------------------
948 uVar :: UMEnv
949 -> TyVar -- Variable to be unified
950 -> Type -- with this Type
951 -> Coercion -- :: kind tv ~N kind ty
952 -> UM ()
953
954 uVar env tv1 ty kco
955 = do { -- Check to see whether tv1 is refined by the substitution
956 subst <- getTvSubstEnv
957 ; case (lookupVarEnv subst tv1) of
958 Just ty' | um_unif env -- Unifying, so call
959 -> unify_ty env ty' ty kco -- back into unify
960 | otherwise
961 -> -- Matching, we don't want to just recur here.
962 -- this is because the range of the subst is the target
963 -- type, not the template type. So, just check for
964 -- normal type equality.
965 guard ((ty' `mkCastTy` kco) `eqType` ty)
966 Nothing -> uUnrefined env tv1 ty ty kco } -- No, continue
967
968 uUnrefined :: UMEnv
969 -> TyVar -- variable to be unified
970 -> Type -- with this Type
971 -> Type -- (version w/ expanded synonyms)
972 -> Coercion -- :: kind tv ~N kind ty
973 -> UM ()
974
975 -- We know that tv1 isn't refined
976
977 uUnrefined env tv1 ty2 ty2' kco
978 | Just ty2'' <- coreView ty2'
979 = uUnrefined env tv1 ty2 ty2'' kco -- Unwrap synonyms
980 -- This is essential, in case we have
981 -- type Foo a = a
982 -- and then unify a ~ Foo a
983
984 | TyVarTy tv2 <- ty2'
985 = do { let tv1' = umRnOccL env tv1
986 tv2' = umRnOccR env tv2
987 ; unless (tv1' == tv2' && um_unif env) $ do
988 -- If we are unifying a ~ a, just return immediately
989 -- Do not extend the substitution
990 -- See Note [Self-substitution when matching]
991
992 -- Check to see whether tv2 is refined
993 { subst <- getTvSubstEnv
994 ; case lookupVarEnv subst tv2 of
995 { Just ty' | um_unif env -> uUnrefined env tv1 ty' ty' kco
996 ; _ ->
997
998 do { -- So both are unrefined
999 -- Bind one or the other, depending on which is bindable
1000 ; let b1 = tvBindFlagL env tv1
1001 b2 = tvBindFlagR env tv2
1002 ty1 = mkTyVarTy tv1
1003 ; case (b1, b2) of
1004 (BindMe, _) -> do { checkRnEnvR env ty2 -- make sure ty2 is not a local
1005 ; extendTvEnv tv1 (ty2 `mkCastTy` mkSymCo kco) }
1006 (_, BindMe) | um_unif env
1007 -> do { checkRnEnvL env ty1 -- ditto for ty1
1008 ; extendTvEnv tv2 (ty1 `mkCastTy` kco) }
1009
1010 _ | tv1' == tv2' -> return ()
1011 -- How could this happen? If we're only matching and if
1012 -- we're comparing forall-bound variables.
1013
1014 _ -> maybeApart -- See Note [Unification with skolems]
1015 }}}}
1016
1017 uUnrefined env tv1 ty2 ty2' kco -- ty2 is not a type variable
1018 = do { occurs <- elemNiSubstSet tv1 (tyCoVarsOfType ty2')
1019 ; if um_unif env && occurs -- See Note [Self-substitution when matching]
1020 then maybeApart -- Occurs check, see Note [Fine-grained unification]
1021 else bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco) }
1022 -- Bind tyvar to the synonym if poss
1023
1024 elemNiSubstSet :: TyVar -> TyCoVarSet -> UM Bool
1025 elemNiSubstSet v set
1026 = do { tsubst <- getTvSubstEnv
1027 ; return $ v `elemVarSet` niSubstTvSet tsubst set }
1028
1029 bindTv :: UMEnv -> TyVar -> Type -> UM ()
1030 bindTv env tv ty -- ty is not a variable
1031 = do { checkRnEnvR env ty -- make sure ty mentions no local variables
1032 ; case tvBindFlagL env tv of
1033 Skolem -> maybeApart -- See Note [Unification with skolems]
1034 BindMe -> extendTvEnv tv ty
1035 }
1036
1037 {-
1038 %************************************************************************
1039 %* *
1040 Binding decisions
1041 * *
1042 ************************************************************************
1043 -}
1044
1045 data BindFlag
1046 = BindMe -- A regular type variable
1047
1048 | Skolem -- This type variable is a skolem constant
1049 -- Don't bind it; it only matches itself
1050 deriving Eq
1051
1052 {-
1053 ************************************************************************
1054 * *
1055 Unification monad
1056 * *
1057 ************************************************************************
1058 -}
1059
1060 data UMEnv = UMEnv { um_bind_fun :: TyVar -> BindFlag
1061 -- User-supplied BindFlag function
1062 , um_unif :: AmIUnifying
1063 , um_inj_tf :: Bool -- Checking for injectivity?
1064 -- See (end of) Note [Specification of unification]
1065 , um_rn_env :: RnEnv2 }
1066
1067 data UMState = UMState
1068 { um_tv_env :: TvSubstEnv
1069 , um_cv_env :: CvSubstEnv }
1070
1071 newtype UM a = UM { unUM :: UMState -> UnifyResultM (UMState, a) }
1072
1073 instance Functor UM where
1074 fmap = liftM
1075
1076 instance Applicative UM where
1077 pure a = UM (\s -> pure (s, a))
1078 (<*>) = ap
1079
1080 instance Monad UM where
1081 fail = MonadFail.fail
1082 m >>= k = UM (\state ->
1083 do { (state', v) <- unUM m state
1084 ; unUM (k v) state' })
1085
1086 -- need this instance because of a use of 'guard' above
1087 instance Alternative UM where
1088 empty = UM (\_ -> Control.Applicative.empty)
1089 m1 <|> m2 = UM (\state ->
1090 unUM m1 state <|>
1091 unUM m2 state)
1092
1093 instance MonadPlus UM
1094
1095 instance MonadFail.MonadFail UM where
1096 fail _ = UM (\_ -> SurelyApart) -- failed pattern match
1097
1098 initUM :: TvSubstEnv -- subst to extend
1099 -> CvSubstEnv
1100 -> UM a -> UnifyResultM a
1101 initUM subst_env cv_subst_env um
1102 = case unUM um state of
1103 Unifiable (_, subst) -> Unifiable subst
1104 MaybeApart (_, subst) -> MaybeApart subst
1105 SurelyApart -> SurelyApart
1106 where
1107 state = UMState { um_tv_env = subst_env
1108 , um_cv_env = cv_subst_env }
1109
1110 tvBindFlagL :: UMEnv -> TyVar -> BindFlag
1111 tvBindFlagL env tv
1112 | inRnEnvL (um_rn_env env) tv = Skolem
1113 | otherwise = um_bind_fun env tv
1114
1115 tvBindFlagR :: UMEnv -> TyVar -> BindFlag
1116 tvBindFlagR env tv
1117 | inRnEnvR (um_rn_env env) tv = Skolem
1118 | otherwise = um_bind_fun env tv
1119
1120 getTvSubstEnv :: UM TvSubstEnv
1121 getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state)
1122
1123 getCvSubstEnv :: UM CvSubstEnv
1124 getCvSubstEnv = UM $ \state -> Unifiable (state, um_cv_env state)
1125
1126 getSubst :: UMEnv -> UM TCvSubst
1127 getSubst env = do { tv_env <- getTvSubstEnv
1128 ; cv_env <- getCvSubstEnv
1129 ; let in_scope = rnInScopeSet (um_rn_env env)
1130 ; return (mkTCvSubst in_scope (tv_env, cv_env)) }
1131
1132 extendTvEnv :: TyVar -> Type -> UM ()
1133 extendTvEnv tv ty = UM $ \state ->
1134 Unifiable (state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())
1135
1136 extendCvEnv :: CoVar -> Coercion -> UM ()
1137 extendCvEnv cv co = UM $ \state ->
1138 Unifiable (state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())
1139
1140 umRnBndr2 :: UMEnv -> TyCoVar -> TyCoVar -> UMEnv
1141 umRnBndr2 env v1 v2
1142 = env { um_rn_env = rnBndr2 (um_rn_env env) v1 v2 }
1143
1144 checkRnEnv :: (RnEnv2 -> VarEnv Var) -> UMEnv -> VarSet -> UM ()
1145 checkRnEnv get_set env varset = UM $ \ state ->
1146 let env_vars = get_set (um_rn_env env) in
1147 if isEmptyVarEnv env_vars || (getUniqSet varset `disjointVarEnv` env_vars)
1148 -- NB: That isEmptyVarSet is a critical optimization; it
1149 -- means we don't have to calculate the free vars of
1150 -- the type, often saving quite a bit of allocation.
1151 then Unifiable (state, ())
1152 else MaybeApart (state, ())
1153
1154 -- | Converts any SurelyApart to a MaybeApart
1155 don'tBeSoSure :: UM () -> UM ()
1156 don'tBeSoSure um = UM $ \ state ->
1157 case unUM um state of
1158 SurelyApart -> MaybeApart (state, ())
1159 other -> other
1160
1161 checkRnEnvR :: UMEnv -> Type -> UM ()
1162 checkRnEnvR env ty = checkRnEnv rnEnvR env (tyCoVarsOfType ty)
1163
1164 checkRnEnvL :: UMEnv -> Type -> UM ()
1165 checkRnEnvL env ty = checkRnEnv rnEnvL env (tyCoVarsOfType ty)
1166
1167 checkRnEnvRCo :: UMEnv -> Coercion -> UM ()
1168 checkRnEnvRCo env co = checkRnEnv rnEnvR env (tyCoVarsOfCo co)
1169
1170 umRnOccL :: UMEnv -> TyVar -> TyVar
1171 umRnOccL env v = rnOccL (um_rn_env env) v
1172
1173 umRnOccR :: UMEnv -> TyVar -> TyVar
1174 umRnOccR env v = rnOccR (um_rn_env env) v
1175
1176 umSwapRn :: UMEnv -> UMEnv
1177 umSwapRn env = env { um_rn_env = rnSwap (um_rn_env env) }
1178
1179 maybeApart :: UM ()
1180 maybeApart = UM (\state -> MaybeApart (state, ()))
1181
1182 surelyApart :: UM a
1183 surelyApart = UM (\_ -> SurelyApart)
1184
1185 {-
1186 %************************************************************************
1187 %* *
1188 Matching a (lifted) type against a coercion
1189 %* *
1190 %************************************************************************
1191
1192 This section defines essentially an inverse to liftCoSubst. It is defined
1193 here to avoid a dependency from Coercion on this module.
1194
1195 -}
1196
1197 data MatchEnv = ME { me_tmpls :: TyVarSet
1198 , me_env :: RnEnv2 }
1199
1200 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
1201 -- @liftCoMatch vars ty co == Just s@, then @listCoSubst s ty == co@,
1202 -- where @==@ there means that the result of 'liftCoSubst' has the same
1203 -- type as the original co; but may be different under the hood.
1204 -- That is, it matches a type against a coercion of the same
1205 -- "shape", and returns a lifting substitution which could have been
1206 -- used to produce the given coercion from the given type.
1207 -- Note that this function is incomplete -- it might return Nothing
1208 -- when there does indeed exist a possible lifting context.
1209 --
1210 -- This function is incomplete in that it doesn't respect the equality
1211 -- in `eqType`. That is, it's possible that this will succeed for t1 and
1212 -- fail for t2, even when t1 `eqType` t2. That's because it depends on
1213 -- there being a very similar structure between the type and the coercion.
1214 -- This incompleteness shouldn't be all that surprising, especially because
1215 -- it depends on the structure of the coercion, which is a silly thing to do.
1216 --
1217 -- The lifting context produced doesn't have to be exacting in the roles
1218 -- of the mappings. This is because any use of the lifting context will
1219 -- also require a desired role. Thus, this algorithm prefers mapping to
1220 -- nominal coercions where it can do so.
1221 liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
1222 liftCoMatch tmpls ty co
1223 = do { cenv1 <- ty_co_match menv emptyVarEnv ki ki_co ki_ki_co ki_ki_co
1224 ; cenv2 <- ty_co_match menv cenv1 ty co
1225 (mkNomReflCo co_lkind) (mkNomReflCo co_rkind)
1226 ; return (LC (mkEmptyTCvSubst in_scope) cenv2) }
1227 where
1228 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
1229 in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
1230 -- Like tcMatchTy, assume all the interesting variables
1231 -- in ty are in tmpls
1232
1233 ki = typeKind ty
1234 ki_co = promoteCoercion co
1235 ki_ki_co = mkNomReflCo liftedTypeKind
1236
1237 Pair co_lkind co_rkind = coercionKind ki_co
1238
1239 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
1240 ty_co_match :: MatchEnv -- ^ ambient helpful info
1241 -> LiftCoEnv -- ^ incoming subst
1242 -> Type -- ^ ty, type to match
1243 -> Coercion -- ^ co, coercion to match against
1244 -> Coercion -- ^ :: kind of L type of substed ty ~N L kind of co
1245 -> Coercion -- ^ :: kind of R type of substed ty ~N R kind of co
1246 -> Maybe LiftCoEnv
1247 ty_co_match menv subst ty co lkco rkco
1248 | Just ty' <- coreView ty = ty_co_match menv subst ty' co lkco rkco
1249
1250 -- handle Refl case:
1251 | tyCoVarsOfType ty `isNotInDomainOf` subst
1252 , Just (ty', _) <- isReflCo_maybe co
1253 , ty `eqType` ty'
1254 = Just subst
1255
1256 where
1257 isNotInDomainOf :: VarSet -> VarEnv a -> Bool
1258 isNotInDomainOf set env
1259 = noneSet (\v -> elemVarEnv v env) set
1260
1261 noneSet :: (Var -> Bool) -> VarSet -> Bool
1262 noneSet f = allVarSet (not . f)
1263
1264 ty_co_match menv subst ty co lkco rkco
1265 | CastTy ty' co' <- ty
1266 = ty_co_match menv subst ty' co (co' `mkTransCo` lkco) (co' `mkTransCo` rkco)
1267
1268 | CoherenceCo co1 co2 <- co
1269 = ty_co_match menv subst ty co1 (lkco `mkTransCo` mkSymCo co2) rkco
1270
1271 | SymCo co' <- co
1272 = swapLiftCoEnv <$> ty_co_match menv (swapLiftCoEnv subst) ty co' rkco lkco
1273
1274 -- Match a type variable against a non-refl coercion
1275 ty_co_match menv subst (TyVarTy tv1) co lkco rkco
1276 | Just co1' <- lookupVarEnv subst tv1' -- tv1' is already bound to co1
1277 = if eqCoercionX (nukeRnEnvL rn_env) co1' co
1278 then Just subst
1279 else Nothing -- no match since tv1 matches two different coercions
1280
1281 | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
1282 = if any (inRnEnvR rn_env) (tyCoVarsOfCoList co)
1283 then Nothing -- occurs check failed
1284 else Just $ extendVarEnv subst tv1' $
1285 castCoercionKind co (mkSymCo lkco) (mkSymCo rkco)
1286
1287 | otherwise
1288 = Nothing
1289
1290 where
1291 rn_env = me_env menv
1292 tv1' = rnOccL rn_env tv1
1293
1294 -- just look through SubCo's. We don't really care about roles here.
1295 ty_co_match menv subst ty (SubCo co) lkco rkco
1296 = ty_co_match menv subst ty co lkco rkco
1297
1298 ty_co_match menv subst (AppTy ty1a ty1b) co _lkco _rkco
1299 | Just (co2, arg2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy
1300 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1301 ty_co_match menv subst ty1 (AppCo co2 arg2) _lkco _rkco
1302 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
1303 -- yes, the one from Type, not TcType; this is for coercion optimization
1304 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1305
1306 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos) _lkco _rkco
1307 = ty_co_match_tc menv subst tc1 tys tc2 cos
1308 ty_co_match menv subst (FunTy ty1 ty2) co _lkco _rkco
1309 -- Despite the fact that (->) is polymorphic in four type variables (two
1310 -- runtime rep and two types), we shouldn't need to explicitly unify the
1311 -- runtime reps here; unifying the types themselves should be sufficient.
1312 -- See Note [Representation of function types].
1313 | Just (tc, [_,_,co1,co2]) <- splitTyConAppCo_maybe co
1314 , tc == funTyCon
1315 = let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) [co1,co2]
1316 in ty_co_match_args menv subst [ty1, ty2] [co1, co2] lkcos rkcos
1317
1318 ty_co_match menv subst (ForAllTy (TvBndr tv1 _) ty1)
1319 (ForAllCo tv2 kind_co2 co2)
1320 lkco rkco
1321 = do { subst1 <- ty_co_match menv subst (tyVarKind tv1) kind_co2
1322 ki_ki_co ki_ki_co
1323 ; let rn_env0 = me_env menv
1324 rn_env1 = rnBndr2 rn_env0 tv1 tv2
1325 menv' = menv { me_env = rn_env1 }
1326 ; ty_co_match menv' subst1 ty1 co2 lkco rkco }
1327 where
1328 ki_ki_co = mkNomReflCo liftedTypeKind
1329
1330 ty_co_match _ subst (CoercionTy {}) _ _ _
1331 = Just subst -- don't inspect coercions
1332
1333 ty_co_match menv subst ty co lkco rkco
1334 | Just co' <- pushRefl co = ty_co_match menv subst ty co' lkco rkco
1335 | otherwise = Nothing
1336
1337 ty_co_match_tc :: MatchEnv -> LiftCoEnv
1338 -> TyCon -> [Type]
1339 -> TyCon -> [Coercion]
1340 -> Maybe LiftCoEnv
1341 ty_co_match_tc menv subst tc1 tys1 tc2 cos2
1342 = do { guard (tc1 == tc2)
1343 ; ty_co_match_args menv subst tys1 cos2 lkcos rkcos }
1344 where
1345 Pair lkcos rkcos
1346 = traverse (fmap mkNomReflCo . coercionKind) cos2
1347
1348 ty_co_match_app :: MatchEnv -> LiftCoEnv
1349 -> Type -> [Type] -> Coercion -> [Coercion]
1350 -> Maybe LiftCoEnv
1351 ty_co_match_app menv subst ty1 ty1args co2 co2args
1352 | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
1353 , Just (co2', co2a) <- splitAppCo_maybe co2
1354 = ty_co_match_app menv subst ty1' (ty1a : ty1args) co2' (co2a : co2args)
1355
1356 | otherwise
1357 = do { subst1 <- ty_co_match menv subst ki1 ki2 ki_ki_co ki_ki_co
1358 ; let Pair lkco rkco = mkNomReflCo <$> coercionKind ki2
1359 ; subst2 <- ty_co_match menv subst1 ty1 co2 lkco rkco
1360 ; let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) co2args
1361 ; ty_co_match_args menv subst2 ty1args co2args lkcos rkcos }
1362 where
1363 ki1 = typeKind ty1
1364 ki2 = promoteCoercion co2
1365 ki_ki_co = mkNomReflCo liftedTypeKind
1366
1367 ty_co_match_args :: MatchEnv -> LiftCoEnv -> [Type]
1368 -> [Coercion] -> [Coercion] -> [Coercion]
1369 -> Maybe LiftCoEnv
1370 ty_co_match_args _ subst [] [] _ _ = Just subst
1371 ty_co_match_args menv subst (ty:tys) (arg:args) (lkco:lkcos) (rkco:rkcos)
1372 = do { subst' <- ty_co_match menv subst ty arg lkco rkco
1373 ; ty_co_match_args menv subst' tys args lkcos rkcos }
1374 ty_co_match_args _ _ _ _ _ _ = Nothing
1375
1376 pushRefl :: Coercion -> Maybe Coercion
1377 pushRefl (Refl Nominal (AppTy ty1 ty2))
1378 = Just (AppCo (Refl Nominal ty1) (mkNomReflCo ty2))
1379 pushRefl (Refl r (FunTy ty1 ty2))
1380 | Just rep1 <- getRuntimeRep_maybe ty1
1381 , Just rep2 <- getRuntimeRep_maybe ty2
1382 = Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2
1383 , mkReflCo r ty1, mkReflCo r ty2 ])
1384 pushRefl (Refl r (TyConApp tc tys))
1385 = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
1386 pushRefl (Refl r (ForAllTy (TvBndr tv _) ty))
1387 = Just (mkHomoForAllCos_NoRefl [tv] (Refl r ty))
1388 -- NB: NoRefl variant. Otherwise, we get a loop!
1389 pushRefl (Refl r (CastTy ty co)) = Just (castCoercionKind (Refl r ty) co co)
1390 pushRefl _ = Nothing