Dependent pattern matching function seen as total when it's not

[peter-divianszky]

Given the following code

data Polarity : Type where
  Value       : Polarity
  Computation : Polarity

-- object types
data Ty : Polarity -> Type where
  Int' : Ty Value
  Fun  : List (Ty Value) -> Ty Computation

-- object codes
data Code : Ty p -> Type where
  App  : Code (Fun (t :: ts)) -> Code t -> Code (Fun ts)
  Halt : Code (Fun ts)

data Env : List (Ty Value) -> Type where
  ECons : Code t -> Env ts -> Env (t :: ts)
  ENil  : Env []

halt : Env ts -> Code (Fun us)
halt ENil = Halt
halt (ECons c cs) = App (halt cs) c   -- BUG: this line can be commented out

Steps to Reproduce

Comment out the last line.

Expected Behavior

The compiler should tell that halt is partial.

Observed Behavior

The compiler accepts the code without warnings (when the last line is commented out).

[dunhamsteve]

It is considering the missing impossible because of an internal error while checking it:

LOG declare.def.impossible:5: impossible because INTERNAL ERROR: Empty pattern in coverage check

Thrown from this case: https://github.com/idris-lang/Idris2/blob/6f537291904e26f104cea931d1602e65d39f188a/src/TTImp/Elab/ImplicitBind.idr#L352-L358

I added logging, and it thinks the type Main.Code Main.Value ?{_:887}_[]) is empty.

If you re-add the clause and put a hole:

halt : Env ts -> Code (Fun us)
halt ENil = Halt
halt (ECons c cs) = ?hole

In the hole, you see:

Main> :ti hole
 0 us : List (Ty Value)
   cs : Env ts
   c : Code {p = Value} t
 0 ts : List (Ty Value)
------------------------------
hole : Code {p = Computation} (Fun us)

c is uninhabited there, there is no constructor for Code with polarity Value.

[peter-divianszky]

Thanks for the detailed answer.

After adding a Var constructor to Code {Value} the compiler thinks that the last line is needed, which is the behavior I expect.

Now I am wondering, is there a bug here? Should Idris tell me that the last line is not needed if I don't add the Var constructor to Code? Anyway, I can go on with my project, I will not fear that I miss an important case.

[spcfox]

As mentioned above, the original example does not contain an error — the second case is indeed impossible.

Now I am wondering, is there a bug here? Should Idris tell me that the last line is not needed if I don't add the Var constructor to Code?

When analysing unreachable cases, Idris looks at the case tree. The compiler does not check whether the cases are actually possible; essentially, it only checks that a function does not match the same pattern twice.

In theory, we could try to detect impossible cases for which the user has still provided a definition, but then the compiler would issue a warning on the following function. I don’t think we want that.

foo : True = False -> Void
foo prf = absurd prf