I tried to write Rational type: #lang typed/racket (define-type Rational (U Integer (Pair Rational Non-Zero-Rational))) (define-type Zero-Rational (U Zero (Pair Zero-Rational Non-Zero-Rational))) (define-type Non-Zero-Rational (Refine [num : Rational] (! num Zero-Rational))) (define-predicate rat? Rational) But I get a strange error message: car: contract violation expected: pair? given: #f context...: /usr/share/racket/pkgs/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt:90:2: loop /usr/share/racket/pkgs/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt:80:0: compute-defs /usr/share/racket/pkgs/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt:109:0: compute-constraints /usr/share/racket/pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt:230:0: get-max-contract-kind /usr/share/racket/pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt:438:10: for-loop f934 /usr/share/racket/pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/name.rkt:77:0: register-name-sc f952 f794 /usr/share/racket/collects/racket/private/map.rkt:40:19: loop /usr/share/racket/collects/racket/private/map.rkt:35:13: map f1476 /usr/share/racket/pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/name.rkt:77:0: register-name-sc f952 /usr/share/racket/pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt:287:2 /usr/share/racket/pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt:84:0: generate-contract-def I guess it was caused by (define-predicate rat? Rational) . Is define-predicate suitable for making predicate for Refine ?