I'm not sure this is really a good idea, but it did come up in practice. Consider the following rather contrived program:

{-# LANGUAGE TypeFamilies, RankNTypes, ScopedTypeVariables,
             AllowAmbiguousTypes, TypeApplications #-}

module E where

type family T a
type instance T Int = Char
type instance T String = Char
type instance T Bool = ()

newtype FT a = FT [T a]

m :: forall a. (forall x. T x -> Int) -> FT a -> [Int]
m f (FT xs) = map f xs

GHC rejects it with the error:

E.hs:14:21: error:
    • Couldn't match type ‘T a’ with ‘T x0’
      Expected type: [T x0]
        Actual type: [T a]
      NB: ‘T’ is a type function, and may not be injective
      The type variable ‘x0’ is ambiguous
    • In the second argument of ‘map’, namely ‘xs’
      In the expression: map f xs
      In an equation for ‘m’: m f (FT xs) = map f xs
    • Relevant bindings include
        xs :: [T a] (bound at E.hs:14:9)
        m :: (forall x. T x -> Int) -> FT a -> [Int] (bound at E.hs:14:1)

The problem seems to be that GHC doesn't know at what type to instantiate f, because it can't conclude from the argument of f being T a that the type parameter of f needs to be x. In fact, T here really is not injective, so if a is Int, x could just as well be String.

However, in this case the ambiguity doesn't actually matter. If f @Int and f @String have the same type because T Int ~ T String, then they are actually the same value too by parametricity, because there is no class constraint on x. Since GHC prints a message saying that T is not known to be injective, it sounds like it knows about the possible solution x0 = a. So it could just pick it, and accept the original program.

With TypeApplications I can just specify the intended value of x by writing

m f (FT xs) = map (f @a) xs

which is a reasonable workaround in my real use case also. Interestingly I can't seem to achieve the same thing without TypeApplications without adding a proxy argument to f, which I don't much want to do.