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