Polymorphic functions over chains of nested tuples

Question

Suppose I have a list of types, of kind [*]:

let Ts = '[Int, Bool, Char]

I want to convert this to a chain of tuples:

type family Tupled (ts :: [*]) z :: *
type instance Tupled (t ': ts) z = (t, Tupled ts z)
type instance Tupled '[] z = z

So far so good:

> :kind! Tupled Ts ()
Tupled Ts () :: *
= (Int, (Bool, (Char, ())))

Now I’d like to be able to write a type Fun to represent functions that are polymorphic in the “bottom” of this chain. For example, Fun Ts Ts should work on either of these types:

(Int, (Bool, (Char, (String, ()))))
(Int, (Bool, (Char, (Word, (ByteString, ())))))

I tried this:

newtype Fun as bs = Fun
  { unfun :: forall z. Tupled as z -> Tupled bs z }

But it fails to typecheck:

Couldn't match type ‘Tupled bs z’ with ‘Tupled bs z0’
NB: ‘Tupled’ is a type function, and may not be injective
The type variable ‘z0’ is ambiguous
Expected type: Tupled as z -> Tupled bs z
  Actual type: Tupled as z0 -> Tupled bs z0
In the ambiguity check for the type of the constructor ‘Fun’:
  Fun :: forall z. Tupled as z -> Tupled bs z
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the definition of data constructor ‘Fun’
In the newtype declaration for ‘Fun’

I’ve seen recommendations to use a data family to avoid problems with injectivity:

data family Tupled (ts :: [*]) z :: *
data instance Tupled (t ': ts) z = Cons t (Tupled ts z)
data instance Tupled '[] z = Nil

And indeed that makes Fun compile, but it looks like that gets me “stuck” in the land of Cons and Nil when I’m looking to work with tuples, like this:

Fun $ \ (i, (b, (c, z))) -> (succ i, (not b, (pred c, z)))

Can I work around this somehow?

Answer 1

Enable AllowAmbiguousTypes. From GHC 8, the ambiguity check is completely superfluous, because any (fundamentally resolvable) ambiguity can be resolved with type applications. Also, your case seems to be just a false positive for ambiguity check, since we can clearly use Fun even without type applications.