Zulip Chat Archive

Stream: general

Topic: instance loop?

Reid Barton (Oct 22 2018 at 18:20):

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 (Oct 22 2018 at 18:21):

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 (Oct 22 2018 at 18:22):

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 (Oct 22 2018 at 18:23):

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 (Oct 22 2018 at 18:23):

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

Reid Barton (Oct 22 2018 at 18:25):

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 (Oct 22 2018 at 18:26):

I guess it would still be somewhat expensive

Reid Barton (Oct 22 2018 at 18:31):

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 (Oct 22 2018 at 18:34):

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

Last updated: Dec 20 2023 at 11:08 UTC