Add a Flow/TypeScript bug around untagged union refinement

[wchargin]

If x: T | Box<T>, and x instanceof Box, it is not necessarily true that x: Box<T>, because T could itself be Box<U> for some U. This kills the crab.

I've always found this bug interesting because it's a great example of how endomorphisms (here, Box<_>) can be either your sharpest tool or your sharpest edge, depending on whether you understand their implications or even notice that they're there. Plus, it's Yet Another Untagged Union Bug, which might almost be cheating at this point.

wchargin-branch: polymorphic-union-refinement

[wchargin]

I ran make serve to build this on my machine, which works nicely except that the KaTeX isn't rendering for me, and neither are the TAGS: wired up. I'd appreciate if you could double-check my handiwork.

[samth]

Might be worth including a Typed Racket example, where this works correctly:

#lang typed/racket

(: f (All (T) (U T (Boxof T)) -> T))
(define (f x)
  (if (box? x)
      (unbox x) ;; type error here
      x))

[wchargin]

Ooh, of course; how could I forget my favorite refinement type system… Thanks! Added an example of both valid and invalid refinements in typed/racket.

[stedolan]

This is great, thanks!

The KaTeX and tags stuff requires node.js to be installed and available as /usr/bin/env node. Try:

echo '[{},{"sections":[]}]' | mdbook-katex/mdbook-katex

It should print {"sections":[]} if everything's working.

I've pushed a couple of small edits to this branch:

• more tags
• added a cross-ref from the runtime misinformation entry
• changed a use of "unsound" (type systems are sound/unsound, and programs work/crash, but it doesn't make sense to me to call a program unsound)

Also, I think this might be the same as an issue that showed up in Dotty?

[wchargin]

The KaTeX and tags stuff requires node.js to be installed and available as /usr/bin/env node.

Thanks; this all works as described.

I've pushed a couple of small edits to this branch:

All your edits look good to me (just nixed an unnecessary newline); thank you! Feel free to merge at your discretion/convenience.

Also, I think this might be the same as an issue that showed up in Dotty?

Yep, this definitely looks like the same thing, and fails in the same way when when transliterated into Flow. Feel free to add a reference if you think it appropriate.

[stedolan]

Merged, thanks! (https://counterexamples.org/polymorphic-union-refinement.html now exists)