GHCi 派生类型在手动编写时会导致编译错误

Question

请考虑以下代码：

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
import GHC.Exts (Constraint)
data Poly (c :: * -> Constraint) where
  Poly :: { getPoly :: (forall a. c a => a) } -> Poly c
type family Arg1 a where
  Arg1 (a -> _) = a
type family Result a where
  Result (_ -> a) = a
type IsOneArgFunc a = a ~ (Arg1 a -> Result a)
type NegateConstraint a = (IsOneArgFunc a, Real (Result a), Arg1 a ~ Result a)
class NegateConstraint a => NegateConstraintC a
instance NegateConstraint a => NegateConstraintC a
polyNegate :: Poly NegateConstraintC
polyNegate = Poly negate
testOp f x y = toRational (getPoly f x) == toRational (getPoly f y)
main = do
  print $ testOp polyNegate (2 :: Float) (2 :: Double)

(注意：部分是从我的多边形数据和索引类型包中提取的，但我提取了下面的代码以避免依赖(：

这编译和运行得很好。

请注意，testOp 没有类型签名。

将其加载到ghci并询问:t testOp我得到以下内容：

testOp
  :: (Real a1, Real a, c (t1 -> a1), c (t -> a)) =>
     Poly c -> t1 -> t -> Bool

这似乎是一个合理的推导类型。但是，当我将其复制到代码中时，如下所示：

testOp
  :: (Real a1, Real a, c (t1 -> a1), c (t -> a)) =>
     Poly c -> t1 -> t -> Bool
testOp f x y = toRational (getPoly f x) == toRational (getPoly f y)

我收到一堆错误：

• Could not deduce (Real a0) arising from a use of ‘toRational’
  from the context: (Real a2, Real a, c (t1 -> a2), c (t -> a))
    bound by the type signature for:
               testOp :: (Real a2, Real a, c (t1 -> a2), c (t -> a)) =>
                         Poly c -> t1 -> t -> Bool
    at polyerror.hs:(31,1)-(33,30)
  The type variable ‘a0’ is ambiguous
  These potential instances exist:
    instance Real Integer -- Defined in ‘GHC.Real’
    instance Real Double -- Defined in ‘GHC.Float’
    instance Real Float -- Defined in ‘GHC.Float’
    ...plus two others
    ...plus two instances involving out-of-scope types
    (use -fprint-potential-instances to see them all)
• In the first argument of ‘(==)’, namely
    ‘toRational (getPoly f x)’
  In the expression:
    toRational (getPoly f x) == toRational (getPoly f y)
  In an equation for ‘testOp’:
      testOp f x y = toRational (getPoly f x) == toRational (getPoly f y)
• Could not deduce: c (t1 -> a0) arising from a use of ‘getPoly’
  from the context: (Real a2, Real a, c (t1 -> a2), c (t -> a))
    bound by the type signature for:
               testOp :: (Real a2, Real a, c (t1 -> a2), c (t -> a)) =>
                         Poly c -> t1 -> t -> Bool
    at polyerror.hs:(31,1)-(33,30)
• In the first argument of ‘toRational’, namely ‘(getPoly f x)’
  In the first argument of ‘(==)’, namely ‘toRational (getPoly f x)’
  In the expression:
    toRational (getPoly f x) == toRational (getPoly f y)
• Relevant bindings include
    x :: t1 (bound at polyerror.hs:34:10)
    f :: Poly c (bound at polyerror.hs:34:8)
    testOp :: Poly c -> t1 -> t -> Bool (bound at polyerror.hs:34:1)
• Could not deduce (Real a1) arising from a use of ‘toRational’
  from the context: (Real a2, Real a, c (t1 -> a2), c (t -> a))
    bound by the type signature for:
               testOp :: (Real a2, Real a, c (t1 -> a2), c (t -> a)) =>
                         Poly c -> t1 -> t -> Bool
    at polyerror.hs:(31,1)-(33,30)
  The type variable ‘a1’ is ambiguous
  These potential instances exist:
    instance Real Integer -- Defined in ‘GHC.Real’
    instance Real Double -- Defined in ‘GHC.Float’
    instance Real Float -- Defined in ‘GHC.Float’
    ...plus two others
    ...plus two instances involving out-of-scope types
    (use -fprint-potential-instances to see them all)
• In the second argument of ‘(==)’, namely
    ‘toRational (getPoly f y)’
  In the expression:
    toRational (getPoly f x) == toRational (getPoly f y)
  In an equation for ‘testOp’:
      testOp f x y = toRational (getPoly f x) == toRational (getPoly f y)
• Could not deduce: c (t -> a1) arising from a use of ‘getPoly’
  from the context: (Real a2, Real a, c (t1 -> a2), c (t -> a))
    bound by the type signature for:
               testOp :: (Real a2, Real a, c (t1 -> a2), c (t -> a)) =>
                         Poly c -> t1 -> t -> Bool
    at polyerror.hs:(31,1)-(33,30)
• In the first argument of ‘toRational’, namely ‘(getPoly f y)’
  In the second argument of ‘(==)’, namely ‘toRational (getPoly f y)’
  In the expression:
    toRational (getPoly f x) == toRational (getPoly f y)
• Relevant bindings include
    y :: t (bound at polyerror.hs:34:12)
    f :: Poly c (bound at polyerror.hs:34:8)
    testOp :: Poly c -> t1 -> t -> Bool (bound at polyerror.hs:34:1)

是否有我可以手动为testOp编写的类型签名，该类型签名作为推断的签名是通用的，如果有，它是什么？如果不是，是设计使然，某些函数无法在不失去通用性的情况下为其编写手动类型签名，还是这是一个 GHC 错误(我目前正在使用 8.0.2(？

Answer 1

是的，您可以为其提供该类型签名，但您需要给它一些提示，说明签名中的类型如何与代码中的表达式相对应。打开ScopedTypeVariables ;然后进行以下编译：

testOp
  :: forall a1 a t1 t c.
     (Real a1, Real a, c (t1 -> a1), c (t -> a)) =>
     Poly c -> t1 -> t -> Bool
testOp f x y = toRational (getPoly f x :: a1) == toRational (getPoly f y :: a)

toRational . getPoly f模棱两可的原因与show . read基本相同，这里的解决方案是类似的。对于show . read，您在某处提供了一个类型签名来修复read的返回类型，对于您的示例，我给出了一个修复getPoly f返回类型的类型签名。