[Git][ghc/ghc][wip/backports-9.8] 4 commits: Consider Wanteds with rewriters as insoluble

Ben Gamari (@bgamari) gitlab at gitlab.haskell.org
Mon Oct 14 15:57:06 UTC 2024



Ben Gamari pushed to branch wip/backports-9.8 at Glasgow Haskell Compiler / GHC


Commits:
7326051e by Simon Peyton Jones at 2024-10-14T11:53:29-04:00
Consider Wanteds with rewriters as insoluble

This MR fixes #25325

See GHC.Tc.Types.Constraint, Note [Insoluble Wanteds], especially (IW2)

There is a small change in the error message for T14172, but it looks
entirely acceptable to me.

(cherry picked from commit 083703a12cd34369e7ed2f0efc4a5baee47aedab)

- - - - -
6b790e6c by Simon Peyton Jones at 2024-10-14T11:53:58-04:00
Wibbles

(cherry picked from commit 0dfaeb66fb8457e7339abbd44d5c53a81ad8ae3a)

- - - - -
454e2165 by Simon Peyton Jones at 2024-10-14T11:53:58-04:00
Spelling errors

(cherry picked from commit 09d24d828e48c2588a317e6dad711f8673983703)

- - - - -
a3a6da7e by Torsten Schmits at 2024-10-14T11:53:58-04:00
add test that runs MakeDepend on thousands of modules

(cherry picked from commit 7875e8cbe5d9b69a1a77354317b2bf9478172686)

- - - - -


9 changed files:

- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Types/Constraint.hs
- testsuite/driver/testlib.py
- + testsuite/tests/perf/compiler/large-project/all.T
- + testsuite/tests/perf/compiler/large-project/large-project.sh
- testsuite/tests/polykinds/T14172.stderr
- + testsuite/tests/typecheck/should_fail/T25325.hs
- + testsuite/tests/typecheck/should_fail/T25325.stderr
- testsuite/tests/typecheck/should_fail/all.T


Changes:

=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -469,6 +469,8 @@ mkErrorItem ct
              flav = ctFlavour ct
 
        ; (suppress, m_evdest) <- case ctEvidence ct of
