[Git][ghc/ghc][wip/romes/eqsat-pmc] Fixes

Rodrigo Mesquita (@alt-romes) gitlab at gitlab.haskell.org
Tue Aug 1 17:29:54 UTC 2023



Rodrigo Mesquita pushed to branch wip/romes/eqsat-pmc at Glasgow Haskell Compiler / GHC


Commits:
ba19d6dd by Rodrigo Mesquita at 2023-08-01T18:29:41+01:00
Fixes

- - - - -


4 changed files:

- compiler/GHC/Core.hs
- compiler/GHC/Core/Equality.hs
- compiler/GHC/HsToCore/Pmc.hs
- compiler/GHC/HsToCore/Pmc/Check.hs


Changes:

=====================================
compiler/GHC/Core.hs
=====================================
@@ -295,6 +295,7 @@ data AltCon
 -- The instance adheres to the order described in Note [Case expression invariants]
 instance Ord AltCon where
   compare (DataAlt con1) (DataAlt con2) =
+    -- ROMES:TODO: Couldn't simply do this right by comparing the dataConName of the cons?
     assert (dataConTyCon con1 == dataConTyCon con2) $
     compare (dataConTag con1) (dataConTag con2)
   compare (DataAlt _) _ = GT


=====================================
compiler/GHC/Core/Equality.hs
=====================================
@@ -3,17 +3,14 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DerivingVia #-}
 
 module GHC.Core.Equality where
 
--- ROMES:TODO:
--- I think, for the particular usages of Core e-graphs, we can do much better
--- than this for equality.
--- E.g. representation could transform the CoreExpr to an actual debruijnized one (with Ints for Vars)
-
 import GHC.Prelude
 
 import GHC.Core
+import GHC.Core.DataCon
 import GHC.Core.TyCo.Rep
 import GHC.Core.Map.Type
 import GHC.Types.Var
@@ -37,10 +34,10 @@ import Control.Monad.Trans.Reader
 -- Perhaps it'd really be better to make DeBruijn work over these types
 
 -- In the pattern match checker, expressions will always be kind of shallow.
--- In practice, no-one writes gigantic lambda expressions
+-- In practice, no-one writes gigantic lambda expressions in guards and view patterns
 
 data AltF a
-    = AltF AltCon [()] a
+    = AltF AltCon' [()] a
     deriving (Functor, Foldable, Traversable, Eq, Ord)
 
 data BindF a
@@ -60,7 +57,7 @@ data ExprF a
 
   -- | CastF a (DeBruijn CoercionR) -- can we drop this
   -- | TickF CoreTickish a          -- this, when representing expressions for equality?
-  -- but it'll be pretty hard to trigger any bug related to equality matching wrt coercions and casts on view patterns solely
+  -- but it'll be pretty hard to trigger any bug related to equality matching wrt coercions and casts on view and guard patterns solely
   | TypeF DBType
   | CoercionF DBCoercion
   deriving (Functor, Foldable, Traversable, Eq, Ord)
