How can I ‘convince’ GHC that I've excluded a certain case?

Question

I have the following toy implementation of a non-empty list (NEList) datatype:

-- A type to describe whether or not a list is empty.
data Emptiness :: Type where
  Empty    :: Emptiness
  NotEmpty :: Emptiness

-- The list itself. Note the existential type in `Cons'.
data List :: Emptiness -> Type -> Type where
  Nil :: List 'Empty a
  Cons :: a -> List e a -> List 'NotEmpty a

type EList a = List 'Empty a
type NEList a = List 'NotEmpty a

For example it's very easy to define a 'safe head' function that only operates on non-empty lists:

eHead :: NEList a -> a
eHead (Cons a _) = a

The last is similarly easy, but has a little complication:

eLast :: NEList a -> a
eLast (Cons a Nil) = a
eLast (Cons _ b@(Cons _ _)) = eLast b

The reason the pattern needs to be like this is to convince GHC that the type of b is indeed List 'NotEmpty, instead of an unknown existential type. The following code fails for that reason: (Couldn't match type ‘e’ with ‘'NotEmpty’ ...)

eLast :: NEList a -> a
eLast (Cons a Nil) = a
eLast (Cons _ b) = eLast b

I'm fully aware why this is happening. What I'd like to know is, can I avoid having to write b@(Cons _ _) every time? Is there some other way I can restrict the type, so that GHC knows that b is referring strictly to something of type List 'NotEmpty?

One obvious way is to use unsafeCoerce but this defeats the point of the exercise.

---

For the sake of reproducibility, here is my preamble:

{-# OPTIONS_GHC -Wall -Werror #-} -- To prevent missed cases.
{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE GADTs            #-}
{-# LANGUAGE KindSignatures   #-}
import Data.Kind

Answer 1

您可以做的一件事是传递空列表的替代方案：

lastDef :: a -> List e a -> a
lastDef a Nil = a
lastDef _ (Cons a b) = lastDef a b

然后在顶层将其包裹一次。

last :: NEList a -> a
last (Cons a b) = lastDef a b

将此模式扩展到foldr并foldr1留给读者作为练习。