when does clojure.core.typed/cf in core.typed evaluate and infer the type

Question

I don't quite understand the behavior or clojure.core.typed/cf as explained below.

I assume cf is used to infer the type of a form

(t/cf (+ 1 2)) => Long

Now, this fails

(t/cf (/ 1 0)) => Error

This indicates to me that the sexpr was evaluated prior to be type checked. I had expected Long.

When I define a custom function:

(t/ann my-fn [t/Any -> t/Num])
(defn my-fn [x]
  (assert (number? x))
  (println "CALLED")
  x)

I can used this in the same expression again and it fails, indicating that the fn was indeed called.

(t/cf (/ 1 (my-fn 0)) => Error, because it evaluates my-fn. no type inference here??

However, then the following makes no sense to me.

(t/cf (range)) => (t/ASeq t/AnyInteger)

Why is in this case function range NOT evaluated, also if it did evaluate the expression, the following examples should return the same type:

(t/cf (->> (range 2) vec)) =>  (t/AVec (t/U Short Byte Integer BigInteger Long BigInt))
(t/cf [0 1]) =>  [(t/HVec [(t/Val 0) (t/Val 1)]) {:then tt, :else ff}]

But they return different types.

My gut feeling is that it has to do with constants, i.e. when I type check a form that contains t/Val's, then core.typed autoamtically evaluates it. This however doesn't explain why for certain functions it does not evaluate it. The 2 in (range 2) is definitely a constant, so why this difference in behavior.

If the forms are evaluated before type checking then the following should have the same behavior

(t/cf (map inc (range 10))))
(t/cf (map #(inc %) (range 10))))

But core.typed does indeed see a difference. The second example fails because the anonymous fn receives a t/Any by default and you cannot call inc on it. So this means that core.typed must do some analysis of the form plus it also evaluates it. I find this a bit confusing I confess, maybe someone can enlighten me.

Edit: A short summary

Why does the following relation seems to be true in some but not all cases?

(t/cf form) <=> (let [x form] (t/cf x))

Answer 1

core.typed performs completely static type checking.

The compilation pipleline for cf is read -> analyze -> type check -> eval.

If there is a static type error, that is considered fatal.

Otherwise the evaluation will be performed.

(cf (/ 1 0)) throws a runtime error because (/ 1 0) is a well-typed expression.

The reason evaluation is needed is related to the practicalities of analysing Clojure code — strange things happen if you analyze code then don’t evaluate it.