Type Infering

[HoshinoTented]

open data Wrapper (P : Type)
| wrap (P -> False)

def what? (m : Nat) : Wrapper (suc m = 0) =>
  wrap (\ x => z≠s (sym x))

Aya said:

In file Arith\Nat\Properties.aya:65:20 ->

  63 |   
  64 |   def what? (m : Nat) : Wrapper (suc m = 0) =>
  65 |     wrap (\ x => z≠s (sym x))
     |                       ^---^

Error: The boundary
         x 1
       disagrees with
         0

at (1859-1863) [65,20-65,24]

It looks like aya doesn't know what the type of x is (hole), so aya is unable to normalize x 1. However, this code makes aya happy:

open data NeqWrapper (m n : Nat)
| newNeq ((m = n) -> False)

def what (m : Nat) : NeqWrapper (suc m) 0 =>
  newNeq (\ x => z≠s (sym x))

This problem can be solved by telling aya the type of x.

[ice1000]

This requires putting cubical boundary conditions into the constraints... It's blocked by a meta so it's reasonable

[ice1000]

Fixed by the new version. Why?