Figure out why the CommRingSolver doesn't work in this case

[felixwellen]

When looking at the goal type in the case below, it is actually something the CommRingSolver should be able to solve. But when trying to solve this, the solver actually gets meta-variables it cannot use.

[felixwellen]

Here is another case, which might be related (or not):

[felixwellen]

When looking at the goal type in the case below, it is actually something the CommRingSolver should be able to solve. But when trying to solve this, the solver actually gets meta-variables it cannot use.

It seems like the marco gets only the type in the message below: So the task is to figure out how to use the reflection interface to tell agda to get more information on the type of the hole.

[ncfavier]

Links are more useful than screenshots: https://github.com/agda/cubical/pull/1093#discussion_r1476059816 https://github.com/agda/cubical/pull/1093#discussion_r1476066747

It looks like adding wait-for-type goal in solve!-macro does it.

[felixwellen]

Yes - it does! Many thanks!

[felixwellen]

1093 is merged and solves both problems -> closing.