Can not handle abstraction over constructor

[xieyuheng]

The following definition of sub-to-zero
with an abstraction my-add1 over constructor add1
can not pass termination-check:

(data Nat () ()
  [zero () Nat]
  [add1 ([prev Nat]) Nat])

(fn my-add1 (-> Nat Nat)
  [(x) (add1 x)])

(fn sub-to-zero (-> Nat Nat)
  [((zero)) zero]
  [((add1 (zero))) zero]
  [((add1 (add1 x))) (sub-to-zero (my-add1 x))])

test: https://github.com/cicada-lang/mugda/blob/master/tests/termination/sub-to-zero-indirect-add1.error.mu

[xieyuheng]

We need to compare with Coq and Agda to see should this work or not.

[xieyuheng]

Maybe we can solve this by

• comparing Value with Pattern
• instead of comparing Exp with Pattern