19 Jui
2023
19 Jui
'23
20:12
So we have to keep the `f` argument of `Eq_eq` as non-erased, indeed!!
Actually, that's not quite true: we can get the runtime info needed for `Eq.uneq` to return the proper function either from the `Eq.eq` object (like you have currently), or from the `x` and `y` args passed to `Eq.uneq`.
IOW, we could make all `Eq.eq` arguments erasable, and instead make the `x` and `y` args to `Eq.uneq` non-erasable.
My first reaction to seeing `Eq.eq` take a non-erasable arg was one of horror, but after thinking some more about it, it's probably not that bad: it's still a "singleton type" (i.e. compatible with axiom K), so we can still make the proof passed to `Eq.cast` erasable, and equality proofs themselves are still almost universally erasable.
Stefan