Or-patternify the codebase

[effectfully]

It's extremely easy to introduce a bug by adding a new binder to any of the ASTs because of functions like

termSubstClosedTerm
    :: Eq name
    => name
    -> Term tyname name uni fun a
    -> Term tyname name uni fun a
    -> Term tyname name uni fun a
termSubstClosedTerm varFor new = go where
    go = \case
         Var    a var         -> if var == varFor then new else Var a var
         LamAbs a var ty body -> LamAbs a var ty (goUnder var body)
         t                    -> t & over termSubterms go
    goUnder var term = if var == varFor then term else go term

I added Fix to the AST and this function didn't give me any warning or error, it just started silently doing the wrong thing. And we have a number of those scattered over the entire codebase. This means that adding any kind of binder to any kind of AST is now blocked on us cleaning up this mess, because otherwise we'll just end up introducing bugs.

What we should do is rewrite the last clause to

termSubstClosedTerm
    :: Eq name
    => name
    -> Term tyname name uni fun a
    -> Term tyname name uni fun a
    -> Term tyname name uni fun a
termSubstClosedTerm varFor new = go where
    go = \case
         Var a var -> if var == varFor then new else Var a var
         LamAbs a var ty body -> LamAbs a var ty (goUnder var body)
         t@(Apply{}; TyAbs{}; <...>; Error{}) -> t & over termSubterms go
    goUnder var term = if var == varFor then term else go term

i.e. explicitly list all the constructors in an Or-pattern (potentially pattern-synonym'd), so that adding new constructors forces the programmer to make a choice regarding how to handle the new constructor.

Or-patterns are only available since GHC-9.12 though.