To alleviate this we’re looking into ways to abstract this away.
To start, we would like do define something like
class Some t where
type SomeT t
useSome :: (forall a. t a -> c) -> SomeT t -> c
This fails when we try to write instance Some Foo because Foo has two type parameters, while, in the definition of Some, t is required to have only one.
We noticed that we could work around this issue by rewriting Foo as
data Foo' (c :: (Type, Type))
but I was wondering if there were more generic way to approach the issue.
I suspect this may be an XY problem. Perhaps if you explain what the code does you can get help to find a simpler implementation?
Regarding your question, you can define a different data type for each number of type variables. Something like this:
data Some1 f = forall a. Some1 (f a)
useSome1 :: (forall a. f a -> r) -> Some1 f -> r
useSome1 k (Some1 f) = k f
data Some2 f = forall a b. Some2 (f a b)
useSome2 :: (forall a b. f a b -> r) -> Some2 f -> r
useSome2 k (Some2 f) = k f
data Some3 ...
data Foo = forall a. Foo a
data Bar = forall b. Bar b
data Baz = forall c. Baz c
stuff :: Foo -> Bar -> Baz -> ()
stuff foo bar baz = runIdentity do
Foo a <- pure foo
Bar b <- pure bar
Baz c <- pure baz
pure ()
If you are not bothered by a slight performance and verbosity overhead, you can try something like this:
{-# LANGUAGE GADTs #-}
module Some
( Some (..),
Uncurry (..),
some2,
fail,
(>>=),
)
where
import Prelude hiding ((>>=))
data Some f = forall a. Some (f a)
(>>=) :: Some f -> (forall a. f a -> r) -> r
(Some x) >>= k = k x
data Uncurry f t where
UC :: {getUncurry :: f a b} -> Uncurry f (a, b)
some2 :: f a b -> Some (Uncurry f)
some2 x = Some (UC x)
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QualifiedDo #-}
import Some
data Foo1 a = Foo1 Int
data Foo2 a b = Foo2 Int
test :: Int
test = Some.do
Foo1 n <- Some (Foo1 1)
UC (Foo2 m) <- some2 (Foo2 2)
n + m