什么时候-XAllowAmbiguousTypes合适？

Question

我最近发布了一个问题,关于句法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用

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

这是fundep隐含的类型SyntacticN.这允许我避免扩展.当然这是

• 一个很长的类型,可以添加到已经很大的签名中
• 厌倦手动派生
• 由于fundep不必要

我的问题是:

1. 这是可接受的用途-XAllowAmbiguousTypes吗？
2. 一般来说,何时应该使用此扩展名？这里的答案表明"这几乎不是一个好主意".

3. 虽然我已经阅读了文档,但我仍然无法确定约束是否含糊不清.具体来说,请考虑Data.Syntactic.Sugar中的此函数:

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

   在我看来,fi(并且可能sup)在这里应该是模棱两可的,但它在没有扩展的情况下编译.为什么这是sugarSym明确无误share的？既然share是应用sugarSym,那么share约束都是直接来自sugarSym.

Answer 1

我没有看到任何已发布的syntactic版本,其签名sugarSym使用那些确切的类型名称,所以我将在commit 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.实际上,f -> internal函数依赖SyntacticN使用我们f来消除歧义fi,然后f -> sig sym功能依赖ApplySym使用我们新消歧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不再抱怨重叠.

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