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