Coverage checker gets confused in 0 context when indices are involved

[andrevidela]

In the following example, matching on the constructor of a record throw off the coverage checker. Replacing the constructor match by a wildcard or a variable fixes it

Steps to Reproduce

Here is a minimal code sample

record WithName  where
  constructor Name
  name : String

data Def : (n : Nat) -> (b : Bool) -> Type where
  End  : Def (S n) b
  Named  : WithName -> Def (n) b

0
Fn : Def n False -> Type
Fn End = ?h6
Fn (Named (Name _)) = ?h7

The error is

Error: Fn is not covering.

Missing cases:
    Fn (Named _)

However any of the following works

-- removing the 0 annotation
Fn : Def n False -> Type
Fn End = ?h6
Fn (Named (Name _)) = ?h7

-- removing the pattern and replacing it by a field projection
0
Fn : Def n False -> Type
Fn End = ?h6
Fn (Named x) = fn x.name

-- removing the `False` as the boolean parameter
0
Fn : Def n b -> Type
Fn End = ?h6
Fn (Named (Name _)) = ?h7

-- making `n` a parameter rather than in index
data Def : (n : Nat) -> (b : Bool) -> Type where
  End  : Def (n) b  -- remove the `S` here
  Named  : WithName -> Def (n) b

0
Fn : Def n False -> Type
Fn End = ?h6
Fn (Named (Name _)) = ?h7

Expected Behavior

There should be no difference between Fn (Named (Name _)) and Fn (Named _)

Observed Behavior

Coverage checker fails when Fn (Named (Name _)) is present

[andrevidela]

might be related to #1079 and #550 ?

[gallais]

Without the 0 annotation Idris2 will avoid matching on 0 arguments as much as possible. So you get the following case tree which is a straightforward translation of the code you wrote:

LOG compile.casetree.getpmdef:20: Compiled to: case {arg:1}[1] : (Def (S {pat0::1}) False) of
 { End {e:0} {e:1} => [0] ?h6_[{e:1}[1], {arg:0}[2]]
 | Named {e:2} {e:3} {e:4} => case {e:4}[2] : WithName of
   { Name {e:5} => [1] ?h7_[{arg:0}[4], {e:5}[0]]
   }
 }

But with the 0 annotation Idris2's inhibitions are completely lifted and you get...

LOG compile.casetree.getpmdef:20: Compiled to: case {arg:0}[0] : Nat of
 { S {e:4} => case {arg:1}[2] : (Def (S {pat0::1}) False) of
   { End {e:5} {e:6} => case {e:5}[0] : Bool of
     { False => [0] ?h6_[{e:4}[2], {arg:0}[3]]
     | _ => case {arg:1}[4] : (Def {arg:0}[3] False) of
       { Named {e:0} {e:1} {e:2} => case {e:0}[0] : Bool of
         { False => case {e:2}[2] : WithName of
           { Name {e:3} => [1] ?h7_[{arg:0}[7], {e:3}[0]]
           }
         }
       }
     }
   | _ => case {arg:1}[2] : (Def {arg:0}[1] False) of
     { Named {e:0} {e:1} {e:2} => case {e:0}[0] : Bool of
       { False => case {e:2}[2] : WithName of
         { Name {e:3} => [1] ?h7_[{arg:0}[5], {e:3}[0]]
         }
       }
     }
   }
 | _ => case {arg:1}[1] : (Def {arg:0}[0] False) of
   { Named {e:0} {e:1} {e:2} => case {e:0}[0] : Bool of
     { False => case {e:2}[2] : WithName of
       { Name {e:3} => [1] ?h7_[{arg:0}[4], {e:3}[0]]
       }
     }
   }
 }

Most notably you seem to end up matching on the value of type Def n False multiple times and end up in contradictory branches. Very strange.