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