IsLast.idr

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

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

isLast : DecEq a => (xs : List a) -> (val : a) -> Dec (Last xs val)
isLast [] val = No absurd

isLast [x] val = case decEq x val of
                      Yes Refl => Yes LastOne
                      No contra => No (notLastOne contra)
  where
    notLastOne : (contra : (y = v) -> Void) -> Last [y] v -> Void
    notLastOne contra LastOne = contra Refl
    notLastOne contra (LastCons prf) = uninhabited prf

isLast (x :: xs@(x' :: xs')) val = case isLast xs val of
                                        Yes prf => Yes (LastCons prf)
                                        No contra => No ?b -- (notLastCons contra)
  where
    notLastCons : (contra : Last ys v -> Void) -> Last (y :: ys) v -> Void

{-
- + Errors (1)
 `-- CheckEqDec.idr line 84 col 56:
     When checking right hand side of Main.case block in isLast at CheckEqDec.idr:83:41-53 with expected type
             Dec (Last (x :: x' :: xs') val)
     
     When checking argument prf to constructor Main.LastCons:
             Type mismatch between
                     Last xs val (Type of prf)
             and
                     Last (x' :: xs') val (Expected type)
             
             Specifically:
                     Type mismatch between
                             xs
                     and
                             x' :: xs'
-}