{m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Lean.MonadError m] →
      [Monad m] →
        [Lean.Meta.Grind.Arith.CommRing.MonadCanon m] → [Lean.Meta.Grind.Arith.CommRing.MonadSemiring m] → m Lean.Expr