Why I can't use matched variable instead of a variable value?

Question

Here is an example from here. The code looks like that:

sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs

I've tried to use single instead of False in the last line. But it fails. I think the problem is that the type of sum single xs is either Nat or List Nat, but + requires only Nat operands. But we are inside a clause where single equals False either way. Shouldn't Idris infer it? Why I can't use single here? Is there some reason for it?

Here is the error:

main.idr:14:23-41:
   |
14 | sum False (x :: xs) = x + (sum single xs)
   |                       ~~~~~~~~~~~~~~~~~~~
When checking right hand side of Main.sum with expected type
        Nat

When checking argument single to Main.sum:
        No such variable single

Upd: It looks like that the problem here is that I can't directly access the variable from type definition. Then I've tried to use implicit arguments like that:

sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum {single} False (x :: xs) = x + sum single xs

It doesn't help either. Maybe I'm using it wrong. Also I've tried the simplest possible variation like that:

sum : (single: Bool) -> isSingleton single -> Nat
sum s list = case s of 
    True => list
    False => case list of
        [] => 0
        (x::xs) => x + (sum s xs)

But it doesn't compile either:

   |
16 |         (x::xs) => x + (sum s xs)
   |                         ~~~~~~~~
When checking right hand side of Main.case block in case block in sum at main.idr:12:19 at main.idr:14:19-22 with expected type
        Nat

When checking an application of Main.sum:
        Type mismatch between
                List Nat (Type of xs)
        and
                isSingleton s (Expected type)

It looks a bit weird for me, because from one point Idris could prove many interesting and complex things, and from another such a simple thins is unavailable. Or maybe I'm doing it wrong.

joel joel · Accepted Answer · 2020-07-20T15:48:58

It's not so much that it can't infer the type of single, as single isn't in scope on the RHS. You could use a named pattern with single on the LHS

sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum single@False (x :: xs) = x + sum single xs

I can't see a way to avoid the named pattern in this case and just use

sum single (x :: xs) = x + sum single xs

as Idris doesn't infer it's a List Nat without the False. I get

  |
8 | sum single (x :: xs) = x + sum single xs
  | ~~~~~~~~~~~~~~~~~~~~
When checking left hand side of Main.sum:
When checking an application of Main.sum:
        Can't disambiguate since no name has a suitable type: 
                Prelude.List.::, Prelude.Stream.::

Why I can't use matched variable instead of a variable value?

1 Answers