Когда -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с

(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.

Я не вижу ни одной опубликованной версии синтаксиса, подпись которой 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. И действительно, 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]значит?

Я подозреваю, что синтаксический компилируется с 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из GHC.TypeLits .

Чтобы использовать эту функцию, я мог бы написать 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!

Тем не менее, обратите внимание, что если вы двусмысленно, вы не можете вернуться !