Suppose instead that we define a basic + operation which always operates on two values:
(def base-+ (a b)
(...))
Then we simply define + as:
(def + rest
(reduce base-+ (car rest) (cdr rest)))
(def reduce (f z l)
(if l
(reduce f (f z (car l)) (cdr l))
z))
Then, instead of redefining +, we add a rule: if you want your new type to have a + operation and still be optimizable by arco, then redefine base-+, not +
Then we can make type inferences based simply on pairs of values.