How to fully evaluate case block in type

Question

In Idris you can have complex computations in the types themselves, like a case block in this function:

fun_1 : (n : Nat) -> case n of { Z => Bool; _ => Nat}
fun_1 Z = True
fun_1 (S n) = S n

But how would you be able to fully evaluate such a result, given a n : Nat (which would evaluate into Bool or Nat)?

For reference I have this function definition:

fun_2 : (n : Nat) -> n = Z -> Bool
fun_2 n nEqZ = ?fun_2_rhs

How could I implement this function using fun_1 so that it typechecks?

I tried the following two approaches, which both gave an error:

fun_2 : (n : Nat) -> n = Z -> Bool
fun_2 n nEqZ = rewrite nEqZ in (fun_1 n)

This gave the error

When elaborating right hand side of fun_2: rewrite did not change type Bool

fun_2 : (n : Nat) -> n = Z -> Bool
fun_2 n nEqZ = replace nEqZ {P=(\nat => case nat of { Z => Bool; _ => Nat})} (fun_1 n)

And this gave the error

When elaborating right hand side of fun_2: When elaborating an application of function replace:
Can't unify
    case block in fun_1 n n (Type of fun_1 n)
with
    (\__pi_arg => Bool) n (Expected type)

Specifically:
    Can't unify
        case block in fun_1 n n
    with
        Bool

Is the only possible way for it to typecheck to pattern match on Z and call fun_1 Z directly, like this?:

fun_2 : (n : Nat) -> n = Z -> Bool
fun_2 Z Refl = fun_1 Z

I am not very convinced by this method, because the computation in the type can be more complex than a simple pattern case analysis on Z and S n, and I'm not sure it would be possible (or at least straightforward) in those cases

Edwin Brady Edwin Brady · Accepted Answer · 2015-08-20T08:00:32

If you want computation in the type to make progress, it needs some information, so yes, you do need to pattern match. The rewrite didn't work because nothing in the type had the form n=Z.

Quite often, using a computation in a type like this gives some useful hints as to how the corresponding program should work, suggesting where to check for errors etc.

How to fully evaluate case block in type

1 Answers