refinement type runs into an endless loop

[Syntacticlosure]

What version of Racket are you using?

6.12

What program did you run?

#lang typed/racket #:with-refinements
(define-type test (Refine [a : (Pairof Integer Integer)]
                          (<= (car a) (cdr a))))
(ann '(2 . 1) test) 

What should have happened?

a type error

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

Background expansion abnormally(out of memory)

[pnwamk]

Thanks for the report!

Some preliminary investigation, oddly enough this expression type checks:

(ann '(1 . 2) (Refine [a : (Pairof Integer Integer)]
                      (<= (car a) (cdr a))))

and this one gets stuck in an infinite loop during expansion:

(ann '(2 . 1) (Refine [a : (Pairof Integer Integer)]
                      (<= (car a) (cdr a))))

Also (probably somewhat unrelated but I'll jot it down here now while I've got the examples), the version with cons just fails to type check when it should work, probably because there is a bug/deficiency in how inference is working w/ the expected refinement type. i.e. this type checks:

(define p (cons 1 2))

(ann p (Refine [a : (Pairof Integer Integer)]
               (<= (car a) (cdr a))))

but this does not:

(ann (cons 1 2)
     (Refine [a : (Pairof Integer Integer)]
             (<= (car a) (cdr a))))