Add some documentation about redundant constraints

2 files changed, 28 insertions, 5 deletions

diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 244817c4a1..3e900a6d9e 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -2731,8 +2731,8 @@ findUnnecessaryGivens info need_inner givens
   | not (null unused_givens)         -- Some givens are literally unused
   = unused_givens
 
-   | otherwise                       -- All givens are used, but some might
-   = redundant_givens                -- still be redundant e.g. (Eq a, Ord a)
+  | otherwise                       -- All givens are used, but some might
+  = redundant_givens                -- still be redundant e.g. (Eq a, Ord a)
 
   where
     in_instance_decl = case info of { InstSkol {} -> True; _ -> False }
@@ -3084,7 +3084,7 @@ others).
 
    - For example, in a class declaration, the default method *can*
      use the class constraint, but it certainly doesn't *have* to,
-     and we don't want to report an error there.
+     and we don't want to report an error there.  Ditto instance decls.
 
    - More subtly, in a function definition
        f :: (Ord a, Ord a, Ix a) => a -> a
@@ -3105,7 +3105,7 @@ others).
 
 ----- Shortcomings
 
-Consider
+Shortcoming 1.  Consider
 
   j :: (Eq a, a ~ b) => a -> Bool
   j x = x == x
@@ -3118,6 +3118,18 @@ is redundant. This is because j uses the a ~ b constraint to rewrite
 everything to be in terms of b, while k does none of that. This is
 ridiculous, but I (Richard E) don't see a good fix.
 
+Shortcoming 2.  Removing a redundant constraint can cause clients to fail to
+compile, by making the function more polymoprhic. Consider (#16154)
+
+  f :: (a ~ Bool) => a -> Int
+  f x = 3
+
+  g :: String -> Int
+  g s = f (read s)
+
+The constraint in f's signature is redundant; not used to typecheck
+`f`.  And yet if you remove it, `g` won't compile, because there'll
+be an ambiguous variable in `g`.
 -}
 
 -- | Like 'defaultTyVar', but in the TcS monad.
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index fb64b55cde..9c72e2ac4e 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -85,11 +85,22 @@ data UserTypeCtxt
                     -- Also used for types in SPECIALISE pragmas
        Name              -- Name of the function
        ReportRedundantConstraints
-         -- This is usually 'WantRCC', but 'NoRCC' for
+         -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
+         -- This field is usually 'WantRCC', but 'NoRCC' for
          --   * Record selectors (not important here)
          --   * Class and instance methods.  Here the code may legitimately
          --     be more polymorphic than the signature generated from the
          --     class declaration
+         --   * Functions whose type signature has hidden the constraints
+         --     behind a type synonym.  E.g.
+         --          type Foo = forall a. Eq a => a -> a
+         --          id :: Foo
+         --          id x = x
+         --     Here we can't give a good location for the redundant constraints
+         --     (see lhsSigWcTypeContextSpan), so we don't report redundant
+         --     constraints at all. It's not clear that this a good choice;
+         --     perhaps we should report, just with a less informative SrcSpan.
+         --     c.f. #16154
 
   | InfSigCtxt Name     -- Inferred type for function
   | ExprSigCtxt         -- Expression type signature