It would be very convenient to have define-signature output a compile-time binding that allowed a type-checked version of pattern matching over terms in that signature. In other words, it would prevent typos in the match by type-checking the patterns. Example:
(define-signature num
[nat () (TYPE)]
[zero () (nat)]
[succ ([n (nat)]) (nat)])
(define x (zero))
(match/sig num x
[(zero (zero)) #t])
would fail to compile, because the LHS doesn't type-check. This would also allow the elaborating type checker (#6) to elaborate pattern-matches, which can give them a more convenient syntax. And regular old match would always be available for when this is onerous.
It would be very convenient to have define-signature output a compile-time binding that allowed a type-checked version of pattern matching over terms in that signature. In other words, it would prevent typos in the match by type-checking the patterns. Example:
would fail to compile, because the LHS doesn't type-check. This would also allow the elaborating type checker (#6) to elaborate pattern-matches, which can give them a more convenient syntax. And regular old match would always be available for when this is onerous.