Zulip Chat Archive

Stream: lean4

Topic: Failed to show type is inhabited


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 04 2021 at 05:45):

Construct an instance instance inhabited T := ...

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: May 07 2021 at 12:15 UTC