How do you annotate polymorphic core functions in Clojure's core.typed?

Question

I want to apply core.type annotations to my code, but am running into a stumbling block with how/when to instantiate a core function that is polymorphic, called from inside the body of the function.

Troubleshooting this, I have learned that I have to treat filter and count special because they are polymorphic and static respectively, that anonymous functions should be pulled out and annotated in let bindings. If somebody could explain how to annotate this based on the output of the error message below, I would really appreciate it.

Here are my aliases:

(defalias Key-set (Set (Option Kw)))
(defalias Player (Ref1 Key-set))
(defalias Set-vec (Vec (Set Kw)))
(defalias Move (U ':x ':o))

current form that the function is in:

    (ann first-two [Player -> (Option Seq)])
    (defn first-two [player]
      (let [;; best guesses here
            filter>    (inst filter [[(U (Seqable Any) clojure.lang.Counted nil) -> Bool] -> Any] (Option (clojure.lang.Seqable [(U (Seqable Any) clojure.lang.Counted nil) -> Bool])))
            count>     (ann-form count [(U nil (Seqable Any) clojure.lang.Counted) -> Number])

            two-count? :- [(U nil (Seqable Any) clojure.lang.Counted)-> Bool], #(= (count> %) 2)
            couples    :- (Option (Seqable Key-set)), (concat adjacents opposite-corners opposite-sides)]
        (first (filter> two-count?
                        (for [pair :- Key-set, couples]
                          (clojure.set/intersection pair @player))))))

type checker error message:

Type Error (tic_tac_toe/check.clj:52:5) Function filter> could not be applied to arguments:


Domains:
    [[[(U (Seqable Any) Counted nil) -> Bool] -> Any] -> Any :filters {:then (is (Option (clojure.lang.Seqable [(U nil (Seqable Any) clojure.lang.Counted) -> Bool])) 0), :else tt}] (Option (clojure.lang.Seqable [[(U (Seqable Any) Counted nil) -> Bool] -> Any]))
    [[[(U (Seqable Any) Counted nil) -> Bool] -> Any] -> Any :filters {:then (! (Option (clojure.lang.Seqable [(U nil (Seqable Any) clojure.lang.Counted) -> Bool])) 0), :else tt}] (Option (clojure.lang.Seqable [[(U (Seqable Any) Counted nil) -> Bool] -> Any]))
    [[[(U (Seqable Any) Counted nil) -> Bool] -> Any] -> Any] (Option (clojure.lang.Seqable [[(U (Seqable Any) Counted nil) -> Bool] -> Any]))

Arguments:
    [(U nil (Seqable Any) clojure.lang.Counted) -> Bool] (clojure.lang.LazySeq Any)

Ranges:
    (ASeq (Option (clojure.lang.Seqable [(U nil (Seqable Any) clojure.lang.Counted) -> Bool])))
    (ASeq (I [[(U (Seqable Any) Counted nil) -> Bool] -> Any] (Not (Option (clojure.lang.Seqable [(U nil (Seqable Any) clojure.lang.Counted) -> Bool])))))
    (ASeq [[(U (Seqable Any) Counted nil) -> Bool] -> Any])

ExceptionInfo Type Checker: Found 1 error  clojure.core/ex-info (core.clj:4566)

original function:

(defn first-two [player]
  (let [couples (concat adjacents opposite-corners opposite-sides)]
    (first (filter #(= (count %) 2)
                   (for [pair couples]
                     (clojure.set/intersection pair @player))))))

Answer 1

You can provide types elsewhere to avoid instantiating filter.

For example, this type checks.

(ns typed-test.core
  (:refer-clojure :exclude [fn for])
  (:require [clojure.core.typed :as t
             :refer [fn for Vec Coll Any Num]]))

(filter (fn [a :- (Coll Any)] (= (count a) 2))
        (for [pair :- (Vec Num), {1 2 3 4}] 
          :- (Vec Num)
          pair))

Perhaps missing the return type for the call to for was losing too much information.

inst simply replaces the type variables in an All binder with some types.

typed-test.core=> (cf identity)
(t/All [x] [x -> x :filters {:then (! (t/U nil false) 0), :else (is (t/U nil false) 0)} :object {:id 0}])
typed-test.core=> (cf (t/inst identity Num))
[Num -> Num :filters {:then (! (t/U nil false) 0), :else (is (t/U nil false) 0)} :object {:id 0}]

Answer 2

Just a quick idea since I don't have time to check for you right now.

But generally polymorphic type parameters in typed clojure do not map directly to the parameters. With a quick glance I think that's the origin of your problem.

For instance suppose we define a polymorphic fun and we want to instantiate it.

(ann f (All [x] [[x -> Bool] x -> Integer]))
(defn f [predicate? value] (if (f value) 1 0))

To correctly instantiate it you would have to go like that

((inst f String) (typed/fn [x :- String] :- Bool true) "lol")

and not

((inst f [String -> Bool]) (typed/fn [x :- String] :- Bool true) "lol2") ;; baaaad baaaad

Now I have to go back to work t_t spent too much time customizing my emacs today ahah...