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
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,
Thanks for your help.
Eric Wieser (Jan 30 2021 at 21:57):
∃ [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