Problem with `Tactic.MonoidSolver`

[javierdiaz72]

I've been using the monoid solver and found that the following example doesn't work:

module _ {a} {A : Set a} where

  open import Data.List.Properties using (++-monoid)
  open import Tactic.MonoidSolver using (solve)

  test : ∀ (xs ys zs : List A) (x : A) → (xs ++ x ∷ ys) ++ zs ≡ xs ++ x ∷ (ys ++ zs)
  test _ _ _ _ = solve (++-monoid A)

[JacquesCarette]

Could you augment your report with more details than "doesn't work"? Hard error or yellow or does not terminate or .... ?

[javierdiaz72]

Could you augment your report with more details than "doesn't work"? Hard error or yellow or does not terminate or .... ?

Sure, the following error message shows up:

ys ++ zs != ys of type List A
when checking that the expression
Tactic.MonoidSolver.homo {_} {_} (++-monoid {a} A)
(Tactic.MonoidSolver.[ xs ↑] Tactic.MonoidSolver.∙′
 Tactic.MonoidSolver.[ _∷_ {_} {_} x (_++_ {a} {A} ys zs) ↑])
has type
(++-monoid A Algebra.Bundles.Monoid.≈
 Tactic.MonoidSolver.[ ++-monoid A ⇓]
 (Tactic.MonoidSolver.[ xs ↑] Tactic.MonoidSolver.∙′
  Tactic.MonoidSolver.[ x ∷ ys ↑]
  Tactic.MonoidSolver.∙′ Tactic.MonoidSolver.[ zs ↑]))
_k_1073

[TOTBWF]

Looks like the monoid solver isn't normalizing before doing reflection, so it thinks x ∷ (ys ++ zs) has to be treated like a opaque expression. This could be fixed by using a combination of withNormalisation true and withReduceDefs, but this is extremely fragile.

A better solution is to use the relatively recently added instance argument features to let the unifier do the work for us. An example of this can be found in the 1lab's monad solver: https://github.com/the1lab/1lab/blob/a4cdd1bcdc84af9682a910a9bb7c825f6d0c95ae/src/Cat/Diagram/Monad/Solver.agda#L258.

[jamesmckinna]

Is there a good tutorial anywhere for writing Reflection-based macros? Eg, as here, "oh, the definition doesn't normalise in the right place/moment, so... easy fix"

[MatthewDaggitt]

I'm not aware of one... doesn't mean there isn't one out there!