match-define does not type-check argument

[bennn]

What version of Racket are you using?

6.10

What program did you run?

#lang typed/racket/base
(require racket/match)

(: f (-> (Pairof Integer Integer) Integer))
(define (f x)
  (match-define (vector a b) x)
  (+ a b))

(f (cons 1 2))


(: g (-> (U #f (Vector Integer Integer)) Integer))
(define (g x)
  (match-define (vector a b) x)
  (+ a b))

(g #f)


;; on the bright side
(match-define (cons a b) (car (filter (lambda ((x : Any)) x) '(#f (1 . 2) #f))))

What should have happened?

3 type errors
describing how the 3 calls to match-define can obviously fail

If you got an error message, please include it here.

The runtime error message is good:

match-define: no matching clause for '(1 . 2)

[samth]

I don't think it's reasonable to have these become type errors -- match's semantics are that it checks these things dynamically and errors if they fail, and match-define is just a match with only one clause.

We could have a different form that made these type errors, using typecheck-fail, but I don't think that's likely to work as often as you'd like.

[bennn]

Ok.
But I don't want to close this issue (EDIT:) until this point about match is somewhere in the Typed Racket documentation.

[samth]

What do you think the documentation should say?

[bennn]

Either/or:

• an entry for match in "Special Form Reference"
• an entry in a new subsection of "Libraries Provided with Typed Racket"; the new subsection should describe how a Racket identifier corresponds to a TR one when the connection isn't obvious

and it should clarify that match is exactly Racket's match:

• match accepts any argument
• doesn't check that patterns are exhaustive

[samth]

I think the second alternative is the right one -- match can't be documented in "Special Form Reference" since TR has an identical version.

[mfelleisen]

Can we really not do any better?

…

On Aug 14, 2017, at 8:26 PM, Ben Greenman ***@***.***> wrote: Either/or: • an entry for match in "Special Form Reference" • an entry in a new subsection of "Libraries Provided with Typed Racket"; the new subsection should describe how a Racket identifier corresponds to a TR one when the connection isn't obvious and it should clarify that match is exactly Racket's match: • match accepts any argument • doesn't check that patterns are exhaustive — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[samth]

What do you think would be "better" here?

[mfelleisen]

(match-define (vector a b) x) where x is of type Cons could produce an ML-style warning about inexhaustive matches.

…

On Aug 15, 2017, at 9:58 AM, Sam Tobin-Hochstadt ***@***.***> wrote: What do you think would be "better" here? — You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

[rfindler]

What if we changed the expansion of match-define (or other match-related constructs that have only one alternative) so they expanded into something like:

(match-define p e)

==>

(match e 
  [p e]
  [_ (thing-that-type-rackets-type-checker-knows-to-get-upset-about-when-it-isnt-dead-code)])

Could something like be made to that work?

[mfelleisen]

Looks good to me. I bet that exceptions are inserted that way in ML type checkers.

…

On Aug 15, 2017, at 10:41 AM, Robby Findler ***@***.***> wrote: What if we changed the expansion of match-define (or other match-related constructs that have only one alternative) so they expanded into something like: (match-define p e) ==> (match e [p e] [_ (thing-that-type-rackets-type-checker-knows-to-get-upset-about-when-it-isnt-dead-code)]) Could something like be made to that work? — You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

[samth]

I think a general mechanism for macros to annotate expressions where TR should warn if they aren't dead is the right way to do this (a syntax property would be the easiest thing here). We'd have to see how many false positives it would generate.

Another issue is that we don't have a good way to surface warnings from compile-time to users. The compiler (and Typed Racket in some cases) uses log-warning, which you almost never see. When TR has used log-error, that's made people unhappy because it appears to be an error.

I'll use log-warning here, but this is a more general problem.

[rfindler]

I can imagine adding something to DrRacket where it, during online expansion and in the REPL, listens to a specific logger for a warning and then shows it, perhaps in orange instead of red or something?

[samth]

That sounds like it would work for TR, and I assume for the compiler as well.

[tfb]

I like the idea of a syntax property that Typed Racket could complain about if it's not dead code. That would make it possible to retain a lot of existing patterns for macro-expansions that produce clear, specific errors at runtime, but make the information available at type-checking time.