When programming with GHC's type-level natural numbers and `KnownNat` constraints, how can one construct *evidence* of the result of comparisons to be used in further computations? For instance, we might define a type for augmenting the results of `compare` with evidence:
> data CompareEv u v
> = (u < v) => CompareLT
> | (u ~ v) => CompareEQ
> | (u > v) => CompareGT
Then I'd like to define a comparison operation (to be used with `AllowAmbiguousTypes` and `TypeApplications`, alternatively taking proxy arguments):
> compareEv :: (KnownNat m, KnownNat n) => CompareEv u v
With `compareEv`, we can bring evidence into scope in `case` expressions.
I don't know how to implement `compareEv`. The following attempt fails to type-check, since `compare` doesn't produce evidence (which is the motivation for `compareEv` over `compare`):
> compareEv = case natVal (Proxy @ u) `compare` natVal (Proxy @ v) of
> LT -> CompareLT
> EQ -> CompareEQ
> GT -> CompareGT
Can `compareEv` be implemented in GHC Haskell? Is there already an implementation of something similar? Any other advice?
Thanks, -- Conal