Lifted list append is associative

AppendAssoc.hs

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

import Data.Type.Equality

type family (++) (xs :: [*]) (ys :: [*]) where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)
 
data SList (xs :: [*]) where
  Nil  :: SList '[]
  Succ :: SList xs -> SList (x ': xs)
 
appAssoc ::
  SList xs -> SList ys -> SList zs ->
  (xs ++ (ys ++ zs)) :~: ((xs ++ ys) ++ zs)
appAssoc Nil ys zs = Refl
appAssoc (Succ xs) ys zs =
  case appAssoc xs ys zs of Refl -> Refl
 
class WitnessList (xs :: [*]) where
  witness :: SList xs
 
instance WitnessList '[] where
  witness = Nil
 
instance WitnessList xs => WitnessList (x ': xs) where
  witness = Succ witness