Contract violation error in complicated binding forms

[david-christiansen]

I was trying to specify a language that has a sort of rudimentary module system. The idea is that a module consists of 0 or more imports (which are themselves modules), 0 or more definitions, and an expression. The names defined in the definitions are exported to clients of the module.

While working on this, I managed to trigger a contract violation error from substitution. Here's a cut-down version of what I was writing:

#lang racket

(require redex)

(define-language L
  (x variable-not-otherwise-mentioned)
  (e number x)
  (decl (define x e) (define-const x number))
  (imports (import prog ...))
  (prog (unit
          imports
          decl ...
          e))

  #:binding-forms

  (define x e) #:exports x
  (define-const x number) #:exports x

  (import prog_imports
          #:...bind (imported-vars prog_imports (shadow imported-vars prog_imports))) #:exports imported-vars

  (unit imports_libs decl_def #:...bind (defined-vars decl_def (shadow defined-vars decl_def)) e #:refers-to (shadow imports_libs defined-vars ...))

  )

(define test-program
  (term (unit (import) (define-const x 1) (define y x) y)))

(term (substitute ,test-program y 444) #:lang L)

yields

; map: contract violation
;   expected: list?
;   given: (term-and-table '((define-const x«1» 1) ((define y«0» x«1») ())) '((y y«0») (x x«1»)))
; Context (plain; to see better errortrace context, re-run with C-u prefix):
;   /home/dtc/racket/collects/racket/private/map.rkt:257:2 gen-map
;   .../private/map.rkt:40:19 loop
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:334:0 pass-...
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:438:2 interp-betas
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:664:4 loop
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:664:4 loop
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:664:4 loop
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:664:4 loop
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:664:4 loop
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:661:0 rec-freshen-spec
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/binding-forms.rkt:165:0 safe-subst
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/reduction-semantics.rkt:1550:37
;   .../private/map.rkt:40:19 loop
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/reduction-semantics.rkt:1843:16 metafunc
;   /home/dtc/racket/share/pkgs/redex-lib/redex/private/term.rkt:80:18

[david-christiansen]

The errortrace version is actually less informative:

; map: contract violation
;   expected: list?
;   given: (term-and-table '((define-const x«1» 1) ((define y«0» x«1») ())) '((y y«0») (x x«1»)))
; Context (errortrace):
;    /home/dtc/tmp/redex-defs.rkt:30:6: ()
;    /home/dtc/racket/share/pkgs/redex-lib/redex/private/term.rkt:412:34: "bad syntax"
;    /home/dtc/tmp/redex-defs.rkt:30:0: ()

[rfindler]

Thanks, @david-christiansen . (The errortrace thing is probably because redex's implementation isn't being instrumented by errortrace.)

@paulstansifer do you have time to look into this one?