Examples of unexpected behavior for integer refinements

[kartik-sabharwal]

What version of Racket are you using?

v8.7.0.6

What program did you run?

#lang typed/racket #:no-optimize #:with-refinements


;; `theorem_1` is accepted by the typechecker. Good.

(: theorem_1 ((Refine (x : Integer) (= x 0)) -> Zero))
(define theorem_1 identity)


;; `theorem_2` is accepted by the typechecker. Good.

(: theorem_2 (Zero -> (Refine (x : Integer) (= x 0))))
(define theorem_2 identity)


;; Contrary to my intuition, the typechecker rejects `theorem_3`.

;; (: theorem_3 ((Refine (x : Integer) (= x 2)) -> 2))
;; (define theorem_3 identity)


;; Contrary to my intuition, the typechecker accepts `theorem_4`

(: theorem_4 (Refine (x : 1) (= x 2)))
(define theorem_4 1)


;; Contrary to my intuition, the typechecker accepts `theorem_5`

(: theorem_5 ((Refine (x : Integer) (= x 1))
              (Refine (x : Integer) (= x 3)) ->
              (Refine (x : Integer) (= x 5))))
(define (theorem_5 m n)
  (+ m n))


;; The typechecker rejects `theorem_6` with the message
;; "Expected result: Nothing". Good.

;; (: theorem_6 (Refine (x : (Pairof Integer Integer))
;;                      (and (= (car x) 1) (= (cdr x) 3)
;;                           (= (+ (car x) (cdr x)) 5))))
;; (define theorem_6 (cons 1 3))


;; Contrary to my intuition, the typechecker rejects `theorem_7`.

;; (: theorem_7 (Refine (x : (Pairof 1 3)) (= (+ (car x) (cdr x)) 4)))
;; (define theorem_7 (cons 1 3))


;; Contrary to my intuition, the typechecker accepts `theorem_8`.

(: theorem_8 (Refine (x : (Pairof 1 1)) (= (+ (car x) (cdr x)) 4)))
(define theorem_8 (cons 1 1))

What should have happened?

Please check the comments in the code above. I think the intuitive behavior should be evident, but I could be mistaken.

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

In some situations, I get an error when I think I should not. In other situations, the typechecker accepts a definition that should not work.