实施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