type checker hangs when checking symmetric monoidal category associator

[marcosh]

at the moment the associator does not work for some mysterious reason. Find out why and fix it

• issue on idris-lang #4690

[marcosh]

At the moment the definition of SymmetricMonoidalCategory is incomplete. As you can see here there is still a hole where the associator should go.

Trying to replace the hole with (associator monoidalCategory), which should be the correct value, the type checker gets stuck and gets killed after a while.

If you want to debug the issue, you can find the logs of the type checker with various levels of logging here

[marcosh]

now you can find a simplified version of the code, which still does not work, on the branch https://github.com/statebox/idris-ct/tree/simplify-smc-context

[wires]

I edited the description and added a link to the idris-lang issue