对类型具有算术约束的类型类实例

Question

基本上，我希望能够做这样的事情：

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
import GHC.TypeLits

newtype Foo (a::Nat) (b::Nat) c = Foo {getFoo :: c}

class Clz a where

instance Clz (Foo a (2*a) c) where

即，仅当 a = 2*b 时才使 Foo a b 成为 Clz 的实例。

我知道问题出在最后一行的(2*a) 表达式中。当我尝试编译它时，我得到：

• Illegal type synonym family application in instance:
    Foo a (2 * a) c
• In the instance declaration for ‘Clz (Foo a (2 * a) c)’

有没有办法克服这个问题？我需要如何更改语法？我需要更多语言扩展吗？我正在使用最新的 GHC (8.0.1)。

Answer 1

您可以使用类型等效约束（通过启用 GADT 或类型族）：

instance (b ~ (2 * a)) => Clz (Foo a b c) where

这是处理类型族的常用技术，如 other answer 所示。这个答案有更多解释：这个约束并不意味着完全与您想要的版本相同，但可能仍然适用于您的目的。