[Git][ghc/ghc][wip/T21909] Fixes #21909

Apoorv Ingle (@ani) gitlab at gitlab.haskell.org
Mon Feb 6 21:21:21 UTC 2023



Apoorv Ingle pushed to branch wip/T21909 at Glasgow Haskell Compiler / GHC


Commits:
93d04d3e by Apoorv Ingle at 2023-02-06T15:09:33-06:00
Fixes #21909
Constraint simplification loop now depends on `ExpansionFuel` instead of a boolean flag in `CDictCan.cc_pend_sc`.
Pending Givens get a fuel of 3 to start of with while Wanted constraints get a fuel of 1.
This helps pending given constraints to keep up with pending wanted constraints.

Added tests T21909, T21909b

- - - - -


6 changed files:

- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- + testsuite/tests/typecheck/should_compile/T21909.hs
- + testsuite/tests/typecheck/should_compile/T21909b.hs
- testsuite/tests/typecheck/should_compile/all.T


Changes:

=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -153,9 +153,9 @@ canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
 -- Precondition: EvVar is class evidence
 canClassNC ev cls tys
   | isGiven ev  -- See Note [Eagerly expand given superclasses]
-  = do { sc_cts <- mkStrictSuperClasses ev [] [] cls tys
+  = do { sc_cts <- mkStrictSuperClasses defaultExpansionFuel ev [] [] cls tys
        ; emitWork sc_cts
-       ; canClass ev cls tys False }
+       ; canClass ev cls tys noExpansionFuel }
 
   | CtWanted { ctev_rewriters = rewriters } <- ev
   , Just ip_name <- isCallStackPred cls tys
@@ -181,14 +181,16 @@ canClassNC ev cls tys
                                   (ctLocSpan loc) (ctEvExpr new_ev)
        ; solveCallStack ev ev_cs
 
-       ; canClass new_ev cls tys False -- No superclasses
+       ; canClass new_ev cls tys noExpansionFuel -- No superclasses
        }
 
   | otherwise
-  = canClass ev cls tys (has_scs cls)
+  = canClass ev cls tys fuel
 
   where
-    has_scs cls = not (null (classSCTheta cls))
+    fuel | cls_has_scs = 1
+         | otherwise = noExpansionFuel
+    cls_has_scs = not (null (classSCTheta cls))
     loc  = ctEvLoc ev
     orig = ctLocOrigin loc
     pred = ctEvPred ev
@@ -205,7 +207,7 @@ solveCallStack ev ev_cs = do
 
 canClass :: CtEvidence
          -> Class -> [Type]
-         -> Bool            -- True <=> un-explored superclasses
+         -> ExpansionFuel            -- n > 0 <=> un-explored superclasses
          -> TcS (StopOrContinue Ct)
 -- Precondition: EvVar is class evidence
 
@@ -497,34 +499,34 @@ makeSuperClasses :: [Ct] -> TcS [Ct]
 --     least produce the immediate superclasses
 makeSuperClasses cts = concatMapM go cts
   where
-    go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
-      = mkStrictSuperClasses ev [] [] cls tys
+    go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys, cc_pend_sc = fuel })
+      = mkStrictSuperClasses fuel ev [] [] cls tys
     go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev }))
       = assertPpr (isClassPred pred) (ppr pred) $  -- The cts should all have
                                                    -- class pred heads
-        mkStrictSuperClasses ev tvs theta cls tys
+        mkStrictSuperClasses defaultExpansionFuel ev tvs theta cls tys
       where
         (tvs, theta, cls, tys) = tcSplitDFunTy (ctEvPred ev)
     go ct = pprPanic "makeSuperClasses" (ppr ct)
 
 mkStrictSuperClasses
-    :: CtEvidence
+    :: ExpansionFuel -> CtEvidence
     -> [TyVar] -> ThetaType  -- These two args are non-empty only when taking
                              -- superclasses of a /quantified/ constraint
     -> Class -> [Type] -> TcS [Ct]
 -- Return constraints for the strict superclasses of
 --   ev :: forall as. theta => cls tys
-mkStrictSuperClasses ev tvs theta cls tys
-  = mk_strict_superclasses (unitNameSet (className cls))
+mkStrictSuperClasses fuel ev tvs theta cls tys
+  = mk_strict_superclasses fuel (unitNameSet (className cls))
                            ev tvs theta cls tys
 
-mk_strict_superclasses :: NameSet -> CtEvidence
+mk_strict_superclasses :: ExpansionFuel -> NameSet -> CtEvidence
                        -> [TyVar] -> ThetaType
                        -> Class -> [Type] -> TcS [Ct]
 -- Always return the immediate superclasses of (cls tys);
 -- and expand their superclasses, provided none of them are in rec_clss
 -- nor are repeated
-mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
+mk_strict_superclasses fuel rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
                        tvs theta cls tys
   = concatMapM do_one_given $
     classSCSelIds cls
