Идрис - Невозможно оценить приложение функции в типе

У меня проблема, когда у меня есть значение типа fun a, где fun является функцией, а a значением, которое не вычисляется при проверке типа и выдает ошибку объединения, когда я заставляю его быть результатом этой функции применение.

Конкретная ошибка такова:

When checking right hand side of testRec2 with expected type
         Record [("A", String), ("C", Nat)]

 Type mismatch between
         Record (projectLeft ["A", "C"]
                             [("A", String),
                              ("B", String),
                              ("C", Nat)]) (Type of hProjectByLabels_comp ["A",
                                                                           "C"]
                                                                          testRec1
                                                                          (getYes (isSet ["A",
                                                                                          "C"])))
 and
         Record [("A", String), ("C", Nat)] (Expected type)

 Specifically:
         Type mismatch between
                 projectLeft ["A", "C"]
                             [("A", String), ("B", String), ("C", Nat)]
         and
                 [("A", String), ("C", Nat)]

Это из реализации HList-подобных записей в Идрисе со следующим примером:

testRec1 : Record [("A", String), ("B", String), ("C", Nat)]
-- testRec1's value is already defined    

testRec2 : Record [("A", String), ("C", Nat)]
testRec2 = hProjectByLabels_comp ["A", "C"] testRec1 (getYes $ isSet ["A", "C"])

... следующие типы:

IsSet : List t -> Type

isSet : DecEq t => (xs : List t) -> Dec (IsSet xs)

LabelList : Type -> Type

IsLabelSet : LabelList lty -> Type

HList : LabelList lty -> Type

Record : LabelList lty -> Type

recToHList : Record ts -> HList ts

recLblIsSet : Record ts -> IsLabelSet ts

hListToRec : DecEq lty => {ts : LabelList lty} -> {prf : IsLabelSet ts} -> HList ts -> Record ts

IsProjectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty -> Type

IsProjectRight : DecEq lty => List lty -> LabelList lty -> LabelList lty -> Type

hProjectByLabelsHList : DecEq lty => {ts : LabelList lty} -> (ls : List lty) -> HList ts -> ((ls1 : LabelList lty ** (HList ls1, IsProjectLeft ls ts ls1)), (ls2 : LabelList lty ** (HList ls2, IsProjectRight ls ts ls2)))

projectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty

hProjectByLabelsLeftIsSet_Lemma2 : DecEq lty => {ls : List lty} -> {ts1, ts2 : LabelList lty} -> IsProjectLeft ls ts1 ts2 -> IsLabelSet ts1 -> IsLabelSet ts2

fromIsProjectLeftToComp : DecEq lty => {ls : List lty} -> {ts1, ts2 : LabelList lty} -> IsProjectLeft ls ts1 ts2 -> IsSet ls -> ts2 = projectLeft ls ts1

hProjectByLabels_comp : DecEq lty => {ts : LabelList lty} -> (ls : List lty) -> Record ts -> IsSet ls -> Record (projectLeft ls ts)

... и следующие (необходимые) определения:

LabelList : Type -> Type
LabelList lty = List (lty, Type)

IsLabelSet : LabelList lty -> Type
IsLabelSet ts = IsSet (map fst ts) 

projectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty
projectLeft [] ts = []
projectLeft ls [] = []
projectLeft ls ((l,ty) :: ts) with (isElem l ls)
  projectLeft ls ((l,ty) :: ts) | Yes lIsInLs = 
    let delLFromLs = deleteElem ls lIsInLs
        rest = projectLeft delLFromLs ts
    in (l,ty) :: rest
  projectLeft ls ((l,ty) :: ts) | No _ = projectLeft ls ts

deleteElem : (xs : List t) -> Elem x xs -> List t
deleteElem (x :: xs) Here = xs
deleteElem (x :: xs) (There inThere) =
  let rest = deleteElem xs inThere
  in x :: rest 

getYes : (d : Dec p) -> case d of { No _ => (); Yes _ => p}
getYes (No _ ) = ()
getYes (Yes prf) = prf

hProjectByLabels_comp : DecEq lty => {ts : LabelList lty} -> (ls : List lty) -> Record ts -> IsSet ls -> Record (projectLeft ls ts)
hProjectByLabels_comp {ts} ls rec lsIsSet =
  let 
    isLabelSet = recLblIsSet rec
    hs = recToHList rec
    (lsRes ** (hsRes, prjLeftRes)) = fst $ hProjectByLabelsHList ls hs
    isLabelSetRes = hProjectByLabelsLeftIsSet_Lemma2 prjLeftRes isLabelSet
    resIsProjComp = fromIsProjectLeftToComp prjLeftRes lsIsSet
    recRes = hListToRec {prf=isLabelSetRes} hsRes
  in rewrite (sym resIsProjComp) in recRes

По сути, есть функция projectLeft, которая применяется к 2 спискам и возвращает новый. Тип hProjectByLabels_comp применяет эту функцию на уровне типа. Чтобы фактически построить результирующий список, у меня есть предикат стиля Pred l1 l2 l3 и лемма стиля Pred l1 l2 l3 -> l3 = projectLeft l1 l2. В hProjectByLabels_comp я применяю лемму к предикату и использую rewrite для получения правильной сигнатуры типа (переписывая l3, который неявно присутствует в предикате, который появляется внутри реализации, в projectLeft l1 l2 или projectLeft ls ts в данном конкретном случае).

Я ожидал, что применение hProjectByLabels_comp к записи будет правильно вычислять projectLeft ls ts. Однако в приведенном выше примере не удается оценить / вычислить projectLeft ["A", "C"] [("A", String), ("B", String), ("C", Nat)]. Это кажется странным, поскольку оценка приложения этой функции в REPL дает ровно [("A", String), ("C", Nat)], чего и ожидает тип, но Идрис не может вычислить эту функцию при проверке типов.

Я не уверен, имеет ли реализация некоторых лемм / функций какое-либо отношение к этому, или это просто что-то только о типах.

Я попытался воспроизвести эту ошибку, используя более простой пример (с предикатами и функциями в Nats), но в этом более простом примере тип проверен правильно, поэтому я не смог найти другого способа воспроизвести эту ошибку.

Я использую Идрис 0.9.20.2

Изменить. Я попытался переписать projectLeft следующим образом, чтобы проверить, не изменилось ли что-нибудь, но он продолжает показывать ту же ошибку

projectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty
projectLeft ls [] = []
projectLeft ls ((l,ty) :: ts) with (isElem l ls)
  projectLeft ls ((l,ty) :: ts) | Yes lIsInLs = 
    let delLFromLs = deleteElem ls lIsInLs
        rest = projectLeft delLFromLs ts
    in (l,ty) :: rest
  projectLeft ls ((l,ty) :: ts) | No _ = projectLeft ls ts