Idris - Computation on types based on decidable property doesn't typecheck

Question

I'm facing a problem in Idris, where I want to create a type-level "check" based on a decidable property, where if the property holds I get the type I want, but if the property fails I get Unit (()), signaling that the program is in an inconsistent state (and should not compile if I decide to use it as my original type).

Here's an example:

TestType : {k : Nat} -> Nat -> Vect k Nat -> Type
TestType n ls with (isElem n ls)
  TestType n ls | Yes _ = Nat
  TestType n ls | No _ = ()

mkTestTypeFromNat : (n : Nat) -> (ls : Vect k Nat) -> Elem n ls -> Nat -> TestType {k=k} n ls
mkTestTypeFromNat n ls prf res = res

mkTestTypeFromUnit : (n : Nat) -> (ls : Vect k Nat) -> Not (Elem n ls) -> TestType {k=k} n ls
mkTestTypeFromUnit n ls prf = ()

When I try to compile this, it shows me the following errors:

When checking right hand side of mkTestTypeFromNat:
Type mismatch between
           Nat (Type of n)
   and
           with block in Extensible_Records.TestType n
                                                     k
                                                     ls
                                                     (isElem n ls) (Expected type)

When checking right hand side of mkTestTypeFromUnit:
Type mismatch between
           () (Type of ())
   and
           with block in Extensible_Records.TestType n
                                                     k
                                                     ls
                                                     (isElem n ls) (Expected type)

In each of these mkTestTypeFrom_ functions I provide the proof of the deciable property, either a proof the element is in the list or the proof it isn't. Shouldn't the typechecker realize it has these proofs, and be able to compute the with (isElem n ls) section without problems, giving me the correct type in each case? Or am I missing something to convince the typechecker of such?

dfeuer dfeuer · Accepted Answer · 2015-09-28T08:56:32

Just having evidence around doesn't really help you until you use it. This is the best I could come up with for your types; I don't know if the code will be optimized sensibly, or if there's a way to make them efficient if not. The compiler will surely recognize that each case analysis has only one reachable branch. What's less clear to me is whether it will realize that it therefore has no need to evaluate the scrutinee.

mkTestTypeFromNat : (n : Nat) -> (ls : Vect k Nat) -> Elem n ls -> Nat -> TestType {k=k} n ls
mkTestTypeFromNat n ls prf res with (isElem n ls)
  mkTestTypeFromNat n ls prf res | (Yes x) = res
  mkTestTypeFromNat n ls prf res | (No contra) = absurd (contra prf)

mkTestTypeFromUnit : (n : Nat) -> (ls : Vect k Nat) -> Not (Elem n ls) -> TestType {k=k} n ls
mkTestTypeFromUnit n ls prf with (isElem n ls)
  mkTestTypeFromUnit n ls prf | (Yes x) = absurd (prf x)
  mkTestTypeFromUnit n ls prf | (No contra) = ()

Idris - Computation on types based on decidable property doesn't typecheck

1 Answers