Clean up coreView/tcView.
[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 -> Bool -- ^ 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 bind_fn unif inj_check rn_env tv_env cv_env $
468 do { when match_kis $
469 unify_tys kis1 kis2
470 ; unify_tys tys1 tys2
471 ; (,) <$> getTvSubstEnv <*> getCvSubstEnv }
472 where
473 kis1 = map typeKind tys1
474 kis2 = map typeKind tys2
475
476 instance Outputable a => Outputable (UnifyResultM a) where
477 ppr SurelyApart = text "SurelyApart"
478 ppr (Unifiable x) = text "Unifiable" <+> ppr x
479 ppr (MaybeApart x) = text "MaybeApart" <+> ppr x
480
481 {-
482 ************************************************************************
483 * *
484 Non-idempotent substitution
485 * *
486 ************************************************************************
487
488 Note [Non-idempotent substitution]
489 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
490 During unification we use a TvSubstEnv/CvSubstEnv pair that is
491 (a) non-idempotent
492 (b) loop-free; ie repeatedly applying it yields a fixed point
493
494 Note [Finding the substitution fixpoint]
495 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
496 Finding the fixpoint of a non-idempotent substitution arising from a
497 unification is harder than it looks, because of kinds. Consider
498 T k (H k (f:k)) ~ T * (g:*)
499 If we unify, we get the substitution
500 [ k -> *
501 , g -> H k (f:k) ]
502 To make it idempotent we don't want to get just
503 [ k -> *
504 , g -> H * (f:k) ]
505 We also want to substitute inside f's kind, to get
506 [ k -> *
507 , g -> H k (f:*) ]
508 If we don't do this, we may apply the substitution to something,
509 and get an ill-formed type, i.e. one where typeKind will fail.
510 This happened, for example, in Trac #9106.
511
512 This is the reason for extending env with [f:k -> f:*], in the
513 definition of env' in niFixTvSubst
514 -}
515
516 niFixTCvSubst :: TvSubstEnv -> TCvSubst
517 -- Find the idempotent fixed point of the non-idempotent substitution
518 -- See Note [Finding the substitution fixpoint]
519 -- ToDo: use laziness instead of iteration?
520 niFixTCvSubst tenv = f tenv
521 where
522 f tenv
523 | not_fixpoint = f (mapVarEnv (substTy subst') tenv)
524 | otherwise = subst
525 where
526 not_fixpoint = anyVarSet in_domain range_tvs
527 in_domain tv = tv `elemVarEnv` tenv
528
529 range_tvs = nonDetFoldUFM (unionVarSet . tyCoVarsOfType) emptyVarSet tenv
530 -- It's OK to use nonDetFoldUFM here because we
531 -- forget the order immediately by creating a set
532 subst = mkTvSubst (mkInScopeSet range_tvs) tenv
533
534 -- env' extends env by replacing any free type with
535 -- that same tyvar with a substituted kind
536 -- See note [Finding the substitution fixpoint]
537 tenv' = extendVarEnvList tenv [ (rtv, mkTyVarTy $
538 setTyVarKind rtv $
539 substTy subst $
540 tyVarKind rtv)
541 | rtv <- nonDetEltsUniqSet range_tvs
542 -- It's OK to use nonDetEltsUniqSet here
543 -- because we forget the order
544 -- immediatedly by putting it in VarEnv
545 , not (in_domain rtv) ]
546 subst' = mkTvSubst (mkInScopeSet range_tvs) tenv'
547
548 niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
549 -- Apply the non-idempotent substitution to a set of type variables,
550 -- remembering that the substitution isn't necessarily idempotent
551 -- This is used in the occurs check, before extending the substitution
552 niSubstTvSet tsubst tvs
553 = nonDetFoldUniqSet (unionVarSet . get) emptyVarSet tvs
554 -- It's OK to nonDetFoldUFM here because we immediately forget the
555 -- ordering by creating a set.
556 where
557 get tv
558 | Just ty <- lookupVarEnv tsubst tv
559 = niSubstTvSet tsubst (tyCoVarsOfType ty)
560
561 | otherwise
562 = unitVarSet tv
563
564 {-
565 ************************************************************************
566 * *
567 unify_ty: the main workhorse
568 * *
569 ************************************************************************
570
571 Note [Specification of unification]
572 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
573 The pure unifier, unify_ty, defined in this module, tries to work out
574 a substitution to make two types say True to eqType. NB: eqType is
575 itself not purely syntactic; it accounts for CastTys;
576 see Note [Non-trivial definitional equality] in TyCoRep
577
578 Unlike the "impure unifiers" in the typechecker (the eager unifier in
579 TcUnify, and the constraint solver itself in TcCanonical), the pure
580 unifier It does /not/ work up to ~.
581
582 The algorithm implemented here is rather delicate, and we depend on it
583 to uphold certain properties. This is a summary of these required
584 properties. Any reference to "flattening" refers to the flattening
585 algorithm in FamInstEnv (See Note [Flattening] in FamInstEnv), not
586 the flattening algorithm in the solver.
587
588 Notation:
589 θ,φ substitutions
590 ξ type-function-free types
591 τ,σ other types
592 τ♭ type τ, flattened
593
594 ≡ eqType
595
596 (U1) Soundness.
597 If (unify τ₁ τ₂) = Unifiable θ, then θ(τ₁) ≡ θ(τ₂).
598 θ is a most general unifier for τ₁ and τ₂.
599
600 (U2) Completeness.
601 If (unify ξ₁ ξ₂) = SurelyApart,
602 then there exists no substitution θ such that θ(ξ₁) ≡ θ(ξ₂).
603
604 These two properties are stated as Property 11 in the "Closed Type Families"
605 paper (POPL'14). Below, this paper is called [CTF].
606
607 (U3) Apartness under substitution.
608 If (unify ξ τ♭) = SurelyApart, then (unify ξ θ(τ)♭) = SurelyApart,
609 for any θ. (Property 12 from [CTF])
610
611 (U4) Apart types do not unify.
612 If (unify ξ τ♭) = SurelyApart, then there exists no θ
613 such that θ(ξ) = θ(τ). (Property 13 from [CTF])
614
615 THEOREM. Completeness w.r.t ~
616 If (unify τ₁♭ τ₂♭) = SurelyApart,
617 then there exists no proof that (τ₁ ~ τ₂).
618
619 PROOF. See appendix of [CTF].
620
621
622 The unification algorithm is used for type family injectivity, as described
623 in the "Injective Type Families" paper (Haskell'15), called [ITF]. When run
624 in this mode, it has the following properties.
625
626 (I1) If (unify σ τ) = SurelyApart, then σ and τ are not unifiable, even
627 after arbitrary type family reductions. Note that σ and τ are
628 not flattened here.
629
630 (I2) If (unify σ τ) = MaybeApart θ, and if some
631 φ exists such that φ(σ) ~ φ(τ), then φ extends θ.
632
633
634 Furthermore, the RULES matching algorithm requires this property,
635 but only when using this algorithm for matching:
636
637 (M1) If (match σ τ) succeeds with θ, then all matchable tyvars
638 in σ are bound in θ.
639
640 Property M1 means that we must extend the substitution with,
641 say (a ↦ a) when appropriate during matching.
642 See also Note [Self-substitution when matching].
643
644 (M2) Completeness of matching.
645 If θ(σ) = τ, then (match σ τ) = Unifiable φ,
646 where θ is an extension of φ.
647
648 Sadly, property M2 and I2 conflict. Consider
649
650 type family F1 a b where
651 F1 Int Bool = Char
652 F1 Double String = Char
653
654 Consider now two matching problems:
655
656 P1. match (F1 a Bool) (F1 Int Bool)
657 P2. match (F1 a Bool) (F1 Double String)
658
659 In case P1, we must find (a ↦ Int) to satisfy M2.
660 In case P2, we must /not/ find (a ↦ Double), in order to satisfy I2. (Note
661 that the correct mapping for I2 is (a ↦ Int). There is no way to discover
662 this, but we musn't map a to anything else!)
663
664 We thus must parameterize the algorithm over whether it's being used
665 for an injectivity check (refrain from looking at non-injective arguments
666 to type families) or not (do indeed look at those arguments). This is
667 implemented by the uf_int_tf field of UmEnv.
668
669 (It's all a question of whether or not to include equation (7) from Fig. 2
670 of [ITF].)
671
672 This extra parameter is a bit fiddly, perhaps, but seemingly less so than
673 having two separate, almost-identical algorithms.
674
675 Note [Self-substitution when matching]
676 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
677 What should happen when we're *matching* (not unifying) a1 with a1? We
678 should get a substitution [a1 |-> a1]. A successful match should map all
679 the template variables (except ones that disappear when expanding synonyms).
680 But when unifying, we don't want to do this, because we'll then fall into
681 a loop.
682
683 This arrangement affects the code in three places:
684 - If we're matching a refined template variable, don't recur. Instead, just
685 check for equality. That is, if we know [a |-> Maybe a] and are matching
686 (a ~? Maybe Int), we want to just fail.
687
688 - Skip the occurs check when matching. This comes up in two places, because
689 matching against variables is handled separately from matching against
690 full-on types.
691
692 Note that this arrangement was provoked by a real failure, where the same
693 unique ended up in the template as in the target. (It was a rule firing when
694 compiling Data.List.NonEmpty.)
695
696 Note [Matching coercion variables]
697 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
698 Consider this:
699
700 type family F a
701
702 data G a where
703 MkG :: F a ~ Bool => G a
704
705 type family Foo (x :: G a) :: F a
706 type instance Foo MkG = False
707
708 We would like that to be accepted. For that to work, we need to introduce
709 a coercion variable on the left an then use it on the right. Accordingly,
710 at use sites of Foo, we need to be able to use matching to figure out the
711 value for the coercion. (See the desugared version:
712
713 axFoo :: [a :: *, c :: F a ~ Bool]. Foo (MkG c) = False |> (sym c)
714
715 ) We never want this action to happen during *unification* though, when
716 all bets are off.
717
718 Note [Kind coercions in Unify]
719 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
720 We wish to match/unify while ignoring casts. But, we can't just ignore
721 them completely, or we'll end up with ill-kinded substitutions. For example,
722 say we're matching `a` with `ty |> co`. If we just drop the cast, we'll
723 return [a |-> ty], but `a` and `ty` might have different kinds. We can't
724 just match/unify their kinds, either, because this might gratuitously
725 fail. After all, `co` is the witness that the kinds are the same -- they
726 may look nothing alike.
727
728 So, we pass a kind coercion to the match/unify worker. This coercion witnesses
729 the equality between the substed kind of the left-hand type and the substed
730 kind of the right-hand type. Note that we do not unify kinds at the leaves
731 (as we did previously). We thus have
732
733 INVARIANT: In the call
734 unify_ty ty1 ty2 kco
735 it must be that subst(kco) :: subst(kind(ty1)) ~N subst(kind(ty2)), where
736 `subst` is the ambient substitution in the UM monad.
737
738 To get this coercion, we first have to match/unify
739 the kinds before looking at the types. Happily, we need look only one level
740 up, as all kinds are guaranteed to have kind *.
741
742 When we're working with type applications (either TyConApp or AppTy) we
743 need to worry about establishing INVARIANT, as the kinds of the function
744 & arguments aren't (necessarily) included in the kind of the result.
745 When unifying two TyConApps, this is easy, because the two TyCons are
746 the same. Their kinds are thus the same. As long as we unify left-to-right,
747 we'll be sure to unify types' kinds before the types themselves. (For example,
748 think about Proxy :: forall k. k -> *. Unifying the first args matches up
749 the kinds of the second args.)
750
751 For AppTy, we must unify the kinds of the functions, but once these are
752 unified, we can continue unifying arguments without worrying further about
753 kinds.
754
755 The interface to this module includes both "...Ty" functions and
756 "...TyKi" functions. The former assume that INVARIANT is already
757 established, either because the kinds are the same or because the
758 list of types being passed in are the well-typed arguments to some
759 type constructor (see two paragraphs above). The latter take a separate
760 pre-pass over the kinds to establish INVARIANT. Sometimes, it's important
761 not to take the second pass, as it caused #12442.
762
763 We thought, at one point, that this was all unnecessary: why should
764 casts be in types in the first place? But they are sometimes. In
765 dependent/should_compile/KindEqualities2, we see, for example the
766 constraint Num (Int |> (blah ; sym blah)). We naturally want to find
767 a dictionary for that constraint, which requires dealing with
768 coercions in this manner.
769 -}
770
771 -------------- unify_ty: the main workhorse -----------
772
773 unify_ty :: Type -> Type -- Types to be unified and a co
774 -> Coercion -- A coercion between their kinds
775 -- See Note [Kind coercions in Unify]
776 -> UM ()
777 -- See Note [Specification of unification]
778 -- Respects newtypes, PredTypes
779
780 unify_ty ty1 ty2 kco
781 -- TODO: More commentary needed here
782 | Just ty1' <- tcView ty1 = unify_ty ty1' ty2 kco
783 | Just ty2' <- tcView ty2 = unify_ty ty1 ty2' kco
784 | CastTy ty1' co <- ty1 = unify_ty ty1' ty2 (co `mkTransCo` kco)
785 | CastTy ty2' co <- ty2 = unify_ty ty1 ty2' (kco `mkTransCo` mkSymCo co)
786
787 unify_ty (TyVarTy tv1) ty2 kco = uVar tv1 ty2 kco
788 unify_ty ty1 (TyVarTy tv2) kco
789 = do { unif <- amIUnifying
790 ; if unif
791 then umSwapRn $ uVar tv2 ty1 (mkSymCo kco)
792 else surelyApart } -- non-tv on left; tv on right: can't match.
793
794 unify_ty ty1 ty2 _kco
795 | Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
796 , Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
797 = if tc1 == tc2 || (tcIsStarKind ty1 && tcIsStarKind ty2)
798 then if isInjectiveTyCon tc1 Nominal
799 then unify_tys tys1 tys2
800 else do { let inj | isTypeFamilyTyCon tc1
801 = case familyTyConInjectivityInfo tc1 of
802 NotInjective -> repeat False
803 Injective bs -> bs
804 | otherwise
805 = repeat False
806
807 (inj_tys1, noninj_tys1) = partitionByList inj tys1
808 (inj_tys2, noninj_tys2) = partitionByList inj tys2
809
810 ; unify_tys inj_tys1 inj_tys2
811 ; inj_tf <- checkingInjectivity
812 ; unless inj_tf $ -- See (end of) Note [Specification of unification]
813 don'tBeSoSure $ unify_tys noninj_tys1 noninj_tys2 }
814 else -- tc1 /= tc2
815 if isGenerativeTyCon tc1 Nominal && isGenerativeTyCon tc2 Nominal
816 then surelyApart
817 else maybeApart
818
819 -- Applications need a bit of care!
820 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
821 -- NB: we've already dealt with type variables,
822 -- so if one type is an App the other one jolly well better be too
823 unify_ty (AppTy ty1a ty1b) ty2 _kco
824 | Just (ty2a, ty2b) <- tcRepSplitAppTy_maybe ty2
825 = unify_ty_app ty1a [ty1b] ty2a [ty2b]
826
827 unify_ty ty1 (AppTy ty2a ty2b) _kco
828 | Just (ty1a, ty1b) <- tcRepSplitAppTy_maybe ty1
829 = unify_ty_app ty1a [ty1b] ty2a [ty2b]
830
831 unify_ty (LitTy x) (LitTy y) _kco | x == y = return ()
832
833 unify_ty (ForAllTy (TvBndr tv1 _) ty1) (ForAllTy (TvBndr tv2 _) ty2) kco
834 = do { unify_ty (tyVarKind tv1) (tyVarKind tv2) (mkNomReflCo liftedTypeKind)
835 ; umRnBndr2 tv1 tv2 $ unify_ty ty1 ty2 kco }
836
837 -- See Note [Matching coercion variables]
838 unify_ty (CoercionTy co1) (CoercionTy co2) kco
839 = do { unif <- amIUnifying
840 ; c_subst <- getCvSubstEnv
841 ; case co1 of
842 CoVarCo cv
843 | not unif
844 , not (cv `elemVarEnv` c_subst)
845 -> do { b <- tvBindFlagL cv
846 ; if b == BindMe
847 then do { checkRnEnvRCo co2
848 ; let (co_l, co_r) = decomposeFunCo kco
849 -- cv :: t1 ~ t2
850 -- co2 :: s1 ~ s2
851 -- co_l :: t1 ~ s1
852 -- co_r :: t2 ~ s2
853 ; extendCvEnv cv (co_l `mkTransCo`
854 co2 `mkTransCo`
855 mkSymCo co_r) }
856 else return () }
857 _ -> return () }
858
859 unify_ty ty1 _ _
860 | Just (tc1, _) <- splitTyConApp_maybe ty1
861 , not (isGenerativeTyCon tc1 Nominal)
862 = maybeApart
863
864 unify_ty _ ty2 _
865 | Just (tc2, _) <- splitTyConApp_maybe ty2
866 , not (isGenerativeTyCon tc2 Nominal)
867 = do { unif <- amIUnifying
868 ; if unif then maybeApart else surelyApart }
869
870 unify_ty _ _ _ = surelyApart
871
872 unify_ty_app :: Type -> [Type] -> Type -> [Type] -> UM ()
873 unify_ty_app ty1 ty1args ty2 ty2args
874 | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
875 , Just (ty2', ty2a) <- repSplitAppTy_maybe ty2
876 = unify_ty_app ty1' (ty1a : ty1args) ty2' (ty2a : ty2args)
877
878 | otherwise
879 = do { let ki1 = typeKind ty1
880 ki2 = typeKind ty2
881 -- See Note [Kind coercions in Unify]
882 ; unify_ty ki1 ki2 (mkNomReflCo liftedTypeKind)
883 ; unify_ty ty1 ty2 (mkNomReflCo ki1)
884 ; unify_tys ty1args ty2args }
885
886 unify_tys :: [Type] -> [Type] -> UM ()
887 unify_tys orig_xs orig_ys
888 = go orig_xs orig_ys
889 where
890 go [] [] = return ()
891 go (x:xs) (y:ys)
892 -- See Note [Kind coercions in Unify]
893 = do { unify_ty x y (mkNomReflCo $ typeKind x)
894 ; go xs ys }
895 go _ _ = maybeApart -- See Note [Lists of different lengths are MaybeApart]
896
897 ---------------------------------
898 uVar :: TyVar -- Variable to be unified
899 -> Type -- with this Type
900 -> Coercion -- :: kind tv ~N kind ty
901 -> UM ()
902
903 uVar tv1 ty kco
904 = do { -- Check to see whether tv1 is refined by the substitution
905 subst <- getTvSubstEnv
906 ; case (lookupVarEnv subst tv1) of
907 Just ty' -> do { unif <- amIUnifying
908 ; if unif
909 then unify_ty ty' ty kco -- Yes, call back into unify
910 else -- when *matching*, we don't want to just recur here.
911 -- this is because the range of the subst is the target
912 -- type, not the template type. So, just check for
913 -- normal type equality.
914 guard ((ty' `mkCastTy` kco) `eqType` ty) }
915 Nothing -> uUnrefined tv1 ty ty kco } -- No, continue
916
917 uUnrefined :: TyVar -- variable to be unified
918 -> Type -- with this Type
919 -> Type -- (version w/ expanded synonyms)
920 -> Coercion -- :: kind tv ~N kind ty
921 -> UM ()
922
923 -- We know that tv1 isn't refined
924
925 uUnrefined tv1 ty2 ty2' kco
926 | Just ty2'' <- coreView ty2'
927 = uUnrefined tv1 ty2 ty2'' kco -- Unwrap synonyms
928 -- This is essential, in case we have
929 -- type Foo a = a
930 -- and then unify a ~ Foo a
931
932 | TyVarTy tv2 <- ty2'
933 = do { tv1' <- umRnOccL tv1
934 ; tv2' <- umRnOccR tv2
935 ; unif <- amIUnifying
936 -- See Note [Self-substitution when matching]
937 ; when (tv1' /= tv2' || not unif) $ do
938 { subst <- getTvSubstEnv
939 -- Check to see whether tv2 is refined
940 ; case lookupVarEnv subst tv2 of
941 { Just ty' | unif -> uUnrefined tv1 ty' ty' kco
942 ; _ -> do
943 { -- So both are unrefined
944
945 -- And then bind one or the other,
946 -- depending on which is bindable
947 ; b1 <- tvBindFlagL tv1
948 ; b2 <- tvBindFlagR tv2
949 ; let ty1 = mkTyVarTy tv1
950 ; case (b1, b2) of
951 (BindMe, _) -> do { checkRnEnvR ty2 -- make sure ty2 is not a local
952 ; extendTvEnv tv1 (ty2 `mkCastTy` mkSymCo kco) }
953 (_, BindMe) | unif -> do { checkRnEnvL ty1 -- ditto for ty1
954 ; extendTvEnv tv2 (ty1 `mkCastTy` kco) }
955
956 _ | tv1' == tv2' -> return ()
957 -- How could this happen? If we're only matching and if
958 -- we're comparing forall-bound variables.
959
960 _ -> maybeApart -- See Note [Unification with skolems]
961 }}}}
962
963 uUnrefined tv1 ty2 ty2' kco -- ty2 is not a type variable
964 = do { occurs <- elemNiSubstSet tv1 (tyCoVarsOfType ty2')
965 ; unif <- amIUnifying
966 ; if unif && occurs -- See Note [Self-substitution when matching]
967 then maybeApart -- Occurs check, see Note [Fine-grained unification]
968 else do bindTv tv1 (ty2 `mkCastTy` mkSymCo kco) }
969 -- Bind tyvar to the synonym if poss
970
971 elemNiSubstSet :: TyVar -> TyCoVarSet -> UM Bool
972 elemNiSubstSet v set
973 = do { tsubst <- getTvSubstEnv
974 ; return $ v `elemVarSet` niSubstTvSet tsubst set }
975
976 bindTv :: TyVar -> Type -> UM ()
977 bindTv tv ty -- ty is not a variable
978 = do { checkRnEnvR ty -- make sure ty mentions no local variables
979 ; b <- tvBindFlagL tv
980 ; case b of
981 Skolem -> maybeApart -- See Note [Unification with skolems]
982 BindMe -> extendTvEnv tv ty
983 }
984
985 {-
986 %************************************************************************
987 %* *
988 Binding decisions
989 * *
990 ************************************************************************
991 -}
992
993 data BindFlag
994 = BindMe -- A regular type variable
995
996 | Skolem -- This type variable is a skolem constant
997 -- Don't bind it; it only matches itself
998 deriving Eq
999
1000 {-
1001 ************************************************************************
1002 * *
1003 Unification monad
1004 * *
1005 ************************************************************************
1006 -}
1007
1008 data UMEnv = UMEnv { um_bind_fun :: TyVar -> BindFlag
1009 -- the user-supplied BindFlag function
1010 , um_unif :: Bool -- unification (True) or matching?
1011 , um_inj_tf :: Bool -- checking for injectivity?
1012 -- See (end of) Note [Specification of unification]
1013 , um_rn_env :: RnEnv2 }
1014
1015 data UMState = UMState
1016 { um_tv_env :: TvSubstEnv
1017 , um_cv_env :: CvSubstEnv }
1018
1019 newtype UM a = UM { unUM :: UMEnv -> UMState
1020 -> UnifyResultM (UMState, a) }
1021
1022 instance Functor UM where
1023 fmap = liftM
1024
1025 instance Applicative UM where
1026 pure a = UM (\_ s -> pure (s, a))
1027 (<*>) = ap
1028
1029 instance Monad UM where
1030 fail _ = UM (\_ _ -> SurelyApart) -- failed pattern match
1031 m >>= k = UM (\env state ->
1032 do { (state', v) <- unUM m env state
1033 ; unUM (k v) env state' })
1034
1035 -- need this instance because of a use of 'guard' above
1036 instance Alternative UM where
1037 empty = UM (\_ _ -> Control.Applicative.empty)
1038 m1 <|> m2 = UM (\env state ->
1039 unUM m1 env state <|>
1040 unUM m2 env state)
1041
1042 instance MonadPlus UM
1043
1044 #if __GLASGOW_HASKELL__ > 710
1045 instance MonadFail.MonadFail UM where
1046 fail _ = UM (\_tvs _subst -> SurelyApart) -- failed pattern match
1047 #endif
1048
1049 initUM :: (TyVar -> BindFlag)
1050 -> Bool -- True <=> unify; False <=> match
1051 -> Bool -- True <=> doing an injectivity check
1052 -> RnEnv2
1053 -> TvSubstEnv -- subst to extend
1054 -> CvSubstEnv
1055 -> UM a -> UnifyResultM a
1056 initUM badtvs unif inj_tf rn_env subst_env cv_subst_env um
1057 = case unUM um env state of
1058 Unifiable (_, subst) -> Unifiable subst
1059 MaybeApart (_, subst) -> MaybeApart subst
1060 SurelyApart -> SurelyApart
1061 where
1062 env = UMEnv { um_bind_fun = badtvs
1063 , um_unif = unif
1064 , um_inj_tf = inj_tf
1065 , um_rn_env = rn_env }
1066 state = UMState { um_tv_env = subst_env
1067 , um_cv_env = cv_subst_env }
1068
1069 tvBindFlagL :: TyVar -> UM BindFlag
1070 tvBindFlagL tv = UM $ \env state ->
1071 Unifiable (state, if inRnEnvL (um_rn_env env) tv
1072 then Skolem
1073 else um_bind_fun env tv)
1074
1075 tvBindFlagR :: TyVar -> UM BindFlag
1076 tvBindFlagR tv = UM $ \env state ->
1077 Unifiable (state, if inRnEnvR (um_rn_env env) tv
1078 then Skolem
1079 else um_bind_fun env tv)
1080
1081 getTvSubstEnv :: UM TvSubstEnv
1082 getTvSubstEnv = UM $ \_ state -> Unifiable (state, um_tv_env state)
1083
1084 getCvSubstEnv :: UM CvSubstEnv
1085 getCvSubstEnv = UM $ \_ state -> Unifiable (state, um_cv_env state)
1086
1087 extendTvEnv :: TyVar -> Type -> UM ()
1088 extendTvEnv tv ty = UM $ \_ state ->
1089 Unifiable (state { um_tv_env = extendVarEnv (um_tv_env state) tv ty }, ())
1090
1091 extendCvEnv :: CoVar -> Coercion -> UM ()
1092 extendCvEnv cv co = UM $ \_ state ->
1093 Unifiable (state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())
1094
1095 umRnBndr2 :: TyCoVar -> TyCoVar -> UM a -> UM a
1096 umRnBndr2 v1 v2 thing = UM $ \env state ->
1097 let rn_env' = rnBndr2 (um_rn_env env) v1 v2 in
1098 unUM thing (env { um_rn_env = rn_env' }) state
1099
1100 checkRnEnv :: (RnEnv2 -> VarEnv Var) -> VarSet -> UM ()
1101 checkRnEnv get_set varset = UM $ \env state ->
1102 let env_vars = get_set (um_rn_env env) in
1103 if isEmptyVarEnv env_vars || (getUniqSet varset `disjointVarEnv` env_vars)
1104 -- NB: That isEmptyVarSet is a critical optimization; it
1105 -- means we don't have to calculate the free vars of
1106 -- the type, often saving quite a bit of allocation.
1107 then Unifiable (state, ())
1108 else MaybeApart (state, ())
1109
1110 -- | Converts any SurelyApart to a MaybeApart
1111 don'tBeSoSure :: UM () -> UM ()
1112 don'tBeSoSure um = UM $ \env state ->
1113 case unUM um env state of
1114 SurelyApart -> MaybeApart (state, ())
1115 other -> other
1116
1117 checkRnEnvR :: Type -> UM ()
1118 checkRnEnvR ty = checkRnEnv rnEnvR (tyCoVarsOfType ty)
1119
1120 checkRnEnvL :: Type -> UM ()
1121 checkRnEnvL ty = checkRnEnv rnEnvL (tyCoVarsOfType ty)
1122
1123 checkRnEnvRCo :: Coercion -> UM ()
1124 checkRnEnvRCo co = checkRnEnv rnEnvR (tyCoVarsOfCo co)
1125
1126 umRnOccL :: TyVar -> UM TyVar
1127 umRnOccL v = UM $ \env state ->
1128 Unifiable (state, rnOccL (um_rn_env env) v)
1129
1130 umRnOccR :: TyVar -> UM TyVar
1131 umRnOccR v = UM $ \env state ->
1132 Unifiable (state, rnOccR (um_rn_env env) v)
1133
1134 umSwapRn :: UM a -> UM a
1135 umSwapRn thing = UM $ \env state ->
1136 let rn_env' = rnSwap (um_rn_env env) in
1137 unUM thing (env { um_rn_env = rn_env' }) state
1138
1139 amIUnifying :: UM Bool
1140 amIUnifying = UM $ \env state -> Unifiable (state, um_unif env)
1141
1142 checkingInjectivity :: UM Bool
1143 checkingInjectivity = UM $ \env state -> Unifiable (state, um_inj_tf env)
1144
1145 maybeApart :: UM ()
1146 maybeApart = UM (\_ state -> MaybeApart (state, ()))
1147
1148 surelyApart :: UM a
1149 surelyApart = UM (\_ _ -> SurelyApart)
1150
1151 {-
1152 %************************************************************************
1153 %* *
1154 Matching a (lifted) type against a coercion
1155 %* *
1156 %************************************************************************
1157
1158 This section defines essentially an inverse to liftCoSubst. It is defined
1159 here to avoid a dependency from Coercion on this module.
1160
1161 -}
1162
1163 data MatchEnv = ME { me_tmpls :: TyVarSet
1164 , me_env :: RnEnv2 }
1165
1166 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
1167 -- @liftCoMatch vars ty co == Just s@, then @listCoSubst s ty == co@,
1168 -- where @==@ there means that the result of 'liftCoSubst' has the same
1169 -- type as the original co; but may be different under the hood.
1170 -- That is, it matches a type against a coercion of the same
1171 -- "shape", and returns a lifting substitution which could have been
1172 -- used to produce the given coercion from the given type.
1173 -- Note that this function is incomplete -- it might return Nothing
1174 -- when there does indeed exist a possible lifting context.
1175 --
1176 -- This function is incomplete in that it doesn't respect the equality
1177 -- in `eqType`. That is, it's possible that this will succeed for t1 and
1178 -- fail for t2, even when t1 `eqType` t2. That's because it depends on
1179 -- there being a very similar structure between the type and the coercion.
1180 -- This incompleteness shouldn't be all that surprising, especially because
1181 -- it depends on the structure of the coercion, which is a silly thing to do.
1182 --
1183 -- The lifting context produced doesn't have to be exacting in the roles
1184 -- of the mappings. This is because any use of the lifting context will
1185 -- also require a desired role. Thus, this algorithm prefers mapping to
1186 -- nominal coercions where it can do so.
1187 liftCoMatch :: TyCoVarSet -> Type -> Coercion -> Maybe LiftingContext
1188 liftCoMatch tmpls ty co
1189 = do { cenv1 <- ty_co_match menv emptyVarEnv ki ki_co ki_ki_co ki_ki_co
1190 ; cenv2 <- ty_co_match menv cenv1 ty co
1191 (mkNomReflCo co_lkind) (mkNomReflCo co_rkind)
1192 ; return (LC (mkEmptyTCvSubst in_scope) cenv2) }
1193 where
1194 menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
1195 in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
1196 -- Like tcMatchTy, assume all the interesting variables
1197 -- in ty are in tmpls
1198
1199 ki = typeKind ty
1200 ki_co = promoteCoercion co
1201 ki_ki_co = mkNomReflCo liftedTypeKind
1202
1203 Pair co_lkind co_rkind = coercionKind ki_co
1204
1205 -- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
1206 ty_co_match :: MatchEnv -- ^ ambient helpful info
1207 -> LiftCoEnv -- ^ incoming subst
1208 -> Type -- ^ ty, type to match
1209 -> Coercion -- ^ co, coercion to match against
1210 -> Coercion -- ^ :: kind of L type of substed ty ~N L kind of co
1211 -> Coercion -- ^ :: kind of R type of substed ty ~N R kind of co
1212 -> Maybe LiftCoEnv
1213 ty_co_match menv subst ty co lkco rkco
1214 | Just ty' <- coreView ty = ty_co_match menv subst ty' co lkco rkco
1215
1216 -- handle Refl case:
1217 | tyCoVarsOfType ty `isNotInDomainOf` subst
1218 , Just (ty', _) <- isReflCo_maybe co
1219 , ty `eqType` ty'
1220 = Just subst
1221
1222 where
1223 isNotInDomainOf :: VarSet -> VarEnv a -> Bool
1224 isNotInDomainOf set env
1225 = noneSet (\v -> elemVarEnv v env) set
1226
1227 noneSet :: (Var -> Bool) -> VarSet -> Bool
1228 noneSet f = allVarSet (not . f)
1229
1230 ty_co_match menv subst ty co lkco rkco
1231 | CastTy ty' co' <- ty
1232 = ty_co_match menv subst ty' co (co' `mkTransCo` lkco) (co' `mkTransCo` rkco)
1233
1234 | CoherenceCo co1 co2 <- co
1235 = ty_co_match menv subst ty co1 (lkco `mkTransCo` mkSymCo co2) rkco
1236
1237 | SymCo co' <- co
1238 = swapLiftCoEnv <$> ty_co_match menv (swapLiftCoEnv subst) ty co' rkco lkco
1239
1240 -- Match a type variable against a non-refl coercion
1241 ty_co_match menv subst (TyVarTy tv1) co lkco rkco
1242 | Just co1' <- lookupVarEnv subst tv1' -- tv1' is already bound to co1
1243 = if eqCoercionX (nukeRnEnvL rn_env) co1' co
1244 then Just subst
1245 else Nothing -- no match since tv1 matches two different coercions
1246
1247 | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
1248 = if any (inRnEnvR rn_env) (tyCoVarsOfCoList co)
1249 then Nothing -- occurs check failed
1250 else Just $ extendVarEnv subst tv1' $
1251 castCoercionKind co (mkSymCo lkco) (mkSymCo rkco)
1252
1253 | otherwise
1254 = Nothing
1255
1256 where
1257 rn_env = me_env menv
1258 tv1' = rnOccL rn_env tv1
1259
1260 -- just look through SubCo's. We don't really care about roles here.
1261 ty_co_match menv subst ty (SubCo co) lkco rkco
1262 = ty_co_match menv subst ty co lkco rkco
1263
1264 ty_co_match menv subst (AppTy ty1a ty1b) co _lkco _rkco
1265 | Just (co2, arg2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy
1266 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1267 ty_co_match menv subst ty1 (AppCo co2 arg2) _lkco _rkco
1268 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
1269 -- yes, the one from Type, not TcType; this is for coercion optimization
1270 = ty_co_match_app menv subst ty1a [ty1b] co2 [arg2]
1271
1272 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos) _lkco _rkco
1273 = ty_co_match_tc menv subst tc1 tys tc2 cos
1274 ty_co_match menv subst (FunTy ty1 ty2) co _lkco _rkco
1275 -- Despite the fact that (->) is polymorphic in four type variables (two
1276 -- runtime rep and two types), we shouldn't need to explicitly unify the
1277 -- runtime reps here; unifying the types themselves should be sufficient.
1278 -- See Note [Representation of function types].
1279 | Just (tc, [_,_,co1,co2]) <- splitTyConAppCo_maybe co
1280 , tc == funTyCon
1281 = let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) [co1,co2]
1282 in ty_co_match_args menv subst [ty1, ty2] [co1, co2] lkcos rkcos
1283
1284 ty_co_match menv subst (ForAllTy (TvBndr tv1 _) ty1)
1285 (ForAllCo tv2 kind_co2 co2)
1286 lkco rkco
1287 = do { subst1 <- ty_co_match menv subst (tyVarKind tv1) kind_co2
1288 ki_ki_co ki_ki_co
1289 ; let rn_env0 = me_env menv
1290 rn_env1 = rnBndr2 rn_env0 tv1 tv2
1291 menv' = menv { me_env = rn_env1 }
1292 ; ty_co_match menv' subst1 ty1 co2 lkco rkco }
1293 where
1294 ki_ki_co = mkNomReflCo liftedTypeKind
1295
1296 ty_co_match _ subst (CoercionTy {}) _ _ _
1297 = Just subst -- don't inspect coercions
1298
1299 ty_co_match menv subst ty co lkco rkco
1300 | Just co' <- pushRefl co = ty_co_match menv subst ty co' lkco rkco
1301 | otherwise = Nothing
1302
1303 ty_co_match_tc :: MatchEnv -> LiftCoEnv
1304 -> TyCon -> [Type]
1305 -> TyCon -> [Coercion]
1306 -> Maybe LiftCoEnv
1307 ty_co_match_tc menv subst tc1 tys1 tc2 cos2
1308 = do { guard (tc1 == tc2)
1309 ; ty_co_match_args menv subst tys1 cos2 lkcos rkcos }
1310 where
1311 Pair lkcos rkcos
1312 = traverse (fmap mkNomReflCo . coercionKind) cos2
1313
1314 ty_co_match_app :: MatchEnv -> LiftCoEnv
1315 -> Type -> [Type] -> Coercion -> [Coercion]
1316 -> Maybe LiftCoEnv
1317 ty_co_match_app menv subst ty1 ty1args co2 co2args
1318 | Just (ty1', ty1a) <- repSplitAppTy_maybe ty1
1319 , Just (co2', co2a) <- splitAppCo_maybe co2
1320 = ty_co_match_app menv subst ty1' (ty1a : ty1args) co2' (co2a : co2args)
1321
1322 | otherwise
1323 = do { subst1 <- ty_co_match menv subst ki1 ki2 ki_ki_co ki_ki_co
1324 ; let Pair lkco rkco = mkNomReflCo <$> coercionKind ki2
1325 ; subst2 <- ty_co_match menv subst1 ty1 co2 lkco rkco
1326 ; let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) co2args
1327 ; ty_co_match_args menv subst2 ty1args co2args lkcos rkcos }
1328 where
1329 ki1 = typeKind ty1
1330 ki2 = promoteCoercion co2
1331 ki_ki_co = mkNomReflCo liftedTypeKind
1332
1333 ty_co_match_args :: MatchEnv -> LiftCoEnv -> [Type]
1334 -> [Coercion] -> [Coercion] -> [Coercion]
1335 -> Maybe LiftCoEnv
1336 ty_co_match_args _ subst [] [] _ _ = Just subst
1337 ty_co_match_args menv subst (ty:tys) (arg:args) (lkco:lkcos) (rkco:rkcos)
1338 = do { subst' <- ty_co_match menv subst ty arg lkco rkco
1339 ; ty_co_match_args menv subst' tys args lkcos rkcos }
1340 ty_co_match_args _ _ _ _ _ _ = Nothing
1341
1342 pushRefl :: Coercion -> Maybe Coercion
1343 pushRefl (Refl Nominal (AppTy ty1 ty2))
1344 = Just (AppCo (Refl Nominal ty1) (mkNomReflCo ty2))
1345 pushRefl (Refl r (FunTy ty1 ty2))
1346 | Just rep1 <- getRuntimeRep_maybe ty1
1347 , Just rep2 <- getRuntimeRep_maybe ty2
1348 = Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2
1349 , mkReflCo r ty1, mkReflCo r ty2 ])
1350 pushRefl (Refl r (TyConApp tc tys))
1351 = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
1352 pushRefl (Refl r (ForAllTy (TvBndr tv _) ty))
1353 = Just (mkHomoForAllCos_NoRefl [tv] (Refl r ty))
1354 -- NB: NoRefl variant. Otherwise, we get a loop!
1355 pushRefl (Refl r (CastTy ty co)) = Just (castCoercionKind (Refl r ty) co co)
1356 pushRefl _ = Nothing