Typed Clojure is an optional type system for Clojure, implemented as an external compiler pass manually triggered by the programmer. This way, Typed Clojure is rather limited, being unable to interact with the normal compilation process despite being able to infer program optimisations. The goal of "gradual typing" also address the issue of interlanguage communication. Currently, any code that is not checked by the type checker is assigned a trusted type by the programmer. This effectively means whenever a Typed Clojure program calls normal Clojure or vice-versa, there is an opportunity to break static invariants assumed by the type checker.
There are several challenges to address to design a satisfying gradual type system for Clojure. Datatypes in Clojure are implemented as public, final and effectively immutable Java classes. The classic approach of proxying is not as useful fields are immutable, so contracts can be implemented as either flat checks or cloning. Creating a proxy for a datatype is actually impossible without redefining the class because java.lang.proxy can only proxy non-final classes. It is also probably useful to be able to intercept method calls to untyped datatypes we have assigned static types to, because their implementation cannot be checked statically. Usually a proxy is used for this purpose, but the aforementioned technical issues may force us to insert checks around such method calls in typed code. We do not want to redundantly check statically-verified datatypes at runtime, so we will have to experiment with multiple approaches.
Choosing access privileges to be public is a common theme in Clojure, and it is impossible to define unaccessible global variables or classes. For example, global variables are implemented as "vars", mutable containers contained in a namespace. All of these concepts can be accessed and changed by foreign code. While this could break static invariants for gradual typing, these are important properties for development-time, so we feel we must assume foreign code does not maliciously redefine typed code (a standard assumption in other Clojure programming).
Multimethods in Clojure consist of a dispatch function and methods, which can be extended by anybody. There are several combinations of typed-untyped worlds we should be concerned with. For example, defining a multimethod in typed land has its definition and typed methods statically checked, but methods installed from untyped code must be protected by runtime contracts. Ideally, the runtime check should be confined to just the untyped method.
Typed Clojure is pessimistic enough in its Java interoperability to prevent null-pointer exceptions in typed code. However, it also exposes ways to override the default assumptions of a method, like non-nil-return which assumes a method cannot return nil. We have an opportunity to actually check this assumption.