Handle non-inductive arguments in pattern matching when they aren't destructed

[dmelcer9]

Say we have the following function:

(define/rec/match fold : (X : Type) (Y : Type) (f : (-> X Y Y)) (List X) Y -> Y
  [(nil X) b => b]
  [(cons X h t) b => (f h (fold X Y f t b))])

Even though we aren't destructing b, cur gives the error:

[...]/cur/cur-lib/cur/stdlib/totality.rkt:18:22: total?: Expected pattern match on an inductively defined type, but #<syntax:[the Y before the arrow in line 1] match-2-310> is not inductive

[stchang]

Nice. I just asked the same thing in this hidden thread

[stchang]

an answer.

To get around it, you could just flip the order of the last two arguments right?

[wilbowma]

I would consider that invalid, since match ought to only get inductive types. Instead, the same thing should be written as something like:

(define/rec/match fold : (X : Type) (Y : Type) (f : (-> X Y Y)) (List X) (b : Y) -> Y
  [(nil X) => b]
  [(cons X h t) => (f h (fold X Y f t b))])

[dmelcer9]

def/rec/match doesn't allow non-inductive arguments to be both before and after inductive ones, I flipped the arguments for now.

[wilbowma]

Ideally, def/rec/match wouldn't be sensitive to position in this way, and could match on named arguments, but that's an improvement for later. Might be able to mimic that by returning a function in the branches if that's the interface you really want.