Fix #7643: coverage: handle blocked sort in isFibrant

[andreasabel]

Fix #7643: coverage: handle blocked sort in isFibrant
WAS: uncaught pattern violation.
NOW: default to non-fibrant.

[jespercockx]

Is defaulting the right thing to do here? In general, defaulting rules tend to make the result of elaboration dependent on the order in which constraints are solved and can result in brittle code as a result. As an alternative, we could add a constraint for postponing the call to checkCoverage so it could be retried once the fibrancy check is no longer blocked.

[andreasabel]

Yeah I guess one could be more careful here.

isFib <- fromRight (const False) <$> lift (isFibrant' t)
...
if isFib && (isHIT || not (null ixs)) && not (null mns) && inserttrailing == DoInsertTrailing
                   then computeHCompSplit delta1 n delta2 d pars ixs x tel ps cps

If we want to block on isFibrant' t we should make sure we only do it when we really want to computeHCompSplit, so, only if all the other conjuncts are true.
My current (lazy) solution is restorative for non-cubical stuff, but maybe a bit anti-Cubical.
In this regression-fix I didn't want to go full circle with a pattern-violation catching mechanism that the coverage checker does not seem to have yet, but I am open to move systematic solution.