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

assoc.hs

#!/usr/bin/env stack
-- stack --resolver lts-16.5 script --package singletons

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

import Data.Proxy
import Data.Type.Equality
import Data.Singletons ( Sing, SingI(..) )
import Data.Singletons.Prelude.List ( SList(..) )

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

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

rnil :: SingI xs => xs ++ '[] :~: xs
rnil = rnilS sing

assocS :: Sing 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. SingI xs => (xs ++ ys) ++ zs :~: xs ++ (ys ++ zs)
assoc = assocS (sing @xs) (Proxy @ys) (Proxy @zs)

main :: IO ()
main = pure ()