Failed to show type is inhabited

Stream: lean4

[Calvin Lee]

I'm getting an issue failed to compile partial definition, failed to show type is inhabited
However, I can create a proof that the type in question is inhabited. How do I get lean to compile my function?

[Mario Carneiro]

Construct an instance instance inhabited T := ...

[Calvin Lee]

Ah I think I see where I went wrong. This is somewhat odd. If I have the two functions

partial def unsafeFn1 {m} [Monad m] (a : α)  : m α :=
  unsafeFn1 a

partial def unsafeFn2 {m} (a : α) [Monad m] : m α :=
  unsafeFn2 a

Then the first is considered inhabited (because of pure) and the second is not. Furthermore, I'm not sure how to prove it is because I'd have to provide arguments to Inhabited in somewhat of an odd way.
My issue is that I wrote the definition the second way instead of the first way (however I wrote the inhabited proof the first way, so they wouldn't line up)

[Mario Carneiro]

When I try to compile that the first definition causes the compiler to loop and the server becomes unresponsive until I restart it

[Calvin Lee]

yes, that's another problem, but if you write it in a different (but still non-total way) it works

[Mario Carneiro]

Adding an inhabited instance such as

instance {m} : Inhabited ((a : α) → [Monad m] → m α) where
  default a := pure a

causes the second definition to work, at least until it hits the same loop as definition 1