Refactor CtEvidence to have separate CtWanted/CtGiven datatypes

Currently, we have:

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):

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:

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:

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.

Edited 1 month ago

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information

Child items 0

No child items are currently assigned. Use child items to break down this issue into smaller parts.

Refactor CtEvidence to have separate CtWanted/CtGiven datatypes

Activity