實現「平等的Vect」與DecEq

Question

我試圖執行以下操作：

headEqual : DecEq a => (x : a) -> (y : a) -> Maybe (Dec (x = y)) 
headEqual x y = case decEq x y of 
        Yes Refl => Just (Yes Refl) 
        No contra => Nothing 

vectEqual : DecEq a => (xs : Vect n a) -> (ys : Vect n a) -> Maybe (Dec (xs = ys)) 
vectEqual []   []   = Just (Yes Refl) 
vectEqual (x :: xxs) (y :: yys) = case headEqual x y of 
            Just (Yes prf) => vectEqual xxs yys 
            No contra  => Nothing 
vectEqual (x :: xxs) []   = Nothing 
vectEqual []   (y :: yys) = Nothing 

然而，它未能編譯：

*section3> :r 
Type checking ./section3.idr 
section3.idr:45:63-66: 
When checking right hand side of Main.case block in vectEqual at section3.idr:44:40 with expected type 
     Maybe (Dec (x :: xxs = y :: yys)) 

When checking argument xs to Main.vectEqual: 
     Unifying len and S len would lead to infinite value 
Holes: Main.y, Main.vectEqual 

我不明白這個編譯時錯誤。有人可以解釋嗎？

Answer 1

對於非空案例，您需要兩個證明 - 一個是頭相等，一個是尾。然後您需要將這些證明合併爲一個輸入向量。在：

Just (Yes prf) => vectEqual xxs yys 

當您需要整個列表的證明時，您試圖返回尾部證明。您需要檢查遞歸調用的結果以構建證明，例如

vectEqual : DecEq a => (xs : Vect n a) -> (ys : Vect n a) -> Maybe (Dec (xs = ys)) 
vectEqual [] [] = Just (Yes Refl) 
vectEqual (x :: xs) (y :: ys) = case decEq x y of 
    Yes hd_prf => case vectEqual xs ys of 
    Just (Yes tl_prf) => ?combine_proofs 
    _ => Nothing 
    No contra => Nothing 

如果加載在REPL上述定義，你會看到各類hd_prf和tl_prf：

hd_prf : x = y 
tl_prf : xs = ys 

可以使用rewrite構建的所需證明(x :: xs) = (y :: ys)

Just (Yes tl_prf) => rewrite hd_prf in rewrite tl_prf in Just (Yes Refl) 

請注意，此函數的返回類型有點奇怪，因爲您使用的是Nothing enco de Dec已經提供使用No構造函數的故障情況，因此您永遠不會返回Just (No _)。