I'm working through Pierce's Types and Programming Languages on my own. I'm attempting to write the typecheckers in Haskell, instead of ML. However, when it comes to his eval function, I'm a little stuck. The original is

let rec eval t =
    try let t' = eval1 t
         in eval t'
    with NoRuleApplies -> t

Where eval1 is a single step evaluation of the abstract syntax tree, and NoRuleApplies is an exception that's raised if there are no rules that can reduce the expression. Now, there's a footnote that it isn't good style in ML. It seems even less natural in Haskell, at least to me, but I still don't know the language that well.

The natural equivalent to what Pierce has in ML is something along the lines of

data ArithExpr
    = TmTrue
    | TmFalse
    | TmIfExpr ArithExpr ArithExpr ArithExpr
    | TmZero
    | TmSucc ArithExpr
    | TmPred ArithExpr
    | TmIsZero ArithExpr
      deriving (Show, Eq)

eval1 :: ArithExpr -> ArithExpr

eval1 (TmIfExpr TmTrue t _) = t

eval1 (TmIfExpr TmFalse _ t) = t

eval1 (TmIfExpr t1 t2 t3) =
    let t1' = eval1 t1
    in TmIfExpr t1' t2 t3
-- and so on

But, how to terminate the recursion in the full eval?

I'm considering changing eval1 to be ArithExpr->Maybe ArithExpr

If the expression is reducible, then I return Just t, and if it's not reducible, then Nothing

It makes eval1 a bit more complicated, and not as straightforward translation from the type system being described, though.
e.g reducing If looks more like

eval1 (TmIfExpr t1 t2 t3) =
    let t1' = eval1 t1
    in case t1' of
            { Just t1'' -> Just $ TmIfExpr t1'' t2 t3
            ; Nothing -> Nothing
            }

and eval then looks like
eval t =
    let t' = eval1 t
    in case t' of
         { Just t'' -> eval t''
         ; Nothing -> t'
         }

I'm looking for some suggestions on the direction to proceed.