@@ -542,7 +544,7 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
       | otherwise
       = do { given_ev <- newGivenEvVar sc_loc $
                          mk_given_desc sel_id sc_pred
-           ; mk_superclasses rec_clss given_ev tvs theta sc_pred }
+           ; mk_superclasses fuel rec_clss given_ev tvs theta sc_pred }
       where
         sc_pred = classMethodInstTy sel_id tys
 
@@ -603,7 +605,7 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
     newly_blocked (InstSkol _ head_size) = isJust (this_size `ltPatersonSize` head_size)
     newly_blocked _                      = False
 
-mk_strict_superclasses rec_clss ev tvs theta cls tys
+mk_strict_superclasses fuel rec_clss ev tvs theta cls tys
   | all noFreeVarsOfType tys
   = return [] -- Wanteds with no variables yield no superclass constraints.
               -- See Note [Improvement from Ground Wanteds]
@@ -618,7 +620,7 @@ mk_strict_superclasses rec_clss ev tvs theta cls tys
     do_one sc_pred
       = do { traceTcS "mk_strict_superclasses Wanted" (ppr (mkClassPred cls tys) $$ ppr sc_pred)
            ; sc_ev <- newWantedNC loc (ctEvRewriters ev) sc_pred
-           ; mk_superclasses rec_clss sc_ev [] [] sc_pred }
+           ; mk_superclasses fuel rec_clss sc_ev [] [] sc_pred }
 
 {- Note [Improvement from Ground Wanteds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -633,29 +635,29 @@ dependencies.  See Note [Why adding superclasses can help] above.
 But no variables means no improvement; case closed.
 -}
 
-mk_superclasses :: NameSet -> CtEvidence
+mk_superclasses :: ExpansionFuel -> NameSet -> CtEvidence
                 -> [TyVar] -> ThetaType -> PredType -> TcS [Ct]
 -- Return this constraint, plus its superclasses, if any
-mk_superclasses rec_clss ev tvs theta pred
+mk_superclasses fuel rec_clss ev tvs theta pred
   | ClassPred cls tys <- classifyPredType pred
-  = mk_superclasses_of rec_clss ev tvs theta cls tys
+  = mk_superclasses_of fuel rec_clss ev tvs theta cls tys
 
   | otherwise   -- Superclass is not a class predicate
   = return [mkNonCanonical ev]
 
-mk_superclasses_of :: NameSet -> CtEvidence
+mk_superclasses_of :: ExpansionFuel -> NameSet -> CtEvidence
                    -> [TyVar] -> ThetaType -> Class -> [Type]
                    -> TcS [Ct]
 -- Always return this class constraint,
 -- and expand its superclasses
-mk_superclasses_of rec_clss ev tvs theta cls tys
+mk_superclasses_of fuel rec_clss ev tvs theta cls tys
   | loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys)
                     ; return [this_ct] }  -- cc_pend_sc of this_ct = True
   | otherwise  = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys
                                                           , ppr (isCTupleClass cls)
                                                           , ppr rec_clss
                                                           ])
-                    ; sc_cts <- mk_strict_superclasses rec_clss' ev tvs theta cls tys
+                    ; sc_cts <- mk_strict_superclasses fuel rec_clss' ev tvs theta cls tys
                     ; return (this_ct : sc_cts) }
                                    -- cc_pend_sc of this_ct = False
   where
@@ -664,9 +666,12 @@ mk_superclasses_of rec_clss ev tvs theta cls tys
                  -- Tuples never contribute to recursion, and can be nested
     rec_clss'  = rec_clss `extendNameSet` cls_nm
 
+    this_cc_pend | loop_found = fuel
+                 | otherwise = 0
+
     this_ct | null tvs, null theta
             = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
-                       , cc_pend_sc = loop_found }
+                       , cc_pend_sc = this_cc_pend }
                  -- NB: If there is a loop, we cut off, so we have not
                  --     added the superclasses, hence cc_pend_sc = True
             | otherwise
@@ -827,7 +832,7 @@ canForAllNC :: CtEvidence -> [TyVar] -> TcThetaType -> TcPredType
 canForAllNC ev tvs theta pred
   | isGiven ev  -- See Note [Eagerly expand given superclasses]
   , Just (cls, tys) <- cls_pred_tys_maybe
