Zulip Chat Archive

Stream: Is there code for X?

Topic: condition on type class

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

view this post on Zulip Eric Wieser (Jan 30 2021 at 21:57):

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

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

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

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