Comprobando si una lista de nivel de tipo contiene otra

¿Es posible escribir una función de nivel de tipo que devuelvaTrue si una lista de nivel de tipo contiene otra lista de nivel de tipo?

Aquí está mi intento:

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module TypePlayground where

import Data.Type.Bool

type family InList (x :: *) (xs :: [*]) where
    InList x '[] = 'False
    InList x (x ': xs) = 'True
    InList x (a ': xs) = InList x xs
type family ListContainsList (xs :: [*]) (ys :: [*]) where
    ListContainsList xs (y ': ys) = InList y xs && ListContainsList xs ys
    ListContainsList xs '[] = 'True

Funciona para casos simples:

data A
data B
data C

test1 :: (ListContainsList '[A, B, C] '[C, A] ~ 'True) => ()
test1 = ()
-- compiles.
test2 :: (ListContainsList '[A, B, C] '[B, C, A] ~ 'True) => ()
test2 = ()
-- compiles.
test3 :: (ListContainsList (A ': B ': '[C]) (B ': A ': '[C]) ~ 'True) => ()
test3 = ()
-- compiles.
test4 :: (ListContainsList '[A, C] '[B, C, A] ~ 'True) => ()
test4 = ()
-- Couldn't match type ‘'False’ with ‘'True’

¿Pero qué pasa con casos como este?

test5 :: (ListContainsList (A ': B ': a) a ~ 'True) => ()
test5 = ()
-- Should compile, but fails:
-- Could not deduce (ListContainsList (A : B : a0) a0 ~ 'True)
-- from the context (ListContainsList (A : B : a) a ~ 'True)

Respuestas a la pregunta(2)

Su respuesta a la pregunta