¿Cuándo es apropiado -XAllowAmbiguousTypes?

Recientemente publiqué una pregunta sobre syntactic-2.0 con respecto a la definición de share. He tenido esto trabajando en 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

Sin embargo, GHC 7.8 quiere -XAllowAmbiguousTypescompilar con esa firma. Alternativamente, puedo reemplazar el ficon

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

cual es el tipo implicado por el fundep en SyntacticN. Esto me permite evitar la extensión. Por supuesto esto es

• un tipo muy largo para agregar a una firma ya grande
• cansado de derivar manualmente
• innecesario debido al fundep

Mis preguntas son:

1. ¿Es este un uso aceptable de -XAllowAmbiguousTypes?
2. En general, ¿cuándo se debe usar esta extensión? Una respuesta aquí sugiere que "casi nunca es una buena idea".

3. Aunque he leído los documentos , todavía tengo problemas para decidir si una restricción es ambigua o no. Específicamente, considere esta función de Data.Syntactic.Sugar:

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

   Me parece que fi(y posiblemente sup) debería ser ambiguo aquí, pero se compila sin la extensión. ¿Por qué es sugarSyminequívoco mientras sharees? Como sharees una aplicación de sugarSym, sharetodas las restricciones provienen directamente sugarSym.

No veo ninguna versión publicada de Syntactic cuya firma sugarSymuse esos nombres de tipo exactos, por lo que usaré la rama de desarrollo en commit 8cfd02 ^ , la última versión que todavía usa esos nombres.

Entonces, ¿por qué GHC se queja de la fifirma de su tipo pero no de la firma sugarSym? La documentación a la que se ha vinculado explica que un tipo es ambiguo si no aparece a la derecha de la restricción, a menos que la restricción esté utilizando dependencias funcionales para inferir el tipo ambiguo de otros tipos no ambiguos. Entonces, comparemos los contextos de las dos funciones y busquemos dependencias funcionales.

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

Entonces sugarSym, los tipos no ambiguos son sub, sigy f, y de ellos deberíamos poder seguir las dependencias funcionales para desambiguar todos los otros tipos utilizados en el contexto, a saber, supy fi. Y, de hecho, la f -> internaldependencia funcional en SyntacticNutiliza nuestro fpara desambiguar nuestro fi, y luego la f -> sig symdependencia funcional en ApplySymusa nuestro recién desambiguado fipara desambiguar sup(y sig, que ya no era ambiguo). Eso explica por qué sugarSymno requiere la AllowAmbiguousTypesextensión.

Veamos ahora sugar. Lo primero que noto es que el compilador no se queja de un tipo ambiguo, sino de instancias superpuestas:

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

Entonces, si estoy leyendo esto correctamente, no es que GHC piense que sus tipos son ambiguos, sino que mientras verifica si sus tipos son ambiguos, GHC encontró un problema diferente y diferente. Luego le dice que si le dijera a GHC que no realizara la verificación de ambigüedad, no habría encontrado ese problema por separado. Esto explica por qué habilitar AllowAmbiguousTypes permite que su código se compile.

Sin embargo, el problema con las instancias superpuestas permanece. Las dos instancias enumeradas por GHC ( SyntacticN f fiy SyntacticN (a -> f) ...) se superponen entre sí. Por extraño que parezca, parece que el primero de estos debería superponerse con cualquier otra instancia, lo que es sospechoso. Y que [overlap ok]significa

Sospecho que Syntactic está compilado con OverlappingInstances. Y mirando el código , de hecho lo hace.

Experimentando un poco, parece que GHC está de acuerdo con instancias superpuestas cuando está claro que una es estrictamente más general que la otra:

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

Pero GHC no está de acuerdo con las instancias superpuestas cuando ninguna de ellas es claramente mejor que la otra:

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

Sus usos tipo de firma SyntacticN (a -> (a -> b) -> b) fi, y ni SyntacticN f fitampoco SyntacticN (a -> f) (AST sym (Full ia) -> fi)es un ajuste mejor que el otro. Si cambio esa parte de su firma tipo a SyntacticN a fio SyntacticN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi), GHC ya no se queja de la superposición.

Si yo fuera usted, miraría la definición de esas dos posibles instancias y determinaría si una de esas dos implementaciones es la que desea.

He descubierto que AllowAmbiguousTypeses muy conveniente para usar TypeApplications. Considere la función natVal :: forall n proxy . KnownNat n => proxy n -> Integerde GHC.TypeLits .

Para usar esta función, podría escribir natVal (Proxy::Proxy5). Un estilo alternativo es usar TypeApplications: natVal @5 Proxy. El tipo de Proxyes inferido por la aplicación de tipo, y es molesto tener que escribirlo cada vez que llama natVal. Así podemos habilitar AmbiguousTypesy escribir:

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

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

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

Sin embargo, tenga en cuenta que una vez que se vuelve ambiguo, ¡no puede regresar !