3 mkCanonical, mkCanonicals, mkCanonicalFEV, mkCanonicalFEVs, canWanteds, canGivens,
4 canOccursCheck, canEqToWorkList,
8 #include "HsVersions.h"
14 import qualified TcMType as TcM
23 import VarEnv ( TidyEnv )
25 import Control.Monad ( unless, when, zipWithM, zipWithM_ )
27 import Control.Applicative ( (<|>) )
37 Note [Canonicalisation]
38 ~~~~~~~~~~~~~~~~~~~~~~~
39 * Converts (Constraint f) _which_does_not_contain_proper_implications_ to CanonicalCts
40 * Unary: treats individual constraints one at a time
41 * Does not do any zonking
42 * Lives in TcS monad so that it can create new skolem variables
45 %************************************************************************
47 %* Flattening (eliminating all function symbols) *
49 %************************************************************************
53 flatten ty ==> (xi, cc)
55 xi has no type functions
56 cc = Auxiliary given (equality) constraints constraining
57 the fresh type variables in xi. Evidence for these
58 is always the identity coercion, because internally the
59 fresh flattening skolem variables are actually identified
60 with the types they have been generated to stand in for.
62 Note that it is flatten's job to flatten *every type function it sees*.
63 flatten is only called on *arguments* to type functions, by canEqGiven.
65 Recall that in comments we use alpha[flat = ty] to represent a
66 flattening skolem variable alpha which has been generated to stand in
69 ----- Example of flattening a constraint: ------
70 flatten (List (F (G Int))) ==> (xi, cc)
73 cc = { G Int ~ beta[flat = G Int],
74 F beta ~ alpha[flat = F beta] }
76 * alpha and beta are 'flattening skolem variables'.
77 * All the constraints in cc are 'given', and all their coercion terms
80 NB: Flattening Skolems only occur in canonical constraints, which
81 are never zonked, so we don't need to worry about zonking doing
82 accidental unflattening.
84 Note that we prefer to leave type synonyms unexpanded when possible,
85 so when the flattener encounters one, it first asks whether its
86 transitive expansion contains any type function applications. If so,
87 it expands the synonym and proceeds; if not, it simply returns the
90 TODO: caching the information about whether transitive synonym
91 expansions contain any type function applications would speed things
92 up a bit; right now we waste a lot of energy traversing the same types
98 -- Flatten a bunch of types all at once.
99 flattenMany :: CtFlavor -> [Type] -> TcS ([Xi], [Coercion], CanonicalCts)
100 -- Coercions :: Xi ~ Type
102 = do { (xis, cos, cts_s) <- mapAndUnzip3M (flatten ctxt) tys
103 ; return (xis, cos, andCCans cts_s) }
105 -- Flatten a type to get rid of type function applications, returning
106 -- the new type-function-free type, and a collection of new equality
107 -- constraints. See Note [Flattening] for more detail.
108 flatten :: CtFlavor -> TcType -> TcS (Xi, Coercion, CanonicalCts)
109 -- Postcondition: Coercion :: Xi ~ TcType
111 | Just ty' <- tcView ty
112 = do { (xi, co, ccs) <- flatten ctxt ty'
113 -- Preserve type synonyms if possible
114 -- We can tell if ty' is function-free by
115 -- whether there are any floated constraints
116 ; if isIdentityCoercion co then
117 return (ty, ty, emptyCCan)
119 return (xi, co, ccs) }
121 flatten _ v@(TyVarTy _)
122 = return (v, v, emptyCCan)
124 flatten ctxt (AppTy ty1 ty2)
125 = do { (xi1,co1,c1) <- flatten ctxt ty1
126 ; (xi2,co2,c2) <- flatten ctxt ty2
127 ; return (mkAppTy xi1 xi2, mkAppCoercion co1 co2, c1 `andCCan` c2) }
129 flatten ctxt (FunTy ty1 ty2)
130 = do { (xi1,co1,c1) <- flatten ctxt ty1
131 ; (xi2,co2,c2) <- flatten ctxt ty2
132 ; return (mkFunTy xi1 xi2, mkFunCoercion co1 co2, c1 `andCCan` c2) }
134 flatten fl (TyConApp tc tys)
135 -- For a normal type constructor or data family application, we just
136 -- recursively flatten the arguments.
137 | not (isSynFamilyTyCon tc)
138 = do { (xis,cos,ccs) <- flattenMany fl tys
139 ; return (mkTyConApp tc xis, mkTyConCoercion tc cos, ccs) }
141 -- Otherwise, it's a type function application, and we have to
142 -- flatten it away as well, and generate a new given equality constraint
143 -- between the application and a newly generated flattening skolem variable.
145 = ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated
146 do { (xis, cos, ccs) <- flattenMany fl tys
147 ; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis
148 (cos_args, cos_rest) = splitAt (tyConArity tc) cos
149 -- The type function might be *over* saturated
150 -- in which case the remaining arguments should
151 -- be dealt with by AppTys
152 fam_ty = mkTyConApp tc xi_args
153 fam_co = fam_ty -- identity
154 ; (ret_co, rhs_var, ct) <-
155 do { is_cached <- lookupFlatCacheMap tc xi_args fl
157 Just (rhs_var,ret_co,_fl) -> return (ret_co, rhs_var, emptyCCan)
159 | isGivenOrSolved fl ->
160 do { rhs_var <- newFlattenSkolemTy fam_ty
161 ; cv <- newGivenCoVar fam_ty rhs_var fam_co
162 ; let ct = CFunEqCan { cc_id = cv
163 , cc_flavor = fl -- Given
165 , cc_tyargs = xi_args
167 ; let ret_co = mkCoVarCoercion cv
168 ; updateFlatCacheMap tc xi_args rhs_var fl ret_co
169 ; return $ (ret_co, rhs_var, singleCCan ct) }
171 -- Derived or Wanted: make a new *unification* flatten variable
172 do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
173 ; cv <- newCoVar fam_ty rhs_var
174 ; let ct = CFunEqCan { cc_id = cv
175 , cc_flavor = mkWantedFlavor fl
176 -- Always Wanted, not Derived
178 , cc_tyargs = xi_args
180 ; let ret_co = mkCoVarCoercion cv
181 ; updateFlatCacheMap tc xi_args rhs_var fl ret_co
182 ; return $ (ret_co, rhs_var, singleCCan ct) } }
183 ; return ( foldl AppTy rhs_var xi_rest
184 , foldl AppTy (mkSymCoercion ret_co
185 `mkTransCoercion` mkTyConCoercion tc cos_args) cos_rest
186 , ccs `andCCan` ct) }
189 flatten ctxt (PredTy pred)
190 = do { (pred', co, ccs) <- flattenPred ctxt pred
191 ; return (PredTy pred', co, ccs) }
193 flatten ctxt ty@(ForAllTy {})
194 -- We allow for-alls when, but only when, no type function
195 -- applications inside the forall involve the bound type variables
196 -- TODO: What if it is a (t1 ~ t2) => t3
197 -- Must revisit when the New Coercion API is here!
198 = do { let (tvs, rho) = splitForAllTys ty
199 ; (rho', co, ccs) <- flatten ctxt rho
200 ; let bad_eqs = filterBag is_bad ccs
201 is_bad c = tyVarsOfCanonical c `intersectsVarSet` tv_set
202 tv_set = mkVarSet tvs
203 ; unless (isEmptyBag bad_eqs)
204 (flattenForAllErrorTcS ctxt ty bad_eqs)
205 ; return (mkForAllTys tvs rho', mkForAllTys tvs co, ccs) }
208 flattenPred :: CtFlavor -> TcPredType -> TcS (TcPredType, Coercion, CanonicalCts)
209 flattenPred ctxt (ClassP cls tys)
210 = do { (tys', cos, ccs) <- flattenMany ctxt tys
211 ; return (ClassP cls tys', mkClassPPredCo cls cos, ccs) }
212 flattenPred ctxt (IParam nm ty)
213 = do { (ty', co, ccs) <- flatten ctxt ty
214 ; return (IParam nm ty', mkIParamPredCo nm co, ccs) }
215 -- TODO: Handling of coercions between EqPreds must be revisited once the New Coercion API is ready!
216 flattenPred ctxt (EqPred ty1 ty2)
217 = do { (ty1', co1, ccs1) <- flatten ctxt ty1
218 ; (ty2', co2, ccs2) <- flatten ctxt ty2
219 ; return (EqPred ty1' ty2', mkEqPredCo co1 co2, ccs1 `andCCan` ccs2) }
223 %************************************************************************
225 %* Canonicalising given constraints *
227 %************************************************************************
230 canWanteds :: [WantedEvVar] -> TcS WorkList
231 canWanteds = fmap unionWorkLists . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
233 canGivens :: GivenLoc -> [EvVar] -> TcS WorkList
234 canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc GivenOrig)) givens
235 ; return (unionWorkLists ccs) }
237 mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList
238 mkCanonicals fl vs = fmap unionWorkLists (mapM (mkCanonical fl) vs)
240 mkCanonicalFEV :: FlavoredEvVar -> TcS WorkList
241 mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev
243 mkCanonicalFEVs :: Bag FlavoredEvVar -> TcS WorkList
244 mkCanonicalFEVs = foldrBagM canon_one emptyWorkList
245 where -- Preserves order (shouldn't be important, but curently
246 -- is important for the vectoriser)
247 canon_one fev wl = do { wl' <- mkCanonicalFEV fev
248 ; return (unionWorkList wl' wl) }
251 mkCanonical :: CtFlavor -> EvVar -> TcS WorkList
252 mkCanonical fl ev = case evVarPred ev of
253 ClassP clas tys -> canClassToWorkList fl ev clas tys
254 IParam ip ty -> canIPToWorkList fl ev ip ty
255 EqPred ty1 ty2 -> canEqToWorkList fl ev ty1 ty2
258 canClassToWorkList :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS WorkList
259 canClassToWorkList fl v cn tys
260 = do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys
261 ; let no_flattening_happened = all isIdentityCoercion cos
262 dict_co = mkTyConCoercion (classTyCon cn) cos
263 ; v_new <- if no_flattening_happened then return v
264 else if isGivenOrSolved fl then return v
265 -- The cos are all identities if fl=Given,
266 -- hence nothing to do
267 else do { v' <- newDictVar cn xis -- D xis
268 ; when (isWanted fl) $ setDictBind v (EvCast v' dict_co)
269 ; when (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCoercion dict_co))
270 -- NB: No more setting evidence for derived now
273 -- Add the superclasses of this one here, See Note [Adding superclasses].
274 -- But only if we are not simplifying the LHS of a rule.
275 ; sctx <- getTcSContext
276 ; sc_cts <- if simplEqsOnly sctx then return emptyWorkList
277 else newSCWorkFromFlavored v_new fl cn xis
279 ; return (sc_cts `unionWorkList`
280 workListFromEqs ccs `unionWorkList`
281 workListFromNonEq CDictCan { cc_id = v_new
284 , cc_tyargs = xis }) }
287 Note [Adding superclasses]
288 ~~~~~~~~~~~~~~~~~~~~~~~~~~
289 Since dictionaries are canonicalized only once in their lifetime, the
290 place to add their superclasses is canonicalisation (The alternative
291 would be to do it during constraint solving, but we'd have to be
292 extremely careful to not repeatedly introduced the same superclass in
293 our worklist). Here is what we do:
296 We add all their superclasses as Givens.
299 Generally speaking we want to be able to add superclasses of
300 wanteds for two reasons:
302 (1) Oportunities for improvement. Example:
303 class (a ~ b) => C a b
304 Wanted constraint is: C alpha beta
305 We'd like to simply have C alpha alpha. Similar
306 situations arise in relation to functional dependencies.
308 (2) To have minimal constraints to quantify over:
309 For instance, if our wanted constraint is (Eq a, Ord a)
310 we'd only like to quantify over Ord a.
312 To deal with (1) above we only add the superclasses of wanteds
313 which may lead to improvement, that is: equality superclasses or
314 superclasses with functional dependencies.
316 We deal with (2) completely independently in TcSimplify. See
317 Note [Minimize by SuperClasses] in TcSimplify.
320 Moreover, in all cases the extra improvement constraints are
321 Derived. Derived constraints have an identity (for now), but
322 we don't do anything with their evidence. For instance they
323 are never used to rewrite other constraints.
325 See also [New Wanted Superclass Work] in TcInteract.
331 Here's an example that demonstrates why we chose to NOT add
332 superclasses during simplification: [Comes from ticket #4497]
334 class Num (RealOf t) => Normed t
337 Assume the generated wanted constraint is:
338 RealOf e ~ e, Normed e
339 If we were to be adding the superclasses during simplification we'd get:
340 Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf
342 e ~ uf, Num uf, Normed e, RealOf e ~ e
343 ==> [Spontaneous solve]
344 Num uf, Normed uf, RealOf uf ~ uf
346 While looks exactly like our original constraint. If we add the superclass again we'd loop.
347 By adding superclasses definitely only once, during canonicalisation, this situation can't
352 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
353 -- Returns superclasses, see Note [Adding superclasses]
354 newSCWorkFromFlavored ev orig_flavor cls xis
355 | isDerived orig_flavor
356 = return emptyWorkList -- Deriveds don't yield more superclasses because we will
357 -- add them transitively in the case of wanteds.
359 | Just gk <- isGiven_maybe orig_flavor
361 GivenOrig -> do { let sc_theta = immSuperClasses cls xis
363 ; sc_vars <- mapM newEvVar sc_theta
364 ; _ <- zipWithM_ setEvBind sc_vars [EvSuperClass ev n | n <- [0..]]
365 ; mkCanonicals flavor sc_vars }
366 GivenSolved -> return emptyWorkList
367 -- Seems very dangerous to add the superclasses for dictionaries that may be
368 -- partially solved because we may end up with evidence loops.
370 | isEmptyVarSet (tyVarsOfTypes xis)
371 = return emptyWorkList -- Wanteds with no variables yield no deriveds.
372 -- See Note [Improvement from Ground Wanteds]
374 | otherwise -- Wanted case, just add those SC that can lead to improvement.
375 = do { let sc_rec_theta = transSuperClasses cls xis
376 impr_theta = filter is_improvement_pty sc_rec_theta
377 Wanted wloc = orig_flavor
378 ; der_ids <- mapM newDerivedId impr_theta
379 ; mkCanonicals (Derived wloc) der_ids }
382 is_improvement_pty :: PredType -> Bool
383 -- Either it's an equality, or has some functional dependency
384 is_improvement_pty (EqPred {}) = True
385 is_improvement_pty (ClassP cls _ty) = not $ null fundeps
386 where (_,fundeps,_,_,_,_) = classExtraBigSig cls
387 is_improvement_pty _ = False
392 canIPToWorkList :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS WorkList
393 -- See Note [Canonical implicit parameter constraints] to see why we don't
394 -- immediately canonicalize (flatten) IP constraints.
395 canIPToWorkList fl v nm ty
396 = return $ workListFromNonEq (CIPCan { cc_id = v
402 canEqToWorkList :: CtFlavor -> EvVar -> Type -> Type -> TcS WorkList
403 canEqToWorkList fl cv ty1 ty2 = do { cts <- canEq fl cv ty1 ty2
404 ; return $ workListFromEqs cts }
406 canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts
408 | tcEqType ty1 ty2 -- Dealing with equality here avoids
409 -- later spurious occurs checks for a~a
410 = do { when (isWanted fl) (setCoBind cv ty1)
413 -- If one side is a variable, orient and flatten,
414 -- WITHOUT expanding type synonyms, so that we tend to
415 -- substitute a ~ Age rather than a ~ Int when @type Age = Int@
416 canEq fl cv ty1@(TyVarTy {}) ty2
417 = do { untch <- getUntouchables
418 ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
419 canEq fl cv ty1 ty2@(TyVarTy {})
420 = do { untch <- getUntouchables
421 ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
422 -- NB: don't use VarCls directly because tv1 or tv2 may be scolems!
424 canEq fl cv (TyConApp fn tys) ty2
425 | isSynFamilyTyCon fn, length tys == tyConArity fn
426 = do { untch <- getUntouchables
427 ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) }
428 canEq fl cv ty1 (TyConApp fn tys)
429 | isSynFamilyTyCon fn, length tys == tyConArity fn
430 = do { untch <- getUntouchables
431 ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) }
434 | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe s1,
435 Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2
437 <- if isWanted fl then -- Wanted
438 do { v1 <- newCoVar t1a t2a
439 ; v2 <- newCoVar t1b t2b
440 ; v3 <- newCoVar t1c t2c
441 ; let res_co = mkCoPredCo (mkCoVarCoercion v1)
442 (mkCoVarCoercion v2) (mkCoVarCoercion v3)
443 ; setCoBind cv res_co
444 ; return (v1,v2,v3) }
445 else if isGivenOrSolved fl then -- Given
446 let co_orig = mkCoVarCoercion cv
447 coa = mkCsel1Coercion co_orig
448 cob = mkCsel2Coercion co_orig
449 coc = mkCselRCoercion co_orig
450 in do { v1 <- newGivenCoVar t1a t2a coa
451 ; v2 <- newGivenCoVar t1b t2b cob
452 ; v3 <- newGivenCoVar t1c t2c coc
453 ; return (v1,v2,v3) }
455 do { v1 <- newDerivedId (EqPred t1a t2a)
456 ; v2 <- newDerivedId (EqPred t1b t2b)
457 ; v3 <- newDerivedId (EqPred t1c t2c)
458 ; return (v1,v2,v3) }
459 ; cc1 <- canEq fl v1 t1a t2a
460 ; cc2 <- canEq fl v2 t1b t2b
461 ; cc3 <- canEq fl v3 t1c t2c
462 ; return (cc1 `andCCan` cc2 `andCCan` cc3) }
465 -- Split up an equality between function types into two equalities.
466 canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
467 = do { (argv, resv) <-
469 do { argv <- newCoVar s1 s2
470 ; resv <- newCoVar t1 t2
472 mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv)
473 ; return (argv,resv) }
475 else if isGivenOrSolved fl then
476 let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv)
477 in do { argv <- newGivenCoVar s1 s2 arg
478 ; resv <- newGivenCoVar t1 t2 res
479 ; return (argv,resv) }
482 do { argv <- newDerivedId (EqPred s1 s2)
483 ; resv <- newDerivedId (EqPred t1 t2)
484 ; return (argv,resv) }
486 ; cc1 <- canEq fl argv s1 s2 -- inherit original kinds and locations
487 ; cc2 <- canEq fl resv t1 t2
488 ; return (cc1 `andCCan` cc2) }
490 canEq fl cv (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2))
492 = if isWanted fl then
493 do { v <- newCoVar t1 t2
494 ; setCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv)
496 else return emptyCCan -- DV: How to decompose given IP coercions?
498 canEq fl cv (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2))
500 = if isWanted fl then
501 do { vs <- zipWithM newCoVar tys1 tys2
502 ; setCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs)
503 ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2
505 else return emptyCCan
506 -- How to decompose given dictionary (and implicit parameter) coercions?
507 -- You may think that the following is right:
508 -- let cos = decomposeCo (length tys1) (mkCoVarCoercion cv)
509 -- in zipWith3M newGivOrDerCoVar tys1 tys2 cos
510 -- But this assumes that the coercion is a type constructor-based
511 -- coercion, and not a PredTy (ClassP cn cos) coercion. So we chose
512 -- to not decompose these coercions. We have to get back to this
513 -- when we clean up the Coercion API.
515 canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
516 | isAlgTyCon tc1 && isAlgTyCon tc2
518 , length tys1 == length tys2
519 = -- Generate equalities for each of the corresponding arguments
521 <- if isWanted fl then
522 do { argsv <- zipWithM newCoVar tys1 tys2
524 mkTyConCoercion tc1 (map mkCoVarCoercion argsv)
527 else if isGivenOrSolved fl then
528 let cos = decomposeCo (length tys1) (mkCoVarCoercion cv)
529 in zipWith3M newGivenCoVar tys1 tys2 cos
532 zipWithM (\t1 t2 -> newDerivedId (EqPred t1 t2)) tys1 tys2
534 ; andCCans <$> zipWith3M (canEq fl) argsv tys1 tys2 }
536 -- See Note [Equality between type applications]
537 -- Note [Care with type applications] in TcUnify
539 | Just (s1,t1) <- tcSplitAppTy_maybe ty1
540 , Just (s2,t2) <- tcSplitAppTy_maybe ty2
543 then do { cv1 <- newCoVar s1 s2
544 ; cv2 <- newCoVar t1 t2
546 mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2)
549 else if isGivenOrSolved fl then
550 let co1 = mkLeftCoercion $ mkCoVarCoercion cv
551 co2 = mkRightCoercion $ mkCoVarCoercion cv
552 in do { cv1 <- newGivenCoVar s1 s2 co1
553 ; cv2 <- newGivenCoVar t1 t2 co2
556 do { cv1 <- newDerivedId (EqPred s1 s2)
557 ; cv2 <- newDerivedId (EqPred t1 t2)
560 ; cc1 <- canEq fl cv1 s1 s2
561 ; cc2 <- canEq fl cv2 t1 t2
562 ; return (cc1 `andCCan` cc2) }
564 canEq fl cv s1@(ForAllTy {}) s2@(ForAllTy {})
565 | tcIsForAllTy s1, tcIsForAllTy s2,
569 = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
572 -- Finally expand any type synonym applications.
573 canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2
574 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2'
575 canEq fl cv _ _ = canEqFailure fl cv
577 canEqFailure :: CtFlavor -> EvVar -> TcS CanonicalCts
578 canEqFailure fl cv = return (singleCCan (mkFrozenError fl cv))
581 Note [Equality between type applications]
582 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
583 If we see an equality of the form s1 t1 ~ s2 t2 we can always split
584 it up into s1 ~ s2 /\ t1 ~ t2, since s1 and s2 can't be type
585 functions (type functions use the TyConApp constructor, which never
586 shows up as the LHS of an AppTy). Other than type functions, types
587 in Haskell are always
589 (1) generative: a b ~ c d implies a ~ c, since different type
590 constructors always generate distinct types
592 (2) injective: a b ~ a d implies b ~ d; we never generate the
593 same type from different type arguments.
596 Note [Canonical ordering for equality constraints]
597 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
598 Implemented as (<+=) below:
600 - Type function applications always come before anything else.
601 - Variables always come before non-variables (other than type
602 function applications).
604 Note that we don't need to unfold type synonyms on the RHS to check
605 the ordering; that is, in the rules above it's OK to consider only
606 whether something is *syntactically* a type function application or
607 not. To illustrate why this is OK, suppose we have an equality of the
608 form 'tv ~ S a b c', where S is a type synonym which expands to a
609 top-level application of the type function F, something like
613 Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's
614 expansion contains type function applications the flattener will do
615 the expansion and then generate a skolem variable for the type
616 function application, so we end up with something like this:
621 where x is the skolem variable. This is one extra equation than
622 absolutely necessary (we could have gotten away with just 'F d e ~ tv'
623 if we had noticed that S expanded to a top-level type function
624 application and flipped it around in the first place) but this way
625 keeps the code simpler.
627 Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the
628 ordering of tv ~ tv constraints. There are several reasons why we
631 (1) In order to be able to extract a substitution that doesn't
632 mention untouchable variables after we are done solving, we might
633 prefer to put touchable variables on the left. However, in and
634 of itself this isn't necessary; we can always re-orient equality
635 constraints at the end if necessary when extracting a substitution.
637 (2) To ensure termination we might think it necessary to put
638 variables in lexicographic order. However, this isn't actually
639 necessary as outlined below.
641 While building up an inert set of canonical constraints, we maintain
642 the invariant that the equality constraints in the inert set form an
643 acyclic rewrite system when viewed as L-R rewrite rules. Moreover,
644 the given constraints form an idempotent substitution (i.e. none of
645 the variables on the LHS occur in any of the RHS's, and type functions
646 never show up in the RHS at all), the wanted constraints also form an
647 idempotent substitution, and finally the LHS of a given constraint
648 never shows up on the RHS of a wanted constraint. There may, however,
649 be a wanted LHS that shows up in a given RHS, since we do not rewrite
650 given constraints with wanted constraints.
652 Suppose we have an inert constraint set
655 tg_1 ~ xig_1 -- givens
658 tw_1 ~ xiw_1 -- wanteds
662 where each t_i can be either a type variable or a type function
663 application. Now suppose we take a new canonical equality constraint,
664 t' ~ xi' (note among other things this means t' does not occur in xi')
665 and try to react it with the existing inert set. We show by induction
666 on the number of t_i which occur in t' ~ xi' that this process will
669 There are several ways t' ~ xi' could react with an existing constraint:
671 TODO: finish this proof. The below was for the case where the entire
672 inert set is an idempotent subustitution...
674 (b) We could have t' = t_j for some j. Then we obtain the new
675 equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j. We
676 now canonicalize the new equality, which may involve decomposing it
677 into several canonical equalities, and recurse on these. However,
678 none of the new equalities will contain t_j, so they have fewer
679 occurrences of the t_i than the original equation.
681 (a) We could have t_j occurring in xi' for some j, with t' /=
682 t_j. Then we substitute xi_j for t_j in xi' and continue. However,
683 since none of the t_i occur in xi_j, we have decreased the
684 number of t_i that occur in xi', since we eliminated t_j and did not
685 introduce any new ones.
689 = FskCls TcTyVar -- ^ Flatten skolem
690 | VarCls TcTyVar -- ^ Non-flatten-skolem variable
691 | FunCls TyCon [Type] -- ^ Type function, exactly saturated
692 | OtherCls TcType -- ^ Neither of the above
694 unClassify :: TypeClassifier -> TcType
695 unClassify (VarCls tv) = TyVarTy tv
696 unClassify (FskCls tv) = TyVarTy tv
697 unClassify (FunCls fn tys) = TyConApp fn tys
698 unClassify (OtherCls ty) = ty
700 classify :: TcType -> TypeClassifier
702 classify (TyVarTy tv)
704 FlatSkol {} <- tcTyVarDetails tv = FskCls tv
705 | otherwise = VarCls tv
706 classify (TyConApp tc tys) | isSynFamilyTyCon tc
707 , tyConArity tc == length tys
709 classify ty | Just ty' <- tcView ty
710 = case classify ty' of
711 OtherCls {} -> OtherCls ty
712 var_or_fn -> var_or_fn
716 -- See note [Canonical ordering for equality constraints].
717 reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool
718 -- (t1 `reOrient` t2) responds True
719 -- iff we should flip to (t2~t1)
720 -- We try to say False if possible, to minimise evidence generation
722 -- Postcondition: After re-orienting, first arg is not OTherCls
723 reOrient _fl (OtherCls {}) (FunCls {}) = True
724 reOrient _fl (OtherCls {}) (FskCls {}) = True
725 reOrient _fl (OtherCls {}) (VarCls {}) = True
726 reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
728 reOrient _fl (FunCls {}) (VarCls _tv) = False
729 -- But consider the following variation: isGiven fl && isMetaTyVar tv
731 -- See Note [No touchables as FunEq RHS] in TcSMonad
732 reOrient _fl (FunCls {}) _ = False -- Fun/Other on rhs
734 reOrient _fl (VarCls {}) (FunCls {}) = True
736 reOrient _fl (VarCls {}) (FskCls {}) = False
738 reOrient _fl (VarCls {}) (OtherCls {}) = False
739 reOrient _fl (VarCls tv1) (VarCls tv2)
740 | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True
742 -- Just for efficiency, see CTyEqCan invariants
744 reOrient _fl (FskCls {}) (VarCls tv2) = isMetaTyVar tv2
745 -- Just for efficiency, see CTyEqCan invariants
747 reOrient _fl (FskCls {}) (FskCls {}) = False
748 reOrient _fl (FskCls {}) (FunCls {}) = True
749 reOrient _fl (FskCls {}) (OtherCls {}) = False
752 canEqLeaf :: TcsUntouchables
754 -> TypeClassifier -> TypeClassifier -> TcS CanonicalCts
755 -- Canonicalizing "leaf" equality constraints which cannot be
756 -- decomposed further (ie one of the types is a variable or
757 -- saturated type function application).
760 -- * one of the two arguments is not OtherCls
761 -- * the two types are not equal (looking through synonyms)
762 canEqLeaf _untch fl cv cls1 cls2
763 | cls1 `re_orient` cls2
764 = do { cv' <- if isWanted fl
765 then do { cv' <- newCoVar s2 s1
766 ; setCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
768 else if isGivenOrSolved fl then
769 newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv))
771 newDerivedId (EqPred s2 s1)
772 ; canEqLeafOriented fl cv' cls2 s1 }
775 = do { traceTcS "canEqLeaf" (ppr (unClassify cls1) $$ ppr (unClassify cls2))
776 ; canEqLeafOriented fl cv cls1 s2 }
778 re_orient = reOrient fl
783 canEqLeafOriented :: CtFlavor -> CoVar
784 -> TypeClassifier -> TcType -> TcS CanonicalCts
785 -- First argument is not OtherCls
786 canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1
787 | let k1 = kindAppResult (tyConKind fn) tys1,
788 let k2 = typeKind s2,
789 not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan
791 -- Eagerly fails, see Note [Kind errors] in TcInteract
794 = ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) )
795 do { (xis1,cos1,ccs1) <- flattenMany fl tys1 -- Flatten type function arguments
796 -- cos1 :: xis1 ~ tys1
797 ; (xi2, co2, ccs2) <- flatten fl s2 -- Flatten entire RHS
799 ; let ccs = ccs1 `andCCan` ccs2
800 no_flattening_happened = all isIdentityCoercion (co2:cos1)
801 ; cv_new <- if no_flattening_happened then return cv
802 else if isGivenOrSolved fl then return cv
803 else if isWanted fl then
804 do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2
806 ; let -- fun_co :: F xis1 ~ F tys1
807 fun_co = mkTyConCoercion fn cos1
808 -- want_co :: F tys1 ~ s2
809 want_co = mkSymCoercion fun_co
810 `mkTransCoercion` mkCoVarCoercion cv'
811 `mkTransCoercion` co2
812 ; setCoBind cv want_co
815 newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2)
817 ; let final_cc = CFunEqCan { cc_id = cv_new
822 ; return $ ccs `extendCCans` final_cc }
824 -- Otherwise, we have a variable on the left, so call canEqLeafTyVarLeft
825 canEqLeafOriented fl cv (FskCls tv) s2
826 = canEqLeafTyVarLeft fl cv tv s2
827 canEqLeafOriented fl cv (VarCls tv) s2
828 = canEqLeafTyVarLeft fl cv tv s2
829 canEqLeafOriented _ cv (OtherCls ty1) ty2
830 = pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2)
832 canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS CanonicalCts
833 -- Establish invariants of CTyEqCans
834 canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2
835 | not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan
837 -- Eagerly fails, see Note [Kind errors] in TcInteract
839 = do { (xi2, co, ccs2) <- flatten fl s2 -- Flatten RHS co : xi2 ~ s2
840 ; mxi2' <- canOccursCheck fl tv xi2 -- Do an occurs check, and return a possibly
841 -- unfolded version of the RHS, if we had to
842 -- unfold any type synonyms to get rid of tv.
844 Nothing -> canEqFailure fl cv ;
846 do { let no_flattening_happened = isIdentityCoercion co
847 ; cv_new <- if no_flattening_happened then return cv
848 else if isGivenOrSolved fl then return cv
849 else if isWanted fl then
850 do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
851 ; setCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co)
854 newDerivedId (EqPred (mkTyVarTy tv) xi2')
856 ; return $ ccs2 `extendCCans` CTyEqCan { cc_id = cv_new
859 , cc_rhs = xi2' } } } }
864 -- See Note [Type synonyms and canonicalization].
865 -- Check whether the given variable occurs in the given type. We may
866 -- have needed to do some type synonym unfolding in order to get rid
867 -- of the variable, so we also return the unfolded version of the
868 -- type, which is guaranteed to be syntactically free of the given
869 -- type variable. If the type is already syntactically free of the
870 -- variable, then the same type is returned.
872 -- Precondition: the two types are not equal (looking though synonyms)
873 canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi)
874 canOccursCheck _gw tv xi = return (expandAway tv xi)
877 @expandAway tv xi@ expands synonyms in xi just enough to get rid of
878 occurrences of tv, if that is possible; otherwise, it returns Nothing.
879 For example, suppose we have
882 expandAway b (F Int b) = Just [Int]
884 expandAway a (F a Int) = Nothing
886 We don't promise to do the absolute minimum amount of expanding
887 necessary, but we try not to do expansions we don't need to. We
888 prefer doing inner expansions first. For example,
889 type F a b = (a, Int, a, [a])
892 expandAway b (F (G b)) = F Char
893 even though we could also expand F to get rid of b.
896 expandAway :: TcTyVar -> Xi -> Maybe Xi
897 expandAway tv t@(TyVarTy tv')
898 | tv == tv' = Nothing
901 | not (tv `elemVarSet` tyVarsOfType xi) = Just xi
902 expandAway tv (AppTy ty1 ty2)
903 = do { ty1' <- expandAway tv ty1
904 ; ty2' <- expandAway tv ty2
905 ; return (mkAppTy ty1' ty2') }
906 -- mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2
907 expandAway tv (FunTy ty1 ty2)
908 = do { ty1' <- expandAway tv ty1
909 ; ty2' <- expandAway tv ty2
910 ; return (mkFunTy ty1' ty2') }
911 -- mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2
912 expandAway tv ty@(ForAllTy {})
913 = let (tvs,rho) = splitForAllTys ty
914 tvs_knds = map tyVarKind tvs
915 in if tv `elemVarSet` tyVarsOfTypes tvs_knds then
916 -- Can't expand away the kinds unless we create
917 -- fresh variables which we don't want to do at this point.
919 else do { rho' <- expandAway tv rho
920 ; return (mkForAllTys tvs rho') }
921 expandAway tv (PredTy pred)
922 = do { pred' <- expandAwayPred tv pred
923 ; return (PredTy pred') }
924 -- For a type constructor application, first try expanding away the
925 -- offending variable from the arguments. If that doesn't work, next
926 -- see if the type constructor is a type synonym, and if so, expand
928 expandAway tv ty@(TyConApp tc tys)
929 = (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv)
931 expandAwayPred :: TcTyVar -> TcPredType -> Maybe TcPredType
932 expandAwayPred tv (ClassP cls tys)
933 = do { tys' <- mapM (expandAway tv) tys; return (ClassP cls tys') }
934 expandAwayPred tv (EqPred ty1 ty2)
935 = do { ty1' <- expandAway tv ty1
936 ; ty2' <- expandAway tv ty2
937 ; return (EqPred ty1' ty2') }
938 expandAwayPred tv (IParam nm ty)
939 = do { ty' <- expandAway tv ty
940 ; return (IParam nm ty') }
946 Note [Type synonyms and canonicalization]
947 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
949 We treat type synonym applications as xi types, that is, they do not
950 count as type function applications. However, we do need to be a bit
951 careful with type synonyms: like type functions they may not be
952 generative or injective. However, unlike type functions, they are
953 parametric, so there is no problem in expanding them whenever we see
954 them, since we do not need to know anything about their arguments in
955 order to expand them; this is what justifies not having to treat them
956 as specially as type function applications. The thing that causes
957 some subtleties is that we prefer to leave type synonym applications
958 *unexpanded* whenever possible, in order to generate better error
961 If we encounter an equality constraint with type synonym applications
962 on both sides, or a type synonym application on one side and some sort
963 of type application on the other, we simply must expand out the type
964 synonyms in order to continue decomposing the equality constraint into
965 primitive equality constraints. For example, suppose we have
969 and we encounter the equality
973 In order to continue we must expand F a into [Int], giving us the
978 which we can then decompose into the more primitive equality
983 However, if we encounter an equality constraint with a type synonym
984 application on one side and a variable on the other side, we should
985 NOT (necessarily) expand the type synonym, since for the purpose of
986 good error messages we want to leave type synonyms unexpanded as much
989 However, there is a subtle point with type synonyms and the occurs
990 check that takes place for equality constraints of the form tv ~ xi.
991 As an example, suppose we have
995 and we come across the equality constraint
999 This should not actually fail the occurs check, since expanding out
1000 the type synonym results in the legitimate equality constraint a ~
1001 Int. We must actually do this expansion, because unifying a with F a
1002 will lead the type checker into infinite loops later. Put another
1003 way, canonical equality constraints should never *syntactically*
1004 contain the LHS variable in the RHS type. However, we don't always
1005 need to expand type synonyms when doing an occurs check; for example,
1010 is obviously fine no matter what F expands to. And in this case we
1011 would rather unify a with F b (rather than F b's expansion) in order
1012 to get better error messages later.
1014 So, when doing an occurs check with a type synonym application on the
1015 RHS, we use some heuristics to find an expansion of the RHS which does
1016 not contain the variable from the LHS. In particular, given
1020 we first try expanding each of the ti to types which no longer contain
1021 a. If this turns out to be impossible, we next try expanding F
1025 %************************************************************************
1027 %* Functional dependencies, instantiation of equations
1029 %************************************************************************
1031 When we spot an equality arising from a functional dependency,
1032 we now use that equality (a "wanted") to rewrite the work-item
1033 constraint right away. This avoids two dangers
1035 Danger 1: If we send the original constraint on down the pipeline
1036 it may react with an instance declaration, and in delicate
1037 situations (when a Given overlaps with an instance) that
1038 may produce new insoluble goals: see Trac #4952
1040 Danger 2: If we don't rewrite the constraint, it may re-react
1041 with the same thing later, and produce the same equality
1042 again --> termination worries.
1044 To achieve this required some refactoring of FunDeps.lhs (nicer
1048 rewriteWithFunDeps :: [Equation]
1050 -> TcS (Maybe ([Xi], [Coercion], WorkList))
1051 rewriteWithFunDeps eqn_pred_locs xis fl
1052 = do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
1053 ; let fd_ev_pos :: [(Int,FlavoredEvVar)]
1054 fd_ev_pos = concat fd_ev_poss
1055 (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
1056 ; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
1057 ; let fd_work = unionWorkLists fds
1058 ; if isEmptyWorkList fd_work
1060 else return (Just (rewritten_xis, cos, fd_work)) }
1062 instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived
1064 -> TcS [(Int, FlavoredEvVar)]
1065 -- Post: Returns the position index as well as the corresponding FunDep equality
1066 instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
1067 , fd_pred1 = d1, fd_pred2 = d2 })
1068 = do { let tvs = varSetElems qtvs
1069 ; tvs' <- mapM instFlexiTcS tvs
1070 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
1071 ; mapM (do_one subst) eqs }
1074 Given {} -> panic "mkFunDepEqns"
1075 Wanted loc -> Wanted (push_ctx loc)
1076 Derived loc -> Derived (push_ctx loc)
1078 push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1080 do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
1081 = do { let sty1 = substTy subst ty1
1082 sty2 = substTy subst ty2
1083 ; ev <- newCoVar sty1 sty2
1084 ; return (i, mkEvVarX ev fl') }
1086 rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty)
1087 -> [Type] -- A sequence of types: tys
1088 -> [(Type,Coercion)] -- Returns : [(ty', co : ty' ~ ty)]
1089 rewriteDictParams param_eqs tys
1090 = zipWith do_one tys [0..]
1092 do_one :: Type -> Int -> (Type,Coercion)
1093 do_one ty n = case lookup n param_eqs of
1094 Just wev -> (get_fst_ty wev, mkCoVarCoercion (evVarOf wev))
1095 Nothing -> (ty,ty) -- Identity
1097 get_fst_ty wev = case evVarOfPred wev of
1099 _ -> panic "rewriteDictParams: non equality fundep"
1101 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
1102 -> TcM (TidyEnv, SDoc)
1103 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1104 = do { zpred1 <- TcM.zonkTcPredType pred1
1105 ; zpred2 <- TcM.zonkTcPredType pred2
1106 ; let { tpred1 = tidyPred tidy_env zpred1
1107 ; tpred2 = tidyPred tidy_env zpred2 }
1108 ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1109 nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
1110 nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
1111 ; return (tidy_env, msg) }