+         -- For this `suppress` stuff
+         -- see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
            CtGiven {} -> return (False, Nothing)
            CtWanted { ctev_rewriters = rewriters, ctev_dest = dest }
              -> do { rewriters' <- zonkRewriterSet rewriters


=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -83,7 +83,7 @@ module GHC.Tc.Types.Constraint (
         ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
         ctEvRewriters, ctEvUnique, tcEvDestUnique,
         mkKindEqLoc, toKindLoc, toInvisibleLoc, mkGivenLoc,
-        ctEvRole, setCtEvPredType, setCtEvLoc, arisesFromGivens,
+        ctEvRole, setCtEvPredType, setCtEvLoc,
         tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList,
 
         -- RewriterSet
@@ -1312,25 +1312,51 @@ nonDefaultableTyVarsOfWC (WC { wc_simple = simples, wc_impl = implics, wc_errors
 insolubleWC :: WantedConstraints -> Bool
 insolubleWC (WC { wc_impl = implics, wc_simple = simples, wc_errors = errors })
   =  anyBag insolubleWantedCt simples
+       -- insolubleWantedCt: wanteds only: see Note [Given insolubles]
   || anyBag insolubleImplic implics
   || anyBag is_insoluble errors
-
-    where
+  where
       is_insoluble (DE_Hole hole) = isOutOfScopeHole hole -- See Note [Insoluble holes]
       is_insoluble (DE_NotConcrete {}) = True
 
 insolubleWantedCt :: Ct -> Bool
 -- Definitely insoluble, in particular /excluding/ type-hole constraints
 -- Namely:
---   a) an insoluble constraint as per 'insolubleCt', i.e. either
+--   a) an insoluble constraint as per 'insolubleIrredCt', i.e. either
 --        - an insoluble equality constraint (e.g. Int ~ Bool), or
 --        - a custom type error constraint, TypeError msg :: Constraint
 --   b) that does not arise from a Given or a Wanted/Wanted fundep interaction
+-- See Note [Insoluble Wanteds]
+insolubleWantedCt ct
+  | CIrredCan ir_ct <- ct
+      -- CIrredCan: see (IW1) in Note [Insoluble Wanteds]
+  , IrredCt { ir_ev = ev } <- ir_ct
+  , CtWanted { ctev_loc = loc, ctev_rewriters = rewriters }  <- ev
+      -- It's a Wanted
+  , insolubleIrredCt ir_ct
+      -- It's insoluble
+  , isEmptyRewriterSet rewriters
+      -- It has no rewriters; see (IW2) in Note [Insoluble Wanteds]
+  , not (isGivenLoc loc)
+      -- isGivenLoc: see (IW3) in Note [Insoluble Wanteds]
+  , not (isWantedWantedFunDepOrigin (ctLocOrigin loc))
+      -- origin check: see (IW4) in Note [Insoluble Wanteds]
+  = True
+
+  | otherwise
+  = False
+
+-- | Returns True of constraints that are definitely insoluble,
+--   as well as TypeError constraints.
+-- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'.
 --
--- See Note [Given insolubles].
-insolubleWantedCt ct = insolubleCt ct &&
-                       not (arisesFromGivens ct) &&
-                       not (isWantedWantedFunDepOrigin (ctOrigin ct))
+-- The function is tuned for application /after/ constraint solving
+--       i.e. assuming canonicalisation has been done
+-- That's why it looks only for IrredCt; all insoluble constraints
+-- are put into CIrredCan
+insolubleCt :: Ct -> Bool
+insolubleCt (CIrredCan ir_ct) = insolubleIrredCt ir_ct
+insolubleCt _                 = False
 
 insolubleIrredCt :: IrredCt -> Bool
 -- Returns True of Irred constraints that are /definitely/ insoluble
@@ -1360,18 +1386,6 @@ insolubleIrredCt (IrredCt { ir_ev = ev, ir_reason = reason })
   -- >   Assert 'True  _errMsg = ()
   -- >   Assert _check errMsg  = errMsg
 
--- | Returns True of constraints that are definitely insoluble,
---   as well as TypeError constraints.
--- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'.
---
--- The function is tuned for application /after/ constraint solving
---       i.e. assuming canonicalisation has been done
--- That's why it looks only for IrredCt; all insoluble constraints
--- are put into CIrredCan
-insolubleCt :: Ct -> Bool
-insolubleCt (CIrredCan ir_ct) = insolubleIrredCt ir_ct
-insolubleCt _                 = False
-
 -- | Does this hole represent an "out of scope" error?
 -- See Note [Insoluble holes]
 isOutOfScopeHole :: Hole -> Bool
@@ -1415,6 +1429,31 @@ in GHC.Tc.Errors), so we may fail to report anything at all!  Yikes.
 Bottom line: insolubleWC (called in GHC.Tc.Solver.setImplicationStatus)
              should ignore givens even if they are insoluble.
 
+Note [Insoluble Wanteds]
+~~~~~~~~~~~~~~~~~~~~~~~~
+insolubleWantedCt returns True of a Wanted constraint that definitely
+can't be solved.  But not quite all such constraints; see wrinkles.
+
+(IW1) insolubleWantedCt is tuned for application /after/ constraint
+   solving i.e. assuming canonicalisation has been done.  That's why
+   it looks only for IrredCt; all insoluble constraints are put into
+   CIrredCan
+
+(IW2) We only treat it as insoluble if it has an empty rewriter set.  (See Note
+   [Wanteds rewrite Wanteds].)  Otherwise #25325 happens: a Wanted constraint A
+   that is /not/ insoluble rewrites some other Wanted constraint B, so B has A
+   in its rewriter set.  Now B looks insoluble.  The danger is that we'll
+   suppress reporting B because of its empty rewriter set; and suppress
+   reporting A because there is an insoluble B lying around.  (This suppression
+   happens in GHC.Tc.Errors.mkErrorItem.)  Solution: don't treat B as insoluble.
+
+(IW3) If the Wanted arises from a Given (how can that happen?), don't
+   treat it as a Wanted insoluble (obviously).
+
+(IW4) If the Wanted came from a  Wanted/Wanted fundep interaction, don't
+   treat the constraint as insoluble. See Note [Suppressing confusing errors]
+   in GHC.Tc.Errors
+
 Note [Insoluble holes]
 ~~~~~~~~~~~~~~~~~~~~~~
 Hole constraints that ARE NOT treated as truly insoluble:
