Is there a way to remove an instance?

Stream: Is there code for X?

[Freek Wiedijk]

I would like n - m not to work for natural numbers (so when I write that, then n and m would be coerced to integers first, and the subtraction would be on the integers). I guess for that I'd need to remove an instance of a type class? So is that possible, and if so, how do I do that?

[Matthew Ballard]

instance (priority := high) foo : HSub Nat Nat Int where
  hSub n m := n - m

seems to work for me without removing docs#instSubNat

[Adam Topaz]

attribute [-instance] instSubNat

#eval (1 : Nat) - 3
/-
failed to synthesize instance
  HSub Nat Nat ?m.42
-/

[Adam Topaz]

But this would make things quite inconvenient.

[Matthew Ballard]

Adam actually answers the question lol.

Note this removal is local to the file whereas the high priority hetero sub persists

[Kyle Miller]

That heterogenous instance might interact poorly with expression elaboration (i.e., binop%), so if you use it just be on the lookout for weird results (and please let me know).