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