Issue with match-define

cogumbreiro commented 1 year ago

What version of Racket are you using?

8.2

What program did you run?

(struct point ([x : Number] [y : Number]))
(: add (-> point Number) )
(define (add a)
  (match-define (point a b) a)
  b)

yields a typing error.

What should have happened?

I would expect no typing error, but maybe I'm misunderstanding the semantics of scoping with a match-define. For instance, the following example yields no errors.

(struct point ([x : Number] [y : Number]))

(: add (-> point Number) )
(define (add a)
  (match a
    [(point a b) b]
  )
)

Alternatively, if some error is to be triggered, the existing error message is misleading.

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

example.rkt:7:23: Type Checker: insufficient type information to typecheck. please add more type annotations
  in: a
  location...:
   example.rkt:7:23
  context...:
   .../private/map.rkt:40:19: loop
   [repeats 1 more time]
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt:244:5
   .../private/runtime.rkt:89:23: fail-handler118
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:105:0: tc-lambda-body
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:494:0: check-mono-lambda/expected
   .../match/compiler.rkt:548:40: f620
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt:791:0: tc/lambda
   .../private/runtime.rkt:89:23: fail-handler118
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt:112:0: tc-expr/check
   .../private/parse.rkt:1020:13: dots-loop
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:391:0: type-check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:635:0: tc-module
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/tc-setup.rkt:101:12
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typed-racket.rkt:22:4

AlexKnauth commented 1 year ago

This version of it with #{name : type} annotations works:

(match-define (point #{a : Number} #{b : Number}) a)

(Edit: and by "works" I mean that it typechecks. it errors at runtime with a: undefined; cannot use before initialization)

AlexKnauth commented 1 year ago

Renaming one of the 2 a variables to something else also solves this issue, and allows it to run without the a: undefined; cannot use before initialization error.

cogumbreiro commented 1 year ago

Renaming one of the 2 a variables to something else also solves this issue, and allows it to run without the a: undefined; cannot use before initialization error.

Ah, yes! Sorry, I forgot to add that the issue arises because a appears in the match and as a variable in a pattern. A workaround is naming variable a in the pattern as a1, for instance.

capfredf commented 1 year ago

The problem has nothing to do with match-define. It's just that circular definitions require type annotations to break dependencies. For example, the program below has the same error.

(lambda ([a : Number] [b : Number])
  (define a (point a b))
  (void))

In the match example,

  (match a
    [(point a b) b]

a in the clause shadows a being matched against.

capfredf commented 1 year ago

Alternatively, you can use match-let

(lambda ([a : point])
  (match-let ([(point a b) a])
    b))

cogumbreiro commented 1 year ago

It's just that circular definitions require type annotations to break dependencies.

Can you please clarify why any of these examples are "circular"? I am not really sure I understand the use of circular in this context.

In my understanding, the pattern in the pattern-matching is introducing a new scope after the match-define and within the match-let, which would disambiguate any confusion (cycle?).

samth commented 1 year ago

The program does not work like match-let. Instead, the a on the right hand side refers to the a on the left hand side. If you put this program in DrRacket:

#lang racket

(struct point (x y))
(define (add a)
  (match-define (point a b) a)
  b)

you can see that the binding arrow from the RHS points to the LHS.

racket / typed-racket