This example works in SBCL, where types (possible disjoint sets of values) are treated as assertions. By default I always set "safety" and "debug" to 3 (the max), which helps.
;; Giving names to abstract things a little
(deftype zero () `(eql 0))
(deftype non-zero () `(and number (not zero)))
;; Declaration
(declaim (ftype (function (number non-zero) number) divide))
;; Definition
(defun divide (n d) (/ n d))
;; Test
(lambda (u v)
;; introduce a type constraint here.
(declare (type zero v))
(divide u v)) ;; (nb: underlined in orange)
This message is also printed:
note: deleting unreachable code
warning:
Derived type of V is
(VALUES (INTEGER 0 0) &OPTIONAL),
conflicting with its asserted type
(OR (AND NUMBER (NOT INTEGER)) (INTEGER * -1) (INTEGER 1)).
See also:
SBCL Manual, Handling of Types [:node]
The warning happens when two types are and-ed (intersection), and the resulting set is empty. You still allow code where there is potentially "bad" value flowing from one place to another, because ultimately you know the runtime will detect it. In other words, the goal is to reject false negatives (unwarranted warnings), which contrasts with statically typed languages where you only accept code that is guaranteed to satisfy static typing rules (it makes sense there because the compiler is your last chance of catching those type errors, since the runtime does generally not perform type checks).
(edit: actually use non-zero instead of (not zero))