Сводка противоречия typechecks в Idris

Question

У меня есть следующее определение предиката на векторах, который идентифицирует, является ли это множеством (не имеет повторяющихся элементов) или нет. Я определяю членство с логическим типом уровня:

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) 

Теперь определим некоторые функции, которые позволяют мне создавать этот предикат:

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 работает как процедуры принятия над ElemBool.

Моя проблема с fun_2. Почему сопоставление шаблонов на (False ** isNotMember) = fun_1 x xs typecheck?

Еще более запутанным, что-то вроде следующих typechecks тоже:

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

Это кажется противоречивым, основанный на определении IsSet и ElemBool выше. Значение example Идриса оценивает следующий:

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] 

Является ли это намеренное поведение? Или это противоречие? Почему значение типа IsSet [1,1] - блок корпуса? У меня есть аннотация %default total в верхней части файла, поэтому я не думаю, что это имеет какое-то отношение к пристрастности, не так ли?

Примечание: Я использую Идрис 0.9.18

Answer 1

Существует ошибка в клетчатом покрытии поэтому этот типа проверка. Он будет исправлен в 0.9.19 (это была тривиальная проблема, вызванная сменой имени для внутреннего конструктора зависимых пар, который по какой-то причине остался незамеченным до сих пор, поэтому спасибо, что привлек его к моему вниманию!)

Во всяком случае, я осуществил fun_2 следующим образом:

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) 

поскольку не все Vect s могут быть наборы, это должно возвращать Maybe. К сожалению, он не может вернуть что-то более точное, например, Dec (IsSet xs), потому что вы используете логическое равенство через Eq, а не разрешаемое равенство через DecEq, но, возможно, это то, что вы хотите для своей версии наборов.