core.typed not reporting type error in repl

Question

Here is a part of the example taken from core.typed github repo:

(ns typedclj.rps-async
  (:require [clojure.core.typed :as t]
            [clojure.core.async :as a]
            [clojure.core.typed.async :as ta]))

(t/defalias Move
  "A legal move in rock-paper-scissors"
  (t/U ':rock ':paper ':scissors))

(t/defalias PlayerName
  "A player's name in rock-paper-scissors"
  t/Str)

(t/defalias PlayerMove
  "A move in rock-paper-scissors. A Tuple of player name and move"
  '[PlayerName Move])

(t/defalias RPSResult
  "The result of a rock-paper-scissors match.
  A 3 place vector of the two player moves, and the winner"
  '[PlayerMove PlayerMove PlayerName])

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Implementation
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(t/ann MOVES (t/Vec Move))
(def MOVES [:rock :paper :scissors])

(t/ann BEATS (t/Map Move Move))
(def BEATS {:rock :scissors, :paper :rock, :scissors :paper})
(def BEATS {:a :b})

Note that in the last line I redefined BEATS to {:a :b}, which conflicts its type annotation, but when I eval this in the repl, no error is thrown. I was expecting an error because the latest version of core.typed is said to be able to report type errors at the runtime.

Here is the entire project.clj file:

            (defproject typedclj "0.1.0-SNAPSHOT"
                        :description "FIXME: write description"
                        :url "http://example.com/FIXME"
                        :license {:name "Eclipse Public License"
                                  :url  "http://www.eclipse.org/legal/epl-v10.html"}
                        :dependencies [[org.clojure/clojure "1.6.0"]
                                       [org.clojure/core.async "0.1.346.0-17112a-alpha" :exclusions [org.clojure/tools.analyzer.jvm]]
                                       [org.clojure/core.typed "0.2.92"]
                                       [clj-http "1.1.2"]
                                       [http-kit "2.1.18"]
                                       ]
                        :repl-options {:nrepl-middleware [clojure.core.typed.repl/wrap-clj-repl]}
                        :main ^:skip-aot typedclj.core
                        :target-path "target/%s"
                        :profiles {:uberjar {:aot :all}})

---

With core.typed 0.3.0-alpha2 this type error is nicely catched:

Type Error (/private/var/folders/5d/44ctbbln4dsflgzxph1dm8wr0000gn/T/form-init3488589171262628870.clj:36:12) Type mismatch:

Expected:   typedclj.rps-async/Move

Actual:     (t/Val :b)
in: :b


Type Error (/Users/kaiyin/personal_config_bin_files/workspace/typedclj/src/typedclj/rps_async.clj:36:12) Type mismatch:

Expected:   (t/Map typedclj.rps-async/Move typedclj.rps-async/Move)

Actual:     (t/HMap :mandatory {:a typedclj.rps-async/Move} :complete? true)
in: {:a :b}

Answer 1

You need to explicitly opt-in to implicit type checking. Change your ns form like so:

(ns ^:core.typed typedclj.rps-async
   ...)

Answer 2

Yes, it does report errors at runtime when you explicitly ask it to do so. This is slightly different from statically typed languages, where a type error prevents the program from building successfully – it's just an optional "sanity check" here.

Type checking is separate to compilation and must be explicitly run

Use clojure.core.typed/check-ns to type check the current namespace. This can be done at the REPL.

Note: Global annotations like ann are only valid when found in a namespace currently being checked with check-ns, or wrapped in a cf. raw ann in a REPL has no effect. Global annotations should be top-level forms or inside a (possibly nested) top-level do.

— clojure.typed Quick Guide

In REPL, you should wrap your expressions in cf, so that types are inferred from the given code and printed out. (see this blog post) If you want to type-check code from a namespace defined in source files, use check-ns to type-check the entire namespace.