## Stream: Is there code for X?

### Topic: condition on type class

#### Chase Norman (Jan 30 2021 at 21:49):

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 (Jan 30 2021 at 21:57):

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

#### Reid Barton (Jan 30 2021 at 22:33):

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 (Jan 30 2021 at 22:41):

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 (Jan 30 2021 at 22:42):

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

Last updated: May 16 2021 at 05:21 UTC