类型应用程序和约束种类

Question

(我不完全熟悉Haskell约束求解器的内部工作原理,所以这可能是一个新手问题.)

尝试在GHC 8.0.1上使用类型应用程序时,如以下示例代码所示

{-# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, ScopedTypeVariables, TypeApplications #-}
module Test where

import Data.Constraint

test0 :: forall (b :: *) . (forall a . a -> Bool) -> b -> Bool
test0 g = g @b

test1 :: forall (c :: * -> Constraint) (b :: *) . (c b) => (forall a . c a => a -> Bool) -> b -> Bool
test1 g = g @b

它给了我以下错误

• Could not deduce: c0 b
  from the context: c b
    bound by the type signature for:
               test1 :: c b => (forall a. c a => a -> Bool) -> b -> Bool
    at Test.hs:9:10-101
• In the ambiguity check for ‘test1’
  To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
  In the type signature:
    test1 :: forall (c :: * -> Constraint) (b :: *).
             (c b) => (forall a. c a => a -> Bool) -> b -> Bool

和

• Could not deduce: c a
  from the context: c b
    bound by the type signature for:
               test1 :: c b => (forall a. c a => a -> Bool) -> b -> Bool
    at Test.hs:9:10-101
  or from: c0 a
    bound by the type signature for:
               test1 :: c0 a => a -> Bool
    at Test.hs:9:10-101
• In the ambiguity check for ‘test1’
  To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
  In the type signature:
    test1 :: forall (c :: * -> Constraint) (b :: *).
             (c b) => (forall a. c a => a -> Bool) -> b -> Bool

test0适用于没有约束但没有约束的地方test1.

Answer 1

如果已TypeApplications启用,则应启用AllowAmbiguousTypes.如果这样做,错误就会消失.

该歧义检查拒绝的定义t,使得没有t :: type标注都不能进行类型检查.例如:

test1 :: Show a => Int
test1 = 0

如果我们尝试test1在程序的其他地方使用,我们发现没有办法Show a通过::注释来解决约束.因此,歧义检查拒绝定义本身.

当然,与类型应用的歧义检查变得无意义(可以说,它应该被默认在这种情况下关断)时,由于test1 @type是微细且完全确定每当有一个Show type可用的实例.

请注意,这与着名的show . read歧义不同.这仍然会产生错误AllowAmbiguousTypes:

test2 = show . read 
-- "ambiguous type variable prevents the constraint from being solved"

在操作上,具有c => t类型的值只是从c-typed实例到的函数t.只是定义test1很好,因为我们总是可以定义一个常量函数.但是,show . read我们需要提供实例作为参数(否则没有代码可以运行),并且无法解决它们.在test1没有类型应用程序的情况下使用同样会有歧义.