如何使用通过实例约束的函数依赖关系确定的类型参数作为关联类型族方程的 RHS？

问题描述

我有一个这样的类型类：

class (Coercible a b) => Foo a b | a -> b

我想声明以下 Generic 实例：

data Thing a
  where
  Thing :: Foo a b => b -> Thing a

-- If the @b@ uniquely determined by @a@ is @Generic@,so is @Thing a@ ...
instance (Foo a b,Generic b) => Generic (Thing a)
  where
  type Rep (Thing a) = Rep b

不幸的是这不能编译，错误信息是：

[typecheck] [E] • Type variable ‘r’ is mentioned in the RHS,but not bound on the LHS of the family instance
• In the type instance declaration for ‘Rep’
  In the instance declaration for ‘Generic (UnvalidatedData v)’

我知道我想要的在语义层面上是可能的，因为如果我使用类型族而不是函数依赖，如下所示：

class (Coercible a (B a)) => Foo' a
  where
  type B a :: Type

我可以声明：

data Thing a
  where
  Thing :: Foo' a => B a -> Thing a

-- If the @B a@ uniquely determined by @a@ is @Generic@,so is @Thing a@ ...
instance (Foo' a,Generic (B a)) => Generic (Thing a)
  where
  type Rep (Thing a) = Rep (B a)

不幸的是，关联的类型家族根本没有出现在类型类的种类中，因此在传递类时不可能对关联的类型家族进行高阶推理。出于这个原因，我更喜欢使用函数依赖而不是类型族。

使用多参数类型类的 Foo、Thing 和 Thing 的 Generic 实例的最接近的工作近似值是什么（如果有的话）？

解决方法

我能想到的最好方法是同时使用函数依赖和类型系列，并尝试获得两全其美的情况：

class (Coercible a b,b ~ B a) => Foo a b | a -> b where
  type B a :: Type

data Thing a where
  Thing :: Foo a b => b -> Thing a

instance (Foo a b,Generic b) => Generic (Thing a) where
  type Rep (Thing a) = Rep (B a)

这不是超级优雅，但是在 b ~ B a 的约束中使用 Foo 意味着您不会意外地搞砸 Foo 的实例。例如，你可以这样写：

instance Foo (Sum a) a where
  type B (Sum a) = a

但是如果您尝试编写 type B (Sum a) = Int，则会收到错误 arising from the superclasses of an instance declaration。