different replies to pattern matching `(p ,_ ...) `(p . ,_)

[wllsena]

Racket version 8.0 [cs]

Why does it work

#lang typed/racket

(define-type Term (Listof (U Symbol Term)))

(: get-tokens (-> Term (Listof Symbol)))
(define (get-tokens term)
  (match term
    [`()                       `()]
    [`(,(? list? tk) . ,tks)   `(,@(get-tokens tk) ,@(get-tokens tks))]
    [`(,(? symbol? tk) . ,tks) `(,tk ,@(get-tokens tks))]))

And it doesn't work?

#lang typed/racket

(define-type Term (Listof (U Symbol Term)))

(: get-tokens (-> Term (Listof Symbol)))
(define (get-tokens term)
  (match term
    [`()                         `()]
    [`(,(? list? tk) ,tks ...)   `(,@(get-tokens tk) ,@(get-tokens tks))]
    [`(,(? symbol? tk) ,tks ...) `(,tk ,@(get-tokens tks))]))

Error

. Type Checker: type mismatch
  expected: Term
  given: (Listof Any) in: tks
. Type Checker: type mismatch
  expected: Term
  given: (U Symbol Term) in: tks
. Type Checker: Summary: 2 errors encountered in:
  tks
  tks

[maueroats]

I have no solution, but wrote this to give more context in case someone tries to work on it later.

I guess you know you are matching a quasipattern? I think this report shows the type inferencing for quasipatterns behaving in a different way from "equivalent" non-quasipatterns. (As far as I understand it.)

The good: the type system is making the desired deductions when applied to non-quasipatterns thing ... (see code below), and also when applied to the form . last-qp in a quasipattern (first example in the report above).

The bad: the type system is not making the desired deductions when applied to the quasipattern qp ... (second example in the code above). The type system can only figure out that this is type (Listof Any) but in context above it should be to be of type (Listof Term).

I'm going to give up on it here.

(: get-tokens (-> Term (Listof Symbol)))
(define (get-tokens term)
  (match term
    [`()                           `()]
    [(list (? list? tk) tks ...)   `(,@(get-tokens tk) ,@(get-tokens tks))]
    [(list (? symbol? tk) tks ...) `(,tk ,@(get-tokens tks))]))

[samth]

Here's what's happening:

0. Writing ... implies that the rest is a list, whereas a . b just takes the car and cdr. So the first two examples are different in that way.
1. using quasi-patterns, the pattern matching code generates a loop, which needs additional annotations in order to type check. That's why the second example fails.
2. You can fix this by providing annotations:

   (define (get-tokens term)
   (match term
   [`()                         `()]
   [`(,(? list? tk) ,#{tks : Term} ...)   `(,@(get-tokens tk) ,@(get-tokens tks))]
   [`(,(? symbol? tk) ,#{tks : Term} ...) `(,tk ,@(get-tokens tks))]))

3. The list pattern has an optimization when the pattern before the ... is just an identifier, and just calls list?. That's why the third example works.

match can be improved to use the optimization for quasi-patterns as well, but in general with ... except in the simplest cases you'll need annotations.