Skip to content

Refinement type editor/repl inconsistency #1100

Open
@iamevn

Description

@iamevn

Racket version 8.0 [cs]

I forgot to specify a return type on a function and was having issues with type checking in the repl.

#lang typed/racket #:with-refinements

(define-type Two (Refine [n : Integer] (= n 2)))

(define (f [n : Two]) : Void
  (void))

(define (g [n : Two])
  (void))

(f 1) ;; Type Checker: type mismatch expected: Two given: (Refine (x₀ : One) (= 1 x₀)) in: 1
(f 2) ;; works

(g 1) ;; Type Checker: type mismatch expected: Two given: (Refine (x₀ : One) (= 1 x₀)) in: 1
(g 2) ;; works in definitions window, fails in interactions window

Type checking works as expected in the definitions window but when I try to run (g 2) in the interactions window I get a type error:

 Type Checker: type mismatch
  expected: Two
  given: Positive-Byte in: 2

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions