When is -XAllowAmbiguousTypes appropriate?

Question

I've recently posted a question about syntactic-2.0 regarding the definition of share. I've had this working in 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

However, GHC 7.8 wants -XAllowAmbiguousTypes to compile with that signature. Alternatively, I can replace the fi with

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

which is the type implied by the fundep on SyntacticN. This allows me to avoid the extension. Of course this is

• a very long type to add to an already-large signature
• tiresome to manually derive
• unnecessary due to the fundep

My questions are:

1. Is this an acceptable use of -XAllowAmbiguousTypes?
2. In general, when should this extension be used? An answer here suggests "it is almost never a good idea".

3. Though I've read the docs, I'm still having trouble deciding if a constraint is ambiguous or not. Specifically, consider this function from Data.Syntactic.Sugar:

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

   It appears to me that fi (and possibly sup) should be ambiguous here, but it compiles without the extension. Why is sugarSym unambiguous while share is? Since share is an application of sugarSym, the share constraints all come straight from sugarSym.

Answer 1

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.

Answer 2

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!