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

One thing you can do is pass around an alternative for empty lists:

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

Then wrap it up once at the top level.

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

Extending this pattern to foldr and foldr1 is left as an exercise for the reader.

Answer 2

You've "defined" NEList (I say that in a loose way) the same way base defines NonEmpty: as a single element tacked onto the head of a potentially empty list.

data NonEmpty a = a :| [a]

Another presentation of NonEmpty instead places that single element at the end.

data NonEmpty a = Single a | Multiple a (NonEmpty a)

This presentation, no surprise, makes eLast easy:

eLast (Single x) = x
eLast (Multiple _ xs) = eLast xs

Whenever you want multiple sets of constructors on the same type, look to pattern synonyms. Instead of the base NonEmpty, we can also translate to your List.

pattern Single :: forall e a. () => e ~ 'NotEmpty => a -> List e a
pattern Single x = Cons x Nil
pattern Multiple :: forall e a. () => e ~ 'NotEmpty => a -> List 'NotEmpty a -> List e a
pattern Multiple x xs <- Cons x xs@(Cons _ _)
  where Multiple x xs = Cons x xs
-- my dormant bidirectional pattern synonyms GHC proposal would allow just
-- pattern Multiple x (Cons y xs) = Cons x (Cons y xs)
-- but current pattern synonyms are a little stupid, so Multiple is ugly
{-# COMPLETE Nil, Single, Multiple :: List #-}
-- Single and Multiple are actually patterns on List e a, not List NotEmpty a
-- Therefore the COMPLETE must include Nil, or else we'd show that all
-- Lists are nonempty (\case { Single _ -> Refl; Multiple _ _ -> Refl })
-- They are, however, still complete on List NotEmpty a
-- GHC will "infer" this by "trying" the Nil constructor and deeming it impossible

Giving

eLast :: NEList a -> a
eLast (Single x) = x
eLast (Multiple _ xs) = eLast xs