@@ -2056,9 +2095,6 @@ tcEvDestUnique (HoleDest co_hole) = varUnique (coHoleCoVar co_hole)
 setCtEvLoc :: CtEvidence -> CtLoc -> CtEvidence
 setCtEvLoc ctev loc = ctev { ctev_loc = loc }
 
-arisesFromGivens :: Ct -> Bool
-arisesFromGivens ct = isGivenCt ct || isGivenLoc (ctLoc ct)
-
 -- | Set the type of CtEvidence.
 --
 -- This function ensures that the invariants on 'CtEvidence' hold, by updating


=====================================
testsuite/driver/testlib.py
=====================================
@@ -1538,6 +1538,9 @@ async def multi_compile( name, way, top_mod, extra_mods, extra_hc_opts ):
 async def multi_compile_fail( name, way, top_mod, extra_mods, extra_hc_opts ):
     return await do_compile( name, way, True, top_mod, extra_mods, [], extra_hc_opts)
 
+async def make_depend( name, way, mods, extra_hc_opts ):
+    return await do_compile( name, way, False,  ' '.join(mods), [], [], extra_hc_opts, mode = '-M')
+
 async def do_compile(name: TestName,
                way: WayName,
                should_fail: bool,
@@ -1804,7 +1807,9 @@ async def simple_build(name: Union[TestName, str],
                  addsuf: bool,
                  backpack: bool = False,
                  suppress_stdout: bool = False,
-                 filter_with: str = '') -> Any:
+                 filter_with: str = '',
+                 # Override auto-detection of whether to use --make or -c etc.
+                 mode: Optional[str] = None) -> Any:
     opts = getTestOpts()
 
     # Redirect stdout and stderr to the same file
