Zulip Chat Archive

Stream: lean4

Topic: Failed to show type is inhabited


Calvin Lee (Feb 04 2021 at 05:41):

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 (Feb 04 2021 at 05:45):

Construct an instance instance inhabited T := ...

Calvin Lee (Feb 04 2021 at 05:51):

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 (Feb 04 2021 at 06:05):

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 (Feb 04 2021 at 06:05):

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

Mario Carneiro (Feb 04 2021 at 06:07):

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


Last updated: Dec 20 2023 at 11:08 UTC