## Stream: lean4

### Topic: mathport:instExpected

#### Daniel Selsam (Mar 20 2021 at 22:40):

instExpected means a subgoal encountered during search is not known to be a class (since currently lean4 only unfolds reducibles in this context)

@Mario Carneiro do you want to backport this change or just add the one-character patch (one whnf becomes a whnfD) to the fork? The possible downside of the patch is that one might prefer a fast error rather than try whnfD, which could be expensive.

#### Mario Carneiro (Mar 20 2021 at 22:41):

I'm not sure what the source of these errors is. Do you have an example?

#### Mario Carneiro (Mar 20 2021 at 22:42):

it seems odd that typeclass inference would involve an expression that isn't manifestly a class

#### Mario Carneiro (Mar 20 2021 at 22:42):

unless we're talking about things like decidable_eq, but those should be reducible

#### Mario Carneiro (Mar 20 2021 at 22:43):

it's possible that there are some pi classes in category theory that are only semireducible, but the @[class] def PR changed them all to newtyped classes

#### Daniel Selsam (Mar 20 2021 at 22:45):

This is related to the @[class] def issue (https://github.com/dselsam/mathport/issues/4#issuecomment-771347723). I know you backported some changes but I didn't know if you finished. I will double-check what caused the error.

#### Daniel Selsam (Mar 20 2021 at 22:53):

Here is one of the instExpected errors: category_theory.limits.has_finite_products C

#### Daniel Selsam (Mar 20 2021 at 22:58):

FWIW I think I do prefer the lean4 behavior of requiring these be reducible. I am only raising the possibility of a patch, not suggesting it. It depends on (a) how expensive the backport is, and (b) which behavior most people actually prefer.

#### Mario Carneiro (Mar 20 2021 at 23:03):

I don't think there is any good reason to support semireducible pi classes

Last updated: May 18 2021 at 22:15 UTC