[Feature] Please add tmTry

[JasonGross]

I'd like to see something like

tmTry : forall {A:Type@{t}}, TemplateMonad A -> TemplateMonad (option_try A)

with

Monomorphic Variant exn : Set := GenericError.

Variant option_try (A : Type) : Type := my_Value (val : A) | my_Error (err : exn).

Arguments my_Value {A} val.
Arguments my_Error {A} _.

(and perhaps someday extend exn to hold more kinds of errors?), so that the following work without error:

From MetaCoq.Template Require Import All.

Import MCMonadNotation.
Import bytestring.
Open Scope bs.
Open Scope list_scope.

MetaCoq Run (tmDefinition "a" I;; tmTry (tmDefinition "a" I) >>= tmPrint).
MetaCoq Run (tmTry (tmDefinition "b" I);; mp <- tmCurrentModPath tt;; tmUnquote (tConst (mp, "b") []) >>= tmPrint).
MetaCoq Run (tmDefinition "c" I;; mp <- tmCurrentModPath tt;;
             v <- tmTry (tmUnquoteTyped False (tConst (mp, "c") []));;
             match v with
             | my_Value v => ret (inl v)
             | my_Error _ => v' <- tmUnquoteTyped True (tConst (mp, "c") []);;
                             ret (inr v')
             end >>= tmPrint).
MetaCoq Run (tmAxiom "a'" True;; tmTry (tmAxiom "a'" True) >>= tmPrint).
MetaCoq Run (tmTry (tmAxiom "b'" True);; mp <- tmCurrentModPath tt;; tmUnquote (tConst (mp, "b'") []) >>= tmPrint).
MetaCoq Run (tmAxiom "c'" True;; mp <- tmCurrentModPath tt;;
             v <- tmTry (tmUnquoteTyped False (tConst (mp, "c'") []));;
             match v with
             | my_Value v => ret (inl v)
             | my_Error _ => v' <- tmUnquoteTyped True (tConst (mp, "c'") []);;
                             ret (inr v')
             end >>= tmPrint).
Universes u0 u1.
Constraint u0 < u1.
MetaCoq Run (u <- tmQuote Type@{u0};;
             v <- tmTry (tmUnquoteTyped Type@{u0} u);;
             match v with
             | my_Value v => ret (v -> True)
             | my_Error _ => v' <- tmUnquoteTyped Type@{u1} v;;
                             ret (v' -> True)
             end >>= tmPrint).

(See also this Zulip thread)