Typed Clojure tries to pick up bad arguments to Name's at parse time. This way we get errors early for badly formed types.
This gets problematic with recursive and mutually recursive definitions of protocols and datatypes, especially with type bounds.
This can be broken down into several issues.
We always want to simplify unions at parse time. This is complementary to the decision to resolve all Name applications early to check for badly formed types. If we are able to do the latter, the former should at least be attempted.
Consider this protocol, which includes a self-reference as part of a union.
(ann-protocol SelfProtocol f1 [SelfProtocol -> (U nil SelfProtocol)]) (defprotocol> SelfProtocol (f1 [this]))
This is a protocol called SelfProtocol that defines a method f1, annotated as [SelfProtocol -> (U nil SelfProtocol)].
The code (U nil SelfProtocol) actually simplifies to itself, however to calculate this, we need to compute:
To avoid special-casing this "self reference" case, we might construct a dummy Protocol (internal) type, with information on:
This is simple with unparameterised protocols (we just need the name)
The things we don't need are:
Another interesting point: what if SelfProtocol is extended to nil here? Then the union would simplify to just nil (because nil <: SelfProtocol and SelfProtocol <!: nil).
We need to know this ancestral information at point the protocol is parsed! So we also want to know:
We identified above that we need to know information about Protocol type bounds at parse time. This is again for earlier errors.
Consider this minimal case.
(ann-protocol [[f :variance :covariant :< (HOProtocol f)]] HOProtocol)
HOProtocol is has one type parameter, which is bound by (HOProtocol f). That is, (HOProtocol T) for some type T where Nothing <: T <: (HOProtocol T).
eg. If nil extends (HOProtocol nil), then (HOProtocol nil) is a valid instantiation of HOProtocol, because Nothing <: nil <: (HOProtocol nil).
What are the steps to checking the upper bound is well formed?