@@ -1821,7 +1826,9 @@ async def simple_build(name: Union[TestName, str],
     else:
         srcname = Path(name)
 
-    if top_mod is not None:
+    if mode is not None:
+        to_do = mode
+    elif top_mod is not None:
         to_do = '--make '
         if link:
             to_do = to_do + '-o ' + name


=====================================
testsuite/tests/perf/compiler/large-project/all.T
=====================================
@@ -0,0 +1,21 @@
+# These tests are supposed to prevent severe performance regressions when
+# operating on projects with unusually large numbers of modules.
+# Inefficient algorithms whose complexity depends on the number of modules won't
+# be noticed when running the test suite or compiling medium size projects.
+
+def large_project_makedepend(num):
+    return test(
+        f'large-project-makedepend-{num}',
+        [
+            collect_compiler_stats('bytes allocated', 1),
+            pre_cmd(f'./large-project.sh {num}'),
+            extra_files(['large-project.sh']),
+            ignore_stderr,
+            when(windows,skip),
+        ],
+        make_depend,
+        [[f'Mod{i:04d}' for i in range(0, num - 1)], ''],
+        )
+
+large_project_makedepend(4000)
+large_project_makedepend(10000)


=====================================
testsuite/tests/perf/compiler/large-project/large-project.sh
=====================================
@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+
+set -eu
+
+total="$1"
+
+for ((i = 1; i < $total; i++))
+do
+  # Important to write directly to variables with `-v`, otherwise the script takes a second per 1000 modules
+  printf -v j "%04d" "$i"
+  printf -v k "%04d" "$(($i - 1))"
+  echo -e "module Mod${j} where
+import Mod${k}
+f_${j} :: ()
+f_${j} = f_$k" > "Mod${j}.hs"
+done
+
+echo "
+module Mod0000 where
+f_0000 :: ()
+f_0000 = ()
+" > "Mod0000.hs"


=====================================
testsuite/tests/polykinds/T14172.stderr
=====================================
@@ -1,10 +1,7 @@
-
 T14172.hs:7:46: error: [GHC-88464]
-    • Found type wildcard ‘_’ standing for ‘a'’
-      Where: ‘a'’ is a rigid type variable bound by
-               the inferred type of
-                 traverseCompose :: (a -> f b) -> g a -> f (h a')
-               at T14172.hs:8:1-46
+    • Found type wildcard ‘_’ standing for ‘a'1 :: k0’
+      Where: ‘k0’ is an ambiguous type variable
+             ‘a'1’ is an ambiguous type variable
       To use the inferred type, enable PartialTypeSignatures
     • In the first argument of ‘h’, namely ‘_’
       In the first argument of ‘f’, namely ‘(h _)’
@@ -13,17 +10,19 @@ T14172.hs:7:46: error: [GHC-88464]
 
 T14172.hs:8:19: error: [GHC-25897]
     • Couldn't match type ‘a’ with ‘g'1 a'0’
-      Expected: (f'0 a -> f (f'0 b)) -> g a -> f (h a')
-        Actual: (Unwrapped (Compose f'0 g'1 a'0) -> f (Unwrapped (h a')))
-                -> Compose f'0 g'1 a'0 -> f (h a')
+      Expected: (f'0 a -> f (f'0 b)) -> g a -> f (h a'1)
+        Actual: (Unwrapped (Compose f'0 g'1 a'0)
+                 -> f (Unwrapped (h a'1)))
+                -> Compose f'0 g'1 a'0 -> f (h a'1)
       ‘a’ is a rigid type variable bound by
         the inferred type of
-          traverseCompose :: (a -> f b) -> g a -> f (h a')
+          traverseCompose :: (a -> f b) -> g a -> f (h a'1)
         at T14172.hs:7:1-47
     • In the first argument of ‘(.)’, namely ‘_Wrapping Compose’
       In the expression: _Wrapping Compose . traverse
       In an equation for ‘traverseCompose’:
           traverseCompose = _Wrapping Compose . traverse
     • Relevant bindings include
-        traverseCompose :: (a -> f b) -> g a -> f (h a')
+        traverseCompose :: (a -> f b) -> g a -> f (h a'1)
           (bound at T14172.hs:8:1)
+


=====================================
testsuite/tests/typecheck/should_fail/T25325.hs
=====================================
@@ -0,0 +1,14 @@
+module T25325 where
+
+import Control.Monad.State
+
+data (f :+: g) a = Inl (f a) | Inr (g a)
+
+newtype Buggy f m = Buggy { thing :: m Int }
+
+class GhcBug f where
+  demo :: MonadState (Buggy f m) m => f (m Int) -> m Int
+
+instance (GhcBug f, GhcBug g) => GhcBug (f :+: g) where
+    demo (Inl l) = demo l
+    demo (Inr r) = demo r


=====================================
testsuite/tests/typecheck/should_fail/T25325.stderr
=====================================
@@ -0,0 +1,15 @@
+T25325.hs:14:20: error: [GHC-39999]
+    • Could not deduce ‘MonadState (Buggy g m) m’
+        arising from a use of ‘demo’
+      from the context: (GhcBug f, GhcBug g)
+        bound by the instance declaration at T25325.hs:12:10-49
+      or from: MonadState (Buggy (f :+: g) m) m
+        bound by the type signature for:
+                   demo :: forall (m :: * -> *).
+                           MonadState (Buggy (f :+: g) m) m =>
+                           (:+:) f g (m Int) -> m Int
+        at T25325.hs:13:5-8
+    • In the expression: demo r
+      In an equation for ‘demo’: demo (Inr r) = demo r
+      In the instance declaration for ‘GhcBug (f :+: g)’
+


=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -702,3 +702,4 @@ test('T22684', normal, compile_fail, [''])
 test('T23776', normal, compile, ['']) # to become an error in GHC 9.12
 test('T17940', normal, compile_fail, [''])
 test('T24279', normal, compile_fail, [''])
+test('T25325', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/05152a5765a6a52fda14f1a1f2c8e735b86c7522...a3a6da7e757002a60553416ed61c299d504e3865

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/05152a5765a6a52fda14f1a1f2c8e735b86c7522...a3a6da7e757002a60553416ed61c299d504e3865
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20241014/cccc7382/attachment-0001.html>


More information about the ghc-commits mailing list