Currently, we have: ```hs data CtEvidence = CtGiven { ctev_pred :: TcPredType , ctev_evar :: EvVar , ctev_loc :: CtLoc } | CtWanted { ctev_pred :: TcPredType , ctev_dest :: TcEvDest , ctev_loc :: CtLoc , ctev_rewriters :: RewriterSet } ``` I propose something like (up to naming decisions, particularly the field names): ```hs data CtEvidence = CtGiven GivenCt | CtWanted WantedCt data GivenCt = GivenCt { ctev_pred :: TcPredType , ctev_evar :: EvVar , ctev_loc :: CtLoc } data WantedCt = WantedCt { ctev_pred :: TcPredType , ctev_dest :: TcEvDest , ctev_loc :: CtLoc , ctev_rewriters :: RewriterSet } ``` This would allow simplifying some code: we first match on whether the constraint is Wanted or Given, and then we can pass on the inner data-type as whole instead of separate arguments. This would also be consistent with the definition of `Ct`, where each constructor has a separate datatype: ```hs data Ct = CDictCan DictCt | CIrredCan IrredCt | CEqCan EqCt | CQuantCan QCInst | CNonCanonical CtEvidence ``` In particular, I think `solveForAll` could be written slightly more clearly with this change. Currently we have: ```hs solveForAll ev tvs theta pred fuel = case ev of CtGiven {} -> -- See Note [Solving a Given forall-constraint] do { addInertForAll qci ; stopWith ev "Given forall-constraint" } CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_loc = loc } -> -- See Note [Solving a Wanted forall-constraint] runSolverStage $ do { tryInertQCs qci ; simpleStage $ solveWantedForAll_implic dest rewriters loc tvs theta pred ; stopWithStage ev "Wanted forall-constraint (implication)" } ``` I think it would be clearer if we could do `CtWanted wtd -> ... blah wtd`, as opposed to taking apart various fields.