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
97 -- Flatten a bunch of types all at once.
98 flattenMany :: CtFlavor -> [Type] -> TcS ([Xi], [Coercion], CanonicalCts)
99 -- Coercions :: Xi ~ Type
101 = do { (xis, cos, cts_s) <- mapAndUnzip3M (flatten ctxt) tys
102 ; return (xis, cos, andCCans cts_s) }
104 -- Flatten a type to get rid of type function applications, returning
105 -- the new type-function-free type, and a collection of new equality
106 -- constraints. See Note [Flattening] for more detail.
107 flatten :: CtFlavor -> TcType -> TcS (Xi, Coercion, CanonicalCts)
108 -- Postcondition: Coercion :: Xi ~ TcType
110 | Just ty' <- tcView ty
111 = do { (xi, co, ccs) <- flatten ctxt ty'
112 -- Preserve type synonyms if possible
113 -- We can tell if ty' is function-free by
114 -- whether there are any floated constraints
115 ; if isEmptyCCan ccs then
116 return (ty, ty, emptyCCan)
118 return (xi, co, ccs) }
120 flatten _ v@(TyVarTy _)
121 = return (v, v, emptyCCan)
123 flatten ctxt (AppTy ty1 ty2)
124 = do { (xi1,co1,c1) <- flatten ctxt ty1
125 ; (xi2,co2,c2) <- flatten ctxt ty2
126 ; return (mkAppTy xi1 xi2, mkAppCoercion co1 co2, c1 `andCCan` c2) }
128 flatten ctxt (FunTy ty1 ty2)
129 = do { (xi1,co1,c1) <- flatten ctxt ty1
130 ; (xi2,co2,c2) <- flatten ctxt ty2
131 ; return (mkFunTy xi1 xi2, mkFunCoercion co1 co2, c1 `andCCan` c2) }
133 flatten fl (TyConApp tc tys)
134 -- For a normal type constructor or data family application, we just
135 -- recursively flatten the arguments.
136 | not (isSynFamilyTyCon tc)
137 = do { (xis,cos,ccs) <- flattenMany fl tys
138 ; return (mkTyConApp tc xis, mkTyConCoercion tc cos, ccs) }
140 -- Otherwise, it's a type function application, and we have to
141 -- flatten it away as well, and generate a new given equality constraint
142 -- between the application and a newly generated flattening skolem variable.
144 = ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated
145 do { (xis, cos, ccs) <- flattenMany fl tys
146 ; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis
147 (cos_args, cos_rest) = splitAt (tyConArity tc) cos
148 -- The type function might be *over* saturated
149 -- in which case the remaining arguments should
150 -- be dealt with by AppTys
151 fam_ty = mkTyConApp tc xi_args
152 fam_co = fam_ty -- identity
153 ; (ret_co, rhs_var, ct) <-
154 do { is_cached <- lookupFlatCacheMap tc xi_args fl
156 Just (rhs_var,ret_co,_fl) -> return (ret_co, rhs_var, emptyCCan)
158 | isGivenOrSolved fl ->
159 do { rhs_var <- newFlattenSkolemTy fam_ty
160 ; cv <- newGivenCoVar fam_ty rhs_var fam_co
161 ; let ct = CFunEqCan { cc_id = cv
162 , cc_flavor = fl -- Given
164 , cc_tyargs = xi_args
166 ; let ret_co = mkCoVarCoercion cv
167 ; updateFlatCacheMap tc xi_args rhs_var fl ret_co
168 ; return $ (ret_co, rhs_var, singleCCan ct) }
170 -- Derived or Wanted: make a new *unification* flatten variable
171 do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
172 ; cv <- newCoVar fam_ty rhs_var
173 ; let ct = CFunEqCan { cc_id = cv
174 , cc_flavor = mkWantedFlavor fl
175 -- Always Wanted, not Derived
177 , cc_tyargs = xi_args
179 ; let ret_co = mkCoVarCoercion cv
180 ; updateFlatCacheMap tc xi_args rhs_var fl ret_co
181 ; return $ (ret_co, rhs_var, singleCCan ct) } }
182 ; return ( foldl AppTy rhs_var xi_rest
183 , foldl AppTy (mkSymCoercion ret_co
184 `mkTransCoercion` mkTyConCoercion tc cos_args) cos_rest
185 , ccs `andCCan` ct) }
188 flatten ctxt (PredTy pred)
189 = do { (pred', co, ccs) <- flattenPred ctxt pred
190 ; return (PredTy pred', co, ccs) }
192 flatten ctxt ty@(ForAllTy {})
193 -- We allow for-alls when, but only when, no type function
194 -- applications inside the forall involve the bound type variables
195 -- TODO: What if it is a (t1 ~ t2) => t3
196 -- Must revisit when the New Coercion API is here!
197 = do { let (tvs, rho) = splitForAllTys ty
198 ; (rho', co, ccs) <- flatten ctxt rho
199 ; let bad_eqs = filterBag is_bad ccs
200 is_bad c = tyVarsOfCanonical c `intersectsVarSet` tv_set
201 tv_set = mkVarSet tvs
202 ; unless (isEmptyBag bad_eqs)
203 (flattenForAllErrorTcS ctxt ty bad_eqs)
204 ; return (mkForAllTys tvs rho', mkForAllTys tvs co, ccs) }
207 flattenPred :: CtFlavor -> TcPredType -> TcS (TcPredType, Coercion, CanonicalCts)
208 flattenPred ctxt (ClassP cls tys)
209 = do { (tys', cos, ccs) <- flattenMany ctxt tys
210 ; return (ClassP cls tys', mkClassPPredCo cls cos, ccs) }
211 flattenPred ctxt (IParam nm ty)
212 = do { (ty', co, ccs) <- flatten ctxt ty
213 ; return (IParam nm ty', mkIParamPredCo nm co, ccs) }
214 -- TODO: Handling of coercions between EqPreds must be revisited once the New Coercion API is ready!
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', mkEqPredCo co1 co2, ccs1 `andCCan` ccs2) }
222 %************************************************************************
224 %* Canonicalising given constraints *
226 %************************************************************************
229 canWanteds :: [WantedEvVar] -> TcS WorkList
230 canWanteds = fmap unionWorkLists . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
232 canGivens :: GivenLoc -> [EvVar] -> TcS WorkList
233 canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc GivenOrig)) givens
234 ; return (unionWorkLists ccs) }
236 mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList
237 mkCanonicals fl vs = fmap unionWorkLists (mapM (mkCanonical fl) vs)
239 mkCanonicalFEV :: FlavoredEvVar -> TcS WorkList
240 mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev
242 mkCanonicalFEVs :: Bag FlavoredEvVar -> TcS WorkList
243 mkCanonicalFEVs = foldrBagM canon_one emptyWorkList
244 where -- Preserves order (shouldn't be important, but curently
245 -- is important for the vectoriser)
246 canon_one fev wl = do { wl' <- mkCanonicalFEV fev
247 ; return (unionWorkList wl' wl) }
250 mkCanonical :: CtFlavor -> EvVar -> TcS WorkList
251 mkCanonical fl ev = case evVarPred ev of
252 ClassP clas tys -> canClassToWorkList fl ev clas tys
253 IParam ip ty -> canIPToWorkList fl ev ip ty
254 EqPred ty1 ty2 -> canEqToWorkList fl ev ty1 ty2
257 canClassToWorkList :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS WorkList
258 canClassToWorkList fl v cn tys
259 = do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys
260 ; let no_flattening_happened = isEmptyCCan ccs
261 dict_co = mkTyConCoercion (classTyCon cn) cos
262 ; v_new <- if no_flattening_happened then return v
263 else if isGivenOrSolved fl then return v
264 -- The cos are all identities if fl=Given,
265 -- hence nothing to do
266 else do { v' <- newDictVar cn xis -- D xis
267 ; when (isWanted fl) $ setDictBind v (EvCast v' dict_co)
268 ; when (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCoercion dict_co))
269 -- NB: No more setting evidence for derived now
272 -- Add the superclasses of this one here, See Note [Adding superclasses].
273 -- But only if we are not simplifying the LHS of a rule.
274 ; sctx <- getTcSContext
275 ; sc_cts <- if simplEqsOnly sctx then return emptyWorkList
276 else newSCWorkFromFlavored v_new fl cn xis
278 ; return (sc_cts `unionWorkList`
279 workListFromEqs ccs `unionWorkList`
280 workListFromNonEq CDictCan { cc_id = v_new
283 , cc_tyargs = xis }) }
286 Note [Adding superclasses]
287 ~~~~~~~~~~~~~~~~~~~~~~~~~~
288 Since dictionaries are canonicalized only once in their lifetime, the
289 place to add their superclasses is canonicalisation (The alternative
290 would be to do it during constraint solving, but we'd have to be
291 extremely careful to not repeatedly introduced the same superclass in
292 our worklist). Here is what we do:
295 We add all their superclasses as Givens.
298 Generally speaking we want to be able to add superclasses of
299 wanteds for two reasons:
301 (1) Oportunities for improvement. Example:
302 class (a ~ b) => C a b
303 Wanted constraint is: C alpha beta
304 We'd like to simply have C alpha alpha. Similar
305 situations arise in relation to functional dependencies.
307 (2) To have minimal constraints to quantify over:
308 For instance, if our wanted constraint is (Eq a, Ord a)
309 we'd only like to quantify over Ord a.
311 To deal with (1) above we only add the superclasses of wanteds
312 which may lead to improvement, that is: equality superclasses or
313 superclasses with functional dependencies.
315 We deal with (2) completely independently in TcSimplify. See
316 Note [Minimize by SuperClasses] in TcSimplify.
319 Moreover, in all cases the extra improvement constraints are
320 Derived. Derived constraints have an identity (for now), but
321 we don't do anything with their evidence. For instance they
322 are never used to rewrite other constraints.
324 See also [New Wanted Superclass Work] in TcInteract.
330 Here's an example that demonstrates why we chose to NOT add
331 superclasses during simplification: [Comes from ticket #4497]
333 class Num (RealOf t) => Normed t
336 Assume the generated wanted constraint is:
337 RealOf e ~ e, Normed e
338 If we were to be adding the superclasses during simplification we'd get:
339 Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf
341 e ~ uf, Num uf, Normed e, RealOf e ~ e
342 ==> [Spontaneous solve]
343 Num uf, Normed uf, RealOf uf ~ uf
345 While looks exactly like our original constraint. If we add the superclass again we'd loop.
346 By adding superclasses definitely only once, during canonicalisation, this situation can't
351 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
352 -- Returns superclasses, see Note [Adding superclasses]
353 newSCWorkFromFlavored ev orig_flavor cls xis
354 | isDerived orig_flavor
355 = return emptyWorkList -- Deriveds don't yield more superclasses because we will
356 -- add them transitively in the case of wanteds.
358 | Just gk <- isGiven_maybe orig_flavor
360 GivenOrig -> do { let sc_theta = immSuperClasses cls xis
362 ; sc_vars <- mapM newEvVar sc_theta
363 ; _ <- zipWithM_ setEvBind sc_vars [EvSuperClass ev n | n <- [0..]]
364 ; mkCanonicals flavor sc_vars }
365 GivenSolved -> return emptyWorkList
366 -- Seems very dangerous to add the superclasses for dictionaries that may be
367 -- partially solved because we may end up with evidence loops.
369 | isEmptyVarSet (tyVarsOfTypes xis)
370 = return emptyWorkList -- Wanteds with no variables yield no deriveds.
371 -- See Note [Improvement from Ground Wanteds]
373 | otherwise -- Wanted case, just add those SC that can lead to improvement.
374 = do { let sc_rec_theta = transSuperClasses cls xis
375 impr_theta = filter is_improvement_pty sc_rec_theta
376 Wanted wloc = orig_flavor
377 ; der_ids <- mapM newDerivedId impr_theta
378 ; mkCanonicals (Derived wloc) der_ids }
381 is_improvement_pty :: PredType -> Bool
382 -- Either it's an equality, or has some functional dependency
383 is_improvement_pty (EqPred {}) = True
384 is_improvement_pty (ClassP cls _ty) = not $ null fundeps
385 where (_,fundeps,_,_,_,_) = classExtraBigSig cls
386 is_improvement_pty _ = False
391 canIPToWorkList :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS WorkList
392 -- See Note [Canonical implicit parameter constraints] to see why we don't
393 -- immediately canonicalize (flatten) IP constraints.
394 canIPToWorkList fl v nm ty
395 = return $ workListFromNonEq (CIPCan { cc_id = v
401 canEqToWorkList :: CtFlavor -> EvVar -> Type -> Type -> TcS WorkList
402 canEqToWorkList fl cv ty1 ty2 = do { cts <- canEq fl cv ty1 ty2
403 ; return $ workListFromEqs cts }
405 canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts
407 | tcEqType ty1 ty2 -- Dealing with equality here avoids
408 -- later spurious occurs checks for a~a
409 = do { when (isWanted fl) (setCoBind cv ty1)
412 -- If one side is a variable, orient and flatten,
413 -- WITHOUT expanding type synonyms, so that we tend to
414 -- substitute a ~ Age rather than a ~ Int when @type Age = Int@
415 canEq fl cv ty1@(TyVarTy {}) ty2
416 = do { untch <- getUntouchables
417 ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
418 canEq fl cv ty1 ty2@(TyVarTy {})
419 = do { untch <- getUntouchables
420 ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
421 -- NB: don't use VarCls directly because tv1 or tv2 may be scolems!
423 canEq fl cv (TyConApp fn tys) ty2
424 | isSynFamilyTyCon fn, length tys == tyConArity fn
425 = do { untch <- getUntouchables
426 ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) }
427 canEq fl cv ty1 (TyConApp fn tys)
428 | isSynFamilyTyCon fn, length tys == tyConArity fn
429 = do { untch <- getUntouchables
430 ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) }
433 | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe s1,
434 Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2
436 <- if isWanted fl then -- Wanted
437 do { v1 <- newCoVar t1a t2a
438 ; v2 <- newCoVar t1b t2b
439 ; v3 <- newCoVar t1c t2c
440 ; let res_co = mkCoPredCo (mkCoVarCoercion v1)
441 (mkCoVarCoercion v2) (mkCoVarCoercion v3)
442 ; setCoBind cv res_co
443 ; return (v1,v2,v3) }
444 else if isGivenOrSolved fl then -- Given
445 let co_orig = mkCoVarCoercion cv
446 coa = mkCsel1Coercion co_orig
447 cob = mkCsel2Coercion co_orig
448 coc = mkCselRCoercion co_orig
449 in do { v1 <- newGivenCoVar t1a t2a coa
450 ; v2 <- newGivenCoVar t1b t2b cob
451 ; v3 <- newGivenCoVar t1c t2c coc
452 ; return (v1,v2,v3) }
454 do { v1 <- newDerivedId (EqPred t1a t2a)
455 ; v2 <- newDerivedId (EqPred t1b t2b)
456 ; v3 <- newDerivedId (EqPred t1c t2c)
457 ; return (v1,v2,v3) }
458 ; cc1 <- canEq fl v1 t1a t2a
459 ; cc2 <- canEq fl v2 t1b t2b
460 ; cc3 <- canEq fl v3 t1c t2c
461 ; return (cc1 `andCCan` cc2 `andCCan` cc3) }
464 -- Split up an equality between function types into two equalities.
465 canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
466 = do { (argv, resv) <-
468 do { argv <- newCoVar s1 s2
469 ; resv <- newCoVar t1 t2
471 mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv)
472 ; return (argv,resv) }
474 else if isGivenOrSolved fl then
475 let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv)
476 in do { argv <- newGivenCoVar s1 s2 arg
477 ; resv <- newGivenCoVar t1 t2 res
478 ; return (argv,resv) }
481 do { argv <- newDerivedId (EqPred s1 s2)
482 ; resv <- newDerivedId (EqPred t1 t2)
483 ; return (argv,resv) }
485 ; cc1 <- canEq fl argv s1 s2 -- inherit original kinds and locations
486 ; cc2 <- canEq fl resv t1 t2
487 ; return (cc1 `andCCan` cc2) }
489 canEq fl cv (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2))
491 = if isWanted fl then
492 do { v <- newCoVar t1 t2
493 ; setCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv)
495 else return emptyCCan -- DV: How to decompose given IP coercions?
497 canEq fl cv (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2))
499 = if isWanted fl then
500 do { vs <- zipWithM newCoVar tys1 tys2
501 ; setCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs)
502 ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2
504 else return emptyCCan
505 -- How to decompose given dictionary (and implicit parameter) coercions?
506 -- You may think that the following is right:
507 -- let cos = decomposeCo (length tys1) (mkCoVarCoercion cv)
508 -- in zipWith3M newGivOrDerCoVar tys1 tys2 cos
509 -- But this assumes that the coercion is a type constructor-based
510 -- coercion, and not a PredTy (ClassP cn cos) coercion. So we chose
511 -- to not decompose these coercions. We have to get back to this
512 -- when we clean up the Coercion API.
514 canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
515 | isAlgTyCon tc1 && isAlgTyCon tc2
517 , length tys1 == length tys2
518 = -- Generate equalities for each of the corresponding arguments
520 <- if isWanted fl then
521 do { argsv <- zipWithM newCoVar tys1 tys2
523 mkTyConCoercion tc1 (map mkCoVarCoercion argsv)
526 else if isGivenOrSolved fl then
527 let cos = decomposeCo (length tys1) (mkCoVarCoercion cv)
528 in zipWith3M newGivenCoVar tys1 tys2 cos
531 zipWithM (\t1 t2 -> newDerivedId (EqPred t1 t2)) tys1 tys2
533 ; andCCans <$> zipWith3M (canEq fl) argsv tys1 tys2 }
535 -- See Note [Equality between type applications]
536 -- Note [Care with type applications] in TcUnify
538 | Just (s1,t1) <- tcSplitAppTy_maybe ty1
539 , Just (s2,t2) <- tcSplitAppTy_maybe ty2
542 then do { cv1 <- newCoVar s1 s2
543 ; cv2 <- newCoVar t1 t2
545 mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2)
548 else if isGivenOrSolved fl then
549 let co1 = mkLeftCoercion $ mkCoVarCoercion cv
550 co2 = mkRightCoercion $ mkCoVarCoercion cv
551 in do { cv1 <- newGivenCoVar s1 s2 co1
552 ; cv2 <- newGivenCoVar t1 t2 co2
555 do { cv1 <- newDerivedId (EqPred s1 s2)
556 ; cv2 <- newDerivedId (EqPred t1 t2)
559 ; cc1 <- canEq fl cv1 s1 s2
560 ; cc2 <- canEq fl cv2 t1 t2
561 ; return (cc1 `andCCan` cc2) }
563 canEq fl cv s1@(ForAllTy {}) s2@(ForAllTy {})
564 | tcIsForAllTy s1, tcIsForAllTy s2,
568 = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
571 -- Finally expand any type synonym applications.
572 canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2
573 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2'
574 canEq fl cv _ _ = canEqFailure fl cv
576 canEqFailure :: CtFlavor -> EvVar -> TcS CanonicalCts
577 canEqFailure fl cv = return (singleCCan (mkFrozenError fl cv))
580 Note [Equality between type applications]
581 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
582 If we see an equality of the form s1 t1 ~ s2 t2 we can always split
583 it up into s1 ~ s2 /\ t1 ~ t2, since s1 and s2 can't be type
584 functions (type functions use the TyConApp constructor, which never
585 shows up as the LHS of an AppTy). Other than type functions, types
586 in Haskell are always
588 (1) generative: a b ~ c d implies a ~ c, since different type
589 constructors always generate distinct types
591 (2) injective: a b ~ a d implies b ~ d; we never generate the
592 same type from different type arguments.
595 Note [Canonical ordering for equality constraints]
596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
597 Implemented as (<+=) below:
599 - Type function applications always come before anything else.
600 - Variables always come before non-variables (other than type
601 function applications).
603 Note that we don't need to unfold type synonyms on the RHS to check
604 the ordering; that is, in the rules above it's OK to consider only
605 whether something is *syntactically* a type function application or
606 not. To illustrate why this is OK, suppose we have an equality of the
607 form 'tv ~ S a b c', where S is a type synonym which expands to a
608 top-level application of the type function F, something like
612 Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's
613 expansion contains type function applications the flattener will do
614 the expansion and then generate a skolem variable for the type
615 function application, so we end up with something like this:
620 where x is the skolem variable. This is one extra equation than
621 absolutely necessary (we could have gotten away with just 'F d e ~ tv'
622 if we had noticed that S expanded to a top-level type function
623 application and flipped it around in the first place) but this way
624 keeps the code simpler.
626 Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the
627 ordering of tv ~ tv constraints. There are several reasons why we
630 (1) In order to be able to extract a substitution that doesn't
631 mention untouchable variables after we are done solving, we might
632 prefer to put touchable variables on the left. However, in and
633 of itself this isn't necessary; we can always re-orient equality
634 constraints at the end if necessary when extracting a substitution.
636 (2) To ensure termination we might think it necessary to put
637 variables in lexicographic order. However, this isn't actually
638 necessary as outlined below.
640 While building up an inert set of canonical constraints, we maintain
641 the invariant that the equality constraints in the inert set form an
642 acyclic rewrite system when viewed as L-R rewrite rules. Moreover,
643 the given constraints form an idempotent substitution (i.e. none of
644 the variables on the LHS occur in any of the RHS's, and type functions
645 never show up in the RHS at all), the wanted constraints also form an
646 idempotent substitution, and finally the LHS of a given constraint
647 never shows up on the RHS of a wanted constraint. There may, however,
648 be a wanted LHS that shows up in a given RHS, since we do not rewrite
649 given constraints with wanted constraints.
651 Suppose we have an inert constraint set
654 tg_1 ~ xig_1 -- givens
657 tw_1 ~ xiw_1 -- wanteds
661 where each t_i can be either a type variable or a type function
662 application. Now suppose we take a new canonical equality constraint,
663 t' ~ xi' (note among other things this means t' does not occur in xi')
664 and try to react it with the existing inert set. We show by induction
665 on the number of t_i which occur in t' ~ xi' that this process will
668 There are several ways t' ~ xi' could react with an existing constraint:
670 TODO: finish this proof. The below was for the case where the entire
671 inert set is an idempotent subustitution...
673 (b) We could have t' = t_j for some j. Then we obtain the new
674 equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j. We
675 now canonicalize the new equality, which may involve decomposing it
676 into several canonical equalities, and recurse on these. However,
677 none of the new equalities will contain t_j, so they have fewer
678 occurrences of the t_i than the original equation.
680 (a) We could have t_j occurring in xi' for some j, with t' /=
681 t_j. Then we substitute xi_j for t_j in xi' and continue. However,
682 since none of the t_i occur in xi_j, we have decreased the
683 number of t_i that occur in xi', since we eliminated t_j and did not
684 introduce any new ones.
688 = FskCls TcTyVar -- ^ Flatten skolem
689 | VarCls TcTyVar -- ^ Non-flatten-skolem variable
690 | FunCls TyCon [Type] -- ^ Type function, exactly saturated
691 | OtherCls TcType -- ^ Neither of the above
693 unClassify :: TypeClassifier -> TcType
694 unClassify (VarCls tv) = TyVarTy tv
695 unClassify (FskCls tv) = TyVarTy tv
696 unClassify (FunCls fn tys) = TyConApp fn tys
697 unClassify (OtherCls ty) = ty
699 classify :: TcType -> TypeClassifier
701 classify (TyVarTy tv)
703 FlatSkol {} <- tcTyVarDetails tv = FskCls tv
704 | otherwise = VarCls tv
705 classify (TyConApp tc tys) | isSynFamilyTyCon tc
706 , tyConArity tc == length tys
708 classify ty | Just ty' <- tcView ty
709 = case classify ty' of
710 OtherCls {} -> OtherCls ty
711 var_or_fn -> var_or_fn
715 -- See note [Canonical ordering for equality constraints].
716 reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool
717 -- (t1 `reOrient` t2) responds True
718 -- iff we should flip to (t2~t1)
719 -- We try to say False if possible, to minimise evidence generation
721 -- Postcondition: After re-orienting, first arg is not OTherCls
722 reOrient _fl (OtherCls {}) (FunCls {}) = True
723 reOrient _fl (OtherCls {}) (FskCls {}) = True
724 reOrient _fl (OtherCls {}) (VarCls {}) = True
725 reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
727 reOrient _fl (FunCls {}) (VarCls _tv) = False
728 -- But consider the following variation: isGiven fl && isMetaTyVar tv
730 -- See Note [No touchables as FunEq RHS] in TcSMonad
731 reOrient _fl (FunCls {}) _ = False -- Fun/Other on rhs
733 reOrient _fl (VarCls {}) (FunCls {}) = True
735 reOrient _fl (VarCls {}) (FskCls {}) = False
737 reOrient _fl (VarCls {}) (OtherCls {}) = False
738 reOrient _fl (VarCls tv1) (VarCls tv2)
739 | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True
741 -- Just for efficiency, see CTyEqCan invariants
743 reOrient _fl (FskCls {}) (VarCls tv2) = isMetaTyVar tv2
744 -- Just for efficiency, see CTyEqCan invariants
746 reOrient _fl (FskCls {}) (FskCls {}) = False
747 reOrient _fl (FskCls {}) (FunCls {}) = True
748 reOrient _fl (FskCls {}) (OtherCls {}) = False
751 canEqLeaf :: TcsUntouchables
753 -> TypeClassifier -> TypeClassifier -> TcS CanonicalCts
754 -- Canonicalizing "leaf" equality constraints which cannot be
755 -- decomposed further (ie one of the types is a variable or
756 -- saturated type function application).
759 -- * one of the two arguments is not OtherCls
760 -- * the two types are not equal (looking through synonyms)
761 canEqLeaf _untch fl cv cls1 cls2
762 | cls1 `re_orient` cls2
763 = do { cv' <- if isWanted fl
764 then do { cv' <- newCoVar s2 s1
765 ; setCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
767 else if isGivenOrSolved fl then
768 newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv))
770 newDerivedId (EqPred s2 s1)
771 ; canEqLeafOriented fl cv' cls2 s1 }
774 = do { traceTcS "canEqLeaf" (ppr (unClassify cls1) $$ ppr (unClassify cls2))
775 ; canEqLeafOriented fl cv cls1 s2 }
777 re_orient = reOrient fl
782 canEqLeafOriented :: CtFlavor -> CoVar
783 -> TypeClassifier -> TcType -> TcS CanonicalCts
784 -- First argument is not OtherCls
785 canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1
786 | let k1 = kindAppResult (tyConKind fn) tys1,
787 let k2 = typeKind s2,
788 not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan
790 -- Eagerly fails, see Note [Kind errors] in TcInteract
793 = ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) )
794 do { (xis1,cos1,ccs1) <- flattenMany fl tys1 -- Flatten type function arguments
795 -- cos1 :: xis1 ~ tys1
796 ; (xi2, co2, ccs2) <- flatten fl s2 -- Flatten entire RHS
798 ; let ccs = ccs1 `andCCan` ccs2
799 no_flattening_happened = isEmptyCCan ccs
800 ; cv_new <- if no_flattening_happened then return cv
801 else if isGivenOrSolved fl then return cv
802 else if isWanted fl then
803 do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2
805 ; let -- fun_co :: F xis1 ~ F tys1
806 fun_co = mkTyConCoercion fn cos1
807 -- want_co :: F tys1 ~ s2
808 want_co = mkSymCoercion fun_co
809 `mkTransCoercion` mkCoVarCoercion cv'
810 `mkTransCoercion` co2
811 ; setCoBind cv want_co
814 newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2)
816 ; let final_cc = CFunEqCan { cc_id = cv_new
821 ; return $ ccs `extendCCans` final_cc }
823 -- Otherwise, we have a variable on the left, so call canEqLeafTyVarLeft
824 canEqLeafOriented fl cv (FskCls tv) s2
825 = canEqLeafTyVarLeft fl cv tv s2
826 canEqLeafOriented fl cv (VarCls tv) s2
827 = canEqLeafTyVarLeft fl cv tv s2
828 canEqLeafOriented _ cv (OtherCls ty1) ty2
829 = pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2)
831 canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS CanonicalCts
832 -- Establish invariants of CTyEqCans
833 canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2
834 | not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan
836 -- Eagerly fails, see Note [Kind errors] in TcInteract
838 = do { (xi2, co, ccs2) <- flatten fl s2 -- Flatten RHS co : xi2 ~ s2
839 ; mxi2' <- canOccursCheck fl tv xi2 -- Do an occurs check, and return a possibly
840 -- unfolded version of the RHS, if we had to
841 -- unfold any type synonyms to get rid of tv.
843 Nothing -> canEqFailure fl cv ;
845 do { let no_flattening_happened = isEmptyCCan ccs2
846 ; cv_new <- if no_flattening_happened then return cv
847 else if isGivenOrSolved fl then return cv
848 else if isWanted fl then
849 do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
850 ; setCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co)
853 newDerivedId (EqPred (mkTyVarTy tv) xi2')
855 ; return $ ccs2 `extendCCans` CTyEqCan { cc_id = cv_new
858 , cc_rhs = xi2' } } } }
863 -- See Note [Type synonyms and canonicalization].
864 -- Check whether the given variable occurs in the given type. We may
865 -- have needed to do some type synonym unfolding in order to get rid
866 -- of the variable, so we also return the unfolded version of the
867 -- type, which is guaranteed to be syntactically free of the given
868 -- type variable. If the type is already syntactically free of the
869 -- variable, then the same type is returned.
871 -- Precondition: the two types are not equal (looking though synonyms)
872 canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi)
873 canOccursCheck _gw tv xi = return (expandAway tv xi)
876 @expandAway tv xi@ expands synonyms in xi just enough to get rid of
877 occurrences of tv, if that is possible; otherwise, it returns Nothing.
878 For example, suppose we have
881 expandAway b (F Int b) = Just [Int]
883 expandAway a (F a Int) = Nothing
885 We don't promise to do the absolute minimum amount of expanding
886 necessary, but we try not to do expansions we don't need to. We
887 prefer doing inner expansions first. For example,
888 type F a b = (a, Int, a, [a])
891 expandAway b (F (G b)) = F Char
892 even though we could also expand F to get rid of b.
895 expandAway :: TcTyVar -> Xi -> Maybe Xi
896 expandAway tv t@(TyVarTy tv')
897 | tv == tv' = Nothing
900 | not (tv `elemVarSet` tyVarsOfType xi) = Just xi
901 expandAway tv (AppTy ty1 ty2)
902 = do { ty1' <- expandAway tv ty1
903 ; ty2' <- expandAway tv ty2
904 ; return (mkAppTy ty1' ty2') }
905 -- mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2
906 expandAway tv (FunTy ty1 ty2)
907 = do { ty1' <- expandAway tv ty1
908 ; ty2' <- expandAway tv ty2
909 ; return (mkFunTy ty1' ty2') }
910 -- mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2
911 expandAway tv ty@(ForAllTy {})
912 = let (tvs,rho) = splitForAllTys ty
913 tvs_knds = map tyVarKind tvs
914 in if tv `elemVarSet` tyVarsOfTypes tvs_knds then
915 -- Can't expand away the kinds unless we create
916 -- fresh variables which we don't want to do at this point.
918 else do { rho' <- expandAway tv rho
919 ; return (mkForAllTys tvs rho') }
920 expandAway tv (PredTy pred)
921 = do { pred' <- expandAwayPred tv pred
922 ; return (PredTy pred') }
923 -- For a type constructor application, first try expanding away the
924 -- offending variable from the arguments. If that doesn't work, next
925 -- see if the type constructor is a type synonym, and if so, expand
927 expandAway tv ty@(TyConApp tc tys)
928 = (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv)
930 expandAwayPred :: TcTyVar -> TcPredType -> Maybe TcPredType
931 expandAwayPred tv (ClassP cls tys)
932 = do { tys' <- mapM (expandAway tv) tys; return (ClassP cls tys') }
933 expandAwayPred tv (EqPred ty1 ty2)
934 = do { ty1' <- expandAway tv ty1
935 ; ty2' <- expandAway tv ty2
936 ; return (EqPred ty1' ty2') }
937 expandAwayPred tv (IParam nm ty)
938 = do { ty' <- expandAway tv ty
939 ; return (IParam nm ty') }
945 Note [Type synonyms and canonicalization]
946 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
948 We treat type synonym applications as xi types, that is, they do not
949 count as type function applications. However, we do need to be a bit
950 careful with type synonyms: like type functions they may not be
951 generative or injective. However, unlike type functions, they are
952 parametric, so there is no problem in expanding them whenever we see
953 them, since we do not need to know anything about their arguments in
954 order to expand them; this is what justifies not having to treat them
955 as specially as type function applications. The thing that causes
956 some subtleties is that we prefer to leave type synonym applications
957 *unexpanded* whenever possible, in order to generate better error
960 If we encounter an equality constraint with type synonym applications
961 on both sides, or a type synonym application on one side and some sort
962 of type application on the other, we simply must expand out the type
963 synonyms in order to continue decomposing the equality constraint into
964 primitive equality constraints. For example, suppose we have
968 and we encounter the equality
972 In order to continue we must expand F a into [Int], giving us the
977 which we can then decompose into the more primitive equality
982 However, if we encounter an equality constraint with a type synonym
983 application on one side and a variable on the other side, we should
984 NOT (necessarily) expand the type synonym, since for the purpose of
985 good error messages we want to leave type synonyms unexpanded as much
988 However, there is a subtle point with type synonyms and the occurs
989 check that takes place for equality constraints of the form tv ~ xi.
990 As an example, suppose we have
994 and we come across the equality constraint
998 This should not actually fail the occurs check, since expanding out
999 the type synonym results in the legitimate equality constraint a ~
1000 Int. We must actually do this expansion, because unifying a with F a
1001 will lead the type checker into infinite loops later. Put another
1002 way, canonical equality constraints should never *syntactically*
1003 contain the LHS variable in the RHS type. However, we don't always
1004 need to expand type synonyms when doing an occurs check; for example,
1009 is obviously fine no matter what F expands to. And in this case we
1010 would rather unify a with F b (rather than F b's expansion) in order
1011 to get better error messages later.
1013 So, when doing an occurs check with a type synonym application on the
1014 RHS, we use some heuristics to find an expansion of the RHS which does
1015 not contain the variable from the LHS. In particular, given
1019 we first try expanding each of the ti to types which no longer contain
1020 a. If this turns out to be impossible, we next try expanding F
1024 %************************************************************************
1026 %* Functional dependencies, instantiation of equations
1028 %************************************************************************
1030 When we spot an equality arising from a functional dependency,
1031 we now use that equality (a "wanted") to rewrite the work-item
1032 constraint right away. This avoids two dangers
1034 Danger 1: If we send the original constraint on down the pipeline
1035 it may react with an instance declaration, and in delicate
1036 situations (when a Given overlaps with an instance) that
1037 may produce new insoluble goals: see Trac #4952
1039 Danger 2: If we don't rewrite the constraint, it may re-react
1040 with the same thing later, and produce the same equality
1041 again --> termination worries.
1043 To achieve this required some refactoring of FunDeps.lhs (nicer
1047 rewriteWithFunDeps :: [Equation]
1049 -> TcS (Maybe ([Xi], [Coercion], WorkList))
1050 rewriteWithFunDeps eqn_pred_locs xis fl
1051 = do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
1052 ; let fd_ev_pos :: [(Int,FlavoredEvVar)]
1053 fd_ev_pos = concat fd_ev_poss
1054 (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
1055 ; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
1056 ; let fd_work = unionWorkLists fds
1057 ; if isEmptyWorkList fd_work
1059 else return (Just (rewritten_xis, cos, fd_work)) }
1061 instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived
1063 -> TcS [(Int, FlavoredEvVar)]
1064 -- Post: Returns the position index as well as the corresponding FunDep equality
1065 instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
1066 , fd_pred1 = d1, fd_pred2 = d2 })
1067 = do { let tvs = varSetElems qtvs
1068 ; tvs' <- mapM instFlexiTcS tvs
1069 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
1070 ; mapM (do_one subst) eqs }
1073 Given {} -> panic "mkFunDepEqns"
1074 Wanted loc -> Wanted (push_ctx loc)
1075 Derived loc -> Derived (push_ctx loc)
1077 push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1079 do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
1080 = do { let sty1 = substTy subst ty1
1081 sty2 = substTy subst ty2
1082 ; ev <- newCoVar sty1 sty2
1083 ; return (i, mkEvVarX ev fl') }
1085 rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty)
1086 -> [Type] -- A sequence of types: tys
1087 -> [(Type,Coercion)] -- Returns : [(ty', co : ty' ~ ty)]
1088 rewriteDictParams param_eqs tys
1089 = zipWith do_one tys [0..]
1091 do_one :: Type -> Int -> (Type,Coercion)
1092 do_one ty n = case lookup n param_eqs of
1093 Just wev -> (get_fst_ty wev, mkCoVarCoercion (evVarOf wev))
1094 Nothing -> (ty,ty) -- Identity
1096 get_fst_ty wev = case evVarOfPred wev of
1098 _ -> panic "rewriteDictParams: non equality fundep"
1100 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
1101 -> TcM (TidyEnv, SDoc)
1102 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1103 = do { zpred1 <- TcM.zonkTcPredType pred1
1104 ; zpred2 <- TcM.zonkTcPredType pred2
1105 ; let { tpred1 = tidyPred tidy_env zpred1
1106 ; tpred2 = tidyPred tidy_env zpred2 }
1107 ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1108 nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
1109 nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
1110 ; return (tidy_env, msg) }