Quando -XAllowAmbiguousTypes é apropriado?

Recentemente, publiquei uma pergunta sobre sintático-2.0 com relação à definição de share. Eu tive isso trabalhando no 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

No entanto, o GHC 7.8 deseja -XAllowAmbiguousTypescompilar com essa assinatura. Como alternativa, posso substituir o fipor

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

qual é o tipo implícito no fundep on SyntacticN. Isso me permite evitar a extensão. Claro que isso é

• um tipo muito longo para adicionar a uma assinatura já grande
• cansativo derivar manualmente
• desnecessário devido ao fundep

Minhas perguntas são:

1. Esse é um uso aceitável -XAllowAmbiguousTypes?
2. Em geral, quando essa extensão deve ser usada? Uma resposta aqui sugere "quase nunca é uma boa ideia".

3. Embora eu tenha lido os documentos , ainda estou tendo problemas para decidir se uma restrição é ambígua ou não. Especificamente, considere esta função do Data.Syntactic.Sugar:

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

   Parece-me que fi(e possivelmente sup) deve ser ambíguo aqui, mas compila sem a extensão. Por que é sugarSyminequívoco enquanto shareé? Como shareé uma aplicação de sugarSym, sharetodas as restrições vêm diretamente sugarSym.

Não vejo nenhuma versão publicada do sintático cuja assinatura sugarSymuse exatamente esses nomes de tipos, portanto, usarei o ramo de desenvolvimento em commit 8cfd02 ^ , a última versão que ainda usava esses nomes.

Então, por que o GHC se queixa da fiassinatura do seu tipo, mas não a assinatura sugarSym? A documentação à qual você vinculou explica que um tipo é ambíguo se não aparecer à direita da restrição, a menos que ela esteja usando dependências funcionais para inferir o tipo ambíguo de outros tipos não ambíguos. Então, vamos comparar os contextos das duas funções e procurar dependências funcionais.

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

Portanto sugarSym, os tipos não ambíguos são sub, sige f, dentre esses, devemos ser capazes de seguir dependências funcionais para desambiguar todos os outros tipos usados ​​no contexto, a saber, supe fi. E, de fato, a f -> internaldependência funcional SyntacticNusa nosso fpara desambiguar nossa fie, posteriormente, a f -> sig symdependência funcional ApplySymusa nosso recém-desambiguar fipara desambiguar sup(e sig, que já era não ambíguo). Então, isso explica por sugarSymque não requer a AllowAmbiguousTypesextensão.

Vamos agora olhar sugar. A primeira coisa que noto é que o compilador não está reclamando de um tipo ambíguo, mas sim de instâncias sobrepostas:

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

Portanto, se estou lendo isso corretamente, não é que o GHC pense que seus tipos são ambíguos, mas sim, ao verificar se seus tipos são ambíguos, o GHC encontrou um problema diferente e separado. É então dizer que se você dissesse ao GHC para não executar a verificação de ambiguidade, ele não teria encontrado esse problema separado. Isso explica por que ativar o AllowAmbiguousTypes permite que seu código seja compilado.

No entanto, o problema com as instâncias sobrepostas permanece. As duas instâncias listadas pelo GHC ( SyntacticN f fie SyntacticN (a -> f) ...) se sobrepõem. Estranhamente, parece que o primeiro deles deve se sobrepor a qualquer outra instância, o que é suspeito. E o que isso [overlap ok]significa?

Suspeito que o Syntactic seja compilado com OverlappingInstances. E olhando o código , de fato ele faz.

Experimentando um pouco, parece que o GHC concorda com instâncias sobrepostas quando fica claro que uma é estritamente mais geral que a outra:

{-# 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])

Mas o GHC não concorda com instâncias sobrepostas quando nenhuma delas é claramente mais adequada que a outra:

{-# 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])

Sua assinatura de tipo usa SyntacticN (a -> (a -> b) -> b) fi, e SyntacticN f finem SyntacticN (a -> f) (AST sym (Full ia) -> fi)é melhor que a outra. Se eu alterar essa parte da sua assinatura de tipo para SyntacticN a fiou SyntacticN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi), o GHC não reclamará mais da sobreposição.

Se eu fosse você, examinaria a definição dessas duas instâncias possíveis e determinaria se uma dessas duas implementações é a que você deseja.

Eu descobri que AllowAmbiguousTypesé muito conveniente para uso TypeApplications. Considere a função natVal :: forall n proxy . KnownNat n => proxy n -> Integerde GHC.TypeLits .

Para usar esta função, eu poderia escrever natVal (Proxy::Proxy5). Um estilo alternativo é usar TypeApplications: natVal @5 Proxy. O tipo de Proxyé inferido pelo aplicativo de tipo e é irritante ter que escrevê-lo toda vez que você ligar natVal. Assim, podemos ativar AmbiguousTypese escrever:

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

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

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

No entanto, observe que, uma vez ambíguo, você não pode voltar !