Seeming contradiction typechecks in Idris

Question

I have the following definition of a predicate on vectors that identifies if one is a set (has no repeated elements) or not. I define membership with a type-level boolean:

import Data.Vect

%default total

data ElemBool : Eq t => t -> Vect n t -> Bool -> Type where
  ElemBoolNil : Eq t => ElemBool {t=t} a [] False
  ElemBoolCons : Eq t => ElemBool {t=t} x1 xs b -> ElemBool x1 (x2 :: xs) ((x1 == x2) || b)

data IsSet : Eq t => Vect n t -> Type where
  IsSetNil : Eq t => IsSet {t=t} []
  IsSetCons : Eq t => ElemBool {t=t} x xs False -> IsSet xs -> IsSet (x :: xs)

Now I define some functions that allow me to create this predicate:

fun_1 : Eq t => (x : t) -> (xs : Vect n t) -> (b : Bool ** ElemBool x xs b)
fun_1 x [] = (False ** ElemBoolNil)
fun_1 x1 (x2 :: xs) = 
  let (b ** prfRec) = fun_1 x1 xs
  in (((x1 == x2) || b) ** (ElemBoolCons prfRec))  

fun_2 : Eq t => (xs : Vect n t) -> IsSet xs 
fun_2 [] = IsSetNil
fun_2 (x :: xs) = 
    let prfRec = fun_2 xs
        (False ** isNotMember) = fun_1 x xs
    in IsSetCons isNotMember prfRec

fun_1 works like a decision procedure over ElemBool.

My problem is with fun_2. Why does the pattern matching on (False ** isNotMember) = fun_1 x xs typecheck?

Even more confusing, something like the following typechecks too:

example : IsSet [1,1]
example = fun_2 [1,1]

This seems like a contradiction, based on the definition of IsSet and ElemBool above. The value for example idris evaluates is the following:

case block in fun_2 Integer
                    1
                    1
                    [1]
                    (constructor of Prelude.Classes.Eq (\meth =>
                                                          \meth =>
                                                            intToBool (prim__eqBigInt meth
                                                                                      meth))
                                                       (\meth =>
                                                          \meth =>
                                                            not (intToBool (prim__eqBigInt meth
                                                                                           meth))))
                    (IsSetCons ElemBoolNil IsSetNil)
                    (True ** ElemBoolCons ElemBoolNil) : IsSet [1, 1]

Is this an intended behaviour? Or is it a contradiction? Why is the value of type IsSet [1,1] a case block? I have the %default total annotation at the top of the file so I don't think it has anything to do with partiality, right?

Note: I'm using Idris 0.9.18

I haven't had a chance to look properly, or test in the git master, but it seems the totality checker is getting this wrong. The fact that evaluation gets stuck on the case block is what makes me think this. Something with fun_2's type being total would suggest every vector is a set after all. I will take a look at the case coverage checker when I get to a computer... — Edwin Brady
Yes, it turns out the coverage checker isn't even interested in dependent pairs, so you're not getting an error that should be reported. I'll fix this reasonably soon then try to give a proper answer... — Edwin Brady

Edwin Brady Edwin Brady · Accepted Answer · 2015-08-21T07:55:03

There is a bug in the coverage checker which is why this type checks. It'll be fixed in 0.9.19 (it was a trivial problem cause by a change of name for the internal dependent pair constructor which has, for some reason, gone unnoticed until now, so thanks for bringing it to my attention!)

Anyway, I implemented fun_2 as follows:

fun_2 : Eq t => (xs : Vect n t) -> Maybe (IsSet xs)
fun_2 [] = Just IsSetNil
fun_2 (x :: xs) with (fun_1 x xs)
  fun_2 (x :: xs) | (True ** pf) = Nothing
  fun_2 (x :: xs) | (False ** pf) with (fun_2 xs)
    fun_2 (x :: xs) | (False ** pf) | Nothing = Nothing
    fun_2 (x :: xs) | (False ** pf) | (Just prfRec)
        = Just (IsSetCons pf prfRec)

Since not all Vects can be sets, this needs to return a Maybe. Sadly, it can't return something more precise like Dec (IsSet xs) because you're using a boolean equality via Eq rather than a decidable equality via DecEq but maybe that's what you want for your version of sets.

Seeming contradiction typechecks in Idris

1 Answers