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