## 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 `Fu`of the form `fun (a1 : A1) .... (a : An) => expr : B`
• an expression `Te`of 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):

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