Definition with no RHS is incorrectly accepted as total

[gallais]

trafficstars

Found while looking at the code interactively generated by case splitting in #2242.

%default total

g : Not Bool
g () impossible

f : Void
f = g True

Edit: Happy New Year!

[buzden]

Looks like another example for the same problem, but with a bit deeper type problem:

data Even : Nat -> Type where
  EZ  : Even Z
  ESS : Even n -> Even (2 + n)

notE : (n : Nat) -> Not (Even n)
notE (S $ S n) (ESS n) impossible
notE 0 EZ = notE 2 (ESS EZ)

[gallais]

This is rejected with %default total though:

notE is not total, possibly not terminating due to recursive path Main.notE

[buzden]

This is rejected with %default total though:

notE is not total, possibly not terminating due to recursive path Main.notE

Right, this is because I incorrectly shrunk the original example:

%default total

data Even : Nat -> Type where
  EZ  : Even Z
  ESS : Even n -> Even (2 + n)

data Odd : Nat -> Type where
  OSZ : Odd 1
  OSS : Odd n -> Odd (2 + n)

notE : (n : Nat) -> Not (Even n, Odd n)
notE 0         (_, y) = case y of _ impossible
notE 1         (x, _) = case x of _ impossible
notE (S $ S n) (ESS n, OSS n) impossible

