haskell - 嵌套元组链上的多态函数

Question

假设我有一个类型列表 [*] :

let Ts = '[Int, Bool, Char]

我想将其转换为元组链:

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

到现在为止还挺好:

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

现在我想写一个类型 Fun表示在该链的“底部”中具有多态性的函数。例如， Fun Ts Ts应该适用于以下任何一种类型:

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

我试过这个:

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

但它无法进行类型检查:

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’

我已经看到了使用数据族来避免单射性问题的建议:

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

确实，这使得 Fun编译，但看起来这让我“卡”在 Cons 的土地上和 Nil当我想使用元组时，像这样:

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

我可以以某种方式解决这个问题吗？

Answer 1

启用 AllowAmbiguousTypes .从 GHC 8 开始，歧义检查完全是多余的，因为任何(基本上可解决的)歧义都可以通过类型应用程序解决。此外，您的情况似乎只是歧义检查的误报，因为我们可以清楚地使用 Fun即使没有类型应用程序。