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