public class Int0Demo {

  sealed interface Int0 {}
  record Z() implements Int0 {}
  record NZ(int n) implements Int0 {
    NZ { if (n == 0) throw new IllegalArgumentException("NZ can't be zero"); }
  }

  static Int0 i(int n) {
    if (n == 0) {
      return new Z();
    } else {
      return new NZ(n);
    }
  }

  static Int0 add(Int0 n1, Int0 n2) {
    return switch (n1) {
      case Z() -> switch (n2) {
        case Z() -> new Z();
        case NZ(int b) -> new NZ(b);
      };
      case NZ(int a) -> switch (n2) {
        case Z() -> new NZ(a);
        case NZ(int b) -> i(a + b);
      };
    };
  }

  static Int0 div(Int0 n1, NZ n2) {
    return switch (n1) {
      case Z() -> new Z();
      case NZ(int a) -> i(a / n2.n());
    };
  }

  static void check(Object actual, Object expected) {
    System.out.println((actual.equals(expected) ? "ok: " : "FAIL: ") + actual);
  }

  static void checkRaises(Runnable r, String msg) {
    try {
      r.run();
      System.out.println("FAIL: no exception");
    } catch (RuntimeException e) {
      System.out.println((msg.equals(e.getMessage()) ? "ok: " : "FAIL: ") + e.getMessage());
    }
  }

  public static void main(String[] args) {
    check(add(new NZ(5), new NZ(3)), new NZ(8));
    check(add(new NZ(5), new Z()), new NZ(5));
    check(add(new Z(), new Z()), new Z());
    check(add(new NZ(5), new NZ(-5)), new Z());

    check(div(new NZ(10), new NZ(2)), new NZ(5));
    check(div(new NZ(1), new NZ(2)), new Z());
    checkRaises(() -> div(new NZ(10), new NZ(0)), "NZ can't be zero");      // compiles; throws at runtime

    // type error
    // check(div(new NZ(10), new Z()), new NZ(5));
    // type error, sum is 2
    // check(div(new NZ(10), add(new NZ(1), new NZ(1))), new NZ(5));
    // type error, sum is 0
    // check(div(new NZ(10), add(new NZ(1), new NZ(-1))), new NZ(5));
    // type error
    // check(div(new NZ(10), i(0)), new NZ(5));
    // runs, but requires a dynamic cast
    // check(div(new NZ(10), (NZ) add(new NZ(1), new NZ(1))), new NZ(5));
    // dynamic downcast error
    // check(div(new NZ(10), (NZ) add(new NZ(1), new NZ(-1))), new NZ(5));
  }
}