SomeDictN.hs

class SomeDictNC n k c | n -> k, c -> k where
  data SomeDictN n k c :: Type

instance k ~ Constraint => SomeDictNC 0 k c where
  data SomeDictN 0 k c where
    SomeDict0 :: c => SomeDictN 0 k c

instance (k ~ (k1 -> Constraint), SomeDictNC 1 k c) => SomeDictNC 1 k c where
  data SomeDictN 1 k c where
    SomeDict1 :: c a => Proxy a -> SomeDictN 1 k c

instance (k ~ (k1 -> k2 -> Constraint), SomeDictNC 2 k c) => SomeDictNC 2 k c where
  data SomeDictN 2 k c where
    SomeDict2 :: c a b => Proxy a -> Proxy b -> SomeDictN 2 k c

w :: [SomeDictN _ _ HasCallStack]
w = [SomeDict0]

x :: [SomeDictN _ _ Ord]
x = [SomeDict1 (Proxy @Int)]

y :: [SomeDictN _ _ Monad]
y = [SomeDict1 (Proxy @IO)]

class Foo a b
instance Foo Int Bool

z :: [SomeDictN _ _ Foo]
z = [SomeDict2 (Proxy @Int) (Proxy @Bool)]