When is -XAllowAmbiguousTypes appropriate?

I've discovered that AllowAmbiguousTypes is very convenient for use with TypeApplications. Consider the function natVal :: forall n proxy . KnownNat n => proxy n -> Integer from GHC.TypeLits.

To use this function, I could write natVal (Proxy::Proxy5). An alternate style is to use TypeApplications: natVal @5 Proxy. The type of Proxy is inferred by the type application, and it's annoying to have to write it every time you call natVal. Thus we can enable AmbiguousTypes and write:

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

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

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

However, note that once you go ambiguous, you can't go back!

I don't see any published version of syntactic whose signature for sugarSym uses those exact type names, so I'll be using the development branch at commit 8cfd02^, the last version which still used those names.

So, why does GHC complain about the fi in your type signature but not the one for sugarSym? The documentation you have linked to explains that a type is ambiguous if it doesn't appear to the right of the constraint, unless the constraint is using functional dependencies to infer the otherwise-ambiguous type from other non-ambiguous types. So let's compare the contexts of the two functions and look for functional dependencies.

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

So for sugarSym, the non-ambiguous types are sub, sig and f, and from those we should be able to follow functional dependencies in order to disambiguate all the other types used in the context, namely sup and fi. And indeed, the f -> internal functional dependency in SyntacticN uses our f to disambiguate our fi, and thereafter the f -> sig sym functional dependency in ApplySym uses our newly-disambiguated fi to disambiguate sup (and sig, which was already non-ambiguous). So that explains why sugarSym doesn't require the AllowAmbiguousTypes extension.

Let's now look at sugar. The first thing I notice is that the compiler is not complaining about an ambiguous type, but rather, about overlapping instances:

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

So if I'm reading this right, it's not that GHC thinks that your types are ambiguous, but rather, that while checking whether your types are ambiguous, GHC encountered a different, separate problem. It's then telling you that if you told GHC not to perform the ambiguity check, it would not have encountered that separate problem. This explains why enabling AllowAmbiguousTypes allows your code to compile.

However, the problem with the overlapping instances remain. The two instances listed by GHC (SyntacticN f fi and SyntacticN (a -> f) ...) do overlap with each other. Strangely enough, it seems like the first of these should overlap with any other instance, which is suspicious. And what does [overlap ok] mean?

I suspect that Syntactic is compiled with OverlappingInstances. And looking at the code, indeed it does.

Experimenting a bit, it seems that GHC is okay with overlapping instances when it is clear that one is strictly more general than the other:

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

But GHC is not okay with overlapping instances when neither is clearly a better fit than the other:

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

Your type signature uses SyntacticN (a -> (a -> b) -> b) fi, and neither SyntacticN f fi nor SyntacticN (a -> f) (AST sym (Full ia) -> fi) is a better fit than the other. If I change that part of your type signature to SyntacticN a fi or SyntacticN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi), GHC no longer complains about the overlap.

If I were you, I would look at the definition of those two possible instances and determine whether one of those two implementations is the one you want.