haskell - Checking if one type-level list contains another

Question

Is it possible to write a type-level function that returns True if one type-level list contains another type-level list?

Here is my attempt:

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

It works for simple cases:

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’

But what about cases like this?

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)

Answer 1

The trouble is that you've defined your subset type family by induction on the structure of the contained list, but you're passing in a totally polymorphic (unknown) list whose structure is a mystery to GHC. You might think that GHC would be able to use induction anyway, but you'd be wrong. In particular, just as every type has undefined values, so every kind has "stuck" types. A notable example, which GHC uses internally and exports through (IIRC) GHC.Exts:

{-# LANGUAGE TypeFamilies, PolyKinds #-}

type family Any :: k

The Any type family is in every kind. So you could have a type-level list Int ': Char ': Any, where Any is used at kind [*]. But there's no way to deconstruct the Any into ': or []; it doesn't have any such sensible form. Since type families like Any exist, GHC cannot safely use induction on types the way you wish.

If you want induction to work properly over type lists, you really need to use singletons or similar as Benjamin Hodgson suggests. Rather than passing just the type-level list, you need to pass also a GADT giving evidence that the type-level list is constructed properly. Recursively destructing the GADT performs induction over the type-level list.

The same sorts of limitations hold for type-level natural numbers.

data Nat = Z | S Nat
type family (x :: Nat) :+ (y :: Nat) :: Nat where
   'Z :+ y = y
   ('S x) :+ y = 'S (x :+ y)

data Natty (n :: Nat) where
  Zy :: Natty 'Z
  Sy :: Natty n -> Natty ('S n)

You might wish to prove

associative :: p1 x -> p2 y -> p3 z -> ((x :+ y) :+ z) :~: (x :+ (y :+ z))

but you can't, because this requires induction on x and y. You can, however, prove

associative :: Natty x -> Natty y -> p3 z -> ((x :+ y) :+ z) :~: (x :+ (y :+ z))

with no trouble.