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