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