Typeclass inference and priority

Stream: general

[Clément Blaudeau]

Hi everyone! I'm trying to override the arithmetic operations on Int32 with an addition that can fail on overflow. I've defined an instance of HAdd Int32 Int32 (MyOption Int32) where MyOption is a custom option monad. However, I cannot get the following to work :

inductive MyOption α -- simplified for the example
| some : α -> MyOption α
| none : MyOption α

instance (priority := low) : HAdd Int32 Int32 (MyOption Int32) where
  hAdd n m := if ... then .ok (n + m ) else .none

def x : Int32 := 3
def y : Int32 := 4

#check (x + y : Int32)
#check (x + y : MyOption Int32) -- error : type mismatch

Is there a way to use types to guide inference, so I can have + be the normal plus when used without annotations, and my custom HAdd instance when used with annotation ?
Sorry if a similar question was already answered somewhere, I could not find the answer reading the doc, and I'm still a Lean newbie.

[Aaron Liu]

no, this is not supported

[Aaron Liu]

For this to work the output of docs#HAdd would have to be a docs#semiOutParam

[Robin Arnez]

In the definition of HAdd, the result type is declared as an outParam. In other words, the result type needs to be uniquely determined by the input types. If this is not the case, weird stuff can occur. You might be able to solve this using a coercion:

instance : Coe α (MyOption α) := ⟨.some⟩

You can even be very specific:

instance : CoeDep Int32 (x + y) (MyOption Int32) := ⟨.some (x + y)⟩

[Clément Blaudeau]

Hum... Thank you for your answers! Alternatively, is there a way to write x + y (using the + notation) but specify the instance I want to use ?

[Robin Arnez]

No you can't use notation for this, you'd need #check (@HAdd.hAdd _ _ _  instHAddInt32MyOption x y : MyOption Int32); but don't; this will likely cause issues later. Coercions are probably a better solution

[Aaron Liu]

Coercions don't really work here though

[Clément Blaudeau]

Ok, that's unfortunate. Indeed coercions won't work here because the addition I want to define might return none. I've updated the code snippet of my original question to reflect that

[Robin Arnez]

Just to clarify, this doesn't work?

def MyOption.addInt32 (x y : Int32) : MyOption Int32 :=
  if (x + y).toInt = x.toInt + y.toInt then .some (x + y) else .none

instance : CoeDep Int32 (x + y) (MyOption Int32) := ⟨.addInt32 x y⟩

Then you could try scoped notation:

scoped infix:50 " + " => MyOption.addInt32

or just resort to function application

[Aaron Liu]

That looks terrible

[Robin Arnez]

Hmm you're right function application is probably your best solution

[Clément Blaudeau]

By function application, you mean dropping the notation ?

I would be fine with overriding the usual meaning of + with my own, and using Int32.add everywhere else, but the issue I have is that theorems like Int32.toBitVec_add stops working (hence, breaking bv_decide):

example (x y:Int32) : x = 41 -> y = 1 -> Int32.add x y = 42 := by
  simp [Int32.eq_iff_toBitVec_eq, Int32.toBitVec_add]
  bv_decide

(this worked without my custom instance and using +)

[Kyle Miller]

Aaron Liu said:

For this to work the output of docs#HAdd would have to be a docs#semiOutParam

Even if it were a semiOutParam, it wouldn't work because + uses the binop% elaborator, and that assumes that + wants to be homogeneous, with some support for heterogeneity in the inputs, not outputs.