Note [Ambiguity check and deep subsumption]

GHC/Tc/Utils/Unify.hs:1331 compiler

Consider
   f :: (forall b. Eq b => a -> a) -> Int

Does `f` have an ambiguous type?   The ambiguity check usually checks
that this definition of f' would typecheck, where f' has the exact same
type as f:
   f' :: (forall b. Eq b => a -> a) -> Intp
   f' = f

This will be /rejected/ with DeepSubsumption but /accepted/ with
ShallowSubsumption.  On the other hand, this eta-expanded version f''
would be rejected both ways:
   f'' :: (forall b. Eq b => a -> a) -> Intp
   f'' x = f x

This is squishy in the same way as other examples in GHC.Tc.Validity
Note [The squishiness of the ambiguity check]

The situation in June 2022.  Since we have SimpleSubsumption at the moment,
we don't want introduce new breakage if you add -XDeepSubsumption, by
rejecting types as ambiguous that weren't ambiguous before.  So, as a
holding decision, we /always/ use SimpleSubsumption for the ambiguity check
(erring on the side accepting more programs). Hence tcSubTypeAmbiguity.

References 1

Referenced by 4