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

Comparative

Are you trying to define an analogue to tail :: [a] -> [a] or last :: [a] -> a? – Lydalyddite

@Lydalyddite You're absolutely right, I meant to write last not tail. Let me fix that. Though I think defining an analogue to tail might be very interesting too! – Comparative

Tail will be easy. Unfortunately I don't have an answer for your eLast... – Lydalyddite

@Lydalyddite tail may be harder than you expect. It's minorly tricky (though at least by now a well-known trick) to even write the type for tail. – Meridethmeridian

@DanielWagner My immediate thought was that it was impossible, since the type is existential? – Comparative

@AJFarmar There are two standard tricks for encoding existentials in Haskell: via CPS (exists e. List e a -> (EList a -> b, NEList a -> b) -> b) and existential wrappers (data SomeList a where SomeList :: List e a -> SomeList a; sometimes paired with a GADT that lets you recover e). – Meridethmeridian

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.

Meridethmeridian

I happen to have pre-emptively completed that exercise! I suppose the reason for needing this pattern is that GHC checks for exhaustive patterns only after type-checking? – Comparative

@AJFarmar I think part of what makes it tricky to know that "Cons a Nil doesn't match" implies "Cons a (Cons b _) does match" is that, in the presence of GADTs, it's not always clear that all constructors are type-correct possibilities, so it's not correct to simply try all the constructors not yet listed. For example, suppose that your lists had three constructors; which, if any, of the two remaining patterns' type equalities should be introduced on the right-hand side of last (Cons a Nil) = a; last (Cons a b) = {- here -}? – Meridethmeridian

@AJFarmar And, by the way, if you already have foldr and foldr1, you could consider last = foldr1 (\x y -> y). – Meridethmeridian

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

Mulct