how to remove instance from current scope / disable

Stream: lean4

[Serhii Khoma (srghma)]

How to remove instance from scope?

class MyClass (α : Type) where
  foo : α → String

instance : MyClass Nat where
  foo n := toString n

-- should work here:
def test1 : String := MyClass.foo 42  -- uses the instance automatically

section
-- Now I want to remove it. Is there something like this to prevent Lean from using any instance of MyClass
-- variable [!MyClass Nat]

def test2 : String := MyClass.foo 42  -- ❌ should fail to compile
end

-- should work here too:
def test3 : String := MyClass.foo 42  -- uses the instance automatically

---

more concrete example

we have function

def close (ch : CloseableChannel α) : EIO Error Unit :=
  match ch with
  | .unbounded ch => CloseableChannel.Unbounded.close ch
  | .zero ch => CloseableChannel.Zero.close ch
  | .bounded ch => CloseableChannel.Bounded.close ch

and for example both

example (ch : Std.CloseableChannel o): EIO Std.CloseableChannel.Error Nat := do
  Std.CloseableChannel.close ch
  pure 1

example (ch : Std.CloseableChannel o): IO Nat := do
  Std.CloseableChannel.close ch # implicit conversion
  pure 1

are valid because of

instance : MonadLift (EIO Error) IO where
  monadLift x := EIO.toIO (.userError <| toString ·) x

but lets suppose I make a function def foo: IO (Except Std.CloseableChannel.Error Unit)that tries to handle all Std.CloseableChannel.Error in pure way

and I want to disable this instance Std.CloseableChannel.Error to Error to doublecheck myself that I have catched all such cases

how to do this? is there a way do disable instance altogether? e.g. variable [!MonadLift (EIO Error) IO] doesnt work

[Robin Arnez]

attribute [-instance] instMyClassNat

[Serhii Khoma (srghma)]

and for second example attribute [-instance] Std.CloseableChannel.instMonadLiftEIOErrorIO. Understand now, tnx!