Definition cannot type check

[aya-prover]

Definition cannot type check

[ice1000]

I think it's the program

[ice1000]

The error is now

Error: Cannot check the expression of type
         Path (λ _9 ⇒ Nat) (hfill2d {Nat} {suc (add n (mul' m (suc n)))} {suc (add
        n (mul' m (suc n)))} {suc (add (add m n) (mul' m n))} {suc (add n (mul' m (suc
        n)))} (idp {Nat} suc (add n (mul' m (suc n)))) (idp {Nat} suc (add n (mul'
        m (suc n)))) (*'-suc-suc m n) right left) (hfill2d {Nat} {suc (add n (mul'
        m (suc n)))} {suc (add n (mul' m (suc n)))} {suc (add (add m n) (mul' m n))}
        {suc (add n (mul' m (suc n)))} (idp {Nat} suc (add n (mul' m (suc n)))) (idp
        {Nat} suc (add n (mul' m (suc n)))) (*'-suc-suc m n) right right)
         (Normalized: Path (λ _9 ⇒ Nat) (suc (add (add m n) (mul' m n))) (suc (add
        n (mul' m (suc n)))))
       against the type
         Eq {Nat} (suc (add (add m n) (mul' m n))) (mul' (suc m) (suc n))
         (Normalized: Path (λ i ⇒ Nat) (suc (add (add m n) (mul' m n))) (suc (add n
        (mul' m (suc n)))))

[wsx-ucb]

The end points of the path now agree, but I'll continue to investigate the case.

[ice1000]

The end points of the path now agree, but I'll continue to investigate the case.

I think the trace would be very helpful

[wsx-ucb]

During normalization, the end points don't actually agree (despite when reporting the error, they agree again...). One is still incorrectly reduced to (suc (add n (add m (mul' m n)))) instead of the correct (suc (add (add m n) (mul' m n))). Interesting. I'll try to find the real problem here tomorrow.

[ice1000]

🤷‍♀️

[wsx-ucb]

Here is a simpler (non-working) example:

prim I
prim left
prim right
struct Path (A : I -> Type) (a : A left) (b : A right) : Type
  | at (i : I) : A i {
    | left => a
    | right => b
  }
def path {A : I -> Type} (p : Pi (i : I) -> A i)
  => new Path A (p left) (p right) { | at i => p i }
def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
def idp {A : Type} (a : A) : a = a => path (\ i => a)

bind = looser application

prim arcoe
def hfill2d {A : Type}
  {a b c d : A}
  (p : a = b)
  (q : b = d)
  (r : a = c)
  (i j : I) : A
  => (arcoe (\ k => (r.at k) = (q.at k)) p i).at j
def hcomp2d {A : Type}
  {a b c d : A}
  (p : a = b)
  (q : b = d)
  (r : a = c) : c = d
  => path (hfill2d p q r right)

def pmap {A B : Type} (f : A -> B) {a b : A} (p : a = b)
  : f a = f b => path (\ i => f (p.at i))

open data Nat : Type
  | zero
  | suc Nat

def `+` add (m n : Nat) : Nat
  | zero, n => n
  | n, zero => n
  | suc m, n => suc (add m n)
  | m, suc n => suc (add m n)

bind + tighter =

def +-comm (x y : Nat) : x + y = y + x
  | zero, n => idp n
  | suc n, m => pmap suc (+-comm n m)

def flip (m n : Nat) : Nat =>
  (hcomp2d
    (idp (m + n))
    (idp (m + n))
    (path (\ i => (+-comm m n).at i))).at left

def err_eq (m n : Nat) : (flip m n) = (n + m) => idp _

Notice if you change the definition of flip into

def flip (m n : Nat) : Nat =>
  (hcomp2d
    (idp (m + n))
    (idp (m + n))
    (+-comm m n)).at left

The code compiles without error.