wilbowma/cur

"#%app: expected a typed term" with emacs-mode

Opened this issue · 0 comments

#lang cur

(define-datatype Nat : Type
  (z : Nat)
  (s : (-> Nat Nat)))

(define-datatype Vec (A : Type) : (-> Nat Type)
  (nil : (Vec A z))
  (cons : (forall (a : A) (n : Nat) (Vec A n)
                  (Vec A (s n)))))

Output (in Racket mode):

; /tmp/meow1.rkt:8:16: #%app: expected a typed term
;   at: (z)
;   in: (#%app (Vec A) (z))
; Context:
;  ..../workspace/racket/racket/share/pkgs/macrotypes-lib/macrotypes/typecheck-core.rkt:1003:2 detach/check
;  ..../workspace/cur/cur-lib/cur/curnel/coc.rkt:166:0 app
;  ..../racket/racket/collects/syntax/wrap-modbeg.rkt:46:4 do-wrapping-module-begin
#<procedure:void>
#<procedure:void>
; [Due to errors, REPL is just module language, requires, and stub definitions]

However, it works when run in the REPL (even the Racket mode REPL), and when run via raco or racket -t on the command line.