Flow type-level naturals and addition

type-nat.js

// @flow

// Type-level naturals
type Zero = 0

interface Succ {
  <N>(N): [1, N]
}

// Hey look, we can do type-level pattern matching
// with function-variant interfaces
interface Pred {
  (Zero): Zero,
  <N>([1, N]): N
}

// Now we can get crazy and implement addition
interface Add {
  <N>(Zero, N): N,
  <N>(N, Zero): N,
  <N, M>(N, [1, M]): $Call<Add, [1, N], M>
}

type One = $Call<Succ, Zero>
type Two = $Call<Succ, One>
type Three = $Call<Add, One, Two>

type TwoMinus1 = $Call<Pred, Two>
type OneMinus1 = $Call<Pred, TwoMinus1>

// Let's construct some values to prove these types
let one: One = [1, 0]
let oneAlso: TwoMinus1 = one
let zeroAlso: OneMinus1 = 0
let three: Three = [1, [1, [1, 0]]]

For some reason, $Call<Add, One, Two> accepts anything other than Zero. I tried to fiddle with it but couldn't fix it. See a repro. If you replace one of the operands with Zero it fails as expected though.

Of course it's not a bug report, just an observation.

Yeah, I'm sure this is pushing flow's limits. I've run into several other situations, especially around $Call and union types, where inference breaks down, and flow starts accepting things it shouldn't.

Since it's not Flow's intended purpose, I'm almost sure it would get a wontfix if submitted as an issue. I'm considering getting in the codebase and sending fixes, but I'm not sure if it can be done since these kinds of errors don't really give confidence.