XAllowAmbiguousTypes是否合适？

我最近发布了一个关于语法-2.0关于share定义的问题。 我已经在GHC 7.6中工作过了：

{-# LANGUAGE GADTs, TypeOperators, FlexibleContexts #-}

import Data.Syntactic
import Data.Syntactic.Sugar.BindingT

data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: sup,
          sup ~ Domain b, sup ~ Domain a,
          Syntactic a, Syntactic b,
          Syntactic (a -> b),
          SyntacticN (a -> (a -> b) -> b) 
                     fi)
           => a -> (a -> b) -> b
share = sugarSym Let

但是，GHC 7.8希望使用该签名编译-XAllowAmbiguousTypes 。 或者，我可以用fi替换fi

(ASTF sup (Internal a) -> AST sup ((Internal a) :-> Full (Internal b)) -> ASTF sup (Internal b))

这是通过在fundep隐含的类型SyntacticN 。 这允许我避免扩展。 当然是这样

我的问题是：

sugarSym :: (sub :<: AST sup, ApplySym sig fi sup, SyntacticN f fi) 
         => sub sig -> f
sugarSym = sugarN . appSym

我没有看到sugarSym的签名使用了那些确切类型名称的任何已发布语法版本，所以我将在提交8cfd02 ^处使用开发分支，这是最后一个仍使用这些名称的版本。

那么，为什么GHC会在你的型号签名中抱怨fi ，而不是sugarSym ？ 您链接到的文档解释了，如果类型不出现在约束条件的右侧，则该类型是不明确的，除非约束使用函数依赖关系来从其他非歧义类型推断否则不明确的类型。 所以我们来比较这两个函数的上下文并查找函数依赖关系。

class ApplySym sig f sym | sig sym -> f, f -> sig sym
class SyntacticN f internal | f -> internal

sugarSym :: ( sub :<: AST sup
            , ApplySym sig fi sup
            , SyntacticN f fi
            ) 
         => sub sig -> f

share :: ( Let :<: sup
         , sup ~ Domain b
         , sup ~ Domain a
         , Syntactic a
         , Syntactic b
         , Syntactic (a -> b)
         , SyntacticN (a -> (a -> b) -> b) fi
         )
      => a -> (a -> b) -> b

因此，对于sugarSym ，非模糊类型是sub ， sig和f ，并且从那些我们应该能够遵循函数依赖性来消除上下文中使用的所有其他类型，即sup和fi 。 事实上， SyntacticN的f -> internal函数依赖使用我们的f来消除我们的fi ，然后ApplySym的f -> sig sym函数依赖使用我们新消歧的fi来消除sup （和sig ，暧昧）。 这就解释了为什么sugarSym不需要AllowAmbiguousTypes扩展。

现在我们来看看sugar 。 我注意到的第一件事是，编译器不是抱怨模糊的类型，而是抱怨重叠的实例：

Overlapping instances for SyntacticN b fi
  arising from the ambiguity check for ‘share’
Matching givens (or their superclasses):
  (SyntacticN (a -> (a -> b) -> b) fi1)
Matching instances:
  instance [overlap ok] (Syntactic f, Domain f ~ sym,
                         fi ~ AST sym (Full (Internal f))) =>
                        SyntacticN f fi
    -- Defined in ‘Data.Syntactic.Sugar’
  instance [overlap ok] (Syntactic a, Domain a ~ sym,
                         ia ~ Internal a, SyntacticN f fi) =>
                        SyntacticN (a -> f) (AST sym (Full ia) -> fi)
    -- Defined in ‘Data.Syntactic.Sugar’
(The choice depends on the instantiation of ‘b, fi’)
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes

所以如果我正在阅读这个权利，并不是说GHC认为你的类型是模棱两可的，而是在检查你的类型是否含糊不清时，GHC遇到了另一个单独的问题。 然后它会告诉你，如果你告诉GHC不要执行模糊检查，它不会遇到这个单独的问题。 这就解释了为什么启用AllowAmbiguousTypes可以让你的代码编译。

但是，重叠实例的问题仍然存在。 由GHC（ SyntacticN f fi和SyntacticN (a -> f) ... ）列出的两个实例确实相互重叠。 奇怪的是，它们中的第一个似乎应该与任何其他可疑的实例重叠。 那么[overlap ok]是什么意思？

我怀疑Syntactic是用OverlappingInstances编译的。 看着代码，的确如此。

试验一下，似乎GHC在重叠的情况下是可以的，当它清楚地表明一个比另一个更为一般时：

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

class Foo a where
  whichOne :: a -> String

instance Foo a where
  whichOne _ = "a"

instance Foo [a] where
  whichOne _ = "[a]"

-- |
-- >>> main
-- [a]
main :: IO ()
main = putStrLn $ whichOne (undefined :: [Int])

但GHC对重叠的情况并不合适，因为它们都不比另一个更合适：

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

class Foo a where
  whichOne :: a -> String

instance Foo (f Int) where  -- this is the line which changed
  whichOne _ = "f Int"

instance Foo [a] where
  whichOne _ = "[a]"

-- |
-- >>> main
-- Error: Overlapping instances for Foo [Int]
main :: IO ()
main = putStrLn $ whichOne (undefined :: [Int])

您的类型签名使用SyntacticN (a -> (a -> b) -> b) fi ，并且SyntacticN f fi和SyntacticN (a -> f) (AST sym (Full ia) -> fi)另一个。 如果我将你的类型签名的那部分改为SyntacticN a fi或SyntacticN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi) ，GHC不再抱怨重叠。

如果我是你，我会查看这两个可能实例的定义，并确定这两个实现中的一个是否是你想要的。

我发现， AllowAmbiguousTypes是与使用非常方便TypeApplications 。 考虑函数natVal :: forall n proxy . KnownNat n => proxy n -> Integer natVal :: forall n proxy . KnownNat n => proxy n -> Integer来自GHC.TypeLits的natVal :: forall n proxy . KnownNat n => proxy n -> Integer 。

要使用这个函数，我可以编写natVal (Proxy::Proxy5) 。 另一种风格是使用TypeApplications ： natVal @5 Proxy 。 Proxy类型是由类型应用程序推断出来的，每次调用natVal时都需要编写它，这很烦人。 因此，我们可以启用AmbiguousTypes并编写：

{-# Language AllowAmbiguousTypes, ScopedTypeVariables, TypeApplications #-}

ambiguousNatVal :: forall n . (KnownNat n) => Integer
ambiguousNatVal = natVal @n Proxy

five = ambiguousNatVal @5 -- no `Proxy ` needed!

但是，请注意，一旦你模糊不清，你就不能回去！

上一篇: XAllowAmbiguousTypes appropriate?

下一篇: Is there something better than unsafePerformIO for this....?