parse error raised by `Refinement`.

[NoahStoryM]

What version of Racket are you using?

v8.4 [cs]

What program did you run?

#lang typed/racket

(define _ (gensym 'k))
(define k? (curry symbol=? _))
(declare-refinement k?)
(define-type K (Refinement k?))
(define k (assert _ k?))

What should have happened?

No error. I'm not sure why this code doesn't work and refinement-even.rkt does.

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

draft.rkt:8:15: Type Checker: parse error in type;
 expected a predicate for argument to Refinement
  given: Nothing
  in: (Refinement k?)
  location...:
   draft.rkt:8:15
  context...:
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/private/parse-type.rkt:680:0: parse-for-effects
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/env/type-alias-helper.rkt:102:4: for-loop
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/env/type-alias-helper.rkt:90:0: register-all-type-alias-info
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/env/type-alias-helper.rkt:61:0: register-all-type-aliases
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:414:0: type-check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:653: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

More.

It works in REPL:

Welcome to Racket v8.4 [cs].
> (define _ (gensym 'k))
> (define k? (curry symbol=? _))
> (declare-refinement k?)
> (define-type K (Refinement k?))
> (define k (assert _ k?))
> (:print-type k?)
(-> Symbol Boolean : K)
> (:print-type k)
K
> 

[samth]

I think Refinement needs the function to already be typechecked before the use of Refinement. The best way to do this is to use a separate module.

[NoahStoryM]

Hi @samth , I tried to define k? in a module, but the problem still exists:

#lang typed/racket

(module K typed/racket
  (provide (all-defined-out))

  (define _ (gensym 'k))
  (define k? (curry symbol=? _)))
(require 'K)

(declare-refinement k?)
(define-type K (Refinement k?))
(define k (assert _ k?))