Expansion on singular slice of a singular slice yields a malformed diagram

[jamievicary]

In the attached workspace, navigate to S0, then drag the vertex to the right. The result is a malformed diagram, in the sense that the rewrites in the diagram don't form commuting squares appropriately.

filename_todo (38).zip

[zrho]

90f526137790816ee44bbfb6ed7eb2c95fadd090 fixes a bug in typechecking that made it overlook some invalid diagrams when scalars were involved. Tested locally the problem described in this issue doesn't occur anymore; can you confirm this once the CI is done publishing it?

[jamievicary]

Lukas, does typechecking actually check whether the rewrites are valid in the sense of commuting squares. It would seem reasonable to me that typechecking should not verify this, as it should be guaranteed by all rewrite construction methods in the first place.

[zrho]

It does not check commuting squares explicitly. It just checks that a diagram decomposes into subdiagrams that normalise to the appropriate diagram in the signature.

[jamievicary]

OK, that's what we thought, and I agree that's sensible. The point is that type checking should be able to assume that all these squares do indeed commute, so when fed an invalid example, such as this one, we don't care much about its behaviour. It's great that you identified this bug, however.

[jamievicary]

Something that we thought today is that maybe this non-commutativity issue underlies some of these major issues Hao has identified. That could explain why it has been hard for you to debug, because you may not have considered the possibility that certain squares didn't commute, perhaps yielding undefined behaviour. Could that be a possibility? I think Nick is writing a "deep commutativity checker" to investigate this.

[calintat]

I tested the example again with Lukas' PR and it still produces a malformed diagram. The problem must be with the expansion code.

[calintat]

This was fixed by #150.