Consider this definition:
h : Nat -> Nat -> Nat
h x y = case 1 `isLTE` x of
(Yes prf) => case 1 `isLTE` y of
(Yes prf') => (x - 1) * 2 + (y - 1)
(No contra) => ?sr_3
(No contra) => ?h_2
As innocent as it looks, it would not type check.
|
14 | (Yes prf') => (x - 1) * 2 + (y - 1)
| ^
...
When checking an application of function Prelude.Interfaces.-:
Type mismatch between
Nat (Type of y)
and
LTE 1 x (Expected type)
For some reason, it cannot locate the right prf. (Or is there something else going on?) For some reason again, this error, while appearing in the second summand, can be fixed by annotating the minus in the first. This compiles:
h : Nat -> Nat -> Nat
h x y = case 1 `isLTE` x of
(Yes prf) => case 1 `isLTE` y of
(Yes prf') => ((-) {smaller = prf} x 1) * 2 + (y - 1)
(No contra) => ?sr_3
-, without converting them to prefix form (-)?What is happening?
This seems to be a bug in the unification, I guess. It should be able to infer everything correctly, but for the system it's apparently not clear which type you want to use. +, * are both Num a => a -> a -> a, and - even has two definitions; one with Nat and the proof, the other also in the Num format. So whenever there seems to be strange type mismatches, just clarify the types. (x - 1) * 2 `plus` (y - 1) also works out.
How can I express this logic better?
You can join up both case statements:
g x y = case (1 `isLTE` x, 1 `isLTE` y) of
(Yes lte1x, Yes lte1y) => (x - 1) * 2 `plus` (y - 1)
_ => ?h
Even better, if you only need to subtract one, just do it via pattern matching:
i (S x) (S y) = x * 2 + y
i x y = ?h
Also, Nat is not always good for computation; it is better fitted for structural info for the type system (like in Vect Nat a). If you plan to do something like x - 321 * y + 100 and do not need the result in a type, just drop to Integer for performance reasons.
Can I supply implicit arguments to infix operators, such as -, without converting them to prefix form (-)?
Nope!