Bug in OOP confluence

[ice1000]

Can anyone check this code for me? I'm on a dev branch. It doesn't work.

open data Nat : Type
 | zero
 | suc Nat

def add {a b : Nat} : Nat
 | {zero}, {zero} => b
 | {zero}, {suc (suc a)} => b
 | {suc a}, {zero} => b
 | {suc a}, {b} => b
 | {suc a}, {suc b} => suc b

[ice1000]

open data Nat : Type
 | zero
 | suc Nat

def add {a biu : Nat} : Nat
 | {zero}, {x} => biu
 | {suc a}, {zero} => biu
 | {suc a}, {bua} => bua
 | {suc a}, {suc tasteit} => suc tasteit

The reason is that the b in the parameter is unequal to the b in the binding. In fact they're equal, but a corresponding substitution is missing.

[ice1000]

  70 | def addI-comm (a b : Int) : Eq (addI a b) (addI b a)
  71 | | pos n, pos m => pmap pos (addN-comm n m)
  72 | | neg n, neg m => pmap neg (addN-comm n m)
         ^--------------------------------------^ substituted to `pmap {Nat} {Int}
  (λ _1 ⇒ neg zero) {addN n zero} {addN zero n} (addN-comm n zero)`
  73 | | pos n, neg m => idp _
  74 | | neg n, pos m => idp _
         ^-------------------^ substituted to `new { | at ⇒ neg n }`

Error: The 2nd clause matches on a constructor with condition(s). When checking the
       1st condition, we failed to unify `pmap {Nat} {Int} (λ _1 ⇒ neg zero) {addN
       n zero} {addN zero n} (addN-comm n zero)` and `new { | at ⇒ neg n }`

[ice1000]

Error: The 3rd clause matches on a constructor with condition(s). When checking the
       1st condition, we failed to unify `idp {Int} (subNI n zero)` and `new { |
       at ⇒ pos zero }`

[ice1000]

  70 | def addI-comm (a b : Int) : Eq (addI a b) (addI b a)
  71 | | pos n, pos m => pmap pos (addN-comm n m)
  72 | | neg n, neg m => pmap neg (addN-comm n m)
         ^--------------------------------------^ substituted to `pmap {Nat} {Int}
  (λ _1 ⇒ neg zero) {addN n zero} {addN zero n} (addN-comm n zero)`
  73 | | pos n, neg m => idp _
  74 | | neg n, pos m => idp _
         ^-------------------^ substituted to `new { | at ⇒ neg n }`

Error: The 2nd clause matches on a constructor with condition(s). When checking the
       1st condition, we failed to unify `pmap {Nat} {Int} (λ _1 ⇒ neg zero) {addN
       n zero} {addN zero n} (addN-comm n zero)` and `new { | at ⇒ neg n }`

I think I have caught the problem. It should not be pmap (λ _1 ⇒ neg zero) blabla. It should be pmap (λ _1 ⇒ neg _1). But a correct fix of this problem remains a mystery.

[ice1000]

Don't try to understand the code. Feel it.

[ice1000]

This problem is fixed, and now we have a problem factory.