never executed always true always false
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE ScopedTypeVariables, PatternSynonyms #-}
4
5 {-# LANGUAGE DeriveFunctor, DeriveDataTypeable #-}
6
7 module GHC.Core.Unify (
8 tcMatchTy, tcMatchTyKi,
9 tcMatchTys, tcMatchTyKis,
10 tcMatchTyX, tcMatchTysX, tcMatchTyKisX,
11 tcMatchTyX_BM, ruleMatchTyKiX,
12
13 -- * Rough matching
14 RoughMatchTc(..), roughMatchTcs, instanceCantMatch,
15 typesCantMatch, isRoughOtherTc,
16
17 -- Side-effect free unification
18 tcUnifyTy, tcUnifyTyKi, tcUnifyTys, tcUnifyTyKis,
19 tcUnifyTysFG, tcUnifyTyWithTFs,
20 BindFun, BindFlag(..), matchBindFun, alwaysBindFun,
21 UnifyResult, UnifyResultM(..), MaybeApartReason(..),
22
23 -- Matching a type against a lifted type (coercion)
24 liftCoMatch,
25
26 -- The core flattening algorithm
27 flattenTys, flattenTysX
28 ) where
29
30 import GHC.Prelude
31
32 import GHC.Types.Var
33 import GHC.Types.Var.Env
34 import GHC.Types.Var.Set
35 import GHC.Types.Name( Name, mkSysTvName, mkSystemVarName )
36 import GHC.Core.Type hiding ( getTvSubstEnv )
37 import GHC.Core.Coercion hiding ( getCvSubstEnv )
38 import GHC.Core.TyCon
39 import GHC.Core.TyCo.Rep
40 import GHC.Core.TyCo.FVs ( tyCoVarsOfCoList, tyCoFVsOfTypes )
41 import GHC.Core.TyCo.Subst ( mkTvSubst )
42 import GHC.Core.Map.Type
43 import GHC.Utils.FV( FV, fvVarSet, fvVarList )
44 import GHC.Utils.Misc
45 import GHC.Data.Pair
46 import GHC.Utils.Outputable
47 import GHC.Types.Unique
48 import GHC.Types.Unique.FM
49 import GHC.Types.Unique.Set
50 import {-# SOURCE #-} GHC.Tc.Utils.TcType ( tcEqType )
51 import GHC.Exts( oneShot )
52 import GHC.Utils.Panic
53 import GHC.Utils.Panic.Plain
54 import GHC.Data.FastString
55
56 import Data.Data ( Data )
57 import Data.List ( mapAccumL )
58 import Control.Monad
59 import qualified Data.Semigroup as S
60
61 {-
62
63 Unification is much tricker than you might think.
64
65 1. The substitution we generate binds the *template type variables*
66 which are given to us explicitly.
67
68 2. We want to match in the presence of foralls;
69 e.g (forall a. t1) ~ (forall b. t2)
70
71 That is what the RnEnv2 is for; it does the alpha-renaming
72 that makes it as if a and b were the same variable.
73 Initialising the RnEnv2, so that it can generate a fresh
74 binder when necessary, entails knowing the free variables of
75 both types.
76
77 3. We must be careful not to bind a template type variable to a
78 locally bound variable. E.g.
79 (forall a. x) ~ (forall b. b)
80 where x is the template type variable. Then we do not want to
81 bind x to a/b! This is a kind of occurs check.
82 The necessary locals accumulate in the RnEnv2.
83
84 Note [tcMatchTy vs tcMatchTyKi]
85 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
86 This module offers two variants of matching: with kinds and without.
87 The TyKi variant takes two types, of potentially different kinds,
88 and matches them. Along the way, it necessarily also matches their
89 kinds. The Ty variant instead assumes that the kinds are already
90 eqType and so skips matching up the kinds.
91
92 How do you choose between them?
93
94 1. If you know that the kinds of the two types are eqType, use
95 the Ty variant. It is more efficient, as it does less work.
96
97 2. If the kinds of variables in the template type might mention type families,
98 use the Ty variant (and do other work to make sure the kinds
99 work out). These pure unification functions do a straightforward
100 syntactic unification and do no complex reasoning about type
101 families. Note that the types of the variables in instances can indeed
102 mention type families, so instance lookup must use the Ty variant.
103
104 (Nothing goes terribly wrong -- no panics -- if there might be type
105 families in kinds in the TyKi variant. You just might get match
106 failure even though a reducing a type family would lead to success.)
107
108 3. Otherwise, if you're sure that the variable kinds do not mention
109 type families and you're not already sure that the kind of the template
110 equals the kind of the target, then use the TyKi version.
111 -}
112
113 -- | Some unification functions are parameterised by a 'BindFun', which
114 -- says whether or not to allow a certain unification to take place.
115 -- A 'BindFun' takes the 'TyVar' involved along with the 'Type' it will
116 -- potentially be bound to.
117 --
118 -- It is possible for the variable to actually be a coercion variable
119 -- (Note [Matching coercion variables]), but only when one-way matching.
120 -- In this case, the 'Type' will be a 'CoercionTy'.
121 type BindFun = TyCoVar -> Type -> BindFlag
122
123 -- | @tcMatchTy t1 t2@ produces a substitution (over fvs(t1))
124 -- @s@ such that @s(t1)@ equals @t2@.
125 -- The returned substitution might bind coercion variables,
126 -- if the variable is an argument to a GADT constructor.
127 --
128 -- Precondition: typeKind ty1 `eqType` typeKind ty2
129 --
130 -- We don't pass in a set of "template variables" to be bound
131 -- by the match, because tcMatchTy (and similar functions) are
132 -- always used on top-level types, so we can bind any of the
133 -- free variables of the LHS.
134 -- See also Note [tcMatchTy vs tcMatchTyKi]
135 tcMatchTy :: Type -> Type -> Maybe TCvSubst
136 tcMatchTy ty1 ty2 = tcMatchTys [ty1] [ty2]
137
138 tcMatchTyX_BM :: BindFun -> TCvSubst
139 -> Type -> Type -> Maybe TCvSubst
140 tcMatchTyX_BM bind_me subst ty1 ty2
141 = tc_match_tys_x bind_me False subst [ty1] [ty2]
142
143 -- | Like 'tcMatchTy', but allows the kinds of the types to differ,
144 -- and thus matches them as well.
145 -- See also Note [tcMatchTy vs tcMatchTyKi]
146 tcMatchTyKi :: Type -> Type -> Maybe TCvSubst
147 tcMatchTyKi ty1 ty2
148 = tc_match_tys alwaysBindFun True [ty1] [ty2]
149
150 -- | This is similar to 'tcMatchTy', but extends a substitution
151 -- See also Note [tcMatchTy vs tcMatchTyKi]
152 tcMatchTyX :: TCvSubst -- ^ Substitution to extend
153 -> Type -- ^ Template
154 -> Type -- ^ Target
155 -> Maybe TCvSubst
156 tcMatchTyX subst ty1 ty2
157 = tc_match_tys_x alwaysBindFun False subst [ty1] [ty2]
158
159 -- | Like 'tcMatchTy' but over a list of types.
160 -- See also Note [tcMatchTy vs tcMatchTyKi]
161 tcMatchTys :: [Type] -- ^ Template
162 -> [Type] -- ^ Target
163 -> Maybe TCvSubst -- ^ One-shot; in principle the template
164 -- variables could be free in the target
165 tcMatchTys tys1 tys2
166 = tc_match_tys alwaysBindFun False tys1 tys2
167
168 -- | Like 'tcMatchTyKi' but over a list of types.
169 -- See also Note [tcMatchTy vs tcMatchTyKi]
170 tcMatchTyKis :: [Type] -- ^ Template
171 -> [Type] -- ^ Target
172 -> Maybe TCvSubst -- ^ One-shot substitution
173 tcMatchTyKis tys1 tys2
174 = tc_match_tys alwaysBindFun True tys1 tys2
175
176 -- | Like 'tcMatchTys', but extending a substitution
177 -- See also Note [tcMatchTy vs tcMatchTyKi]
178 tcMatchTysX :: TCvSubst -- ^ Substitution to extend
179 -> [Type] -- ^ Template
180 -> [Type] -- ^ Target
181 -> Maybe TCvSubst -- ^ One-shot substitution
182 tcMatchTysX subst tys1 tys2
183 = tc_match_tys_x alwaysBindFun False subst tys1 tys2
184
185 -- | Like 'tcMatchTyKis', but extending a substitution
186 -- See also Note [tcMatchTy vs tcMatchTyKi]
187 tcMatchTyKisX :: TCvSubst -- ^ Substitution to extend
188 -> [Type] -- ^ Template
189 -> [Type] -- ^ Target
190 -> Maybe TCvSubst -- ^ One-shot substitution
191 tcMatchTyKisX subst tys1 tys2
192 = tc_match_tys_x alwaysBindFun True subst tys1 tys2
193
194 -- | Same as tc_match_tys_x, but starts with an empty substitution
195 tc_match_tys :: BindFun
196 -> Bool -- ^ match kinds?
197 -> [Type]
198 -> [Type]
199 -> Maybe TCvSubst
200 tc_match_tys bind_me match_kis tys1 tys2
201 = tc_match_tys_x bind_me match_kis (mkEmptyTCvSubst in_scope) tys1 tys2
202 where
203 in_scope = mkInScopeSet (tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2)
204
205 -- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX'
206 tc_match_tys_x :: BindFun
207 -> Bool -- ^ match kinds?
208 -> TCvSubst
209 -> [Type]
210 -> [Type]
211 -> Maybe TCvSubst
212 tc_match_tys_x bind_me match_kis (TCvSubst in_scope tv_env cv_env) tys1 tys2
213 = case tc_unify_tys bind_me
214 False -- Matching, not unifying
215 False -- Not an injectivity check
216 match_kis
217 (mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of
218 Unifiable (tv_env', cv_env')
219 -> Just $ TCvSubst in_scope tv_env' cv_env'
220 _ -> Nothing
221
222 -- | This one is called from the expression matcher,
223 -- which already has a MatchEnv in hand
224 ruleMatchTyKiX
225 :: TyCoVarSet -- ^ template variables
226 -> RnEnv2
227 -> TvSubstEnv -- ^ type substitution to extend
228 -> Type -- ^ Template
229 -> Type -- ^ Target
230 -> Maybe TvSubstEnv
231 ruleMatchTyKiX tmpl_tvs rn_env tenv tmpl target
232 -- See Note [Kind coercions in Unify]
233 = case tc_unify_tys (matchBindFun tmpl_tvs) False False
234 True -- <-- this means to match the kinds
235 rn_env tenv emptyCvSubstEnv [tmpl] [target] of
236 Unifiable (tenv', _) -> Just tenv'
237 _ -> Nothing
238
239 -- | Allow binding only for any variable in the set. Variables may
240 -- be bound to any type.
241 -- Used when doing simple matching; e.g. can we find a substitution
242 --
243 -- @
244 -- S = [a :-> t1, b :-> t2] such that
245 -- S( Maybe (a, b->Int ) = Maybe (Bool, Char -> Int)
246 -- @
247 matchBindFun :: TyCoVarSet -> BindFun
248 matchBindFun tvs tv _ty
249 | tv `elemVarSet` tvs = BindMe
250 | otherwise = Apart
251
252 -- | Allow the binding of any variable to any type
253 alwaysBindFun :: BindFun
254 alwaysBindFun _tv _ty = BindMe
255
256 {- *********************************************************************
257 * *
258 Rough matching
259 * *
260 ********************************************************************* -}
261
262 {- Note [Rough matching in class and family instances]
263 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
264 Consider
265 instance C (Maybe [Tree a]) Bool
266 and suppose we are looking up
267 C Bool Bool
268
269 We can very quickly rule the instance out, because the first
270 argument is headed by Maybe, whereas in the constraint we are looking
271 up has first argument headed by Bool. These "headed by" TyCons are
272 called the "rough match TyCons" of the constraint or instance.
273 They are used for a quick filter, to check when an instance cannot
274 possibly match.
275
276 The main motivation is to avoid sucking in whole instance
277 declarations that are utterly useless. See GHC.Core.InstEnv
278 Note [ClsInst laziness and the rough-match fields].
279
280 INVARIANT: a rough-match TyCons `tc` is always a real, generative tycon,
281 like Maybe or Either, including a newtype or a data family, both of
282 which are generative. It replies True to `isGenerativeTyCon tc Nominal`.
283
284 But it is never
285 - A type synonym
286 E.g. Int and (S Bool) might match
287 if (S Bool) is a synonym for Int
288
289 - A type family (#19336)
290 E.g. (Just a) and (F a) might match if (F a) reduces to (Just a)
291 albeit perhaps only after 'a' is instantiated.
292 -}
293
294 data RoughMatchTc
295 = KnownTc Name -- INVARIANT: Name refers to a TyCon tc that responds
296 -- true to `isGenerativeTyCon tc Nominal`. See
297 -- Note [Rough matching in class and family instances]
298 | OtherTc -- e.g. type variable at the head
299 deriving( Data )
300
301 isRoughOtherTc :: RoughMatchTc -> Bool
302 isRoughOtherTc OtherTc = True
303 isRoughOtherTc (KnownTc {}) = False
304
305 roughMatchTcs :: [Type] -> [RoughMatchTc]
306 roughMatchTcs tys = map rough tys
307 where
308 rough ty
309 | Just (ty', _) <- splitCastTy_maybe ty = rough ty'
310 | Just (tc,_) <- splitTyConApp_maybe ty
311 , not (isTypeFamilyTyCon tc) = assertPpr (isGenerativeTyCon tc Nominal) (ppr tc) $
312 KnownTc (tyConName tc)
313 -- See Note [Rough matching in class and family instances]
314 | otherwise = OtherTc
315
316 instanceCantMatch :: [RoughMatchTc] -> [RoughMatchTc] -> Bool
317 -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot
318 -- possibly be instantiated to actual, nor vice versa;
319 -- False is non-committal
320 instanceCantMatch (mt : ts) (ma : as) = itemCantMatch mt ma || instanceCantMatch ts as
321 instanceCantMatch _ _ = False -- Safe
322
323 itemCantMatch :: RoughMatchTc -> RoughMatchTc -> Bool
324 itemCantMatch (KnownTc t) (KnownTc a) = t /= a
325 itemCantMatch _ _ = False
326
327
328 {-
329 ************************************************************************
330 * *
331 GADTs
332 * *
333 ************************************************************************
334
335 Note [Pruning dead case alternatives]
336 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
337 Consider data T a where
338 T1 :: T Int
339 T2 :: T a
340
341 newtype X = MkX Int
342 newtype Y = MkY Char
343
344 type family F a
345 type instance F Bool = Int
346
347 Now consider case x of { T1 -> e1; T2 -> e2 }
348
349 The question before the house is this: if I know something about the type
350 of x, can I prune away the T1 alternative?
351
352 Suppose x::T Char. It's impossible to construct a (T Char) using T1,
353 Answer = YES we can prune the T1 branch (clearly)
354
355 Suppose x::T (F a), where 'a' is in scope. Then 'a' might be instantiated
356 to 'Bool', in which case x::T Int, so
357 ANSWER = NO (clearly)
358
359 We see here that we want precisely the apartness check implemented within
360 tcUnifyTysFG. So that's what we do! Two types cannot match if they are surely
361 apart. Note that since we are simply dropping dead code, a conservative test
362 suffices.
363 -}
364
365 -- | Given a list of pairs of types, are any two members of a pair surely
366 -- apart, even after arbitrary type function evaluation and substitution?
367 typesCantMatch :: [(Type,Type)] -> Bool
368 -- See Note [Pruning dead case alternatives]
369 typesCantMatch prs = any (uncurry cant_match) prs
370 where
371 cant_match :: Type -> Type -> Bool
372 cant_match t1 t2 = case tcUnifyTysFG alwaysBindFun [t1] [t2] of
373 SurelyApart -> True
374 _ -> False
375
376 {-
377 ************************************************************************
378 * *
379 Unification
380 * *
381 ************************************************************************
382
383 Note [Fine-grained unification]
384 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
385 Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
386 no substitution to finite types makes these match. But, a substitution to
387 *infinite* types can unify these two types: [x |-> [[[...]]], y |-> [[[...]]] ].
388 Why do we care? Consider these two type family instances:
389
390 type instance F x x = Int
391 type instance F [y] y = Bool
392
393 If we also have
394
395 type instance Looper = [Looper]
396
397 then the instances potentially overlap. The solution is to use unification
398 over infinite terms. This is possible (see [1] for lots of gory details), but
399 a full algorithm is a little more power than we need. Instead, we make a
400 conservative approximation and just omit the occurs check.
401
402 [1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
403
404 tcUnifyTys considers an occurs-check problem as the same as general unification
405 failure.
406
407 tcUnifyTysFG ("fine-grained") returns one of three results: success, occurs-check
408 failure ("MaybeApart"), or general failure ("SurelyApart").
409
410 See also #8162.
411
412 It's worth noting that unification in the presence of infinite types is not
413 complete. This means that, sometimes, a closed type family does not reduce
414 when it should. See test case indexed-types/should_fail/Overlap15 for an
415 example.
416
417 Note [Unificiation result]
418 ~~~~~~~~~~~~~~~~~~~~~~~~~~
419 When unifying t1 ~ t2, we return
420 * Unifiable s, if s is a substitution such that s(t1) is syntactically the
421 same as s(t2), modulo type-synonym expansion.
422 * SurelyApart, if there is no substitution s such that s(t1) = s(t2),
423 where "=" includes type-family reductions.
424 * MaybeApart mar s, when we aren't sure. `mar` is a MaybeApartReason.
425
426 Examples
427 * [a] ~ Maybe b: SurelyApart, because [] and Maybe can't unify
428 * [(a,Int)] ~ [(Bool,b)]: Unifiable
429 * [F Int] ~ [Bool]: MaybeApart MARTypeFamily, because F Int might reduce to Bool (the unifier
430 does not try this)
431 * a ~ Maybe a: MaybeApart MARInfinite. Not Unifiable clearly, but not SurelyApart either; consider
432 a := Loop
433 where type family Loop where Loop = Maybe Loop
434
435 There is the possibility that two types are MaybeApart for *both* reasons:
436
437 * (a, F Int) ~ (Maybe a, Bool)
438
439 What reason should we use? The *only* consumer of the reason is described
440 in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv. The goal
441 there is identify which instances might match a target later (but don't
442 match now) -- except that we want to ignore the possibility of infinitary
443 substitutions. So let's examine a concrete scenario:
444
445 class C a b c
446 instance C a (Maybe a) Bool
447 -- other instances, including one that will actually match
448 [W] C b b (F Int)
449
450 Do we want the instance as a future possibility? No. The only way that
451 instance can match is in the presence of an infinite type (infinitely
452 nested Maybes). We thus say that MARInfinite takes precedence, so that
453 InstEnv treats this case as an infinitary substitution case; the fact
454 that a type family is involved is only incidental. We thus define
455 the Semigroup instance for MaybeApartReason to prefer MARInfinite.
456
457 Note [The substitution in MaybeApart]
458 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
459 The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why?
460 Because consider unifying these:
461
462 (a, a, Int) ~ (b, [b], Bool)
463
464 If we go left-to-right, we start with [a |-> b]. Then, on the middle terms, we
465 apply the subst we have so far and discover that we need [b |-> [b]]. Because
466 this fails the occurs check, we say that the types are MaybeApart (see above
467 Note [Fine-grained unification]). But, we can't stop there! Because if we
468 continue, we discover that Int is SurelyApart from Bool, and therefore the
469 types are apart. This has practical consequences for the ability for closed
470 type family applications to reduce. See test case
471 indexed-types/should_compile/Overlap14.
472
473 -}
474
475 -- | Simple unification of two types; all type variables are bindable
476 -- Precondition: the kinds are already equal
477 tcUnifyTy :: Type -> Type -- All tyvars are bindable
478 -> Maybe TCvSubst
479 -- A regular one-shot (idempotent) substitution
480 tcUnifyTy t1 t2 = tcUnifyTys alwaysBindFun [t1] [t2]
481
482 -- | Like 'tcUnifyTy', but also unifies the kinds
483 tcUnifyTyKi :: Type -> Type -> Maybe TCvSubst
484 tcUnifyTyKi t1 t2 = tcUnifyTyKis alwaysBindFun [t1] [t2]
485
486 -- | Unify two types, treating type family applications as possibly unifying
487 -- with anything and looking through injective type family applications.
488 -- Precondition: kinds are the same
489 tcUnifyTyWithTFs :: Bool -- ^ True <=> do two-way unification;
490 -- False <=> do one-way matching.
491 -- See end of sec 5.2 from the paper
492 -> Type -> Type -> Maybe TCvSubst
493 -- This algorithm is an implementation of the "Algorithm U" presented in
494 -- the paper "Injective type families for Haskell", Figures 2 and 3.
495 -- The code is incorporated with the standard unifier for convenience, but
496 -- its operation should match the specification in the paper.
497 tcUnifyTyWithTFs twoWay t1 t2
498 = case tc_unify_tys alwaysBindFun twoWay True False
499 rn_env emptyTvSubstEnv emptyCvSubstEnv
500 [t1] [t2] of
501 Unifiable (subst, _) -> Just $ maybe_fix subst
502 MaybeApart _reason (subst, _) -> Just $ maybe_fix subst
503 -- we want to *succeed* in questionable cases. This is a
504 -- pre-unification algorithm.
505 SurelyApart -> Nothing
506 where
507 in_scope = mkInScopeSet $ tyCoVarsOfTypes [t1, t2]
508 rn_env = mkRnEnv2 in_scope
509
510 maybe_fix | twoWay = niFixTCvSubst
511 | otherwise = mkTvSubst in_scope -- when matching, don't confuse
512 -- domain with range
513
514 -----------------
515 tcUnifyTys :: BindFun
516 -> [Type] -> [Type]
517 -> Maybe TCvSubst
518 -- ^ A regular one-shot (idempotent) substitution
519 -- that unifies the erased types. See comments
520 -- for 'tcUnifyTysFG'
521
522 -- The two types may have common type variables, and indeed do so in the
523 -- second call to tcUnifyTys in GHC.Tc.Instance.FunDeps.checkClsFD
524 tcUnifyTys bind_fn tys1 tys2
525 = case tcUnifyTysFG bind_fn tys1 tys2 of
526 Unifiable result -> Just result
527 _ -> Nothing
528
529 -- | Like 'tcUnifyTys' but also unifies the kinds
530 tcUnifyTyKis :: BindFun
531 -> [Type] -> [Type]
532 -> Maybe TCvSubst
533 tcUnifyTyKis bind_fn tys1 tys2
534 = case tcUnifyTyKisFG bind_fn tys1 tys2 of
535 Unifiable result -> Just result
536 _ -> Nothing
537
538 -- This type does double-duty. It is used in the UM (unifier monad) and to
539 -- return the final result. See Note [Fine-grained unification]
540 type UnifyResult = UnifyResultM TCvSubst
541
542 -- | See Note [Unificiation result]
543 data UnifyResultM a = Unifiable a -- the subst that unifies the types
544 | MaybeApart MaybeApartReason
545 a -- the subst has as much as we know
546 -- it must be part of a most general unifier
547 -- See Note [The substitution in MaybeApart]
548 | SurelyApart
549 deriving Functor
550
551 -- | Why are two types 'MaybeApart'? 'MARTypeFamily' takes precedence:
552 -- This is used (only) in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv
553 data MaybeApartReason = MARTypeFamily -- ^ matching e.g. F Int ~? Bool
554 | MARInfinite -- ^ matching e.g. a ~? Maybe a
555
556 instance Outputable MaybeApartReason where
557 ppr MARTypeFamily = text "MARTypeFamily"
558 ppr MARInfinite = text "MARInfinite"
559
560 instance Semigroup MaybeApartReason where
561 -- see end of Note [Unification result] for why
562 MARTypeFamily <> r = r
563 MARInfinite <> _ = MARInfinite
564
565 instance Applicative UnifyResultM where
566 pure = Unifiable
567 (<*>) = ap
568
569 instance Monad UnifyResultM where
570 SurelyApart >>= _ = SurelyApart
571 MaybeApart r1 x >>= f = case f x of
572 Unifiable y -> MaybeApart r1 y
573 MaybeApart r2 y -> MaybeApart (r1 S.<> r2) y
574 SurelyApart -> SurelyApart
575 Unifiable x >>= f = f x
576
577 -- | @tcUnifyTysFG bind_tv tys1 tys2@ attempts to find a substitution @s@ (whose
578 -- domain elements all respond 'BindMe' to @bind_tv@) such that
579 -- @s(tys1)@ and that of @s(tys2)@ are equal, as witnessed by the returned
580 -- Coercions. This version requires that the kinds of the types are the same,
581 -- if you unify left-to-right.
582 tcUnifyTysFG :: BindFun
583 -> [Type] -> [Type]
584 -> UnifyResult
585 tcUnifyTysFG bind_fn tys1 tys2
586 = tc_unify_tys_fg False bind_fn tys1 tys2
587
588 tcUnifyTyKisFG :: BindFun
589 -> [Type] -> [Type]
590 -> UnifyResult
591 tcUnifyTyKisFG bind_fn tys1 tys2
592 = tc_unify_tys_fg True bind_fn tys1 tys2
593
594 tc_unify_tys_fg :: Bool
595 -> BindFun
596 -> [Type] -> [Type]
597 -> UnifyResult
598 tc_unify_tys_fg match_kis bind_fn tys1 tys2
599 = do { (env, _) <- tc_unify_tys bind_fn True False match_kis env
600 emptyTvSubstEnv emptyCvSubstEnv
601 tys1 tys2
602 ; return $ niFixTCvSubst env }
603 where
604 vars = tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2
605 env = mkRnEnv2 $ mkInScopeSet vars
606
607 -- | This function is actually the one to call the unifier -- a little
608 -- too general for outside clients, though.
609 tc_unify_tys :: BindFun
610 -> AmIUnifying -- ^ True <=> unify; False <=> match
611 -> Bool -- ^ True <=> doing an injectivity check
612 -> Bool -- ^ True <=> treat the kinds as well
613 -> RnEnv2
614 -> TvSubstEnv -- ^ substitution to extend
615 -> CvSubstEnv
616 -> [Type] -> [Type]
617 -> UnifyResultM (TvSubstEnv, CvSubstEnv)
618 -- NB: It's tempting to ASSERT here that, if we're not matching kinds, then
619 -- the kinds of the types should be the same. However, this doesn't work,
620 -- as the types may be a dependent telescope, where later types have kinds
621 -- that mention variables occurring earlier in the list of types. Here's an
622 -- example (from typecheck/should_fail/T12709):
623 -- template: [rep :: RuntimeRep, a :: TYPE rep]
624 -- target: [LiftedRep :: RuntimeRep, Int :: TYPE LiftedRep]
625 -- We can see that matching the first pair will make the kinds of the second
626 -- pair equal. Yet, we still don't need a separate pass to unify the kinds
627 -- of these types, so it's appropriate to use the Ty variant of unification.
628 -- See also Note [tcMatchTy vs tcMatchTyKi].
629 tc_unify_tys bind_fn unif inj_check match_kis rn_env tv_env cv_env tys1 tys2
630 = initUM tv_env cv_env $
631 do { when match_kis $
632 unify_tys env kis1 kis2
633 ; unify_tys env tys1 tys2
634 ; (,) <$> getTvSubstEnv <*> getCvSubstEnv }
635 where
636 env = UMEnv { um_bind_fun = bind_fn
637 , um_skols = emptyVarSet
638 , um_unif = unif
639 , um_inj_tf = inj_check
640 , um_rn_env = rn_env }
641
642 kis1 = map typeKind tys1
643 kis2 = map typeKind tys2
644
645 instance Outputable a => Outputable (UnifyResultM a) where
646 ppr SurelyApart = text "SurelyApart"
647 ppr (Unifiable x) = text "Unifiable" <+> ppr x
648 ppr (MaybeApart r x) = text "MaybeApart" <+> ppr r <+> ppr x
649
650 {-
651 ************************************************************************
652 * *
653 Non-idempotent substitution
654 * *
655 ************************************************************************
656
657 Note [Non-idempotent substitution]
658 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
659 During unification we use a TvSubstEnv/CvSubstEnv pair that is
660 (a) non-idempotent
661 (b) loop-free; ie repeatedly applying it yields a fixed point
662
663 Note [Finding the substitution fixpoint]
664 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
665 Finding the fixpoint of a non-idempotent substitution arising from a
666 unification is much trickier than it looks, because of kinds. Consider
667 T k (H k (f:k)) ~ T * (g:*)
668 If we unify, we get the substitution
669 [ k -> *
670 , g -> H k (f:k) ]
671 To make it idempotent we don't want to get just
672 [ k -> *
673 , g -> H * (f:k) ]
674 We also want to substitute inside f's kind, to get
675 [ k -> *
676 , g -> H k (f:*) ]
677 If we don't do this, we may apply the substitution to something,
678 and get an ill-formed type, i.e. one where typeKind will fail.
679 This happened, for example, in #9106.
680
681 It gets worse. In #14164 we wanted to take the fixpoint of
682 this substitution
683 [ xs_asV :-> F a_aY6 (z_aY7 :: a_aY6)
684 (rest_aWF :: G a_aY6 (z_aY7 :: a_aY6))
685 , a_aY6 :-> a_aXQ ]
686
687 We have to apply the substitution for a_aY6 two levels deep inside
688 the invocation of F! We don't have a function that recursively
689 applies substitutions inside the kinds of variable occurrences (and
690 probably rightly so).
691
692 So, we work as follows:
693
694 1. Start with the current substitution (which we are
695 trying to fixpoint
696 [ xs :-> F a (z :: a) (rest :: G a (z :: a))
697 , a :-> b ]
698
699 2. Take all the free vars of the range of the substitution:
700 {a, z, rest, b}
701 NB: the free variable finder closes over
702 the kinds of variable occurrences
703
704 3. If none are in the domain of the substitution, stop.
705 We have found a fixpoint.
706
707 4. Remove the variables that are bound by the substitution, leaving
708 {z, rest, b}
709
710 5. Do a topo-sort to put them in dependency order:
711 [ b :: *, z :: a, rest :: G a z ]
712
713 6. Apply the substitution left-to-right to the kinds of these
714 tyvars, extending it each time with a new binding, so we
715 finish up with
716 [ xs :-> ..as before..
717 , a :-> b
718 , b :-> b :: *
719 , z :-> z :: b
720 , rest :-> rest :: G b (z :: b) ]
721 Note that rest now has the right kind
722
723 7. Apply this extended substitution (once) to the range of
724 the /original/ substitution. (Note that we do the
725 extended substitution would go on forever if you tried
726 to find its fixpoint, because it maps z to z.)
727
728 8. And go back to step 1
729
730 In Step 6 we use the free vars from Step 2 as the initial
731 in-scope set, because all of those variables appear in the
732 range of the substitution, so they must all be in the in-scope
733 set. But NB that the type substitution engine does not look up
734 variables in the in-scope set; it is used only to ensure no
735 shadowing.
736 -}
737
738 niFixTCvSubst :: TvSubstEnv -> TCvSubst
739 -- Find the idempotent fixed point of the non-idempotent substitution
740 -- This is surprisingly tricky:
741 -- see Note [Finding the substitution fixpoint]
742 -- ToDo: use laziness instead of iteration?
743 niFixTCvSubst tenv
744 | not_fixpoint = niFixTCvSubst (mapVarEnv (substTy subst) tenv)
745 | otherwise = subst
746 where
747 range_fvs :: FV
748 range_fvs = tyCoFVsOfTypes (nonDetEltsUFM tenv)
749 -- It's OK to use nonDetEltsUFM here because the
750 -- order of range_fvs, range_tvs is immaterial
751
752 range_tvs :: [TyVar]
753 range_tvs = fvVarList range_fvs
754
755 not_fixpoint = any in_domain range_tvs
756 in_domain tv = tv `elemVarEnv` tenv
757
758 free_tvs = scopedSort (filterOut in_domain range_tvs)
759
760 -- See Note [Finding the substitution fixpoint], Step 6
761 init_in_scope = mkInScopeSet (fvVarSet range_fvs)
762 subst = foldl' add_free_tv
763 (mkTvSubst init_in_scope tenv)
764 free_tvs
765
766 add_free_tv :: TCvSubst -> TyVar -> TCvSubst
767 add_free_tv subst tv
768 = extendTvSubst subst tv (mkTyVarTy tv')
769 where
770 tv' = updateTyVarKind (substTy subst) tv
771
772 niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
773 -- Apply the non-idempotent substitution to a set of type variables,
774 -- remembering that the substitution isn't necessarily idempotent
775 -- This is used in the occurs check, before extending the substitution
776 niSubstTvSet tsubst tvs
777 = nonDetStrictFoldUniqSet (unionVarSet . get) emptyVarSet tvs
778 -- It's OK to use a non-deterministic fold here because we immediately forget
779 -- the ordering by creating a set.
780 where
781 get tv
782 | Just ty <- lookupVarEnv tsubst tv
783 = niSubstTvSet tsubst (tyCoVarsOfType ty)
784
785 | otherwise
786 = unitVarSet tv
787
788 {-
789 ************************************************************************
790 * *
791 unify_ty: the main workhorse
792 * *
793 ************************************************************************
794
795 Note [Specification of unification]
796 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
797 The pure unifier, unify_ty, defined in this module, tries to work out
798 a substitution to make two types say True to eqType. NB: eqType is
799 itself not purely syntactic; it accounts for CastTys;
800 see Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep
801
802 Unlike the "impure unifiers" in the typechecker (the eager unifier in
803 GHC.Tc.Utils.Unify, and the constraint solver itself in GHC.Tc.Solver.Canonical), the pure
804 unifier does /not/ work up to ~.
805
806 The algorithm implemented here is rather delicate, and we depend on it
807 to uphold certain properties. This is a summary of these required
808 properties.
809
810 Notation:
811 θ,φ substitutions
812 ξ type-function-free types
813 τ,σ other types
814 τ♭ type τ, flattened
815
816 ≡ eqType
817
818 (U1) Soundness.
819 If (unify τ₁ τ₂) = Unifiable θ, then θ(τ₁) ≡ θ(τ₂).
820 θ is a most general unifier for τ₁ and τ₂.
821
822 (U2) Completeness.
823 If (unify ξ₁ ξ₂) = SurelyApart,
824 then there exists no substitution θ such that θ(ξ₁) ≡ θ(ξ₂).
825
826 These two properties are stated as Property 11 in the "Closed Type Families"
827 paper (POPL'14). Below, this paper is called [CTF].
828
829 (U3) Apartness under substitution.
830 If (unify ξ τ♭) = SurelyApart, then (unify ξ θ(τ)♭) = SurelyApart,
831 for any θ. (Property 12 from [CTF])
832
833 (U4) Apart types do not unify.
834 If (unify ξ τ♭) = SurelyApart, then there exists no θ
835 such that θ(ξ) = θ(τ). (Property 13 from [CTF])
836
837 THEOREM. Completeness w.r.t ~
838 If (unify τ₁♭ τ₂♭) = SurelyApart,
839 then there exists no proof that (τ₁ ~ τ₂).
840
841 PROOF. See appendix of [CTF].
842
843
844 The unification algorithm is used for type family injectivity, as described
845 in the "Injective Type Families" paper (Haskell'15), called [ITF]. When run
846 in this mode, it has the following properties.
847
848 (I1) If (unify σ τ) = SurelyApart, then σ and τ are not unifiable, even
849 after arbitrary type family reductions. Note that σ and τ are
850 not flattened here.
851
852 (I2) If (unify σ τ) = MaybeApart θ, and if some
853 φ exists such that φ(σ) ~ φ(τ), then φ extends θ.
854
855
856 Furthermore, the RULES matching algorithm requires this property,
857 but only when using this algorithm for matching:
858
859 (M1) If (match σ τ) succeeds with θ, then all matchable tyvars
860 in σ are bound in θ.
861
862 Property M1 means that we must extend the substitution with,
863 say (a ↦ a) when appropriate during matching.
864 See also Note [Self-substitution when matching].
865
866 (M2) Completeness of matching.
867 If θ(σ) = τ, then (match σ τ) = Unifiable φ,
868 where θ is an extension of φ.
869
870 Sadly, property M2 and I2 conflict. Consider
871
872 type family F1 a b where
873 F1 Int Bool = Char
874 F1 Double String = Char
875
876 Consider now two matching problems:
877
878 P1. match (F1 a Bool) (F1 Int Bool)
879 P2. match (F1 a Bool) (F1 Double String)
880
881 In case P1, we must find (a ↦ Int) to satisfy M2.
882 In case P2, we must /not/ find (a ↦ Double), in order to satisfy I2. (Note
883 that the correct mapping for I2 is (a ↦ Int). There is no way to discover
884 this, but we mustn't map a to anything else!)
885
886 We thus must parameterize the algorithm over whether it's being used
887 for an injectivity check (refrain from looking at non-injective arguments
888 to type families) or not (do indeed look at those arguments). This is
889 implemented by the um_inj_tf field of UMEnv.
890
891 (It's all a question of whether or not to include equation (7) from Fig. 2
892 of [ITF].)
893
894 This extra parameter is a bit fiddly, perhaps, but seemingly less so than
895 having two separate, almost-identical algorithms.
896
897 Note [Self-substitution when matching]
898 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
899 What should happen when we're *matching* (not unifying) a1 with a1? We
900 should get a substitution [a1 |-> a1]. A successful match should map all
901 the template variables (except ones that disappear when expanding synonyms).
902 But when unifying, we don't want to do this, because we'll then fall into
903 a loop.
904
905 This arrangement affects the code in three places:
906 - If we're matching a refined template variable, don't recur. Instead, just
907 check for equality. That is, if we know [a |-> Maybe a] and are matching
908 (a ~? Maybe Int), we want to just fail.
909
910 - Skip the occurs check when matching. This comes up in two places, because
911 matching against variables is handled separately from matching against
912 full-on types.
913
914 Note that this arrangement was provoked by a real failure, where the same
915 unique ended up in the template as in the target. (It was a rule firing when
916 compiling Data.List.NonEmpty.)
917
918 Note [Matching coercion variables]
919 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
920 Consider this:
921
922 type family F a
923
924 data G a where
925 MkG :: F a ~ Bool => G a
926
927 type family Foo (x :: G a) :: F a
928 type instance Foo MkG = False
929
930 We would like that to be accepted. For that to work, we need to introduce
931 a coercion variable on the left and then use it on the right. Accordingly,
932 at use sites of Foo, we need to be able to use matching to figure out the
933 value for the coercion. (See the desugared version:
934
935 axFoo :: [a :: *, c :: F a ~ Bool]. Foo (MkG c) = False |> (sym c)
936
937 ) We never want this action to happen during *unification* though, when
938 all bets are off.
939
940 Note [Kind coercions in Unify]
941 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
942 We wish to match/unify while ignoring casts. But, we can't just ignore
943 them completely, or we'll end up with ill-kinded substitutions. For example,
944 say we're matching `a` with `ty |> co`. If we just drop the cast, we'll
945 return [a |-> ty], but `a` and `ty` might have different kinds. We can't
946 just match/unify their kinds, either, because this might gratuitously
947 fail. After all, `co` is the witness that the kinds are the same -- they
948 may look nothing alike.
949
950 So, we pass a kind coercion to the match/unify worker. This coercion witnesses
951 the equality between the substed kind of the left-hand type and the substed
952 kind of the right-hand type. Note that we do not unify kinds at the leaves
953 (as we did previously). We thus have
954
955 INVARIANT: In the call
956 unify_ty ty1 ty2 kco
957 it must be that subst(kco) :: subst(kind(ty1)) ~N subst(kind(ty2)), where
958 `subst` is the ambient substitution in the UM monad.
959
960 To get this coercion, we first have to match/unify
961 the kinds before looking at the types. Happily, we need look only one level
962 up, as all kinds are guaranteed to have kind *.
963
964 When we're working with type applications (either TyConApp or AppTy) we
965 need to worry about establishing INVARIANT, as the kinds of the function
966 & arguments aren't (necessarily) included in the kind of the result.
967 When unifying two TyConApps, this is easy, because the two TyCons are
968 the same. Their kinds are thus the same. As long as we unify left-to-right,
969 we'll be sure to unify types' kinds before the types themselves. (For example,
970 think about Proxy :: forall k. k -> *. Unifying the first args matches up
971 the kinds of the second args.)
972
973 For AppTy, we must unify the kinds of the functions, but once these are
974 unified, we can continue unifying arguments without worrying further about
975 kinds.
976
977 The interface to this module includes both "...Ty" functions and
978 "...TyKi" functions. The former assume that INVARIANT is already
979 established, either because the kinds are the same or because the
980 list of types being passed in are the well-typed arguments to some
981 type constructor (see two paragraphs above). The latter take a separate
982 pre-pass over the kinds to establish INVARIANT. Sometimes, it's important
983 not to take the second pass, as it caused #12442.
984
985 We thought, at one point, that this was all unnecessary: why should
986 casts be in types in the first place? But they are sometimes. In
987 dependent/should_compile/KindEqualities2, we see, for example the
988 constraint Num (Int |> (blah ; sym blah)). We naturally want to find
989 a dictionary for that constraint, which requires dealing with
990 coercions in this manner.
991
992 Note [Matching in the presence of casts (1)]
993 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
994 When matching, it is crucial that no variables from the template
995 end up in the range of the matching substitution (obviously!).
996 When unifying, that's not a constraint; instead we take the fixpoint
997 of the substitution at the end.
998
999 So what should we do with this, when matching?
1000 unify_ty (tmpl |> co) tgt kco
1001
1002 Previously, wrongly, we pushed 'co' in the (horrid) accumulating
1003 'kco' argument like this:
1004 unify_ty (tmpl |> co) tgt kco
1005 = unify_ty tmpl tgt (kco ; co)
1006
1007 But that is obviously wrong because 'co' (from the template) ends
1008 up in 'kco', which in turn ends up in the range of the substitution.
1009
1010 This all came up in #13910. Because we match tycon arguments
1011 left-to-right, the ambient substitution will already have a matching
1012 substitution for any kinds; so there is an easy fix: just apply
1013 the substitution-so-far to the coercion from the LHS.
1014
1015 Note that
1016
1017 * When matching, the first arg of unify_ty is always the template;
1018 we never swap round.
1019
1020 * The above argument is distressingly indirect. We seek a
1021 better way.
1022
1023 * One better way is to ensure that type patterns (the template
1024 in the matching process) have no casts. See #14119.
1025
1026 Note [Matching in the presence of casts (2)]
1027 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1028 There is another wrinkle (#17395). Suppose (T :: forall k. k -> Type)
1029 and we are matching
1030 tcMatchTy (T k (a::k)) (T j (b::j))
1031
1032 Then we'll match k :-> j, as expected. But then in unify_tys
1033 we invoke
1034 unify_tys env (a::k) (b::j) (Refl j)
1035
1036 Although we have unified k and j, it's very important that we put
1037 (Refl j), /not/ (Refl k) as the fourth argument to unify_tys.
1038 If we put (Refl k) we'd end up with the substitution
1039 a :-> b |> Refl k
1040 which is bogus because one of the template variables, k,
1041 appears in the range of the substitution. Eek.
1042
1043 Similar care is needed in unify_ty_app.
1044
1045
1046 Note [Polykinded tycon applications]
1047 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1048 Suppose T :: forall k. Type -> K
1049 and we are unifying
1050 ty1: T @Type Int :: Type
1051 ty2: T @(Type->Type) Int Int :: Type
1052
1053 These two TyConApps have the same TyCon at the front but they
1054 (legitimately) have different numbers of arguments. They
1055 are surelyApart, so we can report that without looking any
1056 further (see #15704).
1057 -}
1058
1059 -------------- unify_ty: the main workhorse -----------
1060
1061 type AmIUnifying = Bool -- True <=> Unifying
1062 -- False <=> Matching
1063
1064 unify_ty :: UMEnv
1065 -> Type -> Type -- Types to be unified and a co
1066 -> CoercionN -- A coercion between their kinds
1067 -- See Note [Kind coercions in Unify]
1068 -> UM ()
1069 -- See Note [Specification of unification]
1070 -- Respects newtypes, PredTypes
1071 -- See Note [Computing equality on types] in GHC.Core.Type
1072 unify_ty env ty1 ty2 kco
1073 -- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
1074 | TyConApp tc1 [] <- ty1
1075 , TyConApp tc2 [] <- ty2
1076 , tc1 == tc2 = return ()
1077
1078 -- TODO: More commentary needed here
1079 | Just ty1' <- tcView ty1 = unify_ty env ty1' ty2 kco
1080 | Just ty2' <- tcView ty2 = unify_ty env ty1 ty2' kco
1081 | CastTy ty1' co <- ty1 = if um_unif env
1082 then unify_ty env ty1' ty2 (co `mkTransCo` kco)
1083 else -- See Note [Matching in the presence of casts (1)]
1084 do { subst <- getSubst env
1085 ; let co' = substCo subst co
1086 ; unify_ty env ty1' ty2 (co' `mkTransCo` kco) }
1087 | CastTy ty2' co <- ty2 = unify_ty env ty1 ty2' (kco `mkTransCo` mkSymCo co)
1088
1089 unify_ty env (TyVarTy tv1) ty2 kco
1090 = uVar env tv1 ty2 kco
1091 unify_ty env ty1 (TyVarTy tv2) kco
1092 | um_unif env -- If unifying, can swap args
1093 = uVar (umSwapRn env) tv2 ty1 (mkSymCo kco)
1094
1095 unify_ty env ty1 ty2 _kco
1096 -- NB: This keeps Constraint and Type distinct, as it should for use in the
1097 -- type-checker.
1098 | Just (tc1, tys1) <- mb_tc_app1
1099 , Just (tc2, tys2) <- mb_tc_app2
1100 , tc1 == tc2
1101 = if isInjectiveTyCon tc1 Nominal
1102 then unify_tys env tys1 tys2
1103 else do { let inj | isTypeFamilyTyCon tc1
1104 = case tyConInjectivityInfo tc1 of
1105 NotInjective -> repeat False
1106 Injective bs -> bs
1107 | otherwise
1108 = repeat False
1109
1110 (inj_tys1, noninj_tys1) = partitionByList inj tys1
1111 (inj_tys2, noninj_tys2) = partitionByList inj tys2
1112
1113 ; unify_tys env inj_tys1 inj_tys2
1114 ; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
1115 don'tBeSoSure MARTypeFamily $ unify_tys env noninj_tys1 noninj_tys2 }
1116
1117 | Just (tc1, _) <- mb_tc_app1
1118 , not (isGenerativeTyCon tc1 Nominal)
1119 -- E.g. unify_ty (F ty1) b = MaybeApart
1120 -- because the (F ty1) behaves like a variable
1121 -- NB: if unifying, we have already dealt
1122 -- with the 'ty2 = variable' case
1123 = maybeApart MARTypeFamily
1124
1125 | Just (tc2, _) <- mb_tc_app2
1126 , not (isGenerativeTyCon tc2 Nominal)
1127 , um_unif env
1128 -- E.g. unify_ty [a] (F ty2) = MaybeApart, when unifying (only)
1129 -- because the (F ty2) behaves like a variable
1130 -- NB: we have already dealt with the 'ty1 = variable' case
1131 = maybeApart MARTypeFamily
1132
1133 where
1134 mb_tc_app1 = tcSplitTyConApp_maybe ty1
1135 mb_tc_app2 = tcSplitTyConApp_maybe ty2
1136
1137 -- Applications need a bit of care!
1138 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1139 -- NB: we've already dealt with type variables,
1140 -- so if one type is an App the other one jolly well better be too
1141 unify_ty env (AppTy ty1a ty1b) ty2 _kco
1142 | Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
1143 = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
1144
1145 unify_ty env ty1 (AppTy ty2a ty2b) _kco
1146 | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
1147 = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
1148
1149 -- tcSplitTyConApp won't split a (=>), so we handle this separately.
1150 unify_ty env (FunTy InvisArg _w1 arg1 res1) (FunTy InvisArg _w2 arg2 res2) _kco
1151 -- Look at result representations, but arg representations would be redundant
1152 -- as anything that can appear to the left of => is lifted.
1153 -- And anything that can appear to the left of => is unrestricted, so skip the
1154 -- multiplicities.
1155 | Just res_rep1 <- getRuntimeRep_maybe res1
1156 , Just res_rep2 <- getRuntimeRep_maybe res2
1157 = unify_tys env [res_rep1, arg1, res1] [res_rep2, arg2, res2]
1158
1159 unify_ty _ (LitTy x) (LitTy y) _kco | x == y = return ()
1160
1161 unify_ty env (ForAllTy (Bndr tv1 _) ty1) (ForAllTy (Bndr tv2 _) ty2) kco
1162 = do { unify_ty env (varType tv1) (varType tv2) (mkNomReflCo liftedTypeKind)
1163 ; let env' = umRnBndr2 env tv1 tv2
1164 ; unify_ty env' ty1 ty2 kco }
1165
1166 -- See Note [Matching coercion variables]
1167 unify_ty env (CoercionTy co1) (CoercionTy co2) kco
1168 = do { c_subst <- getCvSubstEnv
1169 ; case co1 of
1170 CoVarCo cv
1171 | not (um_unif env)
1172 , not (cv `elemVarEnv` c_subst)
1173 , let (_, co_l, co_r) = decomposeFunCo Nominal kco
1174 -- Because the coercion is used in a type, it should be safe to
1175 -- ignore the multiplicity coercion.
1176 -- cv :: t1 ~ t2
1177 -- co2 :: s1 ~ s2
1178 -- co_l :: t1 ~ s1
1179 -- co_r :: t2 ~ s2
1180 rhs_co = co_l `mkTransCo` co2 `mkTransCo` mkSymCo co_r
1181 , BindMe <- tvBindFlag env cv (CoercionTy rhs_co)
1182 -> do { checkRnEnv env (tyCoVarsOfCo co2)
1183 ; extendCvEnv cv rhs_co }
1184 _ -> return () }
1185
1186 unify_ty _ _ _ _ = surelyApart
1187
1188 unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
1189 unify_ty_app env ty1 ty1args ty2 ty2args
1190 | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
1191 , Just (ty2', ty2a) <- repSplitAppTy_maybe ty2
1192 = unify_ty_app env ty1' (ty1a : ty1args) ty2' (ty2a : ty2args)
1193
1194 | otherwise
1195 = do { let ki1 = typeKind ty1
1196 ki2 = typeKind ty2
1197 -- See Note [Kind coercions in Unify]
1198 ; unify_ty env ki1 ki2 (mkNomReflCo liftedTypeKind)
1199 ; unify_ty env ty1 ty2 (mkNomReflCo ki2)
1200 -- Very important: 'ki2' not 'ki1'
1201 -- See Note [Matching in the presence of casts (2)]
1202 ; unify_tys env ty1args ty2args }
1203
1204 unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
1205 unify_tys env orig_xs orig_ys
1206 = go orig_xs orig_ys
1207 where
1208 go [] [] = return ()
1209 go (x:xs) (y:ys)
1210 -- See Note [Kind coercions in Unify]
1211 = do { unify_ty env x y (mkNomReflCo $ typeKind y)
1212 -- Very important: 'y' not 'x'
1213 -- See Note [Matching in the presence of casts (2)]
1214 ; go xs ys }
1215 go _ _ = surelyApart
1216 -- Possibly different saturations of a polykinded tycon
1217 -- See Note [Polykinded tycon applications]
1218
1219 ---------------------------------
1220 uVar :: UMEnv
1221 -> InTyVar -- Variable to be unified
1222 -> Type -- with this Type
1223 -> Coercion -- :: kind tv ~N kind ty
1224 -> UM ()
1225
1226 uVar env tv1 ty kco
1227 = do { -- Apply the ambient renaming
1228 let tv1' = umRnOccL env tv1
1229
1230 -- Check to see whether tv1 is refined by the substitution
1231 ; subst <- getTvSubstEnv
1232 ; case (lookupVarEnv subst tv1') of
1233 Just ty' | um_unif env -- Unifying, so call
1234 -> unify_ty env ty' ty kco -- back into unify
1235 | otherwise
1236 -> -- Matching, we don't want to just recur here.
1237 -- this is because the range of the subst is the target
1238 -- type, not the template type. So, just check for
1239 -- normal type equality.
1240 unless ((ty' `mkCastTy` kco) `tcEqType` ty) $
1241 surelyApart
1242 -- NB: it's important to use `tcEqType` instead of `eqType` here,
1243 -- otherwise we might not reject a substitution
1244 -- which unifies `Type` with `Constraint`, e.g.
1245 -- a call to tc_unify_tys with arguments
1246 --
1247 -- tys1 = [k,k]
1248 -- tys2 = [Type, Constraint]
1249 --
1250 -- See test cases: T11715b, T20521.
1251 Nothing -> uUnrefined env tv1' ty ty kco } -- No, continue
1252
1253 uUnrefined :: UMEnv
1254 -> OutTyVar -- variable to be unified
1255 -> Type -- with this Type
1256 -> Type -- (version w/ expanded synonyms)
1257 -> Coercion -- :: kind tv ~N kind ty
1258 -> UM ()
1259
1260 -- We know that tv1 isn't refined
1261
1262 uUnrefined env tv1' ty2 ty2' kco
1263 -- Use tcView, not coreView. See Note [coreView vs tcView] in GHC.Core.Type.
1264 | Just ty2'' <- tcView ty2'
1265 = uUnrefined env tv1' ty2 ty2'' kco -- Unwrap synonyms
1266 -- This is essential, in case we have
1267 -- type Foo a = a
1268 -- and then unify a ~ Foo a
1269
1270 | TyVarTy tv2 <- ty2'
1271 = do { let tv2' = umRnOccR env tv2
1272 ; unless (tv1' == tv2' && um_unif env) $ do
1273 -- If we are unifying a ~ a, just return immediately
1274 -- Do not extend the substitution
1275 -- See Note [Self-substitution when matching]
1276
1277 -- Check to see whether tv2 is refined
1278 { subst <- getTvSubstEnv
1279 ; case lookupVarEnv subst tv2 of
1280 { Just ty' | um_unif env -> uUnrefined env tv1' ty' ty' kco
1281 ; _ ->
1282
1283 do { -- So both are unrefined
1284 -- Bind one or the other, depending on which is bindable
1285 ; let rhs1 = ty2 `mkCastTy` mkSymCo kco
1286 rhs2 = ty1 `mkCastTy` kco
1287 b1 = tvBindFlag env tv1' rhs1
1288 b2 = tvBindFlag env tv2' rhs2
1289 ty1 = mkTyVarTy tv1'
1290 ; case (b1, b2) of
1291 (BindMe, _) -> bindTv env tv1' rhs1
1292 (_, BindMe) | um_unif env
1293 -> bindTv (umSwapRn env) tv2 rhs2
1294
1295 _ | tv1' == tv2' -> return ()
1296 -- How could this happen? If we're only matching and if
1297 -- we're comparing forall-bound variables.
1298
1299 _ -> surelyApart
1300 }}}}
1301
1302 uUnrefined env tv1' ty2 _ kco -- ty2 is not a type variable
1303 = case tvBindFlag env tv1' rhs of
1304 Apart -> surelyApart
1305 BindMe -> bindTv env tv1' rhs
1306 where
1307 rhs = ty2 `mkCastTy` mkSymCo kco
1308
1309 bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
1310 -- OK, so we want to extend the substitution with tv := ty
1311 -- But first, we must do a couple of checks
1312 bindTv env tv1 ty2
1313 = do { let free_tvs2 = tyCoVarsOfType ty2
1314
1315 -- Make sure tys mentions no local variables
1316 -- E.g. (forall a. b) ~ (forall a. [a])
1317 -- We should not unify b := [a]!
1318 ; checkRnEnv env free_tvs2
1319
1320 -- Occurs check, see Note [Fine-grained unification]
1321 -- Make sure you include 'kco' (which ty2 does) #14846
1322 ; occurs <- occursCheck env tv1 free_tvs2
1323
1324 ; if occurs then maybeApart MARInfinite
1325 else extendTvEnv tv1 ty2 }
1326
1327 occursCheck :: UMEnv -> TyVar -> VarSet -> UM Bool
1328 occursCheck env tv free_tvs
1329 | um_unif env
1330 = do { tsubst <- getTvSubstEnv
1331 ; return (tv `elemVarSet` niSubstTvSet tsubst free_tvs) }
1332
1333 | otherwise -- Matching; no occurs check
1334 = return False -- See Note [Self-substitution when matching]
1335
1336 {-
1337 %************************************************************************
1338 %* *
1339 Binding decisions
1340 * *
1341 ************************************************************************
1342 -}
1343
1344 data BindFlag
1345 = BindMe -- ^ A regular type variable
1346
1347 | Apart -- ^ Declare that this type variable is /apart/ from the
1348 -- type provided. That is, the type variable will never
1349 -- be instantiated to that type.
1350 -- See also Note [Binding when looking up instances]
1351 -- in GHC.Core.InstEnv.
1352 deriving Eq
1353 -- NB: It would be conceivable to have an analogue to MaybeApart here,
1354 -- but there is not yet a need.
1355
1356 {-
1357 ************************************************************************
1358 * *
1359 Unification monad
1360 * *
1361 ************************************************************************
1362 -}
1363
1364 data UMEnv
1365 = UMEnv { um_unif :: AmIUnifying
1366
1367 , um_inj_tf :: Bool
1368 -- Checking for injectivity?
1369 -- See (end of) Note [Specification of unification]
1370
1371 , um_rn_env :: RnEnv2
1372 -- Renaming InTyVars to OutTyVars; this eliminates
1373 -- shadowing, and lines up matching foralls on the left
1374 -- and right
1375
1376 , um_skols :: TyVarSet
1377 -- OutTyVars bound by a forall in this unification;
1378 -- Do not bind these in the substitution!
1379 -- See the function tvBindFlag
1380
1381 , um_bind_fun :: BindFun
1382 -- User-supplied BindFlag function,
1383 -- for variables not in um_skols
1384 }
1385
1386 data UMState = UMState
1387 { um_tv_env :: TvSubstEnv
1388 , um_cv_env :: CvSubstEnv }
1389
1390 newtype UM a
1391 = UM' { unUM :: UMState -> UnifyResultM (UMState, a) }
1392 -- See Note [The one-shot state monad trick] in GHC.Utils.Monad
1393 deriving (Functor)
1394
1395 pattern UM :: (UMState -> UnifyResultM (UMState, a)) -> UM a
1396 -- See Note [The one-shot state monad trick] in GHC.Utils.Monad
1397 pattern UM m <- UM' m
1398 where
1399 UM m = UM' (oneShot m)
1400
1401 instance Applicative UM where
1402 pure a = UM (\s -> pure (s, a))
1403 (<*>) = ap
1404
1405 instance Monad UM where
1406 {-# INLINE (>>=) #-}
1407 -- See Note [INLINE pragmas and (>>)] in GHC.Utils.Monad
1408 m >>= k = UM (\state ->
1409 do { (state', v) <- unUM m state
1410 ; unUM (k v) state' })
1411
1412 instance MonadFail UM where
1413 fail _ = UM (\_ -> SurelyApart) -- failed pattern match
1414
1415 initUM :: TvSubstEnv -- subst to extend
1416 -> CvSubstEnv
1417 -> UM a -> UnifyResultM a
1418 initUM subst_env cv_subst_env um
1419 = case unUM um state of
1420 Unifiable (_, subst) -> Unifiable subst
1421 MaybeApart r (_, subst) -> MaybeApart r subst
1422 SurelyApart -> SurelyApart
1423 where
1424 state = UMState { um_tv_env = subst_env
1425 , um_cv_env = cv_subst_env }
1426
1427 tvBindFlag :: UMEnv -> OutTyVar -> Type -> BindFlag
1428 tvBindFlag env tv rhs
1429 | tv `elemVarSet` um_skols env = Apart
1430 | otherwise = um_bind_fun env tv rhs
1431
1432 getTvSubstEnv :: UM TvSubstEnv
1433 getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state)
1434
1435 getCvSubstEnv :: UM CvSubstEnv
1436 getCvSubstEnv = UM $ \state -> Unifiable (state, um_cv_env state)
1437
1438 getSubst :: UMEnv -> UM TCvSubst
1439 getSubst env = do { tv_env <- getTvSubstEnv
1440 ; cv_env <- getCvSubstEnv
1441 ; let in_scope = rnInScopeSet (um_rn_env env)
1442 ; return (mkTCvSubst in_scope (tv_env, cv_env)) }
1443
1444 extendTvEnv :: TyVar -> Type -> UM ()
1445 extendTvEnv tv ty = UM $ \state ->
1446 Unifiable (state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())
1447
1448 extendCvEnv :: CoVar -> Coercion -> UM ()
1449 extendCvEnv cv co = UM $ \state ->
1450 Unifiable (state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())
1451
1452 umRnBndr2 :: UMEnv -> TyCoVar -> TyCoVar -> UMEnv
1453 umRnBndr2 env v1 v2
1454 = env { um_rn_env = rn_env', um_skols = um_skols env `extendVarSet` v' }
1455 where
1456 (rn_env', v') = rnBndr2_var (um_rn_env env) v1 v2
1457
1458 checkRnEnv :: UMEnv -> VarSet -> UM ()
1459 checkRnEnv env varset
1460 | isEmptyVarSet skol_vars = return ()
1461 | varset `disjointVarSet` skol_vars = return ()
1462 | otherwise = surelyApart
1463 where
1464 skol_vars = um_skols env
1465 -- NB: That isEmptyVarSet guard is a critical optimization;
1466 -- it means we don't have to calculate the free vars of
1467 -- the type, often saving quite a bit of allocation.
1468
1469 -- | Converts any SurelyApart to a MaybeApart
1470 don'tBeSoSure :: MaybeApartReason -> UM () -> UM ()
1471 don'tBeSoSure r um = UM $ \ state ->
1472 case unUM um state of
1473 SurelyApart -> MaybeApart r (state, ())
1474 other -> other
1475
1476 umRnOccL :: UMEnv -> TyVar -> TyVar
1477 umRnOccL env v = rnOccL (um_rn_env env) v
1478
1479 umRnOccR :: UMEnv -> TyVar -> TyVar
1480 umRnOccR env v = rnOccR (um_rn_env env) v
1481
1482 umSwapRn :: UMEnv -> UMEnv
1483 umSwapRn env = env { um_rn_env = rnSwap (um_rn_env env) }
1484
1485 maybeApart :: MaybeApartReason -> UM ()
1486 maybeApart r = UM (\state -> MaybeApart r (state, ()))
1487
1488 surelyApart :: UM a
1489 surelyApart = UM (\_ -> SurelyApart)
1490
1491 {-
1492 %************************************************************************
1493 %* *
1494 Matching a (lifted) type against a coercion
1495 %* *
1496 %************************************************************************
1497
1498 This section defines essentially an inverse to liftCoSubst. It is defined
1499 here to avoid a dependency from Coercion on this module.
1500
1501 -}
1502
1503 data MatchEnv = ME { me_tmpls :: TyVarSet
1504 , me_env :: RnEnv2 }
1505
1506 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
1507 -- @liftCoMatch vars ty co == Just s@, then @liftCoSubst s ty == co@,
1508 -- where @==@ there means that the result of 'liftCoSubst' has the same
1509 -- type as the original co; but may be different under the hood.
1510 -- That is, it matches a type against a coercion of the same
1511 -- "shape", and returns a lifting substitution which could have been
1512 -- used to produce the given coercion from the given type.
1513 -- Note that this function is incomplete -- it might return Nothing
1514 -- when there does indeed exist a possible lifting context.
1515 --
1516 -- This function is incomplete in that it doesn't respect the equality
1517 -- in `eqType`. That is, it's possible that this will succeed for t1 and
1518 -- fail for t2, even when t1 `eqType` t2. That's because it depends on
1519 -- there being a very similar structure between the type and the coercion.
1520 -- This incompleteness shouldn't be all that surprising, especially because
1521 -- it depends on the structure of the coercion, which is a silly thing to do.
1522 --
1523 -- The lifting context produced doesn't have to be exacting in the roles
1524 -- of the mappings. This is because any use of the lifting context will
1525 -- also require a desired role. Thus, this algorithm prefers mapping to
1526 -- nominal coercions where it can do so.
1527 liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
1528 liftCoMatch tmpls ty co
1529 = do { cenv1 <- ty_co_match menv emptyVarEnv ki ki_co ki_ki_co ki_ki_co
1530 ; cenv2 <- ty_co_match menv cenv1 ty co
1531 (mkNomReflCo co_lkind) (mkNomReflCo co_rkind)
1532 ; return (LC (mkEmptyTCvSubst in_scope) cenv2) }
1533 where
1534 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
1535 in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
1536 -- Like tcMatchTy, assume all the interesting variables
1537 -- in ty are in tmpls
1538
1539 ki = typeKind ty
1540 ki_co = promoteCoercion co
1541 ki_ki_co = mkNomReflCo liftedTypeKind
1542
1543 Pair co_lkind co_rkind = coercionKind ki_co
1544
1545 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
1546 ty_co_match :: MatchEnv -- ^ ambient helpful info
1547 -> LiftCoEnv -- ^ incoming subst
1548 -> Type -- ^ ty, type to match
1549 -> Coercion -- ^ co, coercion to match against
1550 -> Coercion -- ^ :: kind of L type of substed ty ~N L kind of co
1551 -> Coercion -- ^ :: kind of R type of substed ty ~N R kind of co
1552 -> Maybe LiftCoEnv
1553 ty_co_match menv subst ty co lkco rkco
1554 | Just ty' <- coreView ty = ty_co_match menv subst ty' co lkco rkco
1555 -- why coreView here, not tcView? Because we're firmly after type-checking.
1556 -- This function is used only during coercion optimisation.
1557
1558 -- handle Refl case:
1559 | tyCoVarsOfType ty `isNotInDomainOf` subst
1560 , Just (ty', _) <- isReflCo_maybe co
1561 , ty `eqType` ty'
1562 -- Why `eqType` and not `tcEqType`? Because this function is only used
1563 -- during coercion optimisation, after type-checking has finished.
1564 = Just subst
1565
1566 where
1567 isNotInDomainOf :: VarSet -> VarEnv a -> Bool
1568 isNotInDomainOf set env
1569 = noneSet (\v -> elemVarEnv v env) set
1570
1571 noneSet :: (Var -> Bool) -> VarSet -> Bool
1572 noneSet f = allVarSet (not . f)
1573
1574 ty_co_match menv subst ty co lkco rkco
1575 | CastTy ty' co' <- ty
1576 -- See Note [Matching in the presence of casts (1)]
1577 = let empty_subst = mkEmptyTCvSubst (rnInScopeSet (me_env menv))
1578 substed_co_l = substCo (liftEnvSubstLeft empty_subst subst) co'
1579 substed_co_r = substCo (liftEnvSubstRight empty_subst subst) co'
1580 in
1581 ty_co_match menv subst ty' co (substed_co_l `mkTransCo` lkco)
1582 (substed_co_r `mkTransCo` rkco)
1583
1584 | SymCo co' <- co
1585 = swapLiftCoEnv <$> ty_co_match menv (swapLiftCoEnv subst) ty co' rkco lkco
1586
1587 -- Match a type variable against a non-refl coercion
1588 ty_co_match menv subst (TyVarTy tv1) co lkco rkco
1589 | Just co1' <- lookupVarEnv subst tv1' -- tv1' is already bound to co1
1590 = if eqCoercionX (nukeRnEnvL rn_env) co1' co
1591 then Just subst
1592 else Nothing -- no match since tv1 matches two different coercions
1593
1594 | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
1595 = if any (inRnEnvR rn_env) (tyCoVarsOfCoList co)
1596 then Nothing -- occurs check failed
1597 else Just $ extendVarEnv subst tv1' $
1598 castCoercionKind co (mkSymCo lkco) (mkSymCo rkco)
1599
1600 | otherwise
1601 = Nothing
1602
1603 where
1604 rn_env = me_env menv
1605 tv1' = rnOccL rn_env tv1
1606
1607 -- just look through SubCo's. We don't really care about roles here.
1608 ty_co_match menv subst ty (SubCo co) lkco rkco
1609 = ty_co_match menv subst ty co lkco rkco
1610
1611 ty_co_match menv subst (AppTy ty1a ty1b) co _lkco _rkco
1612 | Just (co2, arg2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy
1613 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1614 ty_co_match menv subst ty1 (AppCo co2 arg2) _lkco _rkco
1615 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
1616 -- yes, the one from Type, not TcType; this is for coercion optimization
1617 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1618
1619 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos) _lkco _rkco
1620 = ty_co_match_tc menv subst tc1 tys tc2 cos
1621 ty_co_match menv subst (FunTy _ w ty1 ty2) co _lkco _rkco
1622 -- Despite the fact that (->) is polymorphic in five type variables (two
1623 -- runtime rep, a multiplicity and two types), we shouldn't need to
1624 -- explicitly unify the runtime reps here; unifying the types themselves
1625 -- should be sufficient. See Note [Representation of function types].
1626 | Just (tc, [co_mult, _,_,co1,co2]) <- splitTyConAppCo_maybe co
1627 , tc == funTyCon
1628 = let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) [co_mult,co1,co2]
1629 in ty_co_match_args menv subst [w, ty1, ty2] [co_mult, co1, co2] lkcos rkcos
1630
1631 ty_co_match menv subst (ForAllTy (Bndr tv1 _) ty1)
1632 (ForAllCo tv2 kind_co2 co2)
1633 lkco rkco
1634 | isTyVar tv1 && isTyVar tv2
1635 = do { subst1 <- ty_co_match menv subst (tyVarKind tv1) kind_co2
1636 ki_ki_co ki_ki_co
1637 ; let rn_env0 = me_env menv
1638 rn_env1 = rnBndr2 rn_env0 tv1 tv2
1639 menv' = menv { me_env = rn_env1 }
1640 ; ty_co_match menv' subst1 ty1 co2 lkco rkco }
1641 where
1642 ki_ki_co = mkNomReflCo liftedTypeKind
1643
1644 -- ty_co_match menv subst (ForAllTy (Bndr cv1 _) ty1)
1645 -- (ForAllCo cv2 kind_co2 co2)
1646 -- lkco rkco
1647 -- | isCoVar cv1 && isCoVar cv2
1648 -- We seems not to have enough information for this case
1649 -- 1. Given:
1650 -- cv1 :: (s1 :: k1) ~r (s2 :: k2)
1651 -- kind_co2 :: (s1' ~ s2') ~N (t1 ~ t2)
1652 -- eta1 = mkNthCo role 2 (downgradeRole r Nominal kind_co2)
1653 -- :: s1' ~ t1
1654 -- eta2 = mkNthCo role 3 (downgradeRole r Nominal kind_co2)
1655 -- :: s2' ~ t2
1656 -- Wanted:
1657 -- subst1 <- ty_co_match menv subst s1 eta1 kco1 kco2
1658 -- subst2 <- ty_co_match menv subst1 s2 eta2 kco3 kco4
1659 -- Question: How do we get kcoi?
1660 -- 2. Given:
1661 -- lkco :: <*> -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
1662 -- rkco :: <*>
1663 -- Wanted:
1664 -- ty_co_match menv' subst2 ty1 co2 lkco' rkco'
1665 -- Question: How do we get lkco' and rkco'?
1666
1667 ty_co_match _ subst (CoercionTy {}) _ _ _
1668 = Just subst -- don't inspect coercions
1669
1670 ty_co_match menv subst ty (GRefl r t (MCo co)) lkco rkco
1671 = ty_co_match menv subst ty (GRefl r t MRefl) lkco (rkco `mkTransCo` mkSymCo co)
1672
1673 ty_co_match menv subst ty co1 lkco rkco
1674 | Just (CastTy t co, r) <- isReflCo_maybe co1
1675 -- In @pushRefl@, pushing reflexive coercion inside CastTy will give us
1676 -- t |> co ~ t ; <t> ; t ~ t |> co
1677 -- But transitive coercions are not helpful. Therefore we deal
1678 -- with it here: we do recursion on the smaller reflexive coercion,
1679 -- while propagating the correct kind coercions.
1680 = let kco' = mkSymCo co
1681 in ty_co_match menv subst ty (mkReflCo r t) (lkco `mkTransCo` kco')
1682 (rkco `mkTransCo` kco')
1683
1684
1685 ty_co_match menv subst ty co lkco rkco
1686 | Just co' <- pushRefl co = ty_co_match menv subst ty co' lkco rkco
1687 | otherwise = Nothing
1688
1689 ty_co_match_tc :: MatchEnv -> LiftCoEnv
1690 -> TyCon -> [Type]
1691 -> TyCon -> [Coercion]
1692 -> Maybe LiftCoEnv
1693 ty_co_match_tc menv subst tc1 tys1 tc2 cos2
1694 = do { guard (tc1 == tc2)
1695 ; ty_co_match_args menv subst tys1 cos2 lkcos rkcos }
1696 where
1697 Pair lkcos rkcos
1698 = traverse (fmap mkNomReflCo . coercionKind) cos2
1699
1700 ty_co_match_app :: MatchEnv -> LiftCoEnv
1701 -> Type -> [Type] -> Coercion -> [Coercion]
1702 -> Maybe LiftCoEnv
1703 ty_co_match_app menv subst ty1 ty1args co2 co2args
1704 | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
1705 , Just (co2', co2a) <- splitAppCo_maybe co2
1706 = ty_co_match_app menv subst ty1' (ty1a : ty1args) co2' (co2a : co2args)
1707
1708 | otherwise
1709 = do { subst1 <- ty_co_match menv subst ki1 ki2 ki_ki_co ki_ki_co
1710 ; let Pair lkco rkco = mkNomReflCo <$> coercionKind ki2
1711 ; subst2 <- ty_co_match menv subst1 ty1 co2 lkco rkco
1712 ; let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) co2args
1713 ; ty_co_match_args menv subst2 ty1args co2args lkcos rkcos }
1714 where
1715 ki1 = typeKind ty1
1716 ki2 = promoteCoercion co2
1717 ki_ki_co = mkNomReflCo liftedTypeKind
1718
1719 ty_co_match_args :: MatchEnv -> LiftCoEnv -> [Type]
1720 -> [Coercion] -> [Coercion] -> [Coercion]
1721 -> Maybe LiftCoEnv
1722 ty_co_match_args _ subst [] [] _ _ = Just subst
1723 ty_co_match_args menv subst (ty:tys) (arg:args) (lkco:lkcos) (rkco:rkcos)
1724 = do { subst' <- ty_co_match menv subst ty arg lkco rkco
1725 ; ty_co_match_args menv subst' tys args lkcos rkcos }
1726 ty_co_match_args _ _ _ _ _ _ = Nothing
1727
1728 pushRefl :: Coercion -> Maybe Coercion
1729 pushRefl co =
1730 case (isReflCo_maybe co) of
1731 Just (AppTy ty1 ty2, Nominal)
1732 -> Just (AppCo (mkReflCo Nominal ty1) (mkNomReflCo ty2))
1733 Just (FunTy _ w ty1 ty2, r)
1734 | Just rep1 <- getRuntimeRep_maybe ty1
1735 , Just rep2 <- getRuntimeRep_maybe ty2
1736 -> Just (TyConAppCo r funTyCon [ multToCo w, mkReflCo r rep1, mkReflCo r rep2
1737 , mkReflCo r ty1, mkReflCo r ty2 ])
1738 Just (TyConApp tc tys, r)
1739 -> Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
1740 Just (ForAllTy (Bndr tv _) ty, r)
1741 -> Just (ForAllCo tv (mkNomReflCo (varType tv)) (mkReflCo r ty))
1742 -- NB: NoRefl variant. Otherwise, we get a loop!
1743 _ -> Nothing
1744
1745 {-
1746 ************************************************************************
1747 * *
1748 Flattening
1749 * *
1750 ************************************************************************
1751
1752 Note [Flattening type-family applications when matching instances]
1753 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1754 As described in "Closed type families with overlapping equations"
1755 http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
1756 we need to flatten core types before unifying them, when checking for "surely-apart"
1757 against earlier equations of a closed type family.
1758 Flattening means replacing all top-level uses of type functions with
1759 fresh variables, *taking care to preserve sharing*. That is, the type
1760 (Either (F a b) (F a b)) should flatten to (Either c c), never (Either
1761 c d).
1762
1763 Here is a nice example of why it's all necessary:
1764
1765 type family F a b where
1766 F Int Bool = Char
1767 F a b = Double
1768 type family G a -- open, no instances
1769
1770 How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
1771 while the second equation does. But, before reducing, we must make sure that the
1772 target can never become (F Int Bool). Well, no matter what G Float becomes, it
1773 certainly won't become *both* Int and Bool, so indeed we're safe reducing
1774 (F (G Float) (G Float)) to Double.
1775
1776 This is necessary not only to get more reductions (which we might be
1777 willing to give up on), but for substitutivity. If we have (F x x), we
1778 can see that (F x x) can reduce to Double. So, it had better be the
1779 case that (F blah blah) can reduce to Double, no matter what (blah)
1780 is! Flattening as done below ensures this.
1781
1782 We also use this flattening operation to check for class instances.
1783 If we have
1784 instance C (Maybe b)
1785 instance {-# OVERLAPPING #-} C (Maybe Bool)
1786 [W] C (Maybe (F a))
1787 we want to know that the second instance might match later. So we
1788 flatten the (F a) in the target before trying to unify with instances.
1789 (This is done in GHC.Core.InstEnv.lookupInstEnv'.)
1790
1791 The algorithm works by building up a TypeMap TyVar, mapping
1792 type family applications to fresh variables. This mapping must
1793 be threaded through all the function calls, as any entry in
1794 the mapping must be propagated to all future nodes in the tree.
1795
1796 The algorithm also must track the set of in-scope variables, in
1797 order to make fresh variables as it flattens. (We are far from a
1798 source of fresh Uniques.) See Wrinkle 2, below.
1799
1800 There are wrinkles, of course:
1801
1802 1. The flattening algorithm must account for the possibility
1803 of inner `forall`s. (A `forall` seen here can happen only
1804 because of impredicativity. However, the flattening operation
1805 is an algorithm in Core, which is impredicative.)
1806 Suppose we have (forall b. F b) -> (forall b. F b). Of course,
1807 those two bs are entirely unrelated, and so we should certainly
1808 not flatten the two calls F b to the same variable. Instead, they
1809 must be treated separately. We thus carry a substitution that
1810 freshens variables; we must apply this substitution (in
1811 `coreFlattenTyFamApp`) before looking up an application in the environment.
1812 Note that the range of the substitution contains only TyVars, never anything
1813 else.
1814
1815 For the sake of efficiency, we only apply this substitution when absolutely
1816 necessary. Namely:
1817
1818 * We do not perform the substitution at all if it is empty.
1819 * We only need to worry about the arguments of a type family that are within
1820 the arity of said type family, so we can get away with not applying the
1821 substitution to any oversaturated type family arguments.
1822 * Importantly, we do /not/ achieve this substitution by recursively
1823 flattening the arguments, as this would be wrong. Consider `F (G a)`,
1824 where F and G are type families. We might decide that `F (G a)` flattens
1825 to `beta`. Later, the substitution is non-empty (but does not map `a`) and
1826 so we flatten `G a` to `gamma` and try to flatten `F gamma`. Of course,
1827 `F gamma` is unknown, and so we flatten it to `delta`, but it really
1828 should have been `beta`! Argh!
1829
1830 Moral of the story: instead of flattening the arguments, just substitute
1831 them directly.
1832
1833 2. There are two different reasons we might add a variable
1834 to the in-scope set as we work:
1835
1836 A. We have just invented a new flattening variable.
1837 B. We have entered a `forall`.
1838
1839 Annoying here is that in-scope variable source (A) must be
1840 threaded through the calls. For example, consider (F b -> forall c. F c).
1841 Suppose that, when flattening F b, we invent a fresh variable c.
1842 Now, when we encounter (forall c. F c), we need to know c is already in
1843 scope so that we locally rename c to c'. However, if we don't thread through
1844 the in-scope set from one argument of (->) to the other, we won't know this
1845 and might get very confused.
1846
1847 In contrast, source (B) increases only as we go deeper, as in-scope sets
1848 normally do. However, even here we must be careful. The TypeMap TyVar that
1849 contains mappings from type family applications to freshened variables will
1850 be threaded through both sides of (forall b. F b) -> (forall b. F b). We
1851 thus must make sure that the two `b`s don't get renamed to the same b1. (If
1852 they did, then looking up `F b1` would yield the same flatten var for
1853 each.) So, even though `forall`-bound variables should really be in the
1854 in-scope set only when they are in scope, we retain these variables even
1855 outside of their scope. This ensures that, if we encounter a fresh
1856 `forall`-bound b, we will rename it to b2, not b1. Note that keeping a
1857 larger in-scope set than strictly necessary is always OK, as in-scope sets
1858 are only ever used to avoid collisions.
1859
1860 Sadly, the freshening substitution described in (1) really mustn't bind
1861 variables outside of their scope: note that its domain is the *unrenamed*
1862 variables. This means that the substitution gets "pushed down" (like a
1863 reader monad) while the in-scope set gets threaded (like a state monad).
1864 Because a TCvSubst contains its own in-scope set, we don't carry a TCvSubst;
1865 instead, we just carry a TvSubstEnv down, tying it to the InScopeSet
1866 traveling separately as necessary.
1867
1868 3. Consider `F ty_1 ... ty_n`, where F is a type family with arity k:
1869
1870 type family F ty_1 ... ty_k :: res_k
1871
1872 It's tempting to just flatten `F ty_1 ... ty_n` to `alpha`, where alpha is a
1873 flattening skolem. But we must instead flatten it to
1874 `alpha ty_(k+1) ... ty_n`—that is, by only flattening up to the arity of the
1875 type family.
1876
1877 Why is this better? Consider the following concrete example from #16995:
1878
1879 type family Param :: Type -> Type
1880
1881 type family LookupParam (a :: Type) :: Type where
1882 LookupParam (f Char) = Bool
1883 LookupParam x = Int
1884
1885 foo :: LookupParam (Param ())
1886 foo = 42
1887
1888 In order for `foo` to typecheck, `LookupParam (Param ())` must reduce to
1889 `Int`. But if we flatten `Param ()` to `alpha`, then GHC can't be sure if
1890 `alpha` is apart from `f Char`, so it won't fall through to the second
1891 equation. But since the `Param` type family has arity 0, we can instead
1892 flatten `Param ()` to `alpha ()`, about which GHC knows with confidence is
1893 apart from `f Char`, permitting the second equation to be reached.
1894
1895 Not only does this allow more programs to be accepted, it's also important
1896 for correctness. Not doing this was the root cause of the Core Lint error
1897 in #16995.
1898
1899 flattenTys is defined here because of module dependencies.
1900 -}
1901
1902 data FlattenEnv
1903 = FlattenEnv { fe_type_map :: TypeMap (TyVar, TyCon, [Type])
1904 -- domain: exactly-saturated type family applications
1905 -- range: (fresh variable, type family tycon, args)
1906 , fe_in_scope :: InScopeSet }
1907 -- See Note [Flattening type-family applications when matching instances]
1908
1909 emptyFlattenEnv :: InScopeSet -> FlattenEnv
1910 emptyFlattenEnv in_scope
1911 = FlattenEnv { fe_type_map = emptyTypeMap
1912 , fe_in_scope = in_scope }
1913
1914 updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
1915 updateInScopeSet env upd = env { fe_in_scope = upd (fe_in_scope env) }
1916
1917 flattenTys :: InScopeSet -> [Type] -> [Type]
1918 -- See Note [Flattening type-family applications when matching instances]
1919 flattenTys in_scope tys = fst (flattenTysX in_scope tys)
1920
1921 flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
1922 -- See Note [Flattening type-family applications when matching instances]
1923 -- NB: the returned types mention the fresh type variables
1924 -- in the domain of the returned env, whose range includes
1925 -- the original type family applications. Building a substitution
1926 -- from this information and applying it would yield the original
1927 -- types -- almost. The problem is that the original type might
1928 -- have something like (forall b. F a b); the returned environment
1929 -- can't really sensibly refer to that b. So it may include a locally-
1930 -- bound tyvar in its range. Currently, the only usage of this env't
1931 -- checks whether there are any meta-variables in it
1932 -- (in GHC.Tc.Solver.Monad.mightEqualLater), so this is all OK.
1933 flattenTysX in_scope tys
1934 = let (env, result) = coreFlattenTys emptyTvSubstEnv (emptyFlattenEnv in_scope) tys in
1935 (result, build_env (fe_type_map env))
1936 where
1937 build_env :: TypeMap (TyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
1938 build_env env_in
1939 = foldTM (\(tv, tc, tys) env_out -> extendVarEnv env_out tv (tc, tys))
1940 env_in emptyVarEnv
1941
1942 coreFlattenTys :: TvSubstEnv -> FlattenEnv
1943 -> [Type] -> (FlattenEnv, [Type])
1944 coreFlattenTys subst = mapAccumL (coreFlattenTy subst)
1945
1946 coreFlattenTy :: TvSubstEnv -> FlattenEnv
1947 -> Type -> (FlattenEnv, Type)
1948 coreFlattenTy subst = go
1949 where
1950 go env ty | Just ty' <- coreView ty = go env ty'
1951
1952 go env (TyVarTy tv)
1953 | Just ty <- lookupVarEnv subst tv = (env, ty)
1954 | otherwise = let (env', ki) = go env (tyVarKind tv) in
1955 (env', mkTyVarTy $ setTyVarKind tv ki)
1956 go env (AppTy ty1 ty2) = let (env1, ty1') = go env ty1
1957 (env2, ty2') = go env1 ty2 in
1958 (env2, AppTy ty1' ty2')
1959 go env (TyConApp tc tys)
1960 -- NB: Don't just check if isFamilyTyCon: this catches *data* families,
1961 -- which are generative and thus can be preserved during flattening
1962 | not (isGenerativeTyCon tc Nominal)
1963 = coreFlattenTyFamApp subst env tc tys
1964
1965 | otherwise
1966 = let (env', tys') = coreFlattenTys subst env tys in
1967 (env', mkTyConApp tc tys')
1968
1969 go env ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
1970 = let (env1, ty1') = go env ty1
1971 (env2, ty2') = go env1 ty2
1972 (env3, mult') = go env2 mult in
1973 (env3, ty { ft_mult = mult', ft_arg = ty1', ft_res = ty2' })
1974
1975 go env (ForAllTy (Bndr tv vis) ty)
1976 = let (env1, subst', tv') = coreFlattenVarBndr subst env tv
1977 (env2, ty') = coreFlattenTy subst' env1 ty in
1978 (env2, ForAllTy (Bndr tv' vis) ty')
1979
1980 go env ty@(LitTy {}) = (env, ty)
1981
1982 go env (CastTy ty co)
1983 = let (env1, ty') = go env ty
1984 (env2, co') = coreFlattenCo subst env1 co in
1985 (env2, CastTy ty' co')
1986
1987 go env (CoercionTy co)
1988 = let (env', co') = coreFlattenCo subst env co in
1989 (env', CoercionTy co')
1990
1991
1992 -- when flattening, we don't care about the contents of coercions.
1993 -- so, just return a fresh variable of the right (flattened) type
1994 coreFlattenCo :: TvSubstEnv -> FlattenEnv
1995 -> Coercion -> (FlattenEnv, Coercion)
1996 coreFlattenCo subst env co
1997 = (env2, mkCoVarCo covar)
1998 where
1999 (env1, kind') = coreFlattenTy subst env (coercionType co)
2000 covar = mkFlattenFreshCoVar (fe_in_scope env1) kind'
2001 -- Add the covar to the FlattenEnv's in-scope set.
2002 -- See Note [Flattening type-family applications when matching instances], wrinkle 2A.
2003 env2 = updateInScopeSet env1 (flip extendInScopeSet covar)
2004
2005 coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
2006 -> TyCoVar -> (FlattenEnv, TvSubstEnv, TyVar)
2007 coreFlattenVarBndr subst env tv
2008 = (env2, subst', tv')
2009 where
2010 -- See Note [Flattening type-family applications when matching instances], wrinkle 2B.
2011 kind = varType tv
2012 (env1, kind') = coreFlattenTy subst env kind
2013 tv' = uniqAway (fe_in_scope env1) (setVarType tv kind')
2014 subst' = extendVarEnv subst tv (mkTyVarTy tv')
2015 env2 = updateInScopeSet env1 (flip extendInScopeSet tv')
2016
2017 coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv
2018 -> TyCon -- type family tycon
2019 -> [Type] -- args, already flattened
2020 -> (FlattenEnv, Type)
2021 coreFlattenTyFamApp tv_subst env fam_tc fam_args
2022 = case lookupTypeMap type_map fam_ty of
2023 Just (tv, _, _) -> (env', mkAppTys (mkTyVarTy tv) leftover_args')
2024 Nothing ->
2025 let tyvar_name = mkFlattenFreshTyName fam_tc
2026 tv = uniqAway in_scope $
2027 mkTyVar tyvar_name (typeKind fam_ty)
2028
2029 ty' = mkAppTys (mkTyVarTy tv) leftover_args'
2030 env'' = env' { fe_type_map = extendTypeMap type_map fam_ty
2031 (tv, fam_tc, sat_fam_args)
2032 , fe_in_scope = extendInScopeSet in_scope tv }
2033 in (env'', ty')
2034 where
2035 arity = tyConArity fam_tc
2036 tcv_subst = TCvSubst (fe_in_scope env) tv_subst emptyVarEnv
2037 (sat_fam_args, leftover_args) = assert (arity <= length fam_args) $
2038 splitAt arity fam_args
2039 -- Apply the substitution before looking up an application in the
2040 -- environment. See Note [Flattening type-family applications when matching instances],
2041 -- wrinkle 1.
2042 -- NB: substTys short-cuts the common case when the substitution is empty.
2043 sat_fam_args' = substTys tcv_subst sat_fam_args
2044 (env', leftover_args') = coreFlattenTys tv_subst env leftover_args
2045 -- `fam_tc` may be over-applied to `fam_args` (see
2046 -- Note [Flattening type-family applications when matching instances]
2047 -- wrinkle 3), so we split it into the arguments needed to saturate it
2048 -- (sat_fam_args') and the rest (leftover_args')
2049 fam_ty = mkTyConApp fam_tc sat_fam_args'
2050 FlattenEnv { fe_type_map = type_map
2051 , fe_in_scope = in_scope } = env'
2052
2053 mkFlattenFreshTyName :: Uniquable a => a -> Name
2054 mkFlattenFreshTyName unq
2055 = mkSysTvName (getUnique unq) (fsLit "flt")
2056
2057 mkFlattenFreshCoVar :: InScopeSet -> Kind -> CoVar
2058 mkFlattenFreshCoVar in_scope kind
2059 = let uniq = unsafeGetFreshLocalUnique in_scope
2060 name = mkSystemVarName uniq (fsLit "flc")
2061 in mkCoVar name kind