Unification break if I remove a constant modifier to a disjunction symbol

[NotBad4U]

Hi!

I am working with the definitions in Prop.lp of Lambdapi-stdlib. I wanted to implement rewrite rules for the disjunction, so I removed the constant modifier on the constant symbol ∨ : Prop → Prop → Prop; notation ∨ infix left 6;. But then I got a lot of unification errors, like this one on a lemma that I added:

(This is a snippet that isolate the problem)

constant symbol Prop : TYPE;

builtin "Prop" ≔ Prop;

// interpretation of propositions in TYPE

injective symbol π : Prop → TYPE; // `p

builtin "P" ≔ π;

symbol ∨ : Prop → Prop → Prop; notation ∨ infix left 6; // \/ or \vee
// ^^^^^^ Here I removed the constant modifier
constant symbol ∨ᵢ₁ [p q] : π p → π (p ∨ q);
constant symbol ∨ᵢ₂ [p q] : π q → π (p ∨ q);
symbol ∨ₑ [p q r] : π (p ∨ q) → (π p → π r) → (π q → π r) → π r;

opaque symbol ∨_commutative [x y] : π (x ∨ y) → π (y ∨ x) ≔
begin
  assume x y hxy;
  apply ∨ₑ hxy
  { assume hx; apply ∨ᵢ₂; apply hx }
  { assume hy; apply ∨ᵢ₁; apply hy }
end;

I got the unification error:

Missing subproofs (2 subproofs for 5 subgoals):
x: Prop
y: Prop
hxy: π (x ∨ y)

--------------------------------------------------------------------------------
0. x ∨ y ≡ ?611.[x;y;hxy] ∨ ?612.[x;y;hxy]
1. ?611: Prop
2. ?612: Prop
3. ?614: π ?611.[x;y;hxy] → π (y ∨ x)
4. ?615: π ?612.[x;y;hxy] → π (y ∨ x)

With the modifier `constant, everything works well. Some lemma in Nat.lp and Pos.lp also break. Is this the expected behaviour or a bug?

[fblanqui]

As you can see from the first goal, which is a unification goal, the system doesn't know how to solve x ∨ y ≡ ?611.[x;y;hxy] ∨ ?612.[x;y;hxy]. Indeed, since ∨is a defined symbol now, there may be several solutions to this unification problem. One solution is to declare ∨as injective. Note that the system does not check that injectivity actually holds: users have to check it by themselves.