實施isLast會與伊德里斯

Question

從類型驅動開發望着運動9.2與伊德里斯：

data Last : List a -> a -> Type where 
    LastOne : Last [value] value 
    LastCons : (prf : Last xs value) -> Last (x :: xs) value 

Uninhabited (Last [] value) where 
    uninhabited LastOne impossible 
    uninhabited (LastCons _) impossible 

notLast : Not (x = value) -> Last [x] value -> Void 
notLast prf LastOne  impossible 
notLast prf (LastCons _) impossible 

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value) 
isLast []  value = No absurd 
isLast (x::[]) value = case decEq x value of 
         Yes Refl => Yes LastOne 
         No contra => No (notLast contra) 
isLast (x::y::ys) value = ?rhs 

我在notLast prf LastOne情況下得到一個編譯時錯誤：

*section1> :r 
Type checking ./section1.idr 
section1.idr:20:9:notLast prf LastOne is a valid case 
Holes: Main.rhs, Main.notLast 

爲什麼會出現編譯器發現它是一個有效的情況？

Answer 1

伊德里斯是不太能夠看到Not (value = value)同構Void所以你需要解釋的問題是什麼樣的等等，以幫助它：

notLast : Not (x = value) -> Last [x] value -> Void 
notLast prf LastOne  = absurd (prf Refl) 
notLast prf (LastCons _) impossible