Idris refuses to unify types it can already infer.

[Sventimir]

Source code reproducing the issue.

I'm trying to define integers as follows:

data Sign = Positive | Zero | Negative

nonNegative : Sign -> Type
nonNegative Positive = ()
nonNegative Zero = ()
nonNegative Negative = Void

nonPositive : Sign -> Type
nonPositive Positive = Void
nonPositive Zero = ()
nonPositive Negative = ()

nonZero : Sign -> Type
nonZero Positive = ()
nonZero Zero = Void
nonZero Negative = ()

data SignedI : Sign -> Type where
  Z : SignedI Zero
  S : (0 s : Sign) -> (w : nonNegative s) -> (i : SignedI s) -> SignedI Positive
  P : (0 s : Sign) -> (w : nonPositive s) -> (i : SignedI s) -> SignedI Negative
  
data I : Type where
  MkI : (i : SignedI s) -> I
succ' : SignedI s -> (s' : Sign ** SignedI s')
succ' Z = (Positive ** S Zero () Z)
succ' (S s w i) = (Positive ** S Positive () (S s w i))
succ' (P Zero w Z) = (Zero ** Z)
succ' (P Positive w (S s _ i)) = void w
succ' (P Negative w (P s w' i)) = (Negative ** P s w' i)

succ : I -> I
succ (MkI i) = let (_ ** i') = succ' i in MkI i'

pred' : SignedI s -> (s' : Sign ** SignedI s')
pred' Z = (Negative ** P Zero () Z)
pred' (S Zero w Z) = (Zero ** Z)
pred' (S Positive w (S s w' i)) = (Positive ** S s w' i)
pred' (S Negative w (P _ _ _)) = void w
pred' (P s w i) = (Negative ** P Negative () (P s w i))

pred : I -> I
pred (MkI i) = let (_ ** i') = pred' i in MkI i'

succElim : (i, j : I) -> succ i = succ j -> i = j
succElim (MkI Z) (MkI Z) Refl = Refl
succElim (MkI Z) (MkI (P Positive w (S _ _ _))) prf = void w
succElim (MkI (S s w i)) (MkI (S s w i)) Refl = Refl
succElim (MkI (S s _ i)) (MkI (P Positive w (S s' _ j))) prf = void w
succElim (MkI (P Positive w (S _ _ _))) (MkI Z) prf = void w
succElim (MkI (P Positive w (S _ _ _))) (MkI (S _ _ _)) prf = void w
succElim (MkI (P Zero () Z)) (MkI (P Zero () Z)) Refl = Refl
succElim (MkI (P Zero _ Z)) (MkI (P Positive w (S _ _ _))) prf = void w
succElim (MkI (P Positive w (S _ _ _))) (MkI (P _ _ _)) prf = void w
succElim (MkI (P Negative _ (P _ _ _))) (MkI (P Positive w (S _ _ _))) prf = void w
succElim (MkI (P Negative () (P s w i))) (MkI (P Negative x (P s' w' j))) prf = 
  let z = cong pred prf in
  ?succElim_rhs

In the construction above, with P (pred) and S (succ) constructors, we could normally have an infinity of possible representations for each number (P (S Z) would be equivalent to just Z etc.). To eliminate these constructions we assert that inside P we can only find another P or Z, but not S. The mechanism is this: within S sign nonNeg i sign declares the sign of i, and then nonNeg evaluates to () if it's correct or to Void if it's not. Since we cannot construct Void, we cannot also construct a non-canonical integer. In other words nonNeg serves as a witness that the construction is canonical. Analogical argument goes for P.

Problem:
In the last clause for succElim there is this x variable, which should obviously evaluate to () as it does in other cases where we have P Negative ... construction, but for some reason Idris insists that it cannot unify x and (). If I try to replace x with () , it says succElim is not covering:

 `-- src/Report.idr line 59 col 0:
     succElim is not covering.
     
     Report:59:1--59:50
      55 | 
      56 | pred : I -> I
      57 | pred (MkI i) = let (_ ** i') = pred' i in MkI i'
      58 | 
      59 | succElim : (i, j : I) -> succ i = succ j -> i = j
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     
     Missing cases:
         succElim (MkI (P _ () (P _ _ _))) (MkI (P _ _ (P _ _ _))) _
         succElim (MkI (P _ () (P _ _ _))) (MkI (P _ _ (P _ _ _))) _
         succElim (MkI (P _ () (P _ _ _))) (MkI (P _ _ (P _ _ _))) _

Still, when I leave it as is, it happily decides it must be ():

Holes

This buffer displays the unsolved holes from the currently-loaded code. Press
the [P] buttons to solve the holes interactively in the prover.

- + "Report.succElim_rhs" [P]
 `--                   0  s : Sign
                          i : SignedI s
                          w : nonPositive s
                      0  s' : Sign
                          j : SignedI s'
                         w' : nonPositive s'
                          x : ()
                        prf : MkI (P s w i) = MkI (P s' w' j)
                          z : MkI (P Negative () (P s w i)) = MkI (P Negative () (P s' w' j))
     -----------------------------------------------------------------------------------------
      "Report.succElim_rhs" : MkI (P Negative () (P s w i)) = MkI (P Negative x (P s' w' j))

But when I try to return z (which has the right type if you substitute () for x), it complains that it cannot unify x and (). How do I make sense of it? Is it some quirk of the type-checker or simply a bug?

[dunhamsteve]

There are two different (), which confuses discussion a little. For clarity, I may say MkUnit for the value () and Unit for the Type ().

Why the unification error is expected:

Unification can't sort out that x is MkUnit. The x : () that you pasted indicates that Idris has determined that x is a variable with some value of type Unit, but it doesn't know the value of x. I know "there can be only one", but unification in Idris doesn't know that. (Is this what they call "eta expansion of unit"?)

So we have to match against () (MkUnit) to get the value in there in place of the variable. You did this and got some false positives about missing cases. Another way this could be addressed is putting case x of () => cong pred prf on the RHS, but we can actually get it working on the LHS.

The issue with the missing cases:

Putting the () in the left side was the right thing to do, but the case-tree builder got confused. Ideally Idris could sort this out or at least give a more helpful error message / warning.

Idris has to break that case statement into a tree of individual steps. You can see the result by typing :di elimSucc in the repl. I tried putting in the () and adding the missing case:

succElim (MkI (P Negative () (P s w i))) (MkI (P Negative () (P s' w' j))) prf =  ...
succElim (MkI (P Negative () (P s w i))) (MkI (P Negative x (P s' w' j))) prf = ?what

I looked at the case tree and there was a lot of ?what in there (duplicated because of branching). Eventually I sorted out that it was the previous line that confused things:

succElim (MkI (P Negative _ (P _ _ _))) (MkI (P Positive w (S _ _ _))) prf = void w
succElim (MkI (P Negative () (P s w i))) (MkI (P Negative x (P s' w' j))) prf = 

At the beginning it says (MkI Negative _ ... and then (MkI Negative () .... Idris is case splitting at that point, with two subtrees, one for the () case and the other for the _ case. The second line only goes into the () tree, and then it has a bunch of missing cases for the same stuff in the _ tree (which is an impossible branch, since everything is ()).

The code can be made to work by replacing the _ by () on the first line, which collapses the Negative _ and Negative () branches into one:

succElim (MkI (P Negative () (P _ _ _))) (MkI (P Positive w (S _ _ _))) prf = void w
succElim (MkI (P Negative () (P s w i))) (MkI (P Negative () (P s' w' j))) prf = ...

My questions:

• Are there cases where the case-builder can fold these two branches together (I suspect we might not want it for Refl)?
• And if not, should we warn in this situation?

[Sventimir]

On a tangent line, I'm curious, why I have to write void w manually in so many cases. Normally Idris can pattern-match on Void and determine there are no cases to match, but here it didn't work. When I hit C-c C-c on w, I always got elaboration error and had to explicitly return void w on these cases…

[dunhamsteve]

Yeah, I missed that. In Idris we can often leave a case-alt out if it is not possible. (No valid constructor given the context.) So we can remove all of the void cases:

succElim : (i, j : I) -> succ i = succ j -> i = j
succElim (MkI Z) (MkI Z) Refl = Refl
succElim (MkI (S s w i)) (MkI (S s w i)) Refl = Refl
succElim (MkI (P Zero () Z)) (MkI (P Zero () Z)) Refl = Refl
succElim (MkI (P Negative MkUnit (P s w i))) (MkI (P Negative (MkUnit) (P s' w' j))) prf = cong pred prf

One weird thing though, I removed the definition of succElim (leaving the declaration) and idris2-lsp just spins when the cursor hits succElim. The LSP preruns everything to get the list of menu items for the code actions menu. It looks like "Request.CodeAction.GenerateDef" is spinning. In the repl, :gd 48 succElim also spins.