You're totally right that there's a tradeoff here -- in Typed Racket, where we have strong types for the numeric tower plus the flexibility that the parent want

You're totally right that there's a tradeoff here -- in Typed Racket, where we have strong types for the numeric tower plus the flexibility that the parent wants, arithmetic isn't extensible. However, it's not the case that `data Number = ...` gets you everything. In particular, it gives up on the types! :) For example, in Typed Racket: -> (: norm : Real Real -> Real) -> (define (norm x y) (sqrt (+ (sqr x) (sqr y)))) -> (norm -3 12) - : Real 12.36931687685298 We've proved that the `norm` function always produces `Real` answers, even though `sqrt` might produce complex numbers given negative inputs. The sum type you've given won't let you prove that.