(BTW, I don't know why 0 and 1 cases do not work with simple impossible, why I need to case of a part manually.

[buzden]

(BTW, I don't know why 0 and 1 cases do not work with simple impossible, why I need to case of a part manually.

One can do the following to avoid

notE : (n : Nat) -> Not (Even n, Odd n)
notE Z         (_, _) impossible
notE (S Z)     (_, _) impossible
notE (S $ S n) (ESS n, OSS n) impossible

Looks, like a separate bug...

[ohad]

Another one (or related):

View : Type -> Type
View a = a -> Type

-- Pre-image view
data (.inv) : (f : a -> b) -> View b where
  Choose : (x : a) -> f.inv (f x)

LessThanOrEqualTo : Nat -> Nat -> Type
LessThanOrEqualTo n k = (+n).inv k

Ex1 : 3 `LessThanOrEqualTo` 5
Ex1 = Choose 2

Bug : Not (3 `LessThanOrEqualTo` 5)
Bug Refl impossible

Yikes : Void
Yikes = Bug Ex1

[yallop]

Also possibly related:

%default total

v : (0 a: Nat) -> Void
v   Z   impossible
v (S _) impossible

empty : Void
empty = v 0

(accepted as of cf9a73f86)

[buzden]

An example in the flavour of the original one, but with an additional funny difference:

import Data.Nat

%default total

f : n `LTE` m -> Void
f Z impossible
f (LTESucc x) = f x

x : Void
x = f $ LTEZero {right=Z}

If you comment LTESucc case in the f, compiler will complain that the function is not covering, despite the very convincing to the complier the first (nonsense) case.

[dunhamsteve]

The original example in this issue is caused by the IAlternative for (). When the impossible clause is generated, the IAlternative for Unit|MkUnit is replaced by a pattern variable in a fallback case:

https://github.com/idris-lang/Idris2/blob/5d04f89c7b42afba384d19108b5e0cdaee99a224/src/TTImp/Impossible.idr#L169

The function is then covering because the pattern variable covers everything.

The compile does fail when either Unit or MkUnit is used in place of ().

[mjustus]

Good detective work! We had the same issue with as-patterns previously (issue, PR).

At some point, we should address the two larger issues as well:

• impossibleErrOk is too liberal. It not only filters out unification errors caused by an impossible LHS but also genuine type errors, as in the program above.
• There shouldn't be any need to trust that the LHS generated by getImpossibleTerm is actually impossible. We could pass it as evidence to the coverage checker rather than generating a fake clause.

[dunhamsteve]

A little additional information: the last issue posted by buzden, the one by ohad, and #3276 are caused by confusion between types. There is an impossible clause generated with a constructor of the bad type. When Idris looks for coverage, it only compares the tag number of the constructor to the list of needed constructors. So a Z and a Refl would look the same. It happens here:

https://github.com/idris-lang/Idris2/blob/5d04f89c7b42afba384d19108b5e0cdaee99a224/src/Core/Coverage.idr#L151

So I tried having it also check the names. I had to change getCons to return resolved names to make the names comparable. This solved ohad's issue and buzden's last issue, but #3276 was still broken because Idris was discarding the missing constructor due to a visibility error. This I resolved by making InvisibleName a "recoverable" error.

I have prepared a patch for those three issues (but not the IAlternative one) here: https://github.com/idris-lang/Idris2/compare/main...dunhamsteve:Idris2:issue-3276 It works, but I don't know if it is an acceptable solution.

All of this is to work around the issue that constructors at another type slip through into impossible clauses. The InvisibleName thing is legitimate when we have these weird impossible clauses, but I don't think it comes up normally because you've either got a constructor, which means it's visible, or a pattern variable.

To help diagnose issues like the IAlternative case, we might want to add logging in the default case of mkTerm (adding cases for Implicit and IBindVar, which are expected).

[dunhamsteve]

I've updated that branch to handle the IAlternative issue by choosing the default alternative, and it resolves the issue. But it breaks frex.

One spot in frex appears to be leveraging this bug - in Structure.idr these impossible cases have an ambiguous Pair/MkPair in them:

MultHomomorphism : (a : Monoid) -> (s : Setoid) ->
  SetoidHomomorphism
    (cast a `Pair` UltListSetoid s (cast a))
    (UltListSetoid s (cast a))
    (Prelude.uncurry a.mult)
MultHomomorphism a s (i, Ultimate i1) (j, Ultimate j1)
  (MkAnd i_eq_j $ Ultimate i1_eq_i2)
  = Ultimate $ a.cong 2 (Dyn 0 .*. Dyn 1) [_,_] [_,_] [i_eq_j, i1_eq_i2]
MultHomomorphism a s (i, ConsUlt i1 x is) (j,ConsUlt j1 y js)
  (MkAnd i_eq_j $ ConsUlt i1_eq_i2 x_eq_y is_eq_js)
  = ( a.cong 2 (Dyn 0 .*. Dyn 1) [_,_] [_,_] [i_eq_j, i1_eq_i2]
    , x_eq_y
    ) :: is_eq_js
MultHomomorphism _ _ (_, Ultimate _) (_, ConsUlt _ _ _) (MkAnd _ _) impossible
MultHomomorphism _ _ (_, ConsUlt _ _ _) (_, Ultimate _) (MkAnd _ _) impossible

They are intended to be MkPair, but since they're ambiguous, they get treated as wildcards during coverage checking by the existing compiler. If we explicitly say MkPair:

public export
MultHomomorphism : (a : Monoid) -> (s : Setoid) ->
  SetoidHomomorphism
    (cast a `Pair` UltListSetoid s (cast a))
    (UltListSetoid s (cast a))
    (Prelude.uncurry a.mult)
MultHomomorphism a s (i, Ultimate i1) (j, Ultimate j1)
  (MkAnd i_eq_j $ Ultimate i1_eq_i2)
  = Ultimate $ a.cong 2 (Dyn 0 .*. Dyn 1) [_,_] [_,_] [i_eq_j, i1_eq_i2]
MultHomomorphism a s (i, ConsUlt i1 x is) (j,ConsUlt j1 y js)
  (MkAnd i_eq_j $ ConsUlt i1_eq_i2 x_eq_y is_eq_js)
  = ( a.cong 2 (Dyn 0 .*. Dyn 1) [_,_] [_,_] [i_eq_j, i1_eq_i2]
    , x_eq_y
    ) :: is_eq_js
MultHomomorphism _ _ (MkPair _ (Ultimate _)) (MkPair _ (ConsUlt _ _ _)) (MkAnd _ _) impossible
MultHomomorphism _ _ (MkPair _ (ConsUlt _ _ _)) (MkPair _ (Ultimate _)) (MkAnd _ _) impossible

The existing compiler gives a coverage error:

Error: MultHomomorphism is not covering.

Frexlet.Monoid.Frex.Structure:148:1--153:29
 148 | public export
 149 | MultHomomorphism : (a : Monoid) -> (s : Setoid) ->
 150 |   SetoidHomomorphism
 151 |     (cast a `Pair` UltListSetoid s (cast a))
 152 |     (UltListSetoid s (cast a))
 153 |     (Prelude.uncurry a.mult)

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

(Those are MkPair in the error message, I tweaked Resugar.idr to verify.)

The missing cases look like the impossible cases, since MkAnd is a structure constructor. If I put holes on the right, Idris accepts it as covering, so I think the function is covering and this is due to the shape of the case tree.