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
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, mkReflCo ty, emptyCCan)
118 return (xi, co, ccs) }
120 flatten _ v@(TyVarTy _)
121 = return (v, mkReflCo 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, mkAppCo 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, mkFunCo 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, mkTyConAppCo 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 = mkReflCo fam_ty -- identity
154 ; (ret_co, rhs_var, ct) <-
156 do { rhs_var <- newFlattenSkolemTy fam_ty
157 ; cv <- newGivenCoVar fam_ty rhs_var fam_co
158 ; let ct = CFunEqCan { cc_id = cv
159 , cc_flavor = fl -- Given
161 , cc_tyargs = xi_args
163 ; return $ (mkCoVarCo cv, rhs_var, ct) }
164 else -- Derived or Wanted: make a new *unification* flatten variable
165 do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
166 ; cv <- newCoVar fam_ty rhs_var
167 ; let ct = CFunEqCan { cc_id = cv
168 , cc_flavor = mkWantedFlavor fl
169 -- Always Wanted, not Derived
171 , cc_tyargs = xi_args
173 ; return $ (mkCoVarCo cv, rhs_var, ct) }
175 ; return ( foldl AppTy rhs_var xi_rest
178 `mkTransCo` mkTyConAppCo tc cos_args)
180 , ccs `extendCCans` ct) }
183 flatten ctxt (PredTy pred)
184 = do { (pred', co, ccs) <- flattenPred ctxt pred
185 ; return (PredTy pred', co, ccs) }
187 flatten ctxt ty@(ForAllTy {})
188 -- We allow for-alls when, but only when, no type function
189 -- applications inside the forall involve the bound type variables
190 -- TODO: What if it is a (t1 ~ t2) => t3
191 -- Must revisit when the New Coercion API is here!
192 = do { let (tvs, rho) = splitForAllTys ty
193 ; (rho', co, ccs) <- flatten ctxt rho
194 ; let bad_eqs = filterBag is_bad ccs
195 is_bad c = tyVarsOfCanonical c `intersectsVarSet` tv_set
196 tv_set = mkVarSet tvs
197 ; unless (isEmptyBag bad_eqs)
198 (flattenForAllErrorTcS ctxt ty bad_eqs)
199 ; return (mkForAllTys tvs rho', foldr mkForAllCo co tvs, ccs) }
202 flattenPred :: CtFlavor -> TcPredType -> TcS (TcPredType, Coercion, CanonicalCts)
203 flattenPred ctxt (ClassP cls tys)
204 = do { (tys', cos, ccs) <- flattenMany ctxt tys
205 ; return (ClassP cls tys', mkPredCo $ ClassP cls cos, ccs) }
206 flattenPred ctxt (IParam nm ty)
207 = do { (ty', co, ccs) <- flatten ctxt ty
208 ; return (IParam nm ty', mkPredCo $ IParam nm co, ccs) }
209 flattenPred ctxt (EqPred ty1 ty2)
210 = do { (ty1', co1, ccs1) <- flatten ctxt ty1
211 ; (ty2', co2, ccs2) <- flatten ctxt ty2
212 ; return (EqPred ty1' ty2', mkPredCo $ EqPred co1 co2, ccs1 `andCCan` ccs2) }
215 %************************************************************************
217 %* Canonicalising given constraints *
219 %************************************************************************
222 canWanteds :: [WantedEvVar] -> TcS WorkList
223 canWanteds = fmap unionWorkLists . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
225 canGivens :: GivenLoc -> [EvVar] -> TcS WorkList
226 canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens
227 ; return (unionWorkLists ccs) }
229 mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList
230 mkCanonicals fl vs = fmap unionWorkLists (mapM (mkCanonical fl) vs)
232 mkCanonicalFEV :: FlavoredEvVar -> TcS WorkList
233 mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev
235 mkCanonicalFEVs :: Bag FlavoredEvVar -> TcS WorkList
236 mkCanonicalFEVs = foldrBagM canon_one emptyWorkList
237 where -- Preserves order (shouldn't be important, but curently
238 -- is important for the vectoriser)
239 canon_one fev wl = do { wl' <- mkCanonicalFEV fev
240 ; return (unionWorkList wl' wl) }
242 mkCanonical :: CtFlavor -> EvVar -> TcS WorkList
243 mkCanonical fl ev = case evVarPred ev of
244 ClassP clas tys -> canClassToWorkList fl ev clas tys
245 IParam ip ty -> canIPToWorkList fl ev ip ty
246 EqPred ty1 ty2 -> canEqToWorkList fl ev ty1 ty2
249 canClassToWorkList :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS WorkList
250 canClassToWorkList fl v cn tys
251 = do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys
252 ; let no_flattening_happened = isEmptyCCan ccs
253 dict_co = mkTyConAppCo (classTyCon cn) cos
254 ; v_new <- if no_flattening_happened then return v
255 else if isGiven fl then return v
256 -- The cos are all identities if fl=Given,
257 -- hence nothing to do
258 else do { v' <- newDictVar cn xis -- D xis
259 ; when (isWanted fl) $ setDictBind v (EvCast v' dict_co)
260 ; when (isGiven fl) $ setDictBind v' (EvCast v (mkSymCo dict_co))
261 -- NB: No more setting evidence for derived now
264 -- Add the superclasses of this one here, See Note [Adding superclasses].
265 -- But only if we are not simplifying the LHS of a rule.
266 ; sctx <- getTcSContext
267 ; sc_cts <- if simplEqsOnly sctx then return emptyWorkList
268 else newSCWorkFromFlavored v_new fl cn xis
270 ; return (sc_cts `unionWorkList`
271 workListFromEqs ccs `unionWorkList`
272 workListFromNonEq CDictCan { cc_id = v_new
275 , cc_tyargs = xis }) }
278 Note [Adding superclasses]
279 ~~~~~~~~~~~~~~~~~~~~~~~~~~
280 Since dictionaries are canonicalized only once in their lifetime, the
281 place to add their superclasses is canonicalisation (The alternative
282 would be to do it during constraint solving, but we'd have to be
283 extremely careful to not repeatedly introduced the same superclass in
284 our worklist). Here is what we do:
287 We add all their superclasses as Givens.
290 Generally speaking we want to be able to add superclasses of
291 wanteds for two reasons:
293 (1) Oportunities for improvement. Example:
294 class (a ~ b) => C a b
295 Wanted constraint is: C alpha beta
296 We'd like to simply have C alpha alpha. Similar
297 situations arise in relation to functional dependencies.
299 (2) To have minimal constraints to quantify over:
300 For instance, if our wanted constraint is (Eq a, Ord a)
301 we'd only like to quantify over Ord a.
303 To deal with (1) above we only add the superclasses of wanteds
304 which may lead to improvement, that is: equality superclasses or
305 superclasses with functional dependencies.
307 We deal with (2) completely independently in TcSimplify. See
308 Note [Minimize by SuperClasses] in TcSimplify.
311 Moreover, in all cases the extra improvement constraints are
312 Derived. Derived constraints have an identity (for now), but
313 we don't do anything with their evidence. For instance they
314 are never used to rewrite other constraints.
316 See also [New Wanted Superclass Work] in TcInteract.
322 Here's an example that demonstrates why we chose to NOT add
323 superclasses during simplification: [Comes from ticket #4497]
325 class Num (RealOf t) => Normed t
328 Assume the generated wanted constraint is:
329 RealOf e ~ e, Normed e
330 If we were to be adding the superclasses during simplification we'd get:
331 Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf
333 e ~ uf, Num uf, Normed e, RealOf e ~ e
334 ==> [Spontaneous solve]
335 Num uf, Normed uf, RealOf uf ~ uf
337 While looks exactly like our original constraint. If we add the superclass again we'd loop.
338 By adding superclasses definitely only once, during canonicalisation, this situation can't
343 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
344 -- Returns superclasses, see Note [Adding superclasses]
345 newSCWorkFromFlavored ev orig_flavor cls xis
346 | isDerived orig_flavor
347 = return emptyWorkList -- Deriveds don't yield more superclasses because we will
348 -- add them transitively in the case of wanteds.
350 | isGiven orig_flavor
351 = do { let sc_theta = immSuperClasses cls xis
353 ; sc_vars <- mapM newEvVar sc_theta
354 ; _ <- zipWithM_ setEvBind sc_vars [EvSuperClass ev n | n <- [0..]]
355 ; mkCanonicals flavor sc_vars }
357 | isEmptyVarSet (tyVarsOfTypes xis)
358 = return emptyWorkList -- Wanteds with no variables yield no deriveds.
359 -- See Note [Improvement from Ground Wanteds]
361 | otherwise -- Wanted case, just add those SC that can lead to improvement.
362 = do { let sc_rec_theta = transSuperClasses cls xis
363 impr_theta = filter is_improvement_pty sc_rec_theta
364 Wanted wloc = orig_flavor
365 ; der_ids <- mapM newDerivedId impr_theta
366 ; mkCanonicals (Derived wloc) der_ids }
369 is_improvement_pty :: PredType -> Bool
370 -- Either it's an equality, or has some functional dependency
371 is_improvement_pty (EqPred {}) = True
372 is_improvement_pty (ClassP cls _ty) = not $ null fundeps
373 where (_,fundeps,_,_,_,_) = classExtraBigSig cls
374 is_improvement_pty _ = False
379 canIPToWorkList :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS WorkList
380 -- See Note [Canonical implicit parameter constraints] to see why we don't
381 -- immediately canonicalize (flatten) IP constraints.
382 canIPToWorkList fl v nm ty
383 = return $ workListFromNonEq (CIPCan { cc_id = v
389 canEqToWorkList :: CtFlavor -> EvVar -> Type -> Type -> TcS WorkList
390 canEqToWorkList fl cv ty1 ty2 = do { cts <- canEq fl cv ty1 ty2
391 ; return $ workListFromEqs cts }
393 canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts
395 | eqType ty1 ty2 -- Dealing with equality here avoids
396 -- later spurious occurs checks for a~a
397 = do { when (isWanted fl) (setCoBind cv (mkReflCo ty1))
400 -- If one side is a variable, orient and flatten,
401 -- WITHOUT expanding type synonyms, so that we tend to
402 -- substitute a ~ Age rather than a ~ Int when @type Age = Int@
403 canEq fl cv ty1@(TyVarTy {}) ty2
404 = do { untch <- getUntouchables
405 ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
406 canEq fl cv ty1 ty2@(TyVarTy {})
407 = do { untch <- getUntouchables
408 ; canEqLeaf untch fl cv (classify ty1) (classify ty2) }
409 -- NB: don't use VarCls directly because tv1 or tv2 may be scolems!
411 -- Split up an equality between function types into two equalities.
412 canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
413 = do { (argv, resv) <-
415 do { argv <- newCoVar s1 s2
416 ; resv <- newCoVar t1 t2
418 mkFunCo (mkCoVarCo argv) (mkCoVarCo resv)
419 ; return (argv,resv) }
421 else if isGiven fl then
422 let [arg,res] = decomposeCo 2 (mkCoVarCo cv)
423 in do { argv <- newGivenCoVar s1 s2 arg
424 ; resv <- newGivenCoVar t1 t2 res
425 ; return (argv,resv) }
428 do { argv <- newDerivedId (EqPred s1 s2)
429 ; resv <- newDerivedId (EqPred t1 t2)
430 ; return (argv,resv) }
432 ; cc1 <- canEq fl argv s1 s2 -- inherit original kinds and locations
433 ; cc2 <- canEq fl resv t1 t2
434 ; return (cc1 `andCCan` cc2) }
436 canEq fl cv (TyConApp fn tys) ty2
437 | isSynFamilyTyCon fn, length tys == tyConArity fn
438 = do { untch <- getUntouchables
439 ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) }
440 canEq fl cv ty1 (TyConApp fn tys)
441 | isSynFamilyTyCon fn, length tys == tyConArity fn
442 = do { untch <- getUntouchables
443 ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) }
445 canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2)
446 | isDecomposableTyCon tc1 && isDecomposableTyCon tc2
448 , length tys1 == length tys2
449 = -- Generate equalities for each of the corresponding arguments
451 <- if isWanted fl then
452 do { argsv <- zipWithM newCoVar tys1 tys2
454 mkTyConAppCo tc1 (map mkCoVarCo argsv)
457 else if isGiven fl then
458 let cos = decomposeCo (length tys1) (mkCoVarCo cv)
459 in zipWith3M newGivenCoVar tys1 tys2 cos
462 zipWithM (\t1 t2 -> newDerivedId (EqPred t1 t2)) tys1 tys2
464 ; andCCans <$> zipWith3M (canEq fl) argsv tys1 tys2 }
466 -- See Note [Equality between type applications]
467 -- Note [Care with type applications] in TcUnify
469 | Just (s1,t1) <- tcSplitAppTy_maybe ty1
470 , Just (s2,t2) <- tcSplitAppTy_maybe ty2
472 then do { cv1 <- newCoVar s1 s2
473 ; cv2 <- newCoVar t1 t2
475 mkAppCo (mkCoVarCo cv1) (mkCoVarCo cv2)
476 ; cc1 <- canEq fl cv1 s1 s2
477 ; cc2 <- canEq fl cv2 t1 t2
478 ; return (cc1 `andCCan` cc2) }
481 then do { cv1 <- newDerivedId (EqPred s1 s2)
482 ; cv2 <- newDerivedId (EqPred t1 t2)
483 ; cc1 <- canEq fl cv1 s1 s2
484 ; cc2 <- canEq fl cv2 t1 t2
485 ; return (cc1 `andCCan` cc2) }
487 else return emptyCCan -- We cannot decompose given applications
488 -- because we no longer have 'left' and 'right'
490 canEq fl cv s1@(ForAllTy {}) s2@(ForAllTy {})
491 | tcIsForAllTy s1, tcIsForAllTy s2,
495 = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
498 -- Finally expand any type synonym applications.
499 canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2
500 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2'
501 canEq fl cv _ _ = canEqFailure fl cv
503 canEqFailure :: CtFlavor -> EvVar -> TcS CanonicalCts
504 canEqFailure fl cv = return (singleCCan (mkFrozenError fl cv))
507 Note [Equality between type applications]
508 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
509 If we see an equality of the form s1 t1 ~ s2 t2 we can always split
510 it up into s1 ~ s2 /\ t1 ~ t2, since s1 and s2 can't be type
511 functions (type functions use the TyConApp constructor, which never
512 shows up as the LHS of an AppTy). Other than type functions, types
513 in Haskell are always
515 (1) generative: a b ~ c d implies a ~ c, since different type
516 constructors always generate distinct types
518 (2) injective: a b ~ a d implies b ~ d; we never generate the
519 same type from different type arguments.
522 Note [Canonical ordering for equality constraints]
523 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
524 Implemented as (<+=) below:
526 - Type function applications always come before anything else.
527 - Variables always come before non-variables (other than type
528 function applications).
530 Note that we don't need to unfold type synonyms on the RHS to check
531 the ordering; that is, in the rules above it's OK to consider only
532 whether something is *syntactically* a type function application or
533 not. To illustrate why this is OK, suppose we have an equality of the
534 form 'tv ~ S a b c', where S is a type synonym which expands to a
535 top-level application of the type function F, something like
539 Then to canonicalize 'tv ~ S a b c' we flatten the RHS, and since S's
540 expansion contains type function applications the flattener will do
541 the expansion and then generate a skolem variable for the type
542 function application, so we end up with something like this:
547 where x is the skolem variable. This is one extra equation than
548 absolutely necessary (we could have gotten away with just 'F d e ~ tv'
549 if we had noticed that S expanded to a top-level type function
550 application and flipped it around in the first place) but this way
551 keeps the code simpler.
553 Unlike the OutsideIn(X) draft of May 7, 2010, we do not care about the
554 ordering of tv ~ tv constraints. There are several reasons why we
557 (1) In order to be able to extract a substitution that doesn't
558 mention untouchable variables after we are done solving, we might
559 prefer to put touchable variables on the left. However, in and
560 of itself this isn't necessary; we can always re-orient equality
561 constraints at the end if necessary when extracting a substitution.
563 (2) To ensure termination we might think it necessary to put
564 variables in lexicographic order. However, this isn't actually
565 necessary as outlined below.
567 While building up an inert set of canonical constraints, we maintain
568 the invariant that the equality constraints in the inert set form an
569 acyclic rewrite system when viewed as L-R rewrite rules. Moreover,
570 the given constraints form an idempotent substitution (i.e. none of
571 the variables on the LHS occur in any of the RHS's, and type functions
572 never show up in the RHS at all), the wanted constraints also form an
573 idempotent substitution, and finally the LHS of a given constraint
574 never shows up on the RHS of a wanted constraint. There may, however,
575 be a wanted LHS that shows up in a given RHS, since we do not rewrite
576 given constraints with wanted constraints.
578 Suppose we have an inert constraint set
581 tg_1 ~ xig_1 -- givens
584 tw_1 ~ xiw_1 -- wanteds
588 where each t_i can be either a type variable or a type function
589 application. Now suppose we take a new canonical equality constraint,
590 t' ~ xi' (note among other things this means t' does not occur in xi')
591 and try to react it with the existing inert set. We show by induction
592 on the number of t_i which occur in t' ~ xi' that this process will
595 There are several ways t' ~ xi' could react with an existing constraint:
597 TODO: finish this proof. The below was for the case where the entire
598 inert set is an idempotent subustitution...
600 (b) We could have t' = t_j for some j. Then we obtain the new
601 equality xi_j ~ xi'; note that neither xi_j or xi' contain t_j. We
602 now canonicalize the new equality, which may involve decomposing it
603 into several canonical equalities, and recurse on these. However,
604 none of the new equalities will contain t_j, so they have fewer
605 occurrences of the t_i than the original equation.
607 (a) We could have t_j occurring in xi' for some j, with t' /=
608 t_j. Then we substitute xi_j for t_j in xi' and continue. However,
609 since none of the t_i occur in xi_j, we have decreased the
610 number of t_i that occur in xi', since we eliminated t_j and did not
611 introduce any new ones.
615 = FskCls TcTyVar -- ^ Flatten skolem
616 | VarCls TcTyVar -- ^ Non-flatten-skolem variable
617 | FunCls TyCon [Type] -- ^ Type function, exactly saturated
618 | OtherCls TcType -- ^ Neither of the above
620 unClassify :: TypeClassifier -> TcType
621 unClassify (VarCls tv) = TyVarTy tv
622 unClassify (FskCls tv) = TyVarTy tv
623 unClassify (FunCls fn tys) = TyConApp fn tys
624 unClassify (OtherCls ty) = ty
626 classify :: TcType -> TypeClassifier
628 classify (TyVarTy tv)
630 FlatSkol {} <- tcTyVarDetails tv = FskCls tv
631 | otherwise = VarCls tv
632 classify (TyConApp tc tys) | isSynFamilyTyCon tc
633 , tyConArity tc == length tys
635 classify ty | Just ty' <- tcView ty
636 = case classify ty' of
637 OtherCls {} -> OtherCls ty
638 var_or_fn -> var_or_fn
642 -- See note [Canonical ordering for equality constraints].
643 reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool
644 -- (t1 `reOrient` t2) responds True
645 -- iff we should flip to (t2~t1)
646 -- We try to say False if possible, to minimise evidence generation
648 -- Postcondition: After re-orienting, first arg is not OTherCls
649 reOrient _fl (OtherCls {}) (FunCls {}) = True
650 reOrient _fl (OtherCls {}) (FskCls {}) = True
651 reOrient _fl (OtherCls {}) (VarCls {}) = True
652 reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun
654 reOrient _fl (FunCls {}) (VarCls _tv) = False
655 -- But consider the following variation: isGiven fl && isMetaTyVar tv
657 -- See Note [No touchables as FunEq RHS] in TcSMonad
658 reOrient _fl (FunCls {}) _ = False -- Fun/Other on rhs
660 reOrient _fl (VarCls {}) (FunCls {}) = True
662 reOrient _fl (VarCls {}) (FskCls {}) = False
664 reOrient _fl (VarCls {}) (OtherCls {}) = False
665 reOrient _fl (VarCls tv1) (VarCls tv2)
666 | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True
668 -- Just for efficiency, see CTyEqCan invariants
670 reOrient _fl (FskCls {}) (VarCls tv2) = isMetaTyVar tv2
671 -- Just for efficiency, see CTyEqCan invariants
673 reOrient _fl (FskCls {}) (FskCls {}) = False
674 reOrient _fl (FskCls {}) (FunCls {}) = True
675 reOrient _fl (FskCls {}) (OtherCls {}) = False
678 canEqLeaf :: TcsUntouchables
680 -> TypeClassifier -> TypeClassifier -> TcS CanonicalCts
681 -- Canonicalizing "leaf" equality constraints which cannot be
682 -- decomposed further (ie one of the types is a variable or
683 -- saturated type function application).
686 -- * one of the two arguments is not OtherCls
687 -- * the two types are not equal (looking through synonyms)
688 canEqLeaf _untch fl cv cls1 cls2
689 | cls1 `re_orient` cls2
690 = do { cv' <- if isWanted fl
691 then do { cv' <- newCoVar s2 s1
692 ; setCoBind cv $ mkSymCo (mkCoVarCo cv')
694 else if isGiven fl then
695 newGivenCoVar s2 s1 (mkSymCo (mkCoVarCo cv))
697 newDerivedId (EqPred s2 s1)
698 ; canEqLeafOriented fl cv' cls2 s1 }
701 = do { traceTcS "canEqLeaf" (ppr (unClassify cls1) $$ ppr (unClassify cls2))
702 ; canEqLeafOriented fl cv cls1 s2 }
704 re_orient = reOrient fl
709 canEqLeafOriented :: CtFlavor -> CoVar
710 -> TypeClassifier -> TcType -> TcS CanonicalCts
711 -- First argument is not OtherCls
712 canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1
713 | let k1 = kindAppResult (tyConKind fn) tys1,
714 let k2 = typeKind s2,
715 not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan
717 -- Eagerly fails, see Note [Kind errors] in TcInteract
720 = ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) )
721 do { (xis1,cos1,ccs1) <- flattenMany fl tys1 -- Flatten type function arguments
722 -- cos1 :: xis1 ~ tys1
723 ; (xi2, co2, ccs2) <- flatten fl s2 -- Flatten entire RHS
725 ; let ccs = ccs1 `andCCan` ccs2
726 no_flattening_happened = isEmptyCCan ccs
727 ; cv_new <- if no_flattening_happened then return cv
728 else if isGiven fl then return cv
729 else if isWanted fl then
730 do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2
732 ; let -- fun_co :: F xis1 ~ F tys1
733 fun_co = mkTyConAppCo fn cos1
734 -- want_co :: F tys1 ~ s2
735 want_co = mkSymCo fun_co
736 `mkTransCo` mkCoVarCo cv'
738 ; setCoBind cv want_co
741 newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2)
743 ; let final_cc = CFunEqCan { cc_id = cv_new
748 ; return $ ccs `extendCCans` final_cc }
750 -- Otherwise, we have a variable on the left, so call canEqLeafTyVarLeft
751 canEqLeafOriented fl cv (FskCls tv) s2
752 = canEqLeafTyVarLeft fl cv tv s2
753 canEqLeafOriented fl cv (VarCls tv) s2
754 = canEqLeafTyVarLeft fl cv tv s2
755 canEqLeafOriented _ cv (OtherCls ty1) ty2
756 = pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2)
758 canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS CanonicalCts
759 -- Establish invariants of CTyEqCans
760 canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2
761 | not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan
763 -- Eagerly fails, see Note [Kind errors] in TcInteract
765 = do { (xi2, co, ccs2) <- flatten fl s2 -- Flatten RHS co : xi2 ~ s2
766 ; mxi2' <- canOccursCheck fl tv xi2 -- Do an occurs check, and return a possibly
767 -- unfolded version of the RHS, if we had to
768 -- unfold any type synonyms to get rid of tv.
770 Nothing -> canEqFailure fl cv ;
772 do { let no_flattening_happened = isEmptyCCan ccs2
773 ; cv_new <- if no_flattening_happened then return cv
774 else if isGiven fl then return cv
775 else if isWanted fl then
776 do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
777 ; setCoBind cv (mkCoVarCo cv' `mkTransCo` co)
780 newDerivedId (EqPred (mkTyVarTy tv) xi2')
782 ; return $ ccs2 `extendCCans` CTyEqCan { cc_id = cv_new
785 , cc_rhs = xi2' } } } }
790 -- See Note [Type synonyms and canonicalization].
791 -- Check whether the given variable occurs in the given type. We may
792 -- have needed to do some type synonym unfolding in order to get rid
793 -- of the variable, so we also return the unfolded version of the
794 -- type, which is guaranteed to be syntactically free of the given
795 -- type variable. If the type is already syntactically free of the
796 -- variable, then the same type is returned.
798 -- Precondition: the two types are not equal (looking though synonyms)
799 canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi)
800 canOccursCheck _gw tv xi = return (expandAway tv xi)
803 @expandAway tv xi@ expands synonyms in xi just enough to get rid of
804 occurrences of tv, if that is possible; otherwise, it returns Nothing.
805 For example, suppose we have
808 expandAway b (F Int b) = Just [Int]
810 expandAway a (F a Int) = Nothing
812 We don't promise to do the absolute minimum amount of expanding
813 necessary, but we try not to do expansions we don't need to. We
814 prefer doing inner expansions first. For example,
815 type F a b = (a, Int, a, [a])
818 expandAway b (F (G b)) = F Char
819 even though we could also expand F to get rid of b.
822 expandAway :: TcTyVar -> Xi -> Maybe Xi
823 expandAway tv t@(TyVarTy tv')
824 | tv == tv' = Nothing
827 | not (tv `elemVarSet` tyVarsOfType xi) = Just xi
828 expandAway tv (AppTy ty1 ty2)
829 = do { ty1' <- expandAway tv ty1
830 ; ty2' <- expandAway tv ty2
831 ; return (mkAppTy ty1' ty2') }
832 -- mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2
833 expandAway tv (FunTy ty1 ty2)
834 = do { ty1' <- expandAway tv ty1
835 ; ty2' <- expandAway tv ty2
836 ; return (mkFunTy ty1' ty2') }
837 -- mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2
838 expandAway tv ty@(ForAllTy {})
839 = let (tvs,rho) = splitForAllTys ty
840 tvs_knds = map tyVarKind tvs
841 in if tv `elemVarSet` tyVarsOfTypes tvs_knds then
842 -- Can't expand away the kinds unless we create
843 -- fresh variables which we don't want to do at this point.
845 else do { rho' <- expandAway tv rho
846 ; return (mkForAllTys tvs rho') }
847 expandAway tv (PredTy pred)
848 = do { pred' <- expandAwayPred tv pred
849 ; return (PredTy pred') }
850 -- For a type constructor application, first try expanding away the
851 -- offending variable from the arguments. If that doesn't work, next
852 -- see if the type constructor is a type synonym, and if so, expand
854 expandAway tv ty@(TyConApp tc tys)
855 = (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv)
857 expandAwayPred :: TcTyVar -> TcPredType -> Maybe TcPredType
858 expandAwayPred tv (ClassP cls tys)
859 = do { tys' <- mapM (expandAway tv) tys; return (ClassP cls tys') }
860 expandAwayPred tv (EqPred ty1 ty2)
861 = do { ty1' <- expandAway tv ty1
862 ; ty2' <- expandAway tv ty2
863 ; return (EqPred ty1' ty2') }
864 expandAwayPred tv (IParam nm ty)
865 = do { ty' <- expandAway tv ty
866 ; return (IParam nm ty') }
872 Note [Type synonyms and canonicalization]
873 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
875 We treat type synonym applications as xi types, that is, they do not
876 count as type function applications. However, we do need to be a bit
877 careful with type synonyms: like type functions they may not be
878 generative or injective. However, unlike type functions, they are
879 parametric, so there is no problem in expanding them whenever we see
880 them, since we do not need to know anything about their arguments in
881 order to expand them; this is what justifies not having to treat them
882 as specially as type function applications. The thing that causes
883 some subtleties is that we prefer to leave type synonym applications
884 *unexpanded* whenever possible, in order to generate better error
887 If we encounter an equality constraint with type synonym applications
888 on both sides, or a type synonym application on one side and some sort
889 of type application on the other, we simply must expand out the type
890 synonyms in order to continue decomposing the equality constraint into
891 primitive equality constraints. For example, suppose we have
895 and we encounter the equality
899 In order to continue we must expand F a into [Int], giving us the
904 which we can then decompose into the more primitive equality
909 However, if we encounter an equality constraint with a type synonym
910 application on one side and a variable on the other side, we should
911 NOT (necessarily) expand the type synonym, since for the purpose of
912 good error messages we want to leave type synonyms unexpanded as much
915 However, there is a subtle point with type synonyms and the occurs
916 check that takes place for equality constraints of the form tv ~ xi.
917 As an example, suppose we have
921 and we come across the equality constraint
925 This should not actually fail the occurs check, since expanding out
926 the type synonym results in the legitimate equality constraint a ~
927 Int. We must actually do this expansion, because unifying a with F a
928 will lead the type checker into infinite loops later. Put another
929 way, canonical equality constraints should never *syntactically*
930 contain the LHS variable in the RHS type. However, we don't always
931 need to expand type synonyms when doing an occurs check; for example,
936 is obviously fine no matter what F expands to. And in this case we
937 would rather unify a with F b (rather than F b's expansion) in order
938 to get better error messages later.
940 So, when doing an occurs check with a type synonym application on the
941 RHS, we use some heuristics to find an expansion of the RHS which does
942 not contain the variable from the LHS. In particular, given
946 we first try expanding each of the ti to types which no longer contain
947 a. If this turns out to be impossible, we next try expanding F
951 %************************************************************************
953 %* Functional dependencies, instantiation of equations
955 %************************************************************************
957 When we spot an equality arising from a functional dependency,
958 we now use that equality (a "wanted") to rewrite the work-item
959 constraint right away. This avoids two dangers
961 Danger 1: If we send the original constraint on down the pipeline
962 it may react with an instance declaration, and in delicate
963 situations (when a Given overlaps with an instance) that
964 may produce new insoluble goals: see Trac #4952
966 Danger 2: If we don't rewrite the constraint, it may re-react
967 with the same thing later, and produce the same equality
968 again --> termination worries.
970 To achieve this required some refactoring of FunDeps.lhs (nicer
974 rewriteWithFunDeps :: [Equation]
976 -> TcS (Maybe ([Xi], [Coercion], WorkList))
977 rewriteWithFunDeps eqn_pred_locs xis fl
978 = do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
979 ; let fd_ev_pos :: [(Int,FlavoredEvVar)]
980 fd_ev_pos = concat fd_ev_poss
981 (rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
982 ; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
983 ; let fd_work = unionWorkLists fds
984 ; if isEmptyWorkList fd_work
986 else return (Just (rewritten_xis, cos, fd_work)) }
988 instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived
990 -> TcS [(Int, FlavoredEvVar)]
991 -- Post: Returns the position index as well as the corresponding FunDep equality
992 instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
993 , fd_pred1 = d1, fd_pred2 = d2 })
994 = do { let tvs = varSetElems qtvs
995 ; tvs' <- mapM instFlexiTcS tvs
996 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
997 ; mapM (do_one subst) eqs }
1000 Given _ -> panic "mkFunDepEqns"
1001 Wanted loc -> Wanted (push_ctx loc)
1002 Derived loc -> Derived (push_ctx loc)
1004 push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1006 do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
1007 = do { let sty1 = Type.substTy subst ty1
1008 sty2 = Type.substTy subst ty2
1009 ; ev <- newCoVar sty1 sty2
1010 ; return (i, mkEvVarX ev fl') }
1012 rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty)
1013 -> [Type] -- A sequence of types: tys
1014 -> [(Type,Coercion)] -- Returns : [(ty', co : ty' ~ ty)]
1015 rewriteDictParams param_eqs tys
1016 = zipWith do_one tys [0..]
1018 do_one :: Type -> Int -> (Type,Coercion)
1019 do_one ty n = case lookup n param_eqs of
1020 Just wev -> (get_fst_ty wev, mkCoVarCo (evVarOf wev))
1021 Nothing -> (ty, mkReflCo ty) -- Identity
1023 get_fst_ty wev = case evVarOfPred wev of
1025 _ -> panic "rewriteDictParams: non equality fundep"
1027 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
1028 -> TcM (TidyEnv, SDoc)
1029 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1030 = do { zpred1 <- TcM.zonkTcPredType pred1
1031 ; zpred2 <- TcM.zonkTcPredType pred2
1032 ; let { tpred1 = tidyPred tidy_env zpred1
1033 ; tpred2 = tidyPred tidy_env zpred2 }
1034 ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1035 nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
1036 nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
1037 ; return (tidy_env, msg) }