Simplify refinement errors (RefineException)

[raehik]

RefineException is a sum type holding constructors for

• logical predicates holding recursive errors
• Exceptions (RefineSomeException)
• plain strings (RefineOtherException)'

I want to change this to a single constructor, similar to rerefined:

data RefineFailure a = RefineFailure
  { refineFailurePredicate :: a
  -- ^ The predicate that failed.

  , refineFailureDetail    :: a
  -- ^ Failure clarification.

  , refineFailureInner     :: [RefineFailure a]
  -- ^ Any wrapped errors, for combinator predicates.
  --
  -- What these are, and their order, should be noted in 'refineFailureDetail'.
  } deriving stock Show

Logical predicates can note precise failure detail in their detail field, instead of e.g. using These to disambiguate which predicate failed. We lose the ability to place arbitrary Exceptions in refinement failures-- but I wasn't able to find a usage of this in refined's reverse dependencies, and I don't see a clear use myself. We also lose precision in refinement failures i.e. logical predicates no longer have special constructors. But we never use this precision, and I don't think it's useful.

Fairly minimal API impact, throwRefineOtherException will remain the primary way to fail a non-recursive predicate with no type signature change.

The main work would be moving detail in showTree obtained by constructor matching, to detail fields in the relevant Predicate instances, and trying to keep pretty output the same. I've already essentially done this once, in rerefined.

[chessai]

The reason that I defined RefineException like so is to provide a pretty-printed tree which can pinpoint where the refinement failed. Maybe this tradeoff isn't worth it.

[raehik]

I think this design supports the same sort of pretty trees and "drilling down". See e.g. Rerefined.Predicate.Logical.And:

instance (Refine l a, Refine r a, KnownPredicateName (And l r))
  => Refine (And l r) a where
    validate p a =
        case l of
          Just el ->
            case r of
              Just er -> validateFail p "AND:    l&r failed"    [er, el]
              -- ...
          -- ...
      where
        l = validate (proxy# @l) a
        r = validate (proxy# @r) a

-- | Shortcut for returning a predicate validation failure.
validateFail
    :: forall p
    .  (Predicate p, KnownPredicateName p)
    => Proxy# p -> TBL.Builder -> [RefineFailure]
    -> Maybe RefineFailure
validateFail _p msg es =
    Just $ RefineFailure (fromString $ predicateName @p) msg es

Compare to Refined:

instance ( Predicate l x, Predicate r x ) => Predicate (And l r) x where
  validate p x = do
    let a = validate' @l undefined x
    let b = validate' @r undefined x
    let throw err = Just (RefineAndException (typeRep p) err)
    case (a, b) of
      (Just  e, Just e1) -> throw (These e e1)
      -- ...

The same information is recorded: predicate "name", details, and recursive failures.

My initial reasons for suggesting this were

• it makes custom predicates more comfortable, since everything uses the same definitions
• it helps remove the ExceptionTree indirection, which had a "todo remove" note on it

But upon looking, ExceptionTree was removed or moved some time ago. Maybe I was reading dead code.
In which case, this is just a small ergonomics point. oops, ignore me, guess I left some old work in my working tree