instance loop?

Stream: general

[Reid Barton]

I made an instance instance normal_of_compact_t2 [topological_space α] [t2_space α] [compact_space α] : normal_space α where normal_space extends t2_space. Apparently this was a bad idea because Lean now thinks that the way it should try to prove a space is T2 is to use normal_space.to_t2_space and use this instance to reduce the problem to showing the space is T2 and compact...

[Reid Barton]

Is there a way to work around this kind of issue? Or do I just not get to write the instance normal_of_compact_t2?

[Reid Barton]

I would have hoped that maybe Lean wouldn't try to solve a goal which is the same as one it was trying to solve higher up in the recursion

[Reid Barton]

Concretely the issue is that there's also another class regular_space which extends t2_space, and Lean is unable to see that a regular_space is T2 because it falls into this loop instead

[Sebastian Ullrich]

That would be a relatively expensive check. And of course not sufficient to prevent all loops

[Reid Barton]

Doesn't Lean already have some kind of cache it checks for instances in, so couldn't it insert constraints that are in the process of being solved as "gray" nodes in the cache?

[Reid Barton]

I guess it would still be somewhat expensive

[Reid Barton]

What's the general restriction here? If I have class B which extends class A, I can't write an instance which says that A + something else gives me B?

[Reid Barton]

I'm a little confused because somehow I was under the impression that there were actually lots of instance loops and somehow the class inference engine was able to handle them