condition on type class

Stream: Is there code for X?

[Chase Norman]

I want to create a function that outputs a value dependent on a type class being satisfied, otherwise I want the function to output some default value. Here's a mwe:

def some_other_function (X : Type) [inhabited X] : Prop := sorry

def goal : Type → Prop := λ X, ∃ (f : inhabited X), some_other_function X

Ideally, f would be recognized as a type class instance, but instead we get the error failed to synthesize type class instance for inhabited X.

Is there any way I can create a function that is tolerant to types which don't satisfy the type class, so long as there is some default value (in this case, false)?

Thanks for your help.

[Eric Wieser]

Either ∃ [inhabited X], some_other_function X or ∃ [inhabited X], by exactI some_other_function X

[Reid Barton]

This is likely to be a bad idea but you could make a second type class containing an option (inhabited X) with two instances, one that uses an inhabited X and a low-priority catch-all instance

[Reid Barton]

The danger is that the catch-all instance might implicitly be selected when you weren't expecting it to, for example, if you forgot an [inhabited X] instance on an auxiliary function

[Reid Barton]

Actually I'm a bit confused because what you write doesn't seem to match your example very closely.