search

frex-project / idris-frex

Other
46 stars 9 forks source link

[ fix ] Fix coverage issue #74

Closed dunhamsteve closed 1 month ago

dunhamsteve commented 1 month ago

The function MultHomomorphism currently relies on a bug in Idris (idris-lang/Idris2#2250) for coverage. In that issue a (,) or () on the LHS of an impossible clause is treated as a pattern var (wildcard) during coverage checking. If we explicitly put MkPair in MultHomomorphism, the coverage check fails. The PR idris-lang/Idris2#3396 fixes idris-lang/Idris2#2250 by resolving the ambiguity as MkPair instead of inserting a pattern variable and causes frex to fail to build. So we should update frex before that PR is merged.

The Pair/MkPair ambiguity in the current frex code is short-circuiting coverage checking. This coverage check failure can be reproduced with the current Idris by writing MkPair for the pairs in the two impossible clauses of MultHomomorphism to get:

MultHomomorphism is not covering.

Missing cases:
    MultHomomorphism _ _ (_, Ultimate _) (_, ConsUlt _ _ _) _
    MultHomomorphism _ _ (_, ConsUlt _ _ _) (_, Ultimate _) _

The MultHomomorphism function is indeed covering - Idris accepts it as such when there are holes on the RHS instead of impossible. The issue goes away if the MkAnd match is pushed down into a with clause, so that's what I do in this patch. There probably is a bug in coverage checking with respect to impossible clauses here, but I haven't tracked it down and the workaround seems sufficient.

gallais commented 1 month ago

Is there any chance we can define the appropriate Uninhabited instances and use absurd instead? Using with just to case split on a single variable seems way overkill

dunhamsteve commented 1 month ago

Hopefully this version is better. The with was bothering me too.

I'd like to know why the impossible doesn't knock those cases off, but I think it would require a log of digging in logs. The case trees have the same order, with the branch elided in the impossible case.