@@ -72,10 +69,20 @@ newtype DBCoercion = DBC (DeBruijn Coercion) deriving Eq
 instance Ord DBCoercion where
   compare (DBC dt) (DBC dt') = cmpDeBruijnCoercion dt dt'
 
+newtype AltCon' = AC' AltCon deriving Eq
+                             deriving Outputable via AltCon
+
+instance Ord AltCon' where
+  compare (AC' (DataAlt a)) (AC' (DataAlt b))
+    = case compare (dataConName a) (dataConName b) of
+        LT -> LT
+        EQ -> compare (DataAlt a) (DataAlt b) -- AltCon's Ord instance only works for same datatypes
+        GT -> GT
+  compare (AC' a) (AC' b) = compare a b
 
 -- this makes perfect sense, if we already have to represent this in the e-graph
 -- we might as well make it a better suited representation for the e-graph...
--- keeping the on-fly debruijn makes no sense
+-- keeping the on-fly debruijn is harder
 representCoreExprEgr :: forall a
                    . Analysis a CoreExprF
                   => CoreExpr
@@ -93,7 +100,7 @@ representCoreExprEgr expr egr = EGM.runEGraphM egr (runReaderT (go expr) emptyCM
     Type t  -> addE (TypeF (DBT $ deBruijnize t))
     Coercion c -> addE (CoercionF (DBC $ deBruijnize c))
     Tick _ e -> go e -- bypass ticks!
-    Cast e _ -> go e -- bypass casts! ouch?
+    Cast e _ -> go e -- bypass casts! ouch? TODO
     App f a -> do
       f' <- go f
       a' <- go a
@@ -117,305 +124,14 @@ representCoreExprEgr expr egr = EGM.runEGraphM egr (runReaderT (go expr) emptyCM
   goAlt :: CoreAlt -> ReaderT CmEnv (EGM.EGraphM a CoreExprF) (CoreAltF ClassId)
   goAlt (Alt c bs e) = do
     e' <- local (`extendCMEs` bs) $ go e
-    return (AltF c (map (const ()) bs) e')
+    return (AltF (AC' c) (map (const ()) bs) e')
 
   addE :: Analysis a CoreExprF => CoreExprF ClassId -> ReaderT CmEnv (EGM.EGraphM a CoreExprF) ClassId
   addE e = lift $ EGM.add $ Node e
---  Var v   -> add (Node $ DF (D cmenv (VarF v)))   eg0
---  Lit lit -> add (Node $ DF (D cmenv (LitF lit))) eg0
---  Type t  -> add (Node $ DF (D cmenv (TypeF t)))  eg0
---  Coercion c -> add (Node $ DF (D cmenv (CoercionF c))) eg0
---  Cast e co  -> let (eid,eg1) = representDBCoreExpr (D cmenv e) eg0
---                 in add (Node $ DF (D cmenv (CastF eid co))) eg1
---  App f a -> let (fid,eg1) = representDBCoreExpr (D cmenv f) eg0
---                 (aid,eg2) = representDBCoreExpr (D cmenv a) eg1
---              in add (Node $ DF (D cmenv (AppF fid aid))) eg2
---  Tick n e -> let (eid,eg1) = representDBCoreExpr (D cmenv e) eg0
---               in add (Node $ DF (D cmenv (TickF n eid))) eg1
---  Lam b e  -> let (eid,eg1) = representDBCoreExpr (D (extendCME cmenv b) e) eg0
---               in add (Node $ DF (D cmenv (LamF b eid))) eg1
---  Let (NonRec v r) e -> let (rid,eg1) = representDBCoreExpr (D cmenv r) eg0
---                            (eid,eg2) = representDBCoreExpr (D (extendCME cmenv v) e) eg1
---                         in add (Node $ DF (D cmenv (LetF (NonRecF v rid) eid))) eg2
---  Let (Rec (unzip -> (bs,rs))) e ->
---    let cmenv' = extendCMEs cmenv bs
---        (bsids, eg1) = EGM.runEGraphM eg0 $
---                         traverse (state . representDBCoreExpr . D cmenv') rs
---        (eid, eg2)  = representDBCoreExpr (D cmenv' e) eg1
---     in add (Node $ DF (D cmenv (LetF (RecF (zip bs bsids)) eid))) eg2
---  Case e b t as -> let (eid, eg1)  = representDBCoreExpr (D cmenv e) eg0
---                       (as', eg2) = EGM.runEGraphM eg1 $
---                         traverse (state . representDBAltExpr . D (extendCME cmenv b)) as
---                    in add (Node $ DF (D cmenv (CaseF eid b t as'))) eg2
-
-type CoreExprF
-  = ExprF
-type CoreAltF
-  = AltF
-type CoreBindF
-  = BindF
-
---eqDeBruijnExprF :: forall a. Eq a => DeBruijn (CoreExprF a) -> DeBruijn (CoreExprF a) -> Bool
---eqDeBruijnExprF (D env1 e1) (D env2 e2) = go e1 e2 where
---    go :: CoreExprF a -> CoreExprF a -> Bool
---    go (VarF v1) (VarF v2)             = eqDeBruijnVar (D env1 v1) (D env2 v2)
---    go (LitF lit1)    (LitF lit2)      = lit1 == lit2
---    go (TypeF t1)    (TypeF t2)        = eqDeBruijnType (D env1 t1) (D env2 t2)
---    -- See Note [Alpha-equality for Coercion arguments]
---    go (CoercionF {}) (CoercionF {}) = True
---    go (CastF e1 co1) (CastF e2 co2) = D env1 co1 == D env2 co2 && e1 == e2
---    go (AppF f1 a1)   (AppF f2 a2)   = f1 == f2 && a1 == a2
---    go (TickF n1 e1) (TickF n2 e2)
---      =  eqDeBruijnTickish (D env1 n1) (D env2 n2)
---      && e1 == e2
-
---    go (LamF b1 e1)  (LamF b2 e2)
---      =  eqDeBruijnType (D env1 (varType b1)) (D env2 (varType b2))
---      && D env1 (varMultMaybe b1) == D env2 (varMultMaybe b2)
---      && e1 == e2
-
---    go (LetF abs e1) (LetF bbs e2)
---      = D env1 abs == D env2 bbs
---      && e1 == e2
-
---    go (CaseF e1 _b1 t1 a1) (CaseF e2 _b2 t2 a2)
---      | null a1   -- See Note [Empty case alternatives]
---      = null a2 && e1 == e2 && D env1 t1 == D env2 t2
---      | otherwise
---      = e1 == e2 && D env1 a1 == D env2 a2
-
---    go _ _ = False
-
----- ROMES:TODO: This one can be derived automatically, but perhaps it's better
----- to be explicit here? We don't even really require the DeBruijn context here
---eqDeBruijnAltF :: forall a. Eq a => DeBruijn (CoreAltF a) -> DeBruijn (CoreAltF a) -> Bool
---eqDeBruijnAltF (D _env1 a1) (D _env2 a2) = go a1 a2 where
---    go (AltF DEFAULT _ rhs1) (AltF DEFAULT _ rhs2)
---        = rhs1 == rhs2
---    go (AltF (LitAlt lit1) _ rhs1) (AltF (LitAlt lit2) _ rhs2)
---        = lit1 == lit2 && rhs1 == rhs2
---    go (AltF (DataAlt dc1) _bs1 rhs1) (AltF (DataAlt dc2) _bs2 rhs2)
---        = dc1 == dc2 &&
---          rhs1 == rhs2 -- the CM environments were extended on representation (see 'representDBAltExpr')
---    go _ _ = False
-
----- | 'unsafeCoerce' mostly because I'm too lazy to write the boilerplate.
---fromCoreExpr :: CoreExpr -> Fix CoreExprF
---fromCoreExpr = unsafeCoerce
-
---toCoreExpr :: CoreExpr -> Fix CoreExprF
---toCoreExpr = unsafeCoerce
-
----- | Represents a DeBruijn CoreExpr being careful to correctly debruijnizie the expression as it is represented
-----
----- Always represent Ids, at least for now. We're seemingly using inexistent ids
----- ROMES:TODO: do this all inside EGraphM instead
---representDBCoreExpr :: Analysis a (DeBruijnF CoreExprF)
---                    => DeBruijn CoreExpr
---                    -> EGraph a (DeBruijnF CoreExprF)
---                    -> (ClassId, EGraph a (DeBruijnF CoreExprF))
---representDBCoreExpr (D cmenv expr) eg0 = case expr of
---  Var v   -> add (Node $ DF (D cmenv (VarF v)))   eg0
---  Lit lit -> add (Node $ DF (D cmenv (LitF lit))) eg0
---  Type t  -> add (Node $ DF (D cmenv (TypeF t)))  eg0
---  Coercion c -> add (Node $ DF (D cmenv (CoercionF c))) eg0
---  Cast e co  -> let (eid,eg1) = representDBCoreExpr (D cmenv e) eg0
---                 in add (Node $ DF (D cmenv (CastF eid co))) eg1
---  App f a -> let (fid,eg1) = representDBCoreExpr (D cmenv f) eg0
---                 (aid,eg2) = representDBCoreExpr (D cmenv a) eg1
---              in add (Node $ DF (D cmenv (AppF fid aid))) eg2
---  Tick n e -> let (eid,eg1) = representDBCoreExpr (D cmenv e) eg0
---               in add (Node $ DF (D cmenv (TickF n eid))) eg1
---  Lam b e  -> let (eid,eg1) = representDBCoreExpr (D (extendCME cmenv b) e) eg0
---               in add (Node $ DF (D cmenv (LamF b eid))) eg1
---  Let (NonRec v r) e -> let (rid,eg1) = representDBCoreExpr (D cmenv r) eg0
---                            (eid,eg2) = representDBCoreExpr (D (extendCME cmenv v) e) eg1
---                         in add (Node $ DF (D cmenv (LetF (NonRecF v rid) eid))) eg2
---  Let (Rec (unzip -> (bs,rs))) e ->
---    let cmenv' = extendCMEs cmenv bs
---        (bsids, eg1) = EGM.runEGraphM eg0 $
---                         traverse (state . representDBCoreExpr . D cmenv') rs
---        (eid, eg2)  = representDBCoreExpr (D cmenv' e) eg1
---     in add (Node $ DF (D cmenv (LetF (RecF (zip bs bsids)) eid))) eg2
---  Case e b t as -> let (eid, eg1)  = representDBCoreExpr (D cmenv e) eg0
---                       (as', eg2) = EGM.runEGraphM eg1 $
---                         traverse (state . representDBAltExpr . D (extendCME cmenv b)) as
---                    in add (Node $ DF (D cmenv (CaseF eid b t as'))) eg2
-
---representDBAltExpr :: Analysis a (DeBruijnF CoreExprF)
---                   => DeBruijn CoreAlt
---                   -> EGraph a (DeBruijnF CoreExprF)
---                   -> (CoreAltF ClassId, EGraph a (DeBruijnF CoreExprF))
---representDBAltExpr (D cm (Alt cons bs a)) eg0 =
---  let (ai, eg1) = representDBCoreExpr (D (extendCMEs cm bs) a) eg0
---   in (AltF cons bs ai, eg1)
-
---instance Eq a => Eq (DeBruijn (CoreAltF a)) where
---  (==) = eqDeBruijnAltF
-
---instance Eq a => Eq (DeBruijn (CoreExprF a)) where
---  (==) = eqDeBruijnExprF
-
---instance Eq a => Eq (DeBruijnF CoreExprF a) where
---  (==) (DF a) (DF b) = eqDeBruijnExprF a b
-
---instance Eq a => Eq (DeBruijnF CoreAltF a) where
---  (==) (DF a) (DF b) = eqDeBruijnAltF a b
-
---deriving instance Ord a => Ord (DeBruijnF CoreExprF a)
-
---instance Ord a => Ord (DeBruijn (CoreExprF a)) where
---  -- We must assume that if `a` is DeBruijn expression, it is already correctly "extended" because 'representDBCoreExpr' ensures that.
---  -- RM:TODO: We don't yet compare the CmEnv at any point. Should we?
---  -- RM: I don't think so, the CmEnv is used to determine whether bound variables are equal, but they don't otherwise influence the result.
---  -- Or rather, if the subexpression with variables is equal, then the CmEnv is necessarily equal too?
---  -- So I think that just works...
---  -- Wait, in that sense, couldn't we find a way to derive ord? the important part being that to compare Types and Vars we must use the DeBruijn Env ...
---  compare a b
---    = case a of
---        D cma (VarF va)
---          -> case b of
---               D cmb (VarF vb) -> cmpDeBruijnVar (D cma va) (D cmb vb)
---               _ -> LT
---        D _ (LitF la)
---          -> case b of
---               D _ VarF{} -> GT
---               D _ (LitF lb) -> la `compare` lb
---               _ -> LT
---        D _ (AppF af aarg)
---          -> case dataToTag# b of
---               bt
---                 -> if tagToEnum# (bt ># 2#) then
---                        LT
---                    else
---                        case b of
---                          D _ (AppF bf barg)
---                            -> case compare af bf of
---                                 LT -> LT
---                                 EQ -> aarg `compare` barg -- e.g. here, if we had for children other expresssions debruijnized, they would have the *correct* environments, so we needn't worry.
---                                                           -- the issue to automatically deriving is only really the 'Var' and 'Type' parameters ...
---                                 GT -> GT
---                          _ -> GT
---        D _ (LamF _abind abody)
---          -> case dataToTag# b of
---               bt
---                 -> if tagToEnum# (bt ># 3#) then
---                        LT
---                    else
---                        case b of
---                          D _ (LamF _bbind bbody) -- we can ignore the binder since the represented DB expression has the correct DB environments by construction (see 'representDBCoreExpr')
---                            -> compare abody bbody
---                          _ -> GT
---        D cma (LetF as abody)
---          -> case dataToTag# b of
---               bt
---                 -> if tagToEnum# (bt ># 4#) then
---                        LT
---                    else
---                        case b of
---                          D cmb (LetF bs bbody)
---                            -> case compare (D cma as) (D cmb bs) of
---                                 LT -> LT
---                                 EQ -> compare abody bbody
---                                 GT -> GT
---                          _ -> GT
---        D cma (CaseF cax _cabind catype caalt)
---          -> case dataToTag# b of
---               bt
---                 -> if tagToEnum# (bt <# 5#) then
---                        GT
---                    else
---                        case b of
---                          D cmb (CaseF cbx _cbbind cbtype cbalt)
---                            -> case compare cax cbx of
---                                 LT -> LT
---                                 -- ROMES:TODO: Consider changing order of comparisons to a more efficient one
---                                 EQ -> case cmpDeBruijnType (D cma catype) (D cmb cbtype) of
---                                        LT -> LT
---                                        EQ -> D cma caalt `compare` D cmb cbalt
---                                        GT -> GT
---                                 GT -> GT
---                          _ -> LT
---        D cma (CastF cax caco)
---          -> case dataToTag# b of
---               bt
---                 -> if tagToEnum# (bt <# 6#) then
---                        GT
---                    else
---                        case b of
---                          D cmb (CastF cbx cbco)
---                            -> case compare cax cbx of
---                                 LT -> LT
---                                 EQ -> cmpDeBruijnCoercion (D cma caco) (D cmb cbco)
---                                 GT -> GT
---                          _ -> LT
---        D cma (TickF tatickish tax)
---          -> case dataToTag# b of
---               bt
---                 -> if tagToEnum# (bt <# 7#) then
---                        GT
---                    else
---                        case b of
---                          D cmb (TickF tbtickish tbx)
---                            -> case cmpDeBruijnTickish (D cma tatickish) (D cmb tbtickish) of
---                                 LT -> LT
---                                 EQ -> tax `compare` tbx
---                                 GT -> GT
---                          _ -> LT
---        D cma (TypeF at)
---          -> case b of
---               D _    CoercionF{} -> LT
---               D cmb (TypeF bt) -> cmpDeBruijnType (D cma at) (D cmb bt)
---               _ -> GT
---        D cma (CoercionF aco)
---          -> case b of
---               D cmb (CoercionF bco) -> cmpDeBruijnCoercion (D cma aco) (D cmb bco)
---               _ -> GT
-
---instance Eq a => Eq (DeBruijn (CoreBindF a)) where
---  D cma a == D cmb b = go a b where
---    go (NonRecF _v1 r1) (NonRecF _v2 r2)
---      = r1 == r2 -- See Note [Alpha-equality for let-bindings]
-
---    go (RecF ps1) (RecF ps2)
---      =
---      -- See Note [Alpha-equality for let-bindings]
---      all2 (\b1 b2 -> eqDeBruijnType (D cma (varType b1))
---                                     (D cmb (varType b2)))
---           bs1 bs2
---      && rs1 == rs2
---      where
---        (bs1,rs1) = unzip ps1
---        (bs2,rs2) = unzip ps2
-
---    go _ _ = False
-
-
---instance Ord a => Ord (DeBruijn (CoreBindF a)) where
---  compare a b
---    = case a of
---        D _cma (NonRecF _ab ax)
---          -> case b of
---               D _cmb (NonRecF _bb bx) -- Again, we ignore the binders bc on representation they were accounted for correctly.
---                 -> ax `compare` bx
---               _ -> LT
---        D _cma (RecF as)
---          -> case b of
---               D _cmb (RecF bs) -> compare (map snd as) (map snd bs)
---               _ -> GT
-
 
---instance Ord a => Ord (DeBruijn (CoreAltF a)) where
---  compare a b
---    = case a of
---        D _cma (AltF ac _abs arhs)
---          -> case b of
---               D _cmb (AltF bc _bbs brhs)
---                 -> case compare ac bc of
---                      LT -> LT
---                      EQ -> -- Again, we don't look at binders bc we assume on representation they were accounted for correctly.
---                        arhs `compare` brhs
---                      GT -> GT
+type CoreExprF = ExprF
+type CoreAltF = AltF
+type CoreBindF = BindF
 
 cmpDeBruijnTickish :: DeBruijn CoreTickish -> DeBruijn CoreTickish -> Ordering
 cmpDeBruijnTickish (D env1 t1) (D env2 t2) = go t1 t2 where
@@ -433,7 +149,7 @@ cmpDeBruijnType :: DeBruijn Type -> DeBruijn Type -> Ordering
 cmpDeBruijnType d1@(D _ t1) d2@(D _ t2)
   = if eqDeBruijnType d1 d2
        then EQ
-       -- ROMES:TODO: Is this OK?
+       -- ROMES:TODO: This definitely does not look OK.
        else compare (showPprUnsafe t1) (showPprUnsafe t2)
 
 cmpDeBruijnCoercion :: DeBruijn Coercion -> DeBruijn Coercion -> Ordering


=====================================
compiler/GHC/HsToCore/Pmc.hs
=====================================
@@ -103,19 +103,19 @@ noCheckDs = updTopFlags (\dflags -> foldl' wopt_unset dflags allPmCheckWarnings)
 pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM Nablas
 pmcPatBind ctxt@(DsMatchContext match_ctxt loc) var p
   = mb_discard_warnings $ do
-      !missing <- getLdiNablas
+      !missing0 <- getLdiNablas
 
       -- See Note (TODO) [Represent the MatchIds before the CheckAction]
-      let missing' = representIdNablas var missing
+      let missing = representIdNablas var missing0
 
       pat_bind <- noCheckDs $ desugarPatBind loc var p
-      tracePm "pmcPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing'])
-      result <- unCA (checkPatBind pat_bind) missing'
+      tracePm "pmcPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
+      result <- unCA (checkPatBind pat_bind) missing
       let ldi = ldiGRHS $ ( \ pb -> case pb of PmPatBind grhs -> grhs) $ cr_ret result
       tracePm "pmcPatBind }: " $
         vcat [ text "cr_uncov:" <+> ppr (cr_uncov result)
              , text "ldi:" <+> ppr ldi ]
-      formatReportWarnings ReportPatBind ctxt [var] result{cr_uncov = cr_uncov'}
+      formatReportWarnings ReportPatBind ctxt [var] result
       return ldi
   where
     -- See Note [pmcPatBind doesn't warn on pattern guards]
@@ -176,21 +176,22 @@ pmcMatches ctxt vars matches = {-# SCC "pmcMatches" #-} do
   -- We have to force @missing@ before printing out the trace message,
   -- otherwise we get interleaved output from the solver. This function
   -- should be strict in @missing@ anyway!
-  !missing <- getLdiNablas
+  !missing0 <- getLdiNablas
+
+  -- See Note (TODO) [Represent the MatchIds before the CheckAction]
+  let missing = representIdsNablas vars missing0
+
   tracePm "pmcMatches {" $
           hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
                2
                (vcat (map ppr matches) $$ ppr missing)
 
-  -- See Note (TODO) [Represent the MatchIds before the CheckAction]
-  let missing' = representIdsNablas vars missing
-
   case NE.nonEmpty matches of
     Nothing -> do
       -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
       let var = only vars
       empty_case <- noCheckDs $ desugarEmptyCase var
-      result <- unCA (checkEmptyCase empty_case) missing'
+      result <- unCA (checkEmptyCase empty_case) missing
       tracePm "}: " (ppr (cr_uncov result))
       formatReportWarnings ReportEmptyCase ctxt vars result
       return []
@@ -198,7 +199,7 @@ pmcMatches ctxt vars matches = {-# SCC "pmcMatches" #-} do
       matches <- {-# SCC "desugarMatches" #-}
                  noCheckDs $ desugarMatches vars matches
       result  <- {-# SCC "checkMatchGroup" #-}
-                 unCA (checkMatchGroup matches) missing'
+                 unCA (checkMatchGroup matches) missing
       tracePm "}: " (ppr (cr_uncov result))
       {-# SCC "formatReportWarnings" #-} formatReportWarnings ReportMatchGroup ctxt vars result
       return (NE.toList (ldiMatchGroup (cr_ret result)))
@@ -262,7 +263,10 @@ pmcRecSel :: Id       -- ^ Id of the selector
           -> DsM ()
 pmcRecSel sel_id arg
   | RecSelId{ sel_cons = (cons_w_field, _ : _) } <- idDetails sel_id = do
-      !missing <- getLdiNablas
+      !missing0 <- getLdiNablas
+
+      -- See Note (TODO) [Represent the MatchIds before the CheckAction]
+      let missing = representIdNablas sel_id missing0
 
       tracePm "pmcRecSel {" (ppr sel_id)
       CheckResult{ cr_ret = PmRecSel{ pr_arg_var = arg_id }, cr_uncov = uncov_nablas }
@@ -278,7 +282,8 @@ pmcRecSel sel_id arg
             let maxConstructors = maxUncoveredPatterns dflags
             unc_examples <- getNFirstUncovered MinimalCover [arg_id] (maxConstructors + 1) uncov_nablas
             let cons = [con | unc_example <- unc_examples
-                      , Just (PACA (PmAltConLike con) _ _) <- [lookupSolution unc_example arg_id]]
+                                                                                          -- we've represented this Id above, see Note...
+                      , Just (PACA (PmAltConLike con) _ _) <- [lookupSolution unc_example (fromJust (arg_id `lookupMatchIdMap` unc_example))]]
                 not_full_examples = length cons == (maxConstructors + 1)
                 cons' = take maxConstructors cons
             diagnosticDs $ DsIncompleteRecordSelector sel_name cons' not_full_examples
@@ -288,7 +293,6 @@ pmcRecSel _ _ = return ()
 {- Note [pmcPatBind doesn't warn on pattern guards]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 @pmcPatBind@'s main purpose is to check vanilla pattern bindings, like
->>>>>>> 8760510af3 (This MR is an implementation of the proposal #516.)
 @x :: Int; Just x = e@, which is in a @PatBindRhs@ context.
 But its caller is also called for individual pattern guards in a @StmtCtxt at .
 For example, both pattern guards in @f x y | True <- x, False <- y = ...@ will
@@ -550,11 +554,9 @@ addTyCs origin ev_vars m = do
 -- to be added for multiple scrutinees rather than just one.
 addCoreScrutTmCs :: [CoreExpr] -> [Id] -> DsM a -> DsM a
 addCoreScrutTmCs []         _      k = k
-addCoreScrutTmCs (scr:scrs) (x0:xs) k =
-  flip locallyExtendPmNablas (addCoreScrutTmCs scrs xs k) $ \nablas0 ->
-     liftNablasM (\d ->
-       let (x, d') = representId x0 d
-        in addPhiCts d' (unitBag (PhiCoreCt x scr))) nablas0
+addCoreScrutTmCs (scr:scrs) (x:xs) k =
+  flip locallyExtendPmNablas (addCoreScrutTmCs scrs xs k) $ \nablas ->
+    addPhiCtNablasWithRep nablas x (`PhiCoreCt` scr)
 addCoreScrutTmCs _   _   _ = panic "addCoreScrutTmCs: numbers of scrutinees and match ids differ"
 
 -- | 'addCoreScrutTmCs', but desugars the 'LHsExpr's first.


=====================================
compiler/GHC/HsToCore/Pmc/Check.hs
=====================================
@@ -198,10 +198,12 @@ checkRecSel pr@(PmRecSel { pr_arg = arg, pr_cons = cons }) = CA $ \inc -> do
            Var arg_id -> return arg_id
            _ -> mkPmId $ exprType arg
 
-  let con_cts = map (PhiNotConCt arg_id . PmAltConLike) cons
-      arg_ct  = PhiCoreCt arg_id arg
-      phi_cts = listToBag (arg_ct : con_cts)
-  unc <- addPhiCtsNablas inc phi_cts
+  unc <- liftNablasM (\d ->
+    let (arg_id', d') = representId arg_id d
+        con_cts = map (PhiNotConCt arg_id' . PmAltConLike) cons
+        arg_ct  = PhiCoreCt arg_id' arg
+        phi_cts = listToBag (arg_ct : con_cts)
+     in addPhiCts d' phi_cts) inc
   pure CheckResult { cr_ret = pr{ pr_arg_var = arg_id }, cr_uncov = unc, cr_approx = mempty }
 
 



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ba19d6dd042d7fbe4f84c5cbd4bb5d5c19d129d3
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/20230801/3f81d993/attachment-0001.html>


More information about the ghc-commits mailing list