Note [Ambiguity check and deep subsumption]
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
- The squishiness of the ambiguity check GHC.Tc.Validity
Referenced by 4
- GHC.Tc.Utils.Unify call site
- Deep subsumption GHC.Tc.Utils.Unify
- The squishiness of the ambiguity check GHC.Tc.Validity
- GHC.Tc.Validity call site