Proving a type inequality to GHC

Question

For educational purposes, I have been trying to reconstruct an example from the book "Type-Driven Development with Idris" (namely RemoveElem.idr) in Haskell via use of various language extensions and singleton types. The gist of it is a function that removes an element from a non-empty vector, given a proof that the element is in fact in the vector. The following code is self-contained (GHC 8.4 or later). The problem appears at the very end:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind
import Data.Type.Equality
import Data.Void

-- | Inductively defined natural numbers.
data Nat = Z | S Nat deriving (Eq, Show)

-- | Singleton types for natural numbers.
data SNat :: Nat -> Type where
    SZ :: SNat 'Z
    SS :: SNat n -> SNat ('S n)

deriving instance Show (SNat n)

-- | "Demote" a singleton-typed natural number to an ordinary 'Nat'.
fromSNat :: SNat n -> Nat
fromSNat SZ = Z
fromSNat (SS n) = S (fromSNat n)

-- | A decidable proposition.
data Dec a = Yes a | No (a -> Void)

-- | Propositional equality of natural numbers.
eqSNat :: SNat a -> SNat b -> Dec (a :~: b)
eqSNat  SZ     SZ    = Yes Refl
eqSNat  SZ    (SS _) = No (\case {})
eqSNat (SS _)  SZ    = No (\case {})
eqSNat (SS a) (SS b) = case eqSNat a b of
    No  f    -> No (\case Refl -> f Refl)
    Yes Refl -> Yes Refl

-- | A length-indexed list (aka vector).
data Vect :: Nat -> Type -> Type where
    Nil   :: Vect 'Z a
    (:::) :: a -> Vect n a -> Vect ('S n) a

infixr 5 :::

deriving instance Show a => Show (Vect n a)

-- | @Elem a v@ is the proposition that an element of type @a@
-- is contained in a vector of type @v@. To be useful, @a@ and @v@
-- need to refer to singleton types.
data Elem :: forall a n. a -> Vect n a -> Type where
    Here  :: Elem x (x '::: xs)
    There :: Elem x xs -> Elem x (y '::: xs)

deriving instance Show a => Show (Elem a v)

------------------------------------------------------------------------
-- From here on, to simplify things, only vectors of natural
-- numbers are considered.

-- | Singleton types for vectors of 'Nat's.
data SNatVect :: forall n. Nat -> Vect n Nat -> Type where
    SNatNil  :: SNatVect 'Z 'Nil
    SNatCons :: SNat a -> SNatVect n v -> SNatVect ('S n) (a '::: v)

deriving instance Show (SNatVect n v)

-- | "Demote" a singleton-typed vector of 'SNat's to an
-- ordinary vector of 'Nat's.
fromSNatVect :: SNatVect n v -> Vect n Nat
fromSNatVect SNatNil = Nil
fromSNatVect (SNatCons a v) = fromSNat a ::: fromSNatVect v

-- | Decide whether a value is in a vector.
isElem :: SNat a -> SNatVect n v -> Dec (Elem a v)
isElem _  SNatNil        = No (\case {})
isElem a (SNatCons b as) = case eqSNat a b of
    Yes Refl   -> Yes Here
    No notHere -> case isElem a as of
        Yes there   -> Yes (There there)
        No notThere -> No $ \case
            Here        -> notHere Refl
            There there -> notThere there

type family RemoveElem (a :: Nat) (v :: Vect ('S n) Nat) :: Vect n Nat where
    RemoveElem a (a '::: as) = as
    RemoveElem a (b '::: as) = b '::: RemoveElem a as

-- | Remove a (singleton-typed) element from a (non-empty, singleton-typed)
-- vector, given a proof that the element is in the vector.
removeElem :: forall (a :: Nat) (v :: Vect ('S n) Nat)
    . SNat a
    -> Elem a v
    -> SNatVect ('S n) v
    -> SNatVect n (RemoveElem a v)
removeElem x prf (SNatCons y ys) = case prf of
    Here        -> ys
    There later -> case ys of
        SNatNil    -> case later of {}
        SNatCons{} -> SNatCons y (removeElem x later ys)
            -- ^ Could not deduce:
            --            RemoveElem a (y '::: (a2 '::: v2))
            --          ~ (y '::: RemoveElem a (a2 '::: v2))

Apparently, the type system needs convincing that the types of the values x and y cannot possibly be equal in that branch of the code, so that the second equation of the type family can be used unambiguously to reduce the return type as required. I don't know how to do that. Naively, I would like the constructor There and thus the pattern match on There later to carry / reveal a proof of the type inequality to GHC.

The following is an obviously redundant and partial solution that just demonstrates the type inequality that is needed in order for GHC to type-check the recursive call:

        SNatCons{} -> case (x, y) of
            (SZ, SS _) -> SNatCons y (removeElem x later ys)
            (SS _, SZ) -> SNatCons y (removeElem x later ys)

Now e.g. this works:

λ> let vec = SNatCons SZ (SNatCons (SS SZ) (SNatCons SZ SNatNil))
λ> :t vec
vec
  :: SNatVect ('S ('S ('S 'Z))) ('Z '::: ('S 'Z '::: ('Z '::: 'Nil)))
λ> let Yes prf = isElem (SS SZ) vec
λ> :t prf
prf :: Elem ('S 'Z) ('Z '::: ('S 'Z '::: ('Z '::: 'Nil)))
λ> let vec' = removeElem (SS SZ) prf vec
λ> :t vec'
vec' :: SNatVect ('S ('S 'Z)) ('Z '::: ('Z '::: 'Nil))
λ> fromSNatVect vec'
Z ::: (Z ::: Nil)

Resolution

As hinted at in @chi's comment and elaborated in HTNW's answer, I was trying to solve the wrong problem by writing removeElem with the above type signature and type family, and if I would have been able to, the resulting program would have been ill-typed.

The following are the corrections I made based on HTNW's answer (you may want to read it before continuing here).

The first mistake, or unnecessary complication, was to repeat the length of the vector in SNatVects type. I thought it necessary in order to write fromSNatVect, but it certainly isn't:

data SNatVect (v :: Vect n Nat) :: Type where
    SNatNil  :: SNatVect 'Nil
    SNatCons :: SNat a -> SNatVect v -> SNatVect (a '::: v)

deriving instance Show (SNatVect v)

fromSNatVect :: forall (v :: Vect n Nat). SNatVect v -> Vect n Nat
-- implementation unchanged

Now there are two approaches to writing removeElem. The first takes an Elem, an SNatVect and returns a Vect:

removeElem :: forall (a :: Nat) (n :: Nat) (v :: Vect ('S n) Nat)
    . Elem a v
    -> SNatVect v
    -> Vect n Nat
removeElem prf (SNatCons y ys) = case prf of
    Here        -> fromSNatVect ys
    There later -> case ys of
        SNatNil    -> case later of {}
        SNatCons{} -> fromSNat y ::: removeElem later ys

The second takes an SElem, an SNatVect and returns an SNatVect, using a RemoveElem type family that mirrors the value-level function:

data SElem (e :: Elem a (v :: Vect n k)) where
    SHere  :: forall x xs. SElem ('Here :: Elem x (x '::: xs))
    SThere :: forall x y xs (e :: Elem x xs). SElem e -> SElem ('There e :: Elem x (y '::: xs))

type family RemoveElem (xs :: Vect ('S n) a) (e :: Elem x xs) :: Vect n a where
    RemoveElem (x '::: xs) 'Here = xs
    RemoveElem (x '::: xs) ('There later) = x '::: RemoveElem xs later

sRemoveElem :: forall (xs :: Vect ('S n) Nat) (e :: Elem x xs)
    . SElem e
    -> SNatVect xs
    -> SNatVect (RemoveElem xs e)
sRemoveElem prf (SNatCons y ys) = case prf of
    SHere        -> ys
    SThere later -> case ys of
        SNatNil    -> case later of {}
        SNatCons{} -> SNatCons y (sRemoveElem later ys)

Interestingly, both versions do away with passing the element to remove as a separate argument, since that information is contained in the Elem / SElem value. The value argument can also be removed from the Idris version of that function, though then the removeElem_auto variant may be a bit confusing, as it will then only have the vector as an explicit argument and remove the first element of the vector if the implicit prf argument is not explicitly used with a different proof.

Answer 1

Consider [1, 2, 1]. RemoveElem 1 [1, 2, 1] is [2, 1]. Now, the call removeElem 1 (There $ There $ Here) ([1, 2, 1] :: SNatVect 3 [1, 2, 1]) :: SNatVect 2 [2, 1], should compile. This is wrong. The Elem argument says to delete the third element, which would give [1, 2], but the type signature says it must be a [2, 1].

First, SNatVect is a bit broken. It has two Nat arguments:

data SNatVect :: forall n. Nat -> Vect n a -> Type where ...

The first is n, and the second is the unnamed Nat. By the structure of SNatVect, they are always equal. It allows an SNatVect to double as an equality proof, but it's probably not the intention to have it that way. You probably meant

data SNatVect (n :: Nat) :: Vect n Nat -> Type where ...

There is no way to write this signature in source Haskell using just the normal -> syntax. However, when GHC prints this type, you sometimes get

SNatVect :: forall (n :: Nat) -> Vect n Nat -> Type

But this is redundant. You can take the Nat as an implicit forall argument, and have it inferred from the Vects type:

data SNatVect (xs :: Vect n Nat) where
  SNatNil  :: SNatVect 'Nil
  SNatCons :: SNat x -> SNatVect xs -> SNatVect (x '::: xs)

This gives

SNatVect :: forall (n :: Nat). Vect n Nat -> Type

Second, try writing

removeElem :: forall (n :: Nat) (x :: Nat) (xs :: Vect (S n) Nat).
              Elem x xs -> SNatVect xs -> Vect n Nat

Note how the SNat argument is gone, and how the return type is a simple Vect. The SNat argument made the type "too big", so you got caught up making it sort of work when the function just wouldn't make sense. The SNatVect return type meant you were skipping steps. Roughly, every function has three forms: the basic one, f :: a -> b -> c; the type-level one, type family F (x :: a) (y :: b) :: c; and the dependent one, f :: forall (x :: a) (y :: b). Sing x -> Sing y -> Sing (F x y). Each is implemented in the "same" way, but trying to implement one without implementing its predecessors is a surefire way to get confused.

Now, you can lift this up a little bit:

data SElem (e :: Elem x (xs :: Vect n k)) where
  SHere :: forall x xs. SElem ('Here :: Elem x (x '::: xs))
  SThere :: forall x y xs (e :: Elem x xs). SElem e -> SElem ('There e :: Elem x (y '::: xs))

type family RemoveElem (xs :: Vect (S n) a) (e :: Elem x xs) :: Vect n a

Take note of the relationship between the types of removeElem and RemoveElem. The reordering of the arguments is because the type of e depends on xs, so they need to be ordered accordingly. Alternatively: the xs argument was promoted from forall'd-and-implicitly-given to explicitly-given, and then the Sing xs argument was nixed because it contained no information, due to being a singleton.

Finally, you can write this function:

sRemoveElem :: forall (xs :: Vect (S n) Nat) (e :: Elem x xs).
               SElem e -> SNatVect xs -> SNatVect (RemoveElem xs e)