Calling Ltac from the TemplateMonad

(* General imports to work with TemplateMonad *)
From MetaCoq.Template Require Import All.
From MetaCoq Require Import bytestring.
Require Import List.
Import MCMonadNotation ListNotations.
Open Scope bs.

(* Definitions that can be outsourced to a central file *)

MetaCoq Run (tmCurrentModPath tt >>= tmDefinition "solve_ltac_mp").

Definition solve_ltac (tac : string) {args : Type} (a : args) (Goal : Type) := Goal.
Existing Class solve_ltac.

Definition tmDef name {A} a := @tmDefinitionRed name (Some (unfold (solve_ltac_mp, "solve_ltac"))) A a.

(* Local definition adding a new tactic *)

Hint Extern 0 (solve_ltac "tauto" tt _) => unfold solve_ltac; tauto : typeclass_instances.

(* Calling this tactic from the monad *)

MetaCoq Run (oprf <- tmInferInstance None (solve_ltac "tauto" tt (forall P : Prop, P -> ~~ P)) ;;
             match oprf with
             | my_Some prf => tmDef "prf1" prf
             | my_None => tmFail "no proof found"
             end).

Check prf1.
Print prf1.

(* a tactic which takes an argument *)

Hint Extern 0 (solve_ltac "exact" ?P _) => unfold solve_ltac; exact P : typeclass_instances.

MetaCoq Run (oprf <- tmInferInstance None (solve_ltac "exact" 0 nat) ;;
             match oprf with
             | my_Some prf => tmDef "prf2" prf
             | my_None => tmFail "no proof found"
             end).

Check prf2.
Print prf2.