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

Answer 1

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.