In the following script :
From elpi Require Import elpi.
Inductive C (T : Type) := Build_C.
Structure S := {sort :> Type; class : C sort}.
Canonical generic_S (T : Type) (c : C T) := Build_S T c.
Elpi Command bla.
Set Debug "unification".
Elpi Query lp:{{
coq.unify-eq {{ nat }} {{ sort (generic_S nat lp:X) }} Z.
}}.
Coq solves the unification problem by using the canonical solution. However, this introduces new unification variables that might introduce issues later on (see e.g. https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Unable.20to.20reduce.20under.20opaque.20constant.20during.20unification). I am aware that unfolding constants and reducing is dangerous in terms of complexity, but is there a way to have cases where simplifying is preferred over using canonical solutions ?
IDK what elpi does, any way to reproduce without it?
Yes, sorry, I got carried away by my previous unification problem that was hard to trigger. Check fun (n : nat) => n : sort (generic_S nat _).
produces the same debug messages, i.e.
[unification] nat|
sort|ZApp(generic_S nat ?e0)
[unification] generic_S|ZApp(nat, ?e0)
generic_S|ZApp(nat, ?c)
Last updated: Oct 13 2024 at 01:02 UTC