haskell - 如何让 GHC 为上下文中具有 Typeable 的 GADT 生成 Data.Typeable 实例？

Question

假设我有以下代码:

{-# LANGUAGE GADTs, DeriveDataTypeable, StandaloneDeriving #-}
import Data.Typeable

class Eq t => OnlyEq t
class (Eq t, Typeable t) => BothEqAndTypeable t

data Wrapper a where
    Wrap :: BothEqAndTypeable a => a -> Wrapper a

deriving instance Eq (Wrapper a)
deriving instance Typeable1 Wrapper

然后，以下实例声明将起作用，没有对 t 的约束:

instance OnlyEq (Wrapper t)

并执行我期望的操作。

<小时/>

但是以下实例声明不起作用:

instance BothEqAndTypeable (Wrapper t)

自从 GHC - 我使用 7.6.1 - 提示:

No instance for (Typeable t)
  arising from the superclasses of an instance declaration
Possible fix:
  add (Typeable t) to the context of the instance declaration
In the instance declaration for `BothEqAndTypeable (Wrapper t)'

当然，将 Typeable t 添加到上下文中是可行的。但添加以下实例也是如此:

instance Typeable (Wrapper t) where
    typeOf (Wrap x) = typeOf1 (Wrap x) `mkAppTy` typeOf x

有没有办法让 GHC 为我编写后一个实例？如果是这样，怎么办？如果没有，为什么不呢？

我希望 GHC 能够从 Wrap 构造函数的上下文中提取 Typeable 约束，就像它对 Eq 所做的那样> 约束。 我认为我的问题归结为这样一个事实:GHC 明确禁止编写 派生实例 Typeable (Wrapper t) 和标准 (Typeable1 s, Typeable a) => Typeable (s a) 实例无法“查看”s a 来查找可键入 a 字典。

Answer 1

I was hoping GHC would be able to pull the Typeable constraint from the context on the Wrap constructor

如果它有一个 Wrap 构造函数，它可以从中提取 Typeable 约束。

但它没有 Wrap 构造函数。

不同之处在于 Eq 实例使用该值，因此它是一个 Wrap some，其中 Wrap 构造函数使 >Eq 可用包装类型字典，一切都很好，或者是 ⊥，然后一切也都很好，评估 x == y 触底.

注意派生

instance Eq (Wrapper a)

类型变量a没有有Eq约束吗？

Prelude DerivT> (undefined :: Wrapper (Int -> Int)) == undefined
*** Exception: Prelude.undefined
Prelude DerivT> (undefined :: (Int -> Int)) == undefined

<interactive>:3:29:
    No instance for (Eq (Int -> Int)) arising from a use of `=='
    Possible fix: add an instance declaration for (Eq (Int -> Int))
    In the expression: (undefined :: Int -> Int) == undefined
    In an equation for `it':
        it = (undefined :: Int -> Int) == undefined

但是 Typeable 实例不得使用该值，因此如果提供的值不是 Wrap Something，则不会触底。

因此派生的实例 Typeable1 Wrapper 提供了

instance Typeable t => Typeable (Wrapper t)

但不是无约束的

instance Typeable (Wrapper t)

并且该不受约束的实例无法通过 GHC 导出。

因此你必须提供一个约束

instance Typeable t => BothEqAndTypeable (Wrapper t)

或者无约束

instance Typeable (Wrapper t)

你自己。