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

Question

我有一个这样的类型类:

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使用多参数类型类的实例？

Answer 1

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

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)

不是 super 优雅，而是使用 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 .