Let-aliased variables of plain Map lookups should update original map

Problem

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.

(fn [m :- (Map Any Str)] :- String
  (let [e (:foo m)]
    (if e e "asdf")))
;;        ^
;;  Expected Str, actual (U nil Str)

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)).

Solution

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.,

(fn [a :- Any] (:foo a))

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

G |- e : t ; v+ | v- ; o}}, where G |- p and p |- e || v, that o = empty, or p(o) = v.

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

(fn [a :- Any] (:foo a))

that means two invocations of

((fn [a :- Any] (:foo a)) m)

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
might read:

G |- e : t ; v+ | v- ; o}}, where G |- p and p |- e || v, that o = empty, or if serious(o) then p(o) = v.

More information

Discussion here: https://groups.google.com/d/msg/clojure-core-typed/WO8dpY63N2Q/7UWBViNiIYEJ

git bisect code

(do (require '[clojure.core.typed :as t]) (t/cf (t/fn [m :- (t/Map t/Kw String)] :- String (or (:foo m) "asdf"))))

This stopped type checking after https://github.com/clojure/core.typed/commit/9608027bfaf4be268cfa12486c5ae6615d8517f1

bisect result:

9608027bfaf4be268cfa12486c5ae6615d8517f1 is the first bad commit
commit 9608027bfaf4be268cfa12486c5ae6615d8517f1
Author: Ambrose Bonnaire-Sergeant <...@gmail.com>
Date: Sat Jan 3 00:05:23 2015 +0000

enable aliasing support

Pull request:

• CTYP-241
• Rebased
  • Waiting on
    • CTYP-255

Patch:
Commmit:
Release: