[Git][ghc/ghc][master] 2 commits: Fix shadowing lacuna in OccurAnal

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Wed Dec 21 19:32:53 UTC 2022



Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
e193e537 by Simon Peyton Jones at 2022-12-21T14:32:30-05:00
Fix shadowing lacuna in OccurAnal

Issue #22623 demonstrated another lacuna in the implementation
of wrinkle (BS3) in Note [The binder-swap substitution] in
the occurrence analyser.

I was failing to add TyVar lambda binders using
addInScope/addOneInScope and that led to a totally bogus binder-swap
transformation.

Very easy to fix.

- - - - -
3d55d8ab by Simon Peyton Jones at 2022-12-21T14:32:30-05:00
Fix an assertion check in addToEqualCtList

The old assertion saw that a constraint ct could rewrite itself
(of course it can) and complained (stupid).

Fixes #22645

- - - - -


9 changed files:

- compiler/GHC/Core/Opt/OccurAnal.hs
- compiler/GHC/Core/Opt/Simplify.hs
- compiler/GHC/Tc/Solver/Types.hs
- + testsuite/tests/simplCore/should_compile/T22623.hs
- + testsuite/tests/simplCore/should_compile/T22623a.hs
- testsuite/tests/simplCore/should_compile/all.T
- + testsuite/tests/typecheck/should_fail/T22645.hs
- + testsuite/tests/typecheck/should_fail/T22645.stderr
- testsuite/tests/typecheck/should_fail/all.T


Changes:

=====================================
compiler/GHC/Core/Opt/OccurAnal.hs
=====================================
@@ -1820,7 +1820,8 @@ occAnalLam :: OccEnv -> CoreExpr -> (WithUsageDetails CoreExpr)
 
 occAnalLam env (Lam bndr expr)
   | isTyVar bndr
