Non-exhaustive pattern-match warning in code-example from "Dependently Typed Programming with Singletons"

[Herbert Valerio Riedel]

Hello *,

I've been experimenting with the code from the "Dependently Typed
Programming with Singletons" paper[1] from the following is derived (modulo some
irrelevant renamings):

    {-# LANGUAGE TypeOperators, DataKinds, GADTs, TypeFamilies #-}

    module CheckedList where
     
    data Nat = Z | S Nat
     
    data SNat n where
        SZ :: SNat Z
        SS :: SNat n -> SNat (S n)
     
    infixr 5 :-
    data List l t where
        Nil  :: List Z t
        (:-) :: t -> List l t -> List (S l) t
     
    type family n1 :< n2 where
        m     :< Z      = False
        Z     :< (S m)  = True
        (S n) :< (S m)  = n :< m
     
    index :: (i :< l) ~ True => List l t -> SNat i -> t
    index (x :- _)    SZ    = x
    index (_ :- xs)  (SS i) = index xs i

The problem, though, is that with the code above GHC 7.8.2 emits a
warning for the `index` function:

,----
| Pattern match(es) are non-exhaustive
| In an equation for ‘index’: Patterns not matched: Nil _
`----

So I would have expected to workaround that by explicitly wrapping the
length-phantom with the promoted `S` type-constructor, like so

    index :: (i :< S l) ~ True => List (S l) t -> SNat i -> t
    index (x :- _)    SZ    = x
    index (_ :- xs)  (SS i) = index xs i

While this would probably have silenced the pattern-match warning, I now
get a type-checking error I can't seem to get rid of:

,----
| Could not deduce (l1 ~ 'S l0) from the context ((i :< 'S l) ~ 'True)
|   bound by the type signature for
|              index :: (i :< 'S l) ~ 'True => List ('S l) t -> SNat i -> t
|
| or from ('S l ~ 'S l1)
|   bound by a pattern with constructor
|              :- :: forall t (l :: Nat). t -> List l t -> List ('S l) t,
|            in an equation for ‘index’
|
| or from (i ~ 'S n)
|   bound by a pattern with constructor
|              SS :: forall (n :: Nat). SNat n -> SNat ('S n),
|            in an equation for ‘index’
|
|   ‘l1’ is a rigid type variable bound by
|        a pattern with constructor
|          :- :: forall t (l :: Nat). t -> List l t -> List ('S l) t,
|        in an equation for ‘index’
|
| Expected type: List ('S l0) t
|   Actual type: List l1 t
| Relevant bindings include
|   xs :: List l1 t
|
| In the first argument of ‘index’, namely ‘xs’
| In the expression: index xs i
`----

Is there a way to tweak the code so that GHC doesn't think there's a
non-exhaustive pattern-match?

Cheers,
  HVR

 [1]: http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf