Ist es möglich, eine Funktion auf Typebene zu schreiben, die @ zurückgibTrue Wenn eine Liste auf Typebene eine andere Liste auf Typebene enthält?

Hier ist mein Versuch:

{-# 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

Es funktioniert für einfache Fälle:

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’

Aber was ist mit solchen Fällen?

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)