Error "Unification problem outside the pattern fragment." · Elpi users & devs

Stream: Elpi users & devs

Topic: Error "Unification problem outside the pattern fragment."

Pierre Vial (Sep 07 2022 at 13:04):

Hello,
my goal is to produce a tactic with elpi, which, given:

a (non-dependent) function Fuof the form fun (a1 : A1) .... (a : An) => expr : B
an expression Teof type B
produces the statement:
forall (a1 : A1) .... (a : An), expr = Te

For now, I'm doing like this:

Elpi Tactic tryftp.
Elpi Accumulate lp:{{


  pred funtoprod i : term, i : term, o : term.
    funtoprod (fun Na Ty Fu1) Te (prod Na Ty Fu2) :-  pi x\ decl x Na Ty => funtoprod (Fu1 x) Te (Fu2 x).
    funtoprod Fu Bo Re :- coq.unify-eq (app [{{ @eq }}, _ , Fu , Bo]) Re ok.

 solve (goal _ _ _ _ [trm L] as G) GL :-
   funtoprod L ( {{1}}) Re,  coq.ltac.say Re.
}}.

Tactic Notation "tryftp" constr(l) := elpi tryftp (l).

Goal False.
tryftp 0.
tryftp 2.
tryftp (fun (a : nat) => a ).
tryftp (fun (a b : nat) => 0) .

but all the examples fail. For instance, tryftp 0 fails with the following error message:

Unification problem outside the pattern fragment. ((Data.Term.App (global, (Data.Term.App (indc, (Data.Term.CData «O»), [])),
   [])) == (Data.Term.AppArg (2, [(Data.Term.Arg (5, 0))]))) Pass -delay-problems-outside-pattern-fragment (elpi command line utility) or set delay_outside_fragment to true (Elpi_API) in order to delay (deprecated, for Teyjus compatibility).

What does this error indicate? And how to fix this?

Enzo Crance (Sep 07 2022 at 14:02):

Replacing coq.ltac.say with coq.say makes the code work on my machine.

Enzo Crance (Sep 07 2022 at 14:04):

with coq.say {coq.term->string Re}

0 = 1
2 = 1
forall a : nat, a = 1
forall H H0 : nat, 0 = 1

I think it's what you expected

Enzo Crance (Sep 07 2022 at 14:05):

(unrelated) btw I think your call to coq.unify-eq is useless, because Re is still an unconstrained variable when unification is called, so Re will always be equal to the first argument you gave (app[{{ @eq }} ...). In this case you can directly use equality (Re = ...) or put your left hand side term directly in the head of the clause

Pierre Vial (Sep 07 2022 at 14:09):

Ok, my bad! :sweat:
I'll try with = . At first, I tried it with Re is ...but it didn't work though, so I thought I needed some unification to evaluate the elpi hole

Pierre Vial (Sep 07 2022 at 14:11):

it does work!

Last updated: Oct 13 2024 at 01:02 UTC