"Unable to build a covering": how to trace down?

[xuanruiqi]

I have some Agda code that I want to transcribe into Equation, but it doesn't quite work. The code is here, and the problematic definition is balright. Specifically, I get the following error message:

Unable to build a covering for:
balright d cl cr c l v r valid_l valid_r

I suppose this means I am missing cases, but there is no indication of what cases are missing, so that I can add the appropriate impossible clauses.

Are there any pointers to how to begin?

[mattam82]

It might help to use Set Equations Debug to trace where/why covering fails.

[mattam82]

Could you make a smaller example without CpdtTactics?

[xuanruiqi]

Sure. It is here.