mkWantedConstraints, deCanonicaliseWanted,
makeGivens, makeSolved,
- CtFlavor (..), isWanted, isGiven, isDerived, canRewrite,
+ CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, canSolve,
combineCtLoc, mkGivenFlavor,
TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
| CTyEqCan { -- tv ~ xi (recall xi means function free)
-- Invariant:
-- * tv not in tvs(xi) (occurs check)
- -- * If tv is a MetaTyVar, then typeKind xi <: typeKind tv
- -- a skolem, then typeKind xi = typeKind tv
+ -- * If constraint is given then typeKind xi == typeKind tv
+ -- See Note [Spontaneous solving and kind compatibility]
cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_tyvar :: TcTyVar,
-- Invariant: * isSynFamilyTyCon cc_fun
-- * cc_rhs is not a touchable unification variable
-- See Note [No touchables as FunEq RHS]
- -- * typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
+ -- * If constraint is given then
+ -- typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_fun :: TyCon, -- A type function
isDerived (Derived {}) = True
isDerived _ = False
+canSolve :: CtFlavor -> CtFlavor -> Bool
+-- canSolve ctid1 ctid2
+-- The constraint ctid1 can be used to solve ctid2
+-- "to solve" means a reaction where the active parts of the two constraints match.
+-- active(F xis ~ xi) = F xis
+-- active(tv ~ xi) = tv
+-- active(D xis) = D xis
+-- active(IP nm ty) = nm
+-----------------------------------------
+canSolve (Given {}) _ = True
+canSolve (Derived {}) (Wanted {}) = True
+canSolve (Derived {}) (Derived {}) = True
+canSolve (Wanted {}) (Wanted {}) = True
+canSolve _ _ = False
+
canRewrite :: CtFlavor -> CtFlavor -> Bool
-- canRewrite ctid1 ctid2
--- The constraint ctid1 can be used to rewrite ctid2
+-- The *equality_constraint* ctid1 can be used to rewrite inside ctid2
canRewrite (Given {}) _ = True
canRewrite (Derived {}) (Wanted {}) = True
canRewrite (Derived {}) (Derived {}) = True
-canRewrite (Wanted {}) (Wanted {}) = True
+ -- See note [Rewriting wanteds with wanteds]
+canRewrite (Wanted {}) (Wanted {}) = False
canRewrite _ _ = False
+\end{code}
+Note [Rewriting wanteds with wanteds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We will currently never use a wanted to rewrite any other
+constraint (function @canRewrite@). If a rewriting was possible at all,
+we simply wait until the wanted equality becomes given or derived and
+then use it. This way we avoid rewriting by eventually insoluble wanteds,
+such as in the following situation:
+ w1 : a ~ Int
+ w2 : F a ~ a
+ w3 : F Int ~ G Bool
+where 'a' is a skolem variable. If we rewrite using w1 inside w2 we will
+get the perhaps mystifying error at the end that we could not solve
+(a ~ Int) and (G Bool ~ Int). But there is no point in rewriting with
+a ~ Int as long as it is still wanted.
+
+Notice that on the other hand we often do solve one wanted from another,
+(function @canSolve@) for instance in dictionary interactions, which is
+a reaction that enables sharing both in the solver and in the final evidence
+produced.
+
+\begin{code}
+
combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
-- Precondition: At least one of them should be wanted
combineCtLoc (Wanted loc) _ = loc