core.typed 0.2.77 - Verified RBT `restore-right` rebalancing

[Ambrose Bonnaire-Sergeant]

Hi,

[org.clojure/core.typed "0.2.77"]

A combination of let-aliasing and various other occurrence typing optimisations means we can verify the rebalancing invariants of this restore-right implementation.

To get an idea how hard this problem is, this is the type inferred for the "unbalanced" RB tree in the last branch (notice it's actually inferred to be balanced, so it's safe to just return it!).

Try it out! check-ns takes about 9 seconds and you'll see a couple of type errors in `ins1`, which is the next challenge: dependent function types!

dblarons also reported an issue on IRC yesterday which I've fixed. Symptom: the user gets useless type-parsing errors for no apparent reason.

README

CHANGELOG

Thanks,

Ambrose