Exploit proof-irrelevance when lowering

[mvr]

WIP for exploiting proof-irrelevance when lowering. This isn't hooked into the TypeScript FFI at all currently.

The basic-ir tests have a lot of instances where the result changes (for the better). In the monoid example, the tables for the equations disappear and become rules that assert those equalities directly.

Before:

flatrealm
  entities
    table ℜ.car := []
    table ℜ.unit := [.a : ℜ.car] primarykey []
    table ℜ.mul := [.a : ℜ.car, .b : ℜ.car, .c : ℜ.car] primarykey [.a, .b]
    table ℜ.mul/unitl := [.x : ℜ.car] primarykey [.x]
    table ℜ.mul/unitr := [.x : ℜ.car] primarykey [.x]
    table ℜ.mul/assoc := [.x : ℜ.car, .y : ℜ.car, .z : ℜ.car] primarykey [
      .x,
      .y,
      .z
    ]
  end
  rules
    enforced ℜ.car.foreignKey := ℜ.car [] ⊢ ⊤
    enforced ℜ.unit.foreignKey a := ℜ.unit [.a ↦ a] ⊢ a ∈ ℜ.car []
    monitored ℜ.unit.total := ⊤ ⊢ ℜ.unit []
    enforced ℜ.mul.foreignKey a b c := ℜ.mul [
      .a ↦ a,
      .b ↦ b,
      .c ↦ c
    ] ⊢ a ∈ ℜ.car [] ∧ b ∈ ℜ.car [] ∧ c ∈ ℜ.car []
    monitored ℜ.mul.total a b := a ∈ ℜ.car [] ∧ b ∈ ℜ.car [] ⊢ ℜ.mul [
      .a ↦ a,
      .b ↦ b
    ]
    enforced ℜ.mul/unitl.foreignKey x a.lhs a.lhs.a := ℜ.mul/unitl [
      .x ↦ x
    ] ∧ ℜ.unit [.a ↦ a.lhs.a] ∧ ℜ.mul [
      .a ↦ a.lhs.a,
      .b ↦ x,
      .c ↦ a.lhs
    ] ⊢ x ∈ ℜ.car [] ∧ a.lhs = x
    monitored ℜ.mul/unitl.total x := x ∈ ℜ.car [] ⊢ ℜ.mul/unitl [.x ↦ x]
    enforced ℜ.mul/unitr.foreignKey x a.lhs a.lhs.b := ℜ.mul/unitr [
      .x ↦ x
    ] ∧ ℜ.unit [.a ↦ a.lhs.b] ∧ ℜ.mul [
      .a ↦ x,
      .b ↦ a.lhs.b,
      .c ↦ a.lhs
    ] ⊢ x ∈ ℜ.car [] ∧ a.lhs = x
    monitored ℜ.mul/unitr.total x := x ∈ ℜ.car [] ⊢ ℜ.mul/unitr [.x ↦ x]
    enforced ℜ.mul/assoc.foreignKey x y z a.lhs a.lhs.a a.rhs a.rhs.b := ℜ.mul/assoc [
      .x ↦ x,
      .y ↦ y,
      .z ↦ z
    ] ∧ ℜ.mul [.a ↦ x, .b ↦ y, .c ↦ a.lhs.a] ∧ ℜ.mul [
      .a ↦ a.lhs.a,
      .b ↦ z,
      .c ↦ a.lhs
    ] ∧ ℜ.mul [.a ↦ y, .b ↦ z, .c ↦ a.rhs.b] ∧ ℜ.mul [
      .a ↦ x,
      .b ↦ a.rhs.b,
      .c ↦ a.rhs
    ] ⊢ x ∈ ℜ.car [] ∧ y ∈ ℜ.car [] ∧ z ∈ ℜ.car [] ∧ a.lhs = a.rhs
    monitored ℜ.mul/assoc.total x y z := x ∈ ℜ.car [] ∧ y ∈ ℜ.car [] ∧ z ∈ ℜ.car [] ⊢ ℜ.mul/assoc [
      .x ↦ x,
      .y ↦ y,
      .z ↦ z
    ]
  end
end

After:

flatrealm
  entities
    table ℜ.car := []
    table ℜ.unit := [.a : ℜ.car] primarykey []
    table ℜ.mul := [.a : ℜ.car, .b : ℜ.car, .c : ℜ.car] primarykey [.a, .b]
  end
  rules
    enforced ℜ.car.foreignKey := ℜ.car [] ⊢ ⊤
    enforced ℜ.unit.foreignKey a := ℜ.unit [.a ↦ a] ⊢ a ∈ ℜ.car []
    monitored ℜ.unit.total := ⊤ ⊢ ℜ.unit []
    enforced ℜ.mul.foreignKey a b c := ℜ.mul [
      .a ↦ a,
      .b ↦ b,
      .c ↦ c
    ] ⊢ a ∈ ℜ.car [] ∧ b ∈ ℜ.car [] ∧ c ∈ ℜ.car []
    monitored ℜ.mul.total a b := a ∈ ℜ.car [] ∧ b ∈ ℜ.car [] ⊢ ℜ.mul [
      .a ↦ a,
      .b ↦ b
    ]
    monitored ℜ.mul/unitl x a.lhs a.lhs.a := x ∈ ℜ.car [] ∧ ℜ.unit [
      .a ↦ a.lhs.a
    ] ∧ ℜ.mul [.a ↦ a.lhs.a, .b ↦ x, .c ↦ a.lhs] ⊢ a.lhs = x
    monitored ℜ.mul/unitr x a.lhs a.lhs.b := x ∈ ℜ.car [] ∧ ℜ.unit [
      .a ↦ a.lhs.b
    ] ∧ ℜ.mul [.a ↦ x, .b ↦ a.lhs.b, .c ↦ a.lhs] ⊢ a.lhs = x
    monitored ℜ.mul/assoc x y z a.lhs a.lhs.a a.rhs a.rhs.b := x ∈ ℜ.car [] ∧ y ∈ ℜ.car [] ∧ z ∈ ℜ.car [] ∧ ℜ.mul [
      .a ↦ x,
      .b ↦ y,
      .c ↦ a.lhs.a
    ] ∧ ℜ.mul [.a ↦ a.lhs.a, .b ↦ z, .c ↦ a.lhs] ∧ ℜ.mul [
      .a ↦ y,
      .b ↦ z,
      .c ↦ a.rhs.b
    ] ∧ ℜ.mul [.a ↦ x, .b ↦ a.rhs.b, .c ↦ a.rhs] ⊢ a.lhs = a.rhs
  end

Closes #13