3 mkCanonical, mkCanonicals, mkCanonicalFEV, mkCanonicalFEVs, canWanteds, canGivens,
4 canOccursCheck, canEqToWorkList,
8 #include "HsVersions.h"
11 import Id ( evVarPred )
15 import qualified TcMType as TcM
24 import VarEnv ( TidyEnv )
26 import Control.Monad ( unless, when, zipWithM, zipWithM_ )
28 import Control.Applicative ( (<|>) )
38 Note [Canonicalisation]
39 ~~~~~~~~~~~~~~~~~~~~~~~
40 * Converts (Constraint f) _which_does_not_contain_proper_implications_ to CanonicalCts
41 * Unary: treats individual constraints one at a time
42 * Does not do any zonking
43 * Lives in TcS monad so that it can create new skolem variables
46 %************************************************************************
48 %* Flattening (eliminating all function symbols) *
50 %************************************************************************
54 flatten ty ==> (xi, cc)
56 xi has no type functions
57 cc = Auxiliary given (equality) constraints constraining
58 the fresh type variables in xi. Evidence for these
59 is always the identity coercion, because internally the
60 fresh flattening skolem variables are actually identified
61 with the types they have been generated to stand in for.
63 Note that it is flatten's job to flatten *every type function it sees*.
64 flatten is only called on *arguments* to type functions, by canEqGiven.
66 Recall that in comments we use alpha[flat = ty] to represent a
67 flattening skolem variable alpha which has been generated to stand in
70 ----- Example of flattening a constraint: ------
71 flatten (List (F (G Int))) ==> (xi, cc)
74 cc = { G Int ~ beta[flat = G Int],
75 F beta ~ alpha[flat = F beta] }
77 * alpha and beta are 'flattening skolem variables'.
78 * All the constraints in cc are 'given', and all their coercion terms
81 NB: Flattening Skolems only occur in canonical constraints, which
82 are never zonked, so we don't need to worry about zonking doing
83 accidental unflattening.
85 Note that we prefer to leave type synonyms unexpanded when possible,
86 so when the flattener encounters one, it first asks whether its
87 transitive expansion contains any type function applications. If so,
88 it expands the synonym and proceeds; if not, it simply returns the
91 TODO: caching the information about whether transitive synonym
92 expansions contain any type function applications would speed things
93 up a bit; right now we waste a lot of energy traversing the same types
99 -- Flatten a bunch of types all at once.
100 flattenMany :: CtFlavor -> [Type] -> TcS ([Xi], [Coercion], CanonicalCts)
101 -- Coercions :: Xi ~ Type
103 = do { (xis, cos, cts_s) <- mapAndUnzip3M (flatten ctxt) tys
104 ; return (xis, cos, andCCans cts_s) }
106 -- Flatten a type to get rid of type function applications, returning
107 -- the new type-function-free type, and a collection of new equality
108 -- constraints. See Note [Flattening] for more detail.
109 flatten :: CtFlavor -> TcType -> TcS (Xi, Coercion, CanonicalCts)
110 -- Postcondition: Coercion :: Xi ~ TcType
112 | Just ty' <- tcView ty
113 = do { (xi, co, ccs) <- flatten ctxt ty'
114 -- Preserve type synonyms if possible
115 -- We can tell if ty' is function-free by
116 -- whether there are any floated constraints
117 ; if isReflCo co then
118 return (ty, mkReflCo ty, emptyCCan)
120 return (xi, co, ccs) }
122 flatten _ v@(TyVarTy _)
123 = return (v, mkReflCo v, emptyCCan)
125 flatten ctxt (AppTy ty1 ty2)
126 = do { (xi1,co1,c1) <- flatten ctxt ty1
127 ; (xi2,co2,c2) <- flatten ctxt ty2
128 ; return (mkAppTy xi1 xi2, mkAppCo co1 co2, c1 `andCCan` c2) }
130 flatten ctxt (FunTy ty1 ty2)
131 = do { (xi1,co1,c1) <- flatten ctxt ty1
132 ; (xi2,co2,c2) <- flatten ctxt ty2
133 ; return (mkFunTy xi1 xi2, mkFunCo co1 co2, c1 `andCCan` c2) }
135 flatten fl (TyConApp tc tys)
136 -- For a normal type constructor or data family application, we just
137 -- recursively flatten the arguments.
138 | not (isSynFamilyTyCon tc)
139 = do { (xis,cos,ccs) <- flattenMany fl tys
140 ; return (mkTyConApp tc xis, mkTyConAppCo tc cos, ccs) }
142 -- Otherwise, it's a type function application, and we have to
143 -- flatten it away as well, and generate a new given equality constraint
144 -- between the application and a newly generated flattening skolem variable.
146 = ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated
147 do { (xis, cos, ccs) <- flattenMany fl tys
148 ; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis
149 (cos_args, cos_rest) = splitAt (tyConArity tc) cos
150 -- The type function might be *over* saturated
151 -- in which case the remaining arguments should
152 -- be dealt with by AppTys
153 fam_ty = mkTyConApp tc xi_args
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 (mkReflCo fam_ty)
162 ; let ct = CFunEqCan { cc_id = cv
163 , cc_flavor = fl -- Given
165 , cc_tyargs = xi_args
167 ; let ret_co = mkCoVarCo 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 = mkCoVarCo 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 AppCo (mkSymCo ret_co
185 `mkTransCo` mkTyConAppCo tc cos_args)
187 , 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', foldr mkForAllCo co tvs, 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', mkPredCo $ ClassP cls cos, ccs) }
212 flattenPred ctxt (IParam nm ty)
213 = do { (ty', co, ccs) <- flatten ctxt ty
214 ; return (IParam nm ty', mkPredCo $ IParam nm co, ccs) }
215 flattenPred ctxt (EqPred ty1 ty2)
216 = do { (ty1', co1, ccs1) <- flatten ctxt ty1
217 ; (ty2', co2, ccs2) <- flatten ctxt ty2
218 ; return (EqPred ty1' ty2', mkPredCo $ EqPred co1 co2, ccs1 `andCCan` ccs2) }
221 %************************************************************************
223 %* Canonicalising given constraints *
225 %************************************************************************
228 canWanteds :: [WantedEvVar] -> TcS WorkList
229 canWanteds = fmap unionWorkLists . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
231 canGivens :: GivenLoc -> [EvVar] -> TcS WorkList
232 canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc GivenOrig)) givens
233 ; return (unionWorkLists ccs) }
235 mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList
236 mkCanonicals fl vs = fmap unionWorkLists (mapM (mkCanonical fl) vs)
238 mkCanonicalFEV :: FlavoredEvVar -> TcS WorkList
239 mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev
241 mkCanonicalFEVs :: Bag FlavoredEvVar -> TcS WorkList
242 mkCanonicalFEVs = foldrBagM canon_one emptyWorkList
243 where -- Preserves order (shouldn't be important, but curently
244 -- is important for the vectoriser)
245 canon_one fev wl = do { wl' <- mkCanonicalFEV fev
246 ; return (unionWorkList wl' wl) }
249 mkCanonical :: CtFlavor -> EvVar -> TcS WorkList
250 mkCanonical fl ev = case evVarPred ev of
251 ClassP clas tys -> canClassToWorkList fl ev clas tys
252 IParam ip ty -> canIPToWorkList fl ev ip ty
253 EqPred ty1 ty2 -> canEqToWorkList fl ev ty1 ty2
256 canClassToWorkList :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS WorkList
257 canClassToWorkList fl v cn tys
258 = do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys
259 ; let no_flattening_happened = all isReflCo cos
260 dict_co = mkTyConAppCo (classTyCon cn) cos
261 ; v_new <- if no_flattening_happened then return v
262 else if isGivenOrSolved fl then return v
263 -- The cos are all identities if fl=Given,
264 -- hence nothing to do
265 else do { v' <- newDictVar cn xis -- D xis
266 ; when (isWanted fl) $ setDictBind v (EvCast v' dict_co)
267 ; when (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCo dict_co))
268 -- NB: No more setting evidence for derived now
271 -- Add the superclasses of this one here, See Note [Adding superclasses].
272 -- But only if we are not simplifying the LHS of a rule.
273 ; sctx <- getTcSContext
274 ; sc_cts <- if simplEqsOnly sctx then return emptyWorkList
275 else newSCWorkFromFlavored v_new fl cn xis
277 ; return (sc_cts `unionWorkList`
278 workListFromEqs ccs `unionWorkList`
279 workListFromNonEq CDictCan { cc_id = v_new
282 , cc_tyargs = xis }) }
285 Note [Adding superclasses]
286 ~~~~~~~~~~~~~~~~~~~~~~~~~~
287 Since dictionaries are canonicalized only once in their lifetime, the
288 place to add their superclasses is canonicalisation (The alternative
289 would be to do it during constraint solving, but we'd have to be
290 extremely careful to not repeatedly introduced the same superclass in
291 our worklist). Here is what we do:
294 We add all their superclasses as Givens.
297 Generally speaking we want to be able to add superclasses of
298 wanteds for two reasons:
300 (1) Oportunities for improvement. Example:
301 class (a ~ b) => C a b
302 Wanted constraint is: C alpha beta
303 We'd like to simply have C alpha alpha. Similar
304 situations arise in relation to functional dependencies.
306 (2) To have minimal constraints to quantify over:
307 For instance, if our wanted constraint is (Eq a, Ord a)
308 we'd only like to quantify over Ord a.
310 To deal with (1) above we only add the superclasses of wanteds
311 which may lead to improvement, that is: equality superclasses or
312 superclasses with functional dependencies.
314 We deal with (2) completely independently in TcSimplify. See
315 Note [Minimize by SuperClasses] in TcSimplify.
318 Moreover, in all cases the extra improvement constraints are
319 Derived. Derived constraints have an identity (for now), but
320 we don't do anything with their evidence. For instance they
321 are never used to rewrite other constraints.
323 See also [New Wanted Superclass Work] in TcInteract.
329 Here's an example that demonstrates why we chose to NOT add
330 superclasses during simplification: [Comes from ticket #4497]
332 class Num (RealOf t) => Normed t
335 Assume the generated wanted constraint is:
336 RealOf e ~ e, Normed e
337 If we were to be adding the superclasses during simplification we'd get:
338 Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf
340 e ~ uf, Num uf, Normed e, RealOf e ~ e
341 ==> [Spontaneous solve]
342 Num uf, Normed uf, RealOf uf ~ uf
344 While looks exactly like our original constraint. If we add the superclass again we'd loop.
345 By adding superclasses definitely only once, during canonicalisation, this situation can't
350 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
351 -- Returns superclasses, see Note [Adding superclasses]
352 newSCWorkFromFlavored ev orig_flavor cls xis
353 | isDerived orig_flavor
354 = return emptyWorkList -- Deriveds don't yield more superclasses because we will
355 -- add them transitively in the case of wanteds.
357 | Just gk <- isGiven_maybe orig_flavor
359 GivenOrig -> do { let sc_theta = immSuperClasses cls xis
361 ; sc_vars <- mapM newEvVar sc_theta
362 ; _ <- zipWithM_ setEvBind sc_vars [EvSuperClass ev n | n <- [0..]]
363 ; mkCanonicals flavor sc_vars }
364 GivenSolved -> return emptyWorkList
365 -- Seems very dangerous to add the superclasses for dictionaries that may be
366 -- partially solved because we may end up with evidence loops.
368 | isEmptyVarSet (tyVarsOfTypes xis)
369 = return emptyWorkList -- Wanteds with no variables yield no deriveds.
370 -- See Note [Improvement from Ground Wanteds]
372 | otherwise -- Wanted case, just add those SC that can lead to improvement.
373 = do { let sc_rec_theta = transSuperClasses cls xis
374 impr_theta = filter is_improvement_pty sc_rec_theta
375 Wanted wloc = orig_flavor
376 ; der_ids <- mapM newDerivedId impr_theta
377 ; mkCanonicals (Derived wloc) der_ids }
380 is_improvement_pty :: PredType -> Bool
381 -- Either it's an equality, or has some functional dependency
382 is_improvement_pty (EqPred {}) = True
383 is_improvement_pty (ClassP cls _ty) = not $ null fundeps
384 where (_,fundeps,_,_,_,_) = classExtraBigSig cls
385 is_improvement_pty _ = False
390 canIPToWorkList :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS WorkList
391 -- See Note [Canonical implicit parameter constraints] to see why we don't
392 -- immediately canonicalize (flatten) IP constraints.
393 canIPToWorkList fl v nm ty
394 = return $ workListFromNonEq (CIPCan { cc_id = v
400 canEqToWorkList :: CtFlavor -> EvVar -> Type -> Type -> TcS WorkList
401 canEqToWorkList fl cv ty1 ty2 = do { cts <- canEq fl cv ty1 ty2
402 ; return $ workListFromEqs cts }
404 canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts
406 | eqType ty1 ty2 -- Dealing with equality here avoids
407 -- later spurious occurs checks for a~a
408 = do { when (isWanted fl) (setCoBind cv (mkReflCo ty1))
411 -- If one side is a variable, orient and flatten,
412 -- WITHOUT expanding type synonyms, so that we tend to
413 -- substitute a ~ Age rather than a ~ Int when @type Age = Int@
414 canEq fl cv ty1@(TyVarTy {}) ty2
415 = do { untch <- getUntouchables
416 ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
417 canEq fl cv ty1 ty2@(TyVarTy {})
418 = do { untch <- getUntouchables
419 ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
420 -- NB: don't use VarCls directly because tv1 or tv2 may be scolems!
422 -- Split up an equality between function types into two equalities.
423 canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
424 = do { (argv, resv) <-
426 do { argv <- newCoVar s1 s2
427 ; resv <- newCoVar t1 t2
429 mkFunCo (mkCoVarCo argv) (mkCoVarCo resv)
430 ; return (argv,resv) }
431 else if isGivenOrSolved fl then
432 let [arg,res] = decomposeCo 2 (mkCoVarCo cv)
433 in do { argv <- newGivenCoVar s1 s2 arg
434 ; resv <- newGivenCoVar t1 t2 res
435 ; return (argv,resv) }
438 do { argv <- newDerivedId (EqPred s1 s2)
439 ; resv <- newDerivedId (EqPred t1 t2)
440 ; return (argv,resv) }
442 ; cc1 <- canEq fl argv s1 s2 -- inherit original kinds and locations
443 ; cc2 <- canEq fl resv t1 t2
444 ; return (cc1 `andCCan` cc2) }
446 canEq fl cv (TyConApp fn tys) ty2
447 | isSynFamilyTyCon fn, length tys == tyConArity fn
448 = do { untch <- getUntouchables
449 ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) }
450 canEq fl cv ty1 (TyConApp fn tys)
451 | isSynFamilyTyCon fn, length tys == tyConArity fn
452 = do { untch <- getUntouchables
453 ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) }
455 canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
456 | isDecomposableTyCon tc1 && isDecomposableTyCon tc2
458 , length tys1 == length tys2
459 = -- Generate equalities for each of the corresponding arguments
461 <- if isWanted fl then
462 do { argsv <- zipWithM newCoVar tys1 tys2
464 mkTyConAppCo tc1 (map mkCoVarCo argsv)
466 else if isGivenOrSolved fl then
467 let cos = decomposeCo (length tys1) (mkCoVarCo cv)
468 in zipWith3M newGivenCoVar tys1 tys2 cos
471 zipWithM (\t1 t2 -> newDerivedId (EqPred t1 t2)) tys1 tys2
473 ; andCCans <$> zipWith3M (canEq fl) argsv tys1 tys2 }
475 -- See Note [Equality between type applications]
476 -- Note [Care with type applications] in TcUnify
478 | Just (s1,t1) <- tcSplitAppTy_maybe ty1
479 , Just (s2,t2) <- tcSplitAppTy_maybe ty2
481 then do { cv1 <- newCoVar s1 s2
482 ; cv2 <- newCoVar t1 t2
484 mkAppCo (mkCoVarCo cv1) (mkCoVarCo cv2)
485 ; cc1 <- canEq fl cv1 s1 s2
486 ; cc2 <- canEq fl cv2 t1 t2
487 ; return (cc1 `andCCan` cc2) }
490 then do { cv1 <- newDerivedId (EqPred s1 s2)
491 ; cv2 <- newDerivedId (EqPred t1 t2)
492 ; cc1 <- canEq fl cv1 s1 s2
493 ; cc2 <- canEq fl cv2 t1 t2
494 ; return (cc1 `andCCan` cc2) }
496 else return emptyCCan -- We cannot decompose given applications
497 -- because we no longer have 'left' and 'right'
499 canEq fl cv s1@(ForAllTy {}) s2@(ForAllTy {})
500 | tcIsForAllTy s1, tcIsForAllTy s2,
504 = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
507 -- Finally expand any type synonym applications.
508 canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2
509 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2'
510 canEq fl cv _ _ = canEqFailure fl cv
512 canEqFailure :: CtFlavor -> EvVar -> TcS CanonicalCts
513 canEqFailure fl cv = return (singleCCan (mkFrozenError fl cv))
516 Note [Equality between type applications]
517 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
518 If we see an equality of the form s1 t1 ~ s2 t2 we can always split
519 it up into s1 ~ s2 /\ t1 ~ t2, since s1 and s2 can't be type
520 functions (type functions use the TyConApp constructor, which never
521 shows up as the LHS of an AppTy). Other than type functions, types
522 in Haskell are always
524 (1) generative: a b ~ c d implies a ~ c, since different type
525 constructors always generate distinct types
527 (2) injective: a b ~ a d implies b ~ d; we never generate the
528 same type from different type arguments.
531 Note [Canonical ordering for equality constraints]
532 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
533 Implemented as (<+=) below:
535 - Type function applications always come before anything else.
536 - Variables always come before non-variables (other than type
537 function applications).
539 Note that we don't need to unfold type synonyms on the RHS to check
540 the ordering; that is, in the rules above it's OK to consider only
541 whether something is *syntactically* a type function application or
542 not. To illustrate why this is OK, suppose we have an equality of the
543 form 'tv ~ S a b c', where S is a type synonym which expands to a
544 top-level application of the type function F, something like
548 Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's
549 expansion contains type function applications the flattener will do
550 the expansion and then generate a skolem variable for the type
551 function application, so we end up with something like this:
556 where x is the skolem variable. This is one extra equation than
557 absolutely necessary (we could have gotten away with just 'F d e ~ tv'
558 if we had noticed that S expanded to a top-level type function
559 application and flipped it around in the first place) but this way
560 keeps the code simpler.
562 Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the
563 ordering of tv ~ tv constraints. There are several reasons why we
566 (1) In order to be able to extract a substitution that doesn't
567 mention untouchable variables after we are done solving, we might
568 prefer to put touchable variables on the left. However, in and
569 of itself this isn't necessary; we can always re-orient equality
570 constraints at the end if necessary when extracting a substitution.
572 (2) To ensure termination we might think it necessary to put
573 variables in lexicographic order. However, this isn't actually
574 necessary as outlined below.
576 While building up an inert set of canonical constraints, we maintain
577 the invariant that the equality constraints in the inert set form an
578 acyclic rewrite system when viewed as L-R rewrite rules. Moreover,
579 the given constraints form an idempotent substitution (i.e. none of
580 the variables on the LHS occur in any of the RHS's, and type functions
581 never show up in the RHS at all), the wanted constraints also form an
582 idempotent substitution, and finally the LHS of a given constraint
583 never shows up on the RHS of a wanted constraint. There may, however,
584 be a wanted LHS that shows up in a given RHS, since we do not rewrite
585 given constraints with wanted constraints.
587 Suppose we have an inert constraint set
590 tg_1 ~ xig_1 -- givens
593 tw_1 ~ xiw_1 -- wanteds
597 where each t_i can be either a type variable or a type function
598 application. Now suppose we take a new canonical equality constraint,
599 t' ~ xi' (note among other things this means t' does not occur in xi')
600 and try to react it with the existing inert set. We show by induction
601 on the number of t_i which occur in t' ~ xi' that this process will
604 There are several ways t' ~ xi' could react with an existing constraint:
606 TODO: finish this proof. The below was for the case where the entire
607 inert set is an idempotent subustitution...
609 (b) We could have t' = t_j for some j. Then we obtain the new
610 equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j. We
611 now canonicalize the new equality, which may involve decomposing it
612 into several canonical equalities, and recurse on these. However,
613 none of the new equalities will contain t_j, so they have fewer
614 occurrences of the t_i than the original equation.
616 (a) We could have t_j occurring in xi' for some j, with t' /=
617 t_j. Then we substitute xi_j for t_j in xi' and continue. However,
618 since none of the t_i occur in xi_j, we have decreased the
619 number of t_i that occur in xi', since we eliminated t_j and did not
620 introduce any new ones.
624 = FskCls TcTyVar -- ^ Flatten skolem
625 | VarCls TcTyVar -- ^ Non-flatten-skolem variable
626 | FunCls TyCon [Type] -- ^ Type function, exactly saturated
627 | OtherCls TcType -- ^ Neither of the above
629 unClassify :: TypeClassifier -> TcType
630 unClassify (VarCls tv) = TyVarTy tv
631 unClassify (FskCls tv) = TyVarTy tv
632 unClassify (FunCls fn tys) = TyConApp fn tys
633 unClassify (OtherCls ty) = ty
635 classify :: TcType -> TypeClassifier
637 classify (TyVarTy tv)
639 FlatSkol {} <- tcTyVarDetails tv = FskCls tv
640 | otherwise = VarCls tv
641 classify (TyConApp tc tys) | isSynFamilyTyCon tc
642 , tyConArity tc == length tys
644 classify ty | Just ty' <- tcView ty
645 = case classify ty' of
646 OtherCls {} -> OtherCls ty
647 var_or_fn -> var_or_fn
651 -- See note [Canonical ordering for equality constraints].
652 reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool
653 -- (t1 `reOrient` t2) responds True
654 -- iff we should flip to (t2~t1)
655 -- We try to say False if possible, to minimise evidence generation
657 -- Postcondition: After re-orienting, first arg is not OTherCls
658 reOrient _fl (OtherCls {}) (FunCls {}) = True
659 reOrient _fl (OtherCls {}) (FskCls {}) = True
660 reOrient _fl (OtherCls {}) (VarCls {}) = True
661 reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
663 reOrient _fl (FunCls {}) (VarCls _tv) = False
664 -- But consider the following variation: isGiven fl && isMetaTyVar tv
666 -- See Note [No touchables as FunEq RHS] in TcSMonad
667 reOrient _fl (FunCls {}) _ = False -- Fun/Other on rhs
669 reOrient _fl (VarCls {}) (FunCls {}) = True
671 reOrient _fl (VarCls {}) (FskCls {}) = False
673 reOrient _fl (VarCls {}) (OtherCls {}) = False
674 reOrient _fl (VarCls tv1) (VarCls tv2)
675 | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True
677 -- Just for efficiency, see CTyEqCan invariants
679 reOrient _fl (FskCls {}) (VarCls tv2) = isMetaTyVar tv2
680 -- Just for efficiency, see CTyEqCan invariants
682 reOrient _fl (FskCls {}) (FskCls {}) = False
683 reOrient _fl (FskCls {}) (FunCls {}) = True
684 reOrient _fl (FskCls {}) (OtherCls {}) = False
687 canEqLeaf :: TcsUntouchables
689 -> TypeClassifier -> TypeClassifier -> TcS CanonicalCts
690 -- Canonicalizing "leaf" equality constraints which cannot be
691 -- decomposed further (ie one of the types is a variable or
692 -- saturated type function application).
695 -- * one of the two arguments is not OtherCls
696 -- * the two types are not equal (looking through synonyms)
697 canEqLeaf _untch fl cv cls1 cls2
698 | cls1 `re_orient` cls2
699 = do { cv' <- if isWanted fl
700 then do { cv' <- newCoVar s2 s1
701 ; setCoBind cv $ mkSymCo (mkCoVarCo cv')
703 else if isGivenOrSolved fl then
704 newGivenCoVar s2 s1 (mkSymCo (mkCoVarCo cv))
706 newDerivedId (EqPred s2 s1)
707 ; canEqLeafOriented fl cv' cls2 s1 }
710 = do { traceTcS "canEqLeaf" (ppr (unClassify cls1) $$ ppr (unClassify cls2))
711 ; canEqLeafOriented fl cv cls1 s2 }
713 re_orient = reOrient fl
718 canEqLeafOriented :: CtFlavor -> CoVar
719 -> TypeClassifier -> TcType -> TcS CanonicalCts
720 -- First argument is not OtherCls
721 canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1
722 | let k1 = kindAppResult (tyConKind fn) tys1,
723 let k2 = typeKind s2,
724 not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan
726 -- Eagerly fails, see Note [Kind errors] in TcInteract
729 = ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) )
730 do { (xis1,cos1,ccs1) <- flattenMany fl tys1 -- Flatten type function arguments
731 -- cos1 :: xis1 ~ tys1
732 ; (xi2, co2, ccs2) <- flatten fl s2 -- Flatten entire RHS
734 ; let ccs = ccs1 `andCCan` ccs2
735 no_flattening_happened = all isReflCo (co2:cos1)
736 ; cv_new <- if no_flattening_happened then return cv
737 else if isGivenOrSolved fl then return cv
738 else if isWanted fl then
739 do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2
741 ; let -- fun_co :: F xis1 ~ F tys1
742 fun_co = mkTyConAppCo fn cos1
743 -- want_co :: F tys1 ~ s2
744 want_co = mkSymCo fun_co
745 `mkTransCo` mkCoVarCo cv'
747 ; setCoBind cv want_co
750 newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2)
752 ; let final_cc = CFunEqCan { cc_id = cv_new
757 ; return $ ccs `extendCCans` final_cc }
759 -- Otherwise, we have a variable on the left, so call canEqLeafTyVarLeft
760 canEqLeafOriented fl cv (FskCls tv) s2
761 = canEqLeafTyVarLeft fl cv tv s2
762 canEqLeafOriented fl cv (VarCls tv) s2
763 = canEqLeafTyVarLeft fl cv tv s2
764 canEqLeafOriented _ cv (OtherCls ty1) ty2
765 = pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2)
767 canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS CanonicalCts
768 -- Establish invariants of CTyEqCans
769 canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2
770 | not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan
772 -- Eagerly fails, see Note [Kind errors] in TcInteract
774 = do { (xi2, co, ccs2) <- flatten fl s2 -- Flatten RHS co : xi2 ~ s2
775 ; mxi2' <- canOccursCheck fl tv xi2 -- Do an occurs check, and return a possibly
776 -- unfolded version of the RHS, if we had to
777 -- unfold any type synonyms to get rid of tv.
779 Nothing -> canEqFailure fl cv ;
781 do { let no_flattening_happened = isReflCo co
782 ; cv_new <- if no_flattening_happened then return cv
783 else if isGivenOrSolved fl then return cv
784 else if isWanted fl then
785 do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
786 ; setCoBind cv (mkCoVarCo cv' `mkTransCo` co)
789 newDerivedId (EqPred (mkTyVarTy tv) xi2')
791 ; return $ ccs2 `extendCCans` CTyEqCan { cc_id = cv_new
794 , cc_rhs = xi2' } } } }
799 -- See Note [Type synonyms and canonicalization].
800 -- Check whether the given variable occurs in the given type. We may
801 -- have needed to do some type synonym unfolding in order to get rid
802 -- of the variable, so we also return the unfolded version of the
803 -- type, which is guaranteed to be syntactically free of the given
804 -- type variable. If the type is already syntactically free of the
805 -- variable, then the same type is returned.
807 -- Precondition: the two types are not equal (looking though synonyms)
808 canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi)
809 canOccursCheck _gw tv xi = return (expandAway tv xi)
812 @expandAway tv xi@ expands synonyms in xi just enough to get rid of
813 occurrences of tv, if that is possible; otherwise, it returns Nothing.
814 For example, suppose we have
817 expandAway b (F Int b) = Just [Int]
819 expandAway a (F a Int) = Nothing
821 We don't promise to do the absolute minimum amount of expanding
822 necessary, but we try not to do expansions we don't need to. We
823 prefer doing inner expansions first. For example,
824 type F a b = (a, Int, a, [a])
827 expandAway b (F (G b)) = F Char
828 even though we could also expand F to get rid of b.
831 expandAway :: TcTyVar -> Xi -> Maybe Xi
832 expandAway tv t@(TyVarTy tv')
833 | tv == tv' = Nothing
836 | not (tv `elemVarSet` tyVarsOfType xi) = Just xi
837 expandAway tv (AppTy ty1 ty2)
838 = do { ty1' <- expandAway tv ty1
839 ; ty2' <- expandAway tv ty2
840 ; return (mkAppTy ty1' ty2') }
841 -- mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2
842 expandAway tv (FunTy ty1 ty2)
843 = do { ty1' <- expandAway tv ty1
844 ; ty2' <- expandAway tv ty2
845 ; return (mkFunTy ty1' ty2') }
846 -- mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2
847 expandAway tv ty@(ForAllTy {})
848 = let (tvs,rho) = splitForAllTys ty
849 tvs_knds = map tyVarKind tvs
850 in if tv `elemVarSet` tyVarsOfTypes tvs_knds then
851 -- Can't expand away the kinds unless we create
852 -- fresh variables which we don't want to do at this point.
854 else do { rho' <- expandAway tv rho
855 ; return (mkForAllTys tvs rho') }
856 expandAway tv (PredTy pred)
857 = do { pred' <- expandAwayPred tv pred
858 ; return (PredTy pred') }
859 -- For a type constructor application, first try expanding away the
860 -- offending variable from the arguments. If that doesn't work, next
861 -- see if the type constructor is a type synonym, and if so, expand
863 expandAway tv ty@(TyConApp tc tys)
864 = (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv)
866 expandAwayPred :: TcTyVar -> TcPredType -> Maybe TcPredType
867 expandAwayPred tv (ClassP cls tys)
868 = do { tys' <- mapM (expandAway tv) tys; return (ClassP cls tys') }
869 expandAwayPred tv (EqPred ty1 ty2)
870 = do { ty1' <- expandAway tv ty1
871 ; ty2' <- expandAway tv ty2
872 ; return (EqPred ty1' ty2') }
873 expandAwayPred tv (IParam nm ty)
874 = do { ty' <- expandAway tv ty
875 ; return (IParam nm ty') }
881 Note [Type synonyms and canonicalization]
882 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
884 We treat type synonym applications as xi types, that is, they do not
885 count as type function applications. However, we do need to be a bit
886 careful with type synonyms: like type functions they may not be
887 generative or injective. However, unlike type functions, they are
888 parametric, so there is no problem in expanding them whenever we see
889 them, since we do not need to know anything about their arguments in
890 order to expand them; this is what justifies not having to treat them
891 as specially as type function applications. The thing that causes
892 some subtleties is that we prefer to leave type synonym applications
893 *unexpanded* whenever possible, in order to generate better error
896 If we encounter an equality constraint with type synonym applications
897 on both sides, or a type synonym application on one side and some sort
898 of type application on the other, we simply must expand out the type
899 synonyms in order to continue decomposing the equality constraint into
900 primitive equality constraints. For example, suppose we have
904 and we encounter the equality
908 In order to continue we must expand F a into [Int], giving us the
913 which we can then decompose into the more primitive equality
918 However, if we encounter an equality constraint with a type synonym
919 application on one side and a variable on the other side, we should
920 NOT (necessarily) expand the type synonym, since for the purpose of
921 good error messages we want to leave type synonyms unexpanded as much
924 However, there is a subtle point with type synonyms and the occurs
925 check that takes place for equality constraints of the form tv ~ xi.
926 As an example, suppose we have
930 and we come across the equality constraint
934 This should not actually fail the occurs check, since expanding out
935 the type synonym results in the legitimate equality constraint a ~
936 Int. We must actually do this expansion, because unifying a with F a
937 will lead the type checker into infinite loops later. Put another
938 way, canonical equality constraints should never *syntactically*
939 contain the LHS variable in the RHS type. However, we don't always
940 need to expand type synonyms when doing an occurs check; for example,
945 is obviously fine no matter what F expands to. And in this case we
946 would rather unify a with F b (rather than F b's expansion) in order
947 to get better error messages later.
949 So, when doing an occurs check with a type synonym application on the
950 RHS, we use some heuristics to find an expansion of the RHS which does
951 not contain the variable from the LHS. In particular, given
955 we first try expanding each of the ti to types which no longer contain
956 a. If this turns out to be impossible, we next try expanding F
960 %************************************************************************
962 %* Functional dependencies, instantiation of equations
964 %************************************************************************
966 When we spot an equality arising from a functional dependency,
967 we now use that equality (a "wanted") to rewrite the work-item
968 constraint right away. This avoids two dangers
970 Danger 1: If we send the original constraint on down the pipeline
971 it may react with an instance declaration, and in delicate
972 situations (when a Given overlaps with an instance) that
973 may produce new insoluble goals: see Trac #4952
975 Danger 2: If we don't rewrite the constraint, it may re-react
976 with the same thing later, and produce the same equality
977 again --> termination worries.
979 To achieve this required some refactoring of FunDeps.lhs (nicer
983 rewriteWithFunDeps :: [Equation]
985 -> TcS (Maybe ([Xi], [Coercion], WorkList))
986 rewriteWithFunDeps eqn_pred_locs xis fl
987 = do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
988 ; let fd_ev_pos :: [(Int,FlavoredEvVar)]
989 fd_ev_pos = concat fd_ev_poss
990 (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
991 ; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
992 ; let fd_work = unionWorkLists fds
993 ; if isEmptyWorkList fd_work
995 else return (Just (rewritten_xis, cos, fd_work)) }
997 instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived
999 -> TcS [(Int, FlavoredEvVar)]
1000 -- Post: Returns the position index as well as the corresponding FunDep equality
1001 instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
1002 , fd_pred1 = d1, fd_pred2 = d2 })
1003 = do { let tvs = varSetElems qtvs
1004 ; tvs' <- mapM instFlexiTcS tvs
1005 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
1006 ; mapM (do_one subst) eqs }
1009 Given {} -> panic "mkFunDepEqns"
1010 Wanted loc -> Wanted (push_ctx loc)
1011 Derived loc -> Derived (push_ctx loc)
1013 push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1015 do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
1016 = do { let sty1 = Type.substTy subst ty1
1017 sty2 = Type.substTy subst ty2
1018 ; ev <- newCoVar sty1 sty2
1019 ; return (i, mkEvVarX ev fl') }
1021 rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty)
1022 -> [Type] -- A sequence of types: tys
1023 -> [(Type,Coercion)] -- Returns : [(ty', co : ty' ~ ty)]
1024 rewriteDictParams param_eqs tys
1025 = zipWith do_one tys [0..]
1027 do_one :: Type -> Int -> (Type,Coercion)
1028 do_one ty n = case lookup n param_eqs of
1029 Just wev -> (get_fst_ty wev, mkCoVarCo (evVarOf wev))
1030 Nothing -> (ty, mkReflCo ty) -- Identity
1032 get_fst_ty wev = case evVarOfPred wev of
1034 _ -> panic "rewriteDictParams: non equality fundep"
1036 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
1037 -> TcM (TidyEnv, SDoc)
1038 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1039 = do { zpred1 <- TcM.zonkTcPredType pred1
1040 ; zpred2 <- TcM.zonkTcPredType pred2
1041 ; let { tpred1 = tidyPred tidy_env zpred1
1042 ; tpred2 = tidyPred tidy_env zpred2 }
1043 ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1044 nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
1045 nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
1046 ; return (tidy_env, msg) }