-  = do { sc_cts <- mkStrictSuperClasses ev tvs theta cls tys
+  = do { sc_cts <- mkStrictSuperClasses defaultExpansionFuel ev tvs theta cls tys
        ; emitWork sc_cts
        ; canForAll ev False }
 


=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -534,8 +534,8 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts })
 
     (sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
 
-    get_pending :: Ct -> [Ct] -> [Ct]  -- Get dicts with cc_pend_sc = True
-                                       -- but flipping the flag
+    get_pending :: Ct -> [Ct] -> [Ct]  -- Get dicts with cc_pend_sc > 0
+                                       -- but decrementing the fuel
     get_pending dict dicts
         | Just dict' <- pendingScDict_maybe dict
         , belongs_to_this_level (ctEvidence dict)


=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -10,7 +10,7 @@ module GHC.Tc.Types.Constraint (
         QCInst(..), pendingScInst_maybe,
 
         -- Canonical constraints
-        Xi, Ct(..), Cts,
+        Xi, Ct(..), Cts, ExpansionFuel, noExpansionFuel, defaultExpansionFuel,
         emptyCts, andCts, andManyCts, pprCts,
         singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
         isEmptyCts,
@@ -191,6 +191,15 @@ type Xi = TcType
 
 type Cts = Bag Ct
 
+-- | Says how many layers of superclasses can we expand.
+-- see T21909
+type ExpansionFuel = Int
+
+noExpansionFuel, defaultExpansionFuel :: Int
+noExpansionFuel = 0
+defaultExpansionFuel = 3
+
+
 data Ct
   -- Atomic canonical constraints
   = CDictCan {  -- e.g.  Num ty
@@ -199,10 +208,10 @@ data Ct
       cc_class  :: Class,
       cc_tyargs :: [Xi],   -- cc_tyargs are rewritten w.r.t. inerts, so Xi
 
-      cc_pend_sc :: Bool
+      cc_pend_sc :: ExpansionFuel
           -- See Note [The superclass story] in GHC.Tc.Solver.Canonical
-          -- True <=> (a) cc_class has superclasses
-          --          (b) we have not (yet) added those
+          -- n > 0 <=> (a) cc_class has superclasses
+          --           (b) we have not (yet) added those
           --              superclasses as Givens
     }
 
@@ -673,8 +682,8 @@ instance Outputable Ct where
          CEqCan {}        -> text "CEqCan"
          CNonCanonical {} -> text "CNonCanonical"
          CDictCan { cc_pend_sc = psc }
-            | psc          -> text "CDictCan(psc)"
-            | otherwise    -> text "CDictCan"
+            | psc > 0       -> text "CDictCan" <> parens (text "psc" <+> ppr psc)
+            | otherwise     -> text "CDictCan"
          CIrredCan { cc_reason = reason } -> text "CIrredCan" <> ppr reason
          CQuantCan (QCI { qci_pend_sc = pend_sc })
             | pend_sc   -> text "CQuantCan(psc)"
@@ -893,16 +902,17 @@ isUserTypeError pred = case getUserTypeErrorMsg pred of
                              _      -> False
 
 isPendingScDict :: Ct -> Bool
-isPendingScDict (CDictCan { cc_pend_sc = psc }) = psc
--- Says whether this is a CDictCan with cc_pend_sc is True;
+isPendingScDict (CDictCan { cc_pend_sc = psc }) = psc > 0
+-- Says whether this is a CDictCan with cc_pend_sc has positive fuel;
 -- i.e. pending un-expanded superclasses
 isPendingScDict _ = False
 
 pendingScDict_maybe :: Ct -> Maybe Ct
--- Says whether this is a CDictCan with cc_pend_sc is True,
+-- Says whether this is a CDictCan with cc_pend_sc has fuel left,
 -- AND if so flips the flag
-pendingScDict_maybe ct@(CDictCan { cc_pend_sc = True })
-                      = Just (ct { cc_pend_sc = False })
+pendingScDict_maybe ct@(CDictCan { cc_pend_sc = n })
+  | n > 0 = Just (ct { cc_pend_sc = n - 1 })
+  | otherwise = Nothing
 pendingScDict_maybe _ = Nothing
 
 pendingScInst_maybe :: QCInst -> Maybe QCInst


=====================================
testsuite/tests/typecheck/should_compile/T21909.hs
=====================================
@@ -0,0 +1,24 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module T21909 where
+
+import Data.Kind
+
+class (Monad m, MyMonad (Inner m)) => MyMonad m where
+  type Inner m :: Type -> Type
+  foo :: m Int
+
+works :: MyMonad m => m String
+works = show <$> ((+ 1) <$> foo)
+
+fails :: MyMonad m => m String
+fails = show <$> fooPlusOne
+  where
+    fooPlusOne = (+ 1) <$> foo
+
+alsoFails :: MyMonad m => m String
+alsoFails =
+  let fooPlusOne = (+ 1) <$> foo
+   in show <$> fooPlusOne


=====================================
testsuite/tests/typecheck/should_compile/T21909b.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableSuperClasses, FunctionalDependencies, MultiParamTypeClasses, GADTs #-}
+
+module T21909b where
+
+import Data.Kind
+
+class C [a] => C a where
+  foo :: a -> Int
+
+should_work :: C a => a -> Int
+should_work x = foolocal x
+  where
+    foolocal a = foo a


=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -857,3 +857,5 @@ test('T22647', normal, compile, [''])
 test('T19577', normal, compile, [''])
 test('T22383', normal, compile, [''])
 test('T21501', normal, compile, [''])
+test('T21909', normal, compile, [''])
+test('T21909b', normal, compile, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/93d04d3eb5d8a32ef122c298ab3ddacc67305d39

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/93d04d3eb5d8a32ef122c298ab3ddacc67305d39
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/20230206/e44edfe5/attachment-0001.html>


More information about the ghc-commits mailing list