Fixing arguments without triggering type class inference

Stream: lean4

[Markus Schmaus]

In the following example doNothing and doNothing' work perfectly fine. doNothing' is just doNothing with α fixed to Nat. But when I try to define doNothing'' by fixing α to Nat, this triggers type class inference and Lean throws an error. Is it possible to define doNothing' in terms of doNothing without prematurely triggering type class inference?

def doNothing {α : Type u} {stream : Type v} [Stream stream α] (s : stream) : stream := s

#eval doNothing [1, 2, 3]

def doNothing' {stream : Type v} [Stream stream Nat] (s : stream) : stream := s

#eval doNothing' [1, 2, 3]

def doNothing'' := doNothing (α := Nat)

[Eric Rodriguez]

doNothing'' would need a parameter [Stream stream Nat], I think

[Markus Schmaus]

This wasn't what I meant. Let me try to be more precise.

How can I define doNothing'' in terms of doNothing, such that it has the same type signature as doNothing'?

[Mauricio Collares]

def doNothing'' := @doNothing (α := Nat)