A bug in unification

[ice1000]

I have a self-contained piece of code:

The implicit inference gives the wrong result. Manually specifying it would work:

I used latest Arend I've compiled myself (in https://github.com/JetBrains/intellij-arend/pull/284).

[ice1000]

Source code:

\func wow {U : \Type} {T : U -> \Type} (A B : U) (a : T A) (b : T B) : Nat => zero

\func test1 {A B : \Type} {x : A} {y : B} => wow A B x y
\func test2 {A B : \Type} {x : A} {y : B} => wow {_} {\lam _ => A} A B x x

Removing the implicit arguments would trigger the bug.

[ice1000]

The equivalent code works in Agda:

open import Agda.Builtin.Nat
wow : ∀ {ℓ ℓ'} {A : Set ℓ} {B : A -> Set ℓ'} (a b : A) (x : B a) (y : B b) -> Nat
wow _ _ _ _ = zero
test1 : ∀ {ℓ} (A B : Set ℓ) (x : A) (y : B) -> Nat
test1 A B x y = wow A B x x
test2 : ∀ {ℓ} (A B : Set ℓ) (x : A) (y : B) -> Nat
test2 A B x y = wow A B x y

[valis]

It seems the issue is fixed