-  = let (WithUsageDetails usage expr') = occAnalLam env expr
+  = let env1 = addOneInScope env bndr
+        WithUsageDetails usage expr' = occAnalLam env1 expr
     in WithUsageDetails usage (Lam bndr expr')
        -- Important: Keep the 'env' unchanged so that with a RHS like
        --   \(@ x) -> K @x (f @x)
@@ -2466,10 +2467,11 @@ data OccEnv
            -- If  x :-> (y, co)  is in the env,
            -- then please replace x by (y |> mco)
            -- Invariant of course: idType x = exprType (y |> mco)
-           , occ_bs_env  :: !(VarEnv (OutId, MCoercion))
-           , occ_bs_rng  :: !VarSet   -- Vars free in the range of occ_bs_env
+           , occ_bs_env  :: !(IdEnv (OutId, MCoercion))
                    -- Domain is Global and Local Ids
                    -- Range is just Local Ids
+           , occ_bs_rng  :: !VarSet
+                   -- Vars (TyVars and Ids) free in the range of occ_bs_env
     }
 
 
@@ -2546,14 +2548,15 @@ isRhsEnv (OccEnv { occ_encl = cxt }) = case cxt of
                                           _      -> False
 
 addOneInScope :: OccEnv -> CoreBndr -> OccEnv
+-- Needed for all Vars not just Ids
+-- See Note [The binder-swap substitution] (BS3)
 addOneInScope env@(OccEnv { occ_bs_env = swap_env, occ_bs_rng = rng_vars }) bndr
   | bndr `elemVarSet` rng_vars = env { occ_bs_env = emptyVarEnv, occ_bs_rng = emptyVarSet }
   | otherwise                  = env { occ_bs_env = swap_env `delVarEnv` bndr }
 
 addInScope :: OccEnv -> [Var] -> OccEnv
--- See Note [The binder-swap substitution]
--- It's only necessary to call this on in-scope Ids,
--- but harmless to include TyVars too
+-- Needed for all Vars not just Ids
+-- See Note [The binder-swap substitution] (BS3)
 addInScope env@(OccEnv { occ_bs_env = swap_env, occ_bs_rng = rng_vars }) bndrs
   | any (`elemVarSet` rng_vars) bndrs = env { occ_bs_env = emptyVarEnv, occ_bs_rng = emptyVarSet }
   | otherwise                         = env { occ_bs_env = swap_env `delVarEnvList` bndrs }
@@ -2712,25 +2715,29 @@ Some tricky corners:
 
 (BS3) We need care when shadowing.  Suppose [x :-> b] is in occ_bs_env,
       and we encounter:
-         - \x. blah
-           Here we want to delete the x-binding from occ_bs_env
-
-         - \b. blah
-           This is harder: we really want to delete all bindings that
-           have 'b' free in the range.  That is a bit tiresome to implement,
-           so we compromise.  We keep occ_bs_rng, which is the set of
-           free vars of rng(occc_bs_env).  If a binder shadows any of these
-           variables, we discard all of occ_bs_env.  Safe, if a bit
-           brutal.  NB, however: the simplifer de-shadows the code, so the
-           next time around this won't happen.
+         (i) \x. blah
+             Here we want to delete the x-binding from occ_bs_env
+
+         (ii) \b. blah
+              This is harder: we really want to delete all bindings that
+              have 'b' free in the range.  That is a bit tiresome to implement,
+              so we compromise.  We keep occ_bs_rng, which is the set of
+              free vars of rng(occc_bs_env).  If a binder shadows any of these
+              variables, we discard all of occ_bs_env.  Safe, if a bit
+              brutal.  NB, however: the simplifer de-shadows the code, so the
+              next time around this won't happen.
 
       These checks are implemented in addInScope.
-
-      The occurrence analyser itself does /not/ do cloning. It could, in
-      principle, but it'd make it a bit more complicated and there is no
-      great benefit. The simplifer uses cloning to get a no-shadowing
-      situation, the care-when-shadowing behaviour above isn't needed for
-      long.
+      (i) is needed only for Ids, but (ii) is needed for tyvars too (#22623)
+      because if occ_bs_env has [x :-> ...a...] where `a` is a tyvar, we
+      must not replace `x` by `...a...` under /\a. ...x..., or similarly
+      under a case pattern match that binds `a`.
+
+      An alternative would be for the occurrence analyser to do cloning as
+      it goes.  In principle it could do so, but it'd make it a bit more
+      complicated and there is no great benefit. The simplifer uses
+      cloning to get a no-shadowing situation, the care-when-shadowing
+      behaviour above isn't needed for long.
 
 (BS4) The domain of occ_bs_env can include GlobaIds.  Eg
          case M.foo of b { alts }


=====================================
compiler/GHC/Core/Opt/Simplify.hs
=====================================
@@ -132,7 +132,11 @@ data SimplifyOpts = SimplifyOpts
   { so_dump_core_sizes :: !Bool
   , so_iterations      :: !Int
   , so_mode            :: !SimplMode
+
   , so_pass_result_cfg :: !(Maybe LintPassResultConfig)
+                          -- Nothing => Do not Lint
+                          -- Just cfg => Lint like this
+
   , so_hpt_rules       :: !RuleBase
   , so_top_env_cfg     :: !TopEnvConfig
   }


=====================================
compiler/GHC/Tc/Solver/Types.hs
=====================================
@@ -273,21 +273,29 @@ addToEqualCtList ct old_eqs
   | debugIsOn
   = case ct of
       CEqCan { cc_lhs = TyVarLHS tv } ->
-        let shares_lhs (CEqCan { cc_lhs = TyVarLHS old_tv }) = tv == old_tv
-            shares_lhs _other                                = False
-        in
-        assert (all shares_lhs old_eqs) $
-        assert (null ([ (ct1, ct2) | ct1 <- ct : old_eqs
-                                   , ct2 <- ct : old_eqs
-                                   , let { fr1 = ctFlavourRole ct1
-                                         ; fr2 = ctFlavourRole ct2 }
-                                   , fr1 `eqCanRewriteFR` fr2 ])) $
+        assert (all (shares_lhs tv) old_eqs) $
+        assertPpr (null bad_prs)
+                  (vcat [ text "bad_prs" <+> ppr bad_prs
+                        , text "ct:old_eqs" <+> ppr (ct : old_eqs) ]) $
         (ct : old_eqs)
 
       _ -> pprPanic "addToEqualCtList not CEqCan" (ppr ct)
 
   | otherwise
   = ct : old_eqs
+  where
+    shares_lhs tv (CEqCan { cc_lhs = TyVarLHS old_tv }) = tv == old_tv
+    shares_lhs _ _ = False
+    bad_prs = filter is_bad_pair (distinctPairs (ct : old_eqs))
+    is_bad_pair (ct1,ct2) = ctFlavourRole ct1 `eqCanRewriteFR` ctFlavourRole ct2
+
+distinctPairs :: [a] -> [(a,a)]
+-- distinctPairs [x1,...xn] is the list of all pairs [ ...(xi, xj)...]
+--                             where i /= j
+-- NB: does not return pairs (xi,xi), which would be stupid in the
+--     context of addToEqualCtList (#22645)
+distinctPairs []     = []
+distinctPairs (x:xs) = concatMap (\y -> [(x,y),(y,x)]) xs ++ distinctPairs xs
 
 -- returns Nothing when the new list is empty, to keep the environments smaller
 filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList


=====================================
testsuite/tests/simplCore/should_compile/T22623.hs
=====================================
@@ -0,0 +1,34 @@
+{-# LANGUAGE GHC2021 #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module T22623 where
+
+import T22623a
+
+type BindNonEmptyList :: NonEmpty -> NonEmpty -> [Q]
+type family BindNonEmptyList (x :: NonEmpty) (y :: NonEmpty) :: [Q] where
+  BindNonEmptyList ('(:|) a as) c = Tail c ++ Foldr2 a c as
+
+sBindNonEmptyList ::
+  forall (t :: NonEmpty)
+         (c :: NonEmpty). SNonEmpty t -> SNonEmpty c -> SList (BindNonEmptyList t c :: [Q])
+sBindNonEmptyList
+  ((:%|) (sA :: SQ a) (sAs :: SList as)) (sC :: SNonEmpty c)
+  = let
+      sMyHead :: SNonEmpty c -> SQ (MyHead a c)
+      sMyHead ((:%|) x _) = x
+
+      sFoldr :: forall t. SList t -> SList (Foldr2 a c t)
+      sFoldr SNil = SNil
+      sFoldr (SCons _ sYs) = SCons (sMyHead sC) (sFoldr sYs)
+
+      sF :: Id (SLambda (ConstSym1 c))
+      sF = SLambda (const sC)
+
+      sBs :: SList (Tail c)
+      _ :%| sBs = applySing sF sA
+    in
+      sBs %++ sFoldr sAs


=====================================
testsuite/tests/simplCore/should_compile/T22623a.hs
=====================================
@@ -0,0 +1,60 @@
+{-# LANGUAGE GHC2021 #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T22623a where
+
+import Data.Kind
+
+type Id :: Type -> Type
+type family Id x
+type instance Id x = x
+
+data Q
+data SQ (x :: Q)
+
+data NonEmpty where
+  (:|) :: Q -> [Q] -> NonEmpty
+
+type Tail :: NonEmpty -> [Q]
+type family Tail y where
+  Tail ('(:|) _ y) = y
+type MyHead :: Q -> NonEmpty -> Q
+type family MyHead x y where
+  MyHead _ ('(:|) c _) = c
+
+type SList :: [Q] -> Type
+data SList z where
+  SNil  :: SList '[]
+  SCons :: SQ x -> SList xs -> SList (x:xs)
+
+type SNonEmpty :: NonEmpty -> Type
+data SNonEmpty z where
+  (:%|) :: SQ x -> SList xs -> SNonEmpty (x :| xs)
+
+data TyFun
+type F = TyFun -> Type
+
+type Apply :: F -> Q -> NonEmpty
+type family Apply f x
+
+type ConstSym1 :: NonEmpty -> F
+data ConstSym1 (x :: NonEmpty) :: F
+type instance Apply (ConstSym1 x) _ = x
+
+type SLambda :: F -> Type
+newtype SLambda (f :: F) =
+  SLambda { applySing :: forall t. SQ t -> SNonEmpty (f `Apply` t) }
+
+type Foldr2 :: Q -> NonEmpty -> [Q] -> [Q]
+type family Foldr2 a c x where
+  Foldr2 _ _ '[] = '[]
+  Foldr2 a c (_:ys) = MyHead a c : Foldr2 a c ys
+
+type (++) :: [Q] -> [Q] -> [Q]
+type family (++) xs ys where
+  (++) '[] ys = ys
+  (++) ('(:) x xs) ys = '(:) x (xs ++ ys)
+
+(%++) :: forall (x :: [Q]) (y :: [Q]). SList x -> SList y -> SList (x ++ y)
+(%++) SNil sYs = sYs
+(%++) (SCons sX sXs) sYs = SCons sX (sXs %++ sYs)


=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -459,3 +459,4 @@ test('T22491', normal, compile, ['-O2'])
 test('T21476', normal, compile, [''])
 test('T22272', normal, multimod_compile, ['T22272', '-O -fexpose-all-unfoldings -fno-omit-interface-pragmas -fno-ignore-interface-pragmas'])
 test('T22459', normal, compile, [''])
+test('T22623', normal, multimod_compile, ['T22623', '-O -v0'])


=====================================
testsuite/tests/typecheck/should_fail/T22645.hs
=====================================
@@ -0,0 +1,9 @@
+module T22645 where
+
+import Data.Coerce
+
+type T :: (* -> *) -> * -> *
+data T m a = MkT (m a)
+
+p :: Coercible a b => T Maybe a -> T Maybe b
+p = coerce


=====================================
testsuite/tests/typecheck/should_fail/T22645.stderr
=====================================
@@ -0,0 +1,15 @@
+
+T22645.hs:9:5: error: [GHC-25897]
+    • Couldn't match type ‘a’ with ‘b’ arising from a use of ‘coerce’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          p :: forall a b. Coercible a b => T Maybe a -> T Maybe b
+        at T22645.hs:8:1-44
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          p :: forall a b. Coercible a b => T Maybe a -> T Maybe b
+        at T22645.hs:8:1-44
+    • In the expression: coerce
+      In an equation for ‘p’: p = coerce
+    • Relevant bindings include
+        p :: T Maybe a -> T Maybe b (bound at T22645.hs:9:1)


=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -666,3 +666,4 @@ test('T21447', normal, compile_fail, [''])
 test('T21530a', normal, compile_fail, [''])
 test('T21530b', normal, compile_fail, [''])
 test('T22570', normal, compile_fail, [''])
+test('T22645', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/df7bc6b36d16e91f3e9e96e9542885e544bbf4d0...3d55d8ab51ece43c51055c43c9e7aba77cce46c0

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/df7bc6b36d16e91f3e9e96e9542885e544bbf4d0...3d55d8ab51ece43c51055c43c9e7aba77cce46c0
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/20221221/d01a587c/attachment-0001.html>


More information about the ghc-commits mailing list