Prove type-level list's associativity (without singletons)

assoc.hs

#!/usr/bin/env runghc

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Proxy
import Data.Type.Equality

data SList f xs where
  SNil :: SList f '[]
  SCons :: f h -> SList f t -> SList f (h ': t)

type SList' = SList Proxy

class KnownList xs where
  listSing :: SList' xs

instance KnownList '[] where
  listSing = SNil

instance KnownList xs => KnownList (x ': xs) where
  listSing = SCons Proxy listSing

type family xs ++ ys where
  '[] ++ xs = xs
  (x ': xs) ++ ys = x ': (xs ++ ys)

rnilS :: SList' xs -> xs ++ '[] :~: xs
rnilS SNil = Refl
rnilS (SCons _ t) = case rnilS t of Refl -> Refl

rnil :: KnownList xs => xs ++ '[] :~: xs
rnil = rnilS listSing

assocS :: SList' xs -> proxy1 ys -> proxy2 zs -> (xs ++ ys) ++ zs :~: xs ++ (ys ++ zs)
assocS SNil _ _ = Refl
assocS (SCons _ t) ys zs = case assocS t ys zs of Refl -> Refl

assoc :: forall xs ys zs. KnownList xs => (xs ++ ys) ++ zs :~: xs ++ (ys ++ zs)
assoc = assocS (listSing @xs) (Proxy @ys) (Proxy @zs)

main :: IO ()
main = pure ()