org.opentest4j.AssertionFailedError: issue366.aya ==> expected: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:3:12 -> 1 │ open data Nat : Type 0 | zero | suc Nat 2 │ open data Ray (a : Nat) : Type | zero => eldath 3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat │ ╰────────╯ 4 │ | zero, eldath => suc zero │ ╰──────────────────────╯ (confluence check: this clause is substituted to) `suc zero` 5 │ | zero, eldath => zero │ ╰──────────────────╯ (confluence check: this clause is substituted to) `zero` Error: The 2nd and the 1st clauses are not confluent because we failed to unify suc zero and zero In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:5:3 -> 3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat 4 │ | zero, eldath => suc zero 5 │ | zero, eldath => zero │ ╰──────────────────╯ Warning: The 1st clause dominates the 2nd clause. The 2nd clause will be unreachable In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:4:3 -> 2 │ open data Ray (a : Nat) : Type | zero => eldath 3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat 4 │ | zero, eldath => suc zero │ ╰──────────────────────╯ Warning: The 2nd clause dominates the 1st clause. The 1st clause will be unreachable 1 error(s), 2 warning(s). What are you doing? > but was: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:3:12 -> 1 │ open data Nat : Type 0 | zero | suc Nat 2 │ open data Ray (a : Nat) : Type | zero => eldath 3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat │ ╰────────╯ 4 │ | zero, eldath => suc zero │ ╰──────────────────────╯ (confluence check: this clause is substituted to) `suc zero` 5 │ | zero, eldath => zero │ ╰──────────────────╯ (confluence check: this clause is substituted to) `zero` Error: The 2nd and the 1st clauses are not confluent because we failed to unify suc zero (Normalized: 1) and zero (Normalized: 0) In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:5:3 -> 3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat 4 │ | zero, eldath => suc zero 5 │ | zero, eldath => zero │ ╰──────────────────╯ Warning: The 1st clause dominates the 2nd clause. The 2nd clause will be unreachable In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue366.aya:4:3 -> 2 │ open data Ray (a : Nat) : Type | zero => eldath 3 │ overlap def ray-eldath (a : Nat) (ed40 : Ray a) : Nat 4 │ | zero, eldath => suc zero │ ╰──────────────────────╯ Warning: The 2nd clause dominates the 1st clause. The 1st clause will be unreachable 1 error(s), 2 warning(s). What are you doing? >