Let-aliasing means we completely rely on the original binding's
type to find the type for locals derived from lookups on it. If
occurrence typing doesn't update the original binding, then even
very simple control flow does not register.
For example, in core.typed 0.3.7, the following code registers
e as an alias of (Key :foo)m.
e contains the correct propositions and object, however
update ignores propositions that update non-HMap types.
So in the test position, m is still of type (Map Any Str), which means path-type
infers Any for its aliased object (above). (Note: path-type should infer slightly better
types here, eg., this should return (U nil Str)).
The update case for keyword invocations on non-HMaps
need to intersect its known HMap type.
We now make it an error to assign an object to the result of looking up
a possibly-mutable map. ie.,
has no object.
Correspondingly, update will throw an error if told to update via a keyword lookup
on a map type that is not a subtype of (U nil (Map Any Any)).
We cannot have objects that might be wrong — the formalism asserts that in
That means looking up an object o of an expression e must always
result in exactly its evaluation v. If we gave an object to
that means two invocations of
must return exactly the same value — for a mutable m this is clearly false.
Interestingly, this has worked fine in practice until let-aliasing, by compensating
in the update function. We basically only update types that are immutable, checked
at the last minute in update.
Briefly, to handle this idea of "temporarily fake" objects, we probably need a predicate to validate
whether an object should be taken "seriously" as an actual, immutable, path. Then the formalism
This stopped type checking after https://github.com/clojure/core.typed/commit/9608027bfaf4be268cfa12486c5ae6615d8517f1
9608027bfaf4be268cfa12486c5ae6615d8517f1 is the first bad commit
Author: Ambrose Bonnaire-Sergeant <...@gmail.com>
Date: Sat Jan 3 00:05:23 2015 +0000
enable aliasing support