Constrain a type family constraint to be "some pair"

Question

Consider the following, where I'm trying to say "a is a pair":

type family F t a :: Constraint
type instance F Int a = (a ~ (a1, a2))

This doesn't work because both a1 and a2 are not in scope, but is there any way to express this?

Of course in a function signature I can write constraints like (a ~ (a1, a2)) even when a1 and a2 are not mentioned elsewhere, but I need to put this in an instance function signature, which is of course determined by the class. And a in this case is not a parameter to the instance itself, just the instance function, much like Functor only has f as a class parameter, not a and b, so I can't add extra constraints to the instance clause.

Answer 1

Yes! You can do this!

Strong, somewhat built-up version

First, a couple of useful type families:

type family Fst a where
  Fst (x,y) = x

type family Snd a where
  Snd (x,y) = y

Now the one you're after:

type IsPair a = a ~ (Fst a, Snd a)

Here's a test:

type family Con a where
  Con (f x y) = f

test :: IsPair a => proxy a -> Con a :~: (,)
test _ = Refl

And an even simpler one that turns out to test a stronger property:

 test1 :: IsPair a => a -> Fst a
 test1 = fst

And just to make sure it's satisfied when it should be:

data Dict c where
  Dict :: c => Dict c

test2 :: Dict (IsPair (a, b))
test2 = Dict

You can, of course, use this to define your F:

type family F t a
type instance F Int a = IsPair a

Much simpler, but much less powerful

type family Con a where
  Con (f x y) = f
type IsPair a = Con a ~ (,)

The trouble with this one, compared to the first approach, is that it doesn't actually win you the glorious knowledge that a ~ (Fst a, Snd a). So it makes a statement, but you can't do a whole heck of a lot with it.

A little generalization

Why just pairs? If you toss PolyKinds into the mix, you can get very general:

type family Arg1 a where Arg1 (f x) = x
type family Arg2 a where Arg2 (f y x) = y
type family Arg3 a where Arg3 (f z y x) = z
type family Arg4 a where Arg4 (f w z y x) = w

type family IsF (f :: k) (a :: *) :: Constraint
type instance IsF f a = a ~ f (Arg1 a)
type instance IsF f a = a ~ f (Arg2 a) (Arg1 a)
type instance IsF f a = a ~ f (Arg3 a) (Arg2 a) (Arg1 a)
type instance IsF f a = a ~ f (Arg4 a) (Arg3 a) (Arg2 a) (Arg1 a)

You can do this without PolyKinds too, but then you need IsF1, IsF2, etc.

With this in place,

type IsPair a = IsF (,) a
type IsMaybe a = IsF Maybe a
...

Tests for the generalization (this stuff only works for GHC 7.10 or later; polykinds is too flaky before that).

data Dict c where
  Dict :: c => Dict c

test1 :: Dict (IsF f (f a))
test1 = Dict

test2 :: Dict (IsF f (f a b))
test2 = Dict

test3 :: Dict (IsF f (f a b c))
test3 = Dict

test4 :: Dict (IsF f (f a b c d))
test4 = Dict