.ghcid

@@ -2,4 +2,4 @@
 --reload compiler
 --reload ghc
 --reload includes
---restart hadrian/
+--restart hadrian/ghci

.gitignore

@@ -111,6 +111,7 @@ _darcs/
 /compiler/ClosureTypes.h
 /compiler/FunTypes.h
 /compiler/MachRegs.h
+/compiler/MachRegs
 /compiler/ghc-llvm-version.h
 /compiler/ghc.cabal
 /compiler/ghc.cabal.old

.gitlab/ci.sh

@@ -7,7 +7,7 @@
 set -Eeuo pipefail
 
 # Configuration:
-HACKAGE_INDEX_STATE="2020-12-21T14:48:20Z"
+HACKAGE_INDEX_STATE="2023-10-05T11:38:51Z"
 MIN_HAPPY_VERSION="1.20"
 MIN_ALEX_VERSION="3.2.6"
 
@@ -230,7 +230,7 @@ function set_toolchain_paths() {
 function cabal_update() {
   # In principle -w shouldn't be necessary here but with
   # cabal-install 3.8.1.0 it is, due to cabal#8447.
-  run "$CABAL" update -w "$GHC" --index="$HACKAGE_INDEX_STATE"
+  run "$CABAL" update -w "$GHC" "hackage.haskell.org,${HACKAGE_INDEX_STATE}"
 }
 
 
@@ -480,6 +480,9 @@ function build_hadrian() {
 
   check_release_build
 
+  # Just to be sure, use the same hackage index state when building Hadrian.
+  echo "index-state: $HACKAGE_INDEX_STATE" > hadrian/cabal.project.local
+
   # We can safely enable parallel compression for x64. By the time
   # hadrian calls tar/xz to produce bindist, there's no other build
   # work taking place.

.gitlab/test-metrics.sh

@@ -17,7 +17,12 @@ fail() {
 
 function pull() {
   local ref="refs/notes/$REF"
-  run git fetch -f "$NOTES_ORIGIN" "$ref:$ref"
+  # 2023-10-04: `git fetch` started failing, first on Darwin in CI and then on
+  # Linux locally, both using git version 2.40.1. See #24055. One workaround is
+  # to set a larger http.postBuffer, although this is definitely a workaround.
+  # The default should work just fine. The error could be in git, GitLab, or
+  # perhaps the networking tube (including all proxies etc) between the two.
+  run git -c http.postBuffer=2097152 fetch -f "$NOTES_ORIGIN" "$ref:$ref"
   echo "perf notes ref $ref is $(git rev-parse $ref)"
 }
 

compiler/CodeGen.Platform.h

@@ -480,6 +480,7 @@ import GHC.Platform.Reg
 
 #endif
 
+-- See also Note [Caller saves and callee-saves regs.]
 callerSaves :: GlobalReg -> Bool
 #if defined(CALLER_SAVES_Base)
 callerSaves BaseReg           = True

compiler/GHC/Builtin/Types.hs

@@ -636,6 +636,8 @@ pcDataConWithFixity' declared_infix dc_name wrk_key rri
     -- See Note [Constructor tag allocation] and #14657
     data_con = mkDataCon dc_name declared_infix prom_info
                 (map (const no_bang) arg_tys)
+                (map (const HsLazy) arg_tys)
+                (map (const NotMarkedStrict) arg_tys)
                 []      -- No labelled fields
                 tyvars ex_tyvars
                 conc_tyvars

compiler/GHC/CmmToAsm.hs

@@ -15,7 +15,8 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE UnboxedTuples #-}
 
--- | Native code generator
+-- | Note [Native code generator]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 --
 -- The native-code generator has machine-independent and
 -- machine-dependent modules.
@@ -23,45 +24,39 @@
 -- This module ("GHC.CmmToAsm") is the top-level machine-independent
 -- module.  Before entering machine-dependent land, we do some
 -- machine-independent optimisations (defined below) on the
--- 'CmmStmts's.
+-- 'CmmStmts's. (Which ideally would be folded into CmmOpt ...)
 --
 -- We convert to the machine-specific 'Instr' datatype with
 -- 'cmmCodeGen', assuming an infinite supply of registers.  We then use
+-- a (mostly) machine-independent register allocator to rejoin
 -- reality.  Obviously, 'regAlloc' has machine-specific helper
--- reality.  Obviously, 'regAlloc' has machine-specific helper
+-- functions (see the used register allocator for details).
 --
 -- Finally, we order the basic blocks of the function so as to minimise
 -- the number of jumps between blocks, by utilising fallthrough wherever
 -- possible.
 --
---
+-- The machine-dependent bits are generally contained under
+--  GHC/CmmToAsm/<Arch>/* and generally breaks down as follows:
 --
- 
+--   * "Regs": Everything about the target platform's machine
 --     registers (and immediate operands, and addresses, which tend to
 --     intermingle/interact with registers).
 --
---
---   * ["MachInstrs"]  Includes the 'Instr' datatype (possibly should
+--   * "Instr":  Includes the 'Instr' datatype plus a miscellany of other things
 --     (e.g., 'targetDoubleSize', 'smStablePtrTable', ...)
 --
- 
+--   * "CodeGen":  is where 'Cmm' stuff turns into
 --     machine instructions.
 --
- 
+--   * "Ppr": 'pprInstr' turns an 'Instr' into text (well, really
 --     a 'SDoc').
 --
---
---   * ["RegAllocInfo"] In the register allocator, we manipulate
---     'MRegsState's, which are 'BitSet's, one bit per machine register.
---     When we want to say something about a specific machine register
---     (e.g., ``it gets clobbered by this instruction''), we set/unset
---     its bit.  Obviously, we do this 'BitSet' thing for efficiency
+-- The register allocators lives under GHC.CmmToAsm.Reg.*, there is both a Linear and a Graph
+-- based register allocator. Both of which have their own notes describing them. They
+-- are mostly platform independent but there are some platform specific files
+-- encoding architecture details under Reg/<Allocator>/<Arch.hs>
 --
---
---     The 'RegAllocInfo' module collects together the machine-specific
---     info needed to do register allocation.
---
 -- -}
 --
 module GHC.CmmToAsm
@@ -655,13 +650,14 @@ cmmNativeGen logger ncgImpl us fileIds dbgMap cmm count
                                 text "cfg not in lockstep") ()
 
         ---- sequence blocks
-        let sequenced :: [NatCmmDecl statics instr]
-            sequenced =
-                checkLayout shorted $
-                {-# SCC "sequenceBlocks" #-}
-                map (BlockLayout.sequenceTop
-                        ncgImpl optimizedCFG)
-                    shorted
+        -- sequenced :: [NatCmmDecl statics instr]
+        let (sequenced, us_seq) =
+                        {-# SCC "sequenceBlocks" #-}
+                        initUs usAlloc $ mapM (BlockLayout.sequenceTop
+                                ncgImpl optimizedCFG)
+                            shorted
+
+        massert (checkLayout shorted sequenced)
 
         let branchOpt :: [NatCmmDecl statics instr]
             branchOpt =
@@ -684,7 +680,7 @@ cmmNativeGen logger ncgImpl us fileIds dbgMap cmm count
                 addUnwind acc proc =
                     acc `mapUnion` computeUnwinding config ncgImpl proc
 
-        return  ( usAlloc
+        return  ( us_seq
                 , fileIds'
                 , branchOpt
                 , lastMinuteImports ++ imports
@@ -704,10 +700,10 @@ maybeDumpCfg logger (Just cfg) msg proc_name
 
 -- | Make sure all blocks we want the layout algorithm to place have been placed.
 checkLayout :: [NatCmmDecl statics instr] -> [NatCmmDecl statics instr]
-            -> [NatCmmDecl statics instr]
+            -> Bool
 checkLayout procsUnsequenced procsSequenced =
         assertPpr (setNull diff) (text "Block sequencing dropped blocks:" <> ppr diff)
-        procsSequenced
+        True
   where
         blocks1 = foldl' (setUnion) setEmpty $
                         map getBlockIds procsUnsequenced :: LabelSet

compiler/GHC/CmmToAsm/AArch64.hs

@@ -34,9 +34,9 @@ ncgAArch64 config
        ,maxSpillSlots             = AArch64.maxSpillSlots config
        ,allocatableRegs           = AArch64.allocatableRegs platform
        ,ncgAllocMoreStack         = AArch64.allocMoreStack platform
-       ,ncgMakeFarBranches        = const id
+       ,ncgMakeFarBranches        = AArch64.makeFarBranches
        ,extractUnwindPoints       = const []
-       ,invertCondBranches        = \_ _ -> id
+       ,invertCondBranches        = \_ _ blocks -> blocks
   }
     where
       platform = ncgPlatform config

compiler/GHC/CmmToAsm/AArch64/CodeGen.hs

@@ -7,6 +7,7 @@
 module GHC.CmmToAsm.AArch64.CodeGen (
       cmmTopCodeGen
     , generateJumpTableForInstr
+    , makeFarBranches
 )
 
 where
@@ -43,9 +44,11 @@ import GHC.Cmm.Utils
 import GHC.Cmm.Switch
 import GHC.Cmm.CLabel
 import GHC.Cmm.Dataflow.Block
+import GHC.Cmm.Dataflow.Label
 import GHC.Cmm.Dataflow.Graph
 import GHC.Types.Tickish ( GenTickish(..) )
 import GHC.Types.SrcLoc  ( srcSpanFile, srcSpanStartLine, srcSpanStartCol )
+import GHC.Types.Unique.Supply
 
 -- The rest:
 import GHC.Data.OrdList
@@ -61,6 +64,9 @@ import GHC.Data.FastString
 import GHC.Utils.Misc
 import GHC.Utils.Panic
 import GHC.Utils.Constants (debugIsOn)
+import GHC.Utils.Monad (mapAccumLM)
+
+import GHC.Cmm.Dataflow.Collections
 
 -- Note [General layout of an NCG]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -161,15 +167,17 @@ basicBlockCodeGen block = do
   let
         (top,other_blocks,statics) = foldrOL mkBlocks ([],[],[]) instrs
 
-        mkBlocks (NEWBLOCK id) (instrs,blocks,statics)
-          = ([], BasicBlock id instrs : blocks, statics)
-        mkBlocks (LDATA sec dat) (instrs,blocks,statics)
-          = (instrs, blocks, CmmData sec dat:statics)
-        mkBlocks instr (instrs,blocks,statics)
-          = (instr:instrs, blocks, statics)
   return (BasicBlock id top : other_blocks, statics)
 
-
+mkBlocks :: Instr
+          -> ([Instr], [GenBasicBlock Instr], [GenCmmDecl RawCmmStatics h g])
+          -> ([Instr], [GenBasicBlock Instr], [GenCmmDecl RawCmmStatics h g])
+mkBlocks (NEWBLOCK id) (instrs,blocks,statics)
+  = ([], BasicBlock id instrs : blocks, statics)
+mkBlocks (LDATA sec dat) (instrs,blocks,statics)
+  = (instrs, blocks, CmmData sec dat:statics)
+mkBlocks instr (instrs,blocks,statics)
+  = (instr:instrs, blocks, statics)
 -- -----------------------------------------------------------------------------
 -- | Utilities
 ann :: SDoc -> Instr -> Instr
@@ -773,12 +781,12 @@ getRegister' config plat expr
       return $ Any (intFormat w) (\dst -> code_x `snocOL` annExpr expr (LSR (OpReg w dst) (OpReg w reg_x) (OpImm (ImmInteger n))))
 
     -- 3. Logic &&, ||
-    CmmMachOp (MO_And w) [(CmmReg reg), CmmLit (CmmInt n _)] | isAArch64Bitmask (fromIntegral n) ->
+    CmmMachOp (MO_And w) [(CmmReg reg), CmmLit (CmmInt n _)] | isAArch64Bitmask (opRegWidth w') (fromIntegral n) ->
       return $ Any (intFormat w) (\d -> unitOL $ annExpr expr (AND (OpReg w d) (OpReg w' r') (OpImm (ImmInteger n))))
       where w' = formatToWidth (cmmTypeFormat (cmmRegType reg))
             r' = getRegisterReg plat reg
 
-    CmmMachOp (MO_Or w) [(CmmReg reg), CmmLit (CmmInt n _)] | isAArch64Bitmask (fromIntegral n) ->
+    CmmMachOp (MO_Or w) [(CmmReg reg), CmmLit (CmmInt n _)] | isAArch64Bitmask (opRegWidth w') (fromIntegral n) ->
       return $ Any (intFormat w) (\d -> unitOL $ annExpr expr (ORR (OpReg w d) (OpReg w' r') (OpImm (ImmInteger n))))
       where w' = formatToWidth (cmmTypeFormat (cmmRegType reg))
             r' = getRegisterReg plat reg
@@ -1062,13 +1070,16 @@ getRegister' config plat expr
 -- | Is a given number encodable as a bitmask immediate?
 --
 -- https://stackoverflow.com/questions/30904718/range-of-immediate-values-in-armv8-a64-assembly
-isAArch64Bitmask :: Integer -> Bool
+isAArch64Bitmask :: Width -> Integer -> Bool
 -- N.B. zero and ~0 are not encodable as bitmask immediates
-isAArch64Bitmask 0  = False
-isAArch64Bitmask n
-  | n == bit 64 - 1 = False
-isAArch64Bitmask n  =
-    check 64 || check 32 || check 16 || check 8
+isAArch64Bitmask width n =
+  assert (width `elem` [W32,W64]) $
+  case n of
+    0 -> False
+    _ | n == bit (widthInBits width) - 1
+      -> False -- 1111...1111
+      | otherwise
+      -> (width == W64 && check 64) || check 32 || check 16 || check 8
   where
     -- Check whether @n@ can be represented as a subpattern of the given
     -- width.
@@ -1217,6 +1228,7 @@ assignReg_FltCode = assignReg_IntCode
 
 -- -----------------------------------------------------------------------------
 -- Jumps
+
 genJump :: CmmExpr{-the branch target-} -> NatM InstrBlock
 genJump expr@(CmmLit (CmmLabel lbl))
   = return $ unitOL (annExpr expr (J (TLabel lbl)))
@@ -1302,6 +1314,22 @@ genCondJump bid expr = do
           _ -> pprPanic "AArch64.genCondJump:case mop: " (text $ show expr)
       _ -> pprPanic "AArch64.genCondJump: " (text $ show expr)
 
+-- A conditional jump with at least +/-128M jump range
+genCondFarJump :: MonadUnique m => Cond -> Target -> m InstrBlock
+genCondFarJump cond far_target = do
+  skip_lbl_id <- newBlockId
+  jmp_lbl_id <- newBlockId
+
+  -- TODO: We can improve this by inverting the condition
+  -- but it's not quite trivial since we don't know if we
+  -- need to consider float orderings.
+  -- So we take the hit of the additional jump in the false
+  -- case for now.
+  return $ toOL [ BCOND cond (TBlock jmp_lbl_id)
+                , B (TBlock skip_lbl_id)
+                , NEWBLOCK jmp_lbl_id
+                , B far_target
+                , NEWBLOCK skip_lbl_id]
 
 genCondBranch
     :: BlockId      -- the source of the jump
@@ -1816,3 +1844,163 @@ genCCall target dest_regs arg_regs bid = do
       let dst = getRegisterReg platform (CmmLocal dest_reg)
       let code = code_fx `appOL` op (OpReg w dst) (OpReg w reg_fx)
       return (code, Nothing)
+
+{- Note [AArch64 far jumps]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+AArch conditional jump instructions can only encode an offset of +/-1MB
+which is usually enough but can be exceeded in edge cases. In these cases
+we will replace:
+
+  b.cond <cond> foo
+
+with the sequence:
+
+  b.cond <cond> <lbl_true>
+  b <lbl_false>
+  <lbl_true>:
+  b foo
+  <lbl_false>:
+
+Note the encoding of the `b` instruction still limits jumps to
++/-128M offsets, but that seems like an acceptable limitation.
+
+Since AArch64 instructions are all of equal length we can reasonably estimate jumps
+in range by counting the instructions between a jump and its target label.
+
+We make some simplifications in the name of performance which can result in overestimating
+jump <-> label offsets:
+
+* To avoid having to recalculate the label offsets once we replaced a jump we simply
+  assume all jumps will be expanded to a three instruction far jump sequence.
+* For labels associated with a info table we assume the info table is 64byte large.
+  Most info tables are smaller than that but it means we don't have to distinguish
+  between multiple types of info tables.
+
+In terms of implementation we walk the instruction stream at least once calculating
+label offsets, and if we determine during this that the functions body is big enough
+to potentially contain out of range jumps we walk the instructions a second time, replacing
+out of range jumps with the sequence of instructions described above.
+
+-}
+
+-- See Note [AArch64 far jumps]
+data BlockInRange = InRange | NotInRange Target
+
+-- See Note [AArch64 far jumps]
+makeFarBranches :: Platform -> LabelMap RawCmmStatics -> [NatBasicBlock Instr]
+                -> UniqSM [NatBasicBlock Instr]
+makeFarBranches {- only used when debugging -} _platform statics basic_blocks = do
+  -- All offsets/positions are counted in multiples of 4 bytes (the size of AArch64 instructions)
+  -- That is an offset of 1 represents a 4-byte/one instruction offset.
+  let (func_size, lblMap) = foldl' calc_lbl_positions (0, mapEmpty) basic_blocks
+  if func_size < max_jump_dist
+    then pure basic_blocks
+    else do
+      (_,blocks) <- mapAccumLM (replace_blk lblMap) 0 basic_blocks
+      pure $ concat blocks
+      -- pprTrace "lblMap" (ppr lblMap) $ basic_blocks
+
+  where
+    -- 2^18, 19 bit immediate with one bit is reserved for the sign
+    max_jump_dist = 2^(18::Int) - 1 :: Int
+    -- Currently all inline info tables fit into 64 bytes.
+    max_info_size     = 16 :: Int
+    long_bc_jump_size =  3 :: Int
+    long_bz_jump_size =  4 :: Int
+
+    -- Replace out of range conditional jumps with unconditional jumps.
+    replace_blk :: LabelMap Int -> Int -> GenBasicBlock Instr -> UniqSM (Int, [GenBasicBlock Instr])
+    replace_blk !m !pos (BasicBlock lbl instrs) = do
+      -- Account for a potential info table before the label.
+      let !block_pos = pos + infoTblSize_maybe lbl
+      (!pos', instrs') <- mapAccumLM (replace_jump m) block_pos instrs
+      let instrs'' = concat instrs'
+      -- We might have introduced new labels, so split the instructions into basic blocks again if neccesary.
+      let (top, split_blocks, no_data) = foldr mkBlocks ([],[],[]) instrs''
+      -- There should be no data in the instruction stream at this point
+      massert (null no_data)
+
+      let final_blocks = BasicBlock lbl top : split_blocks
+      pure (pos', final_blocks)
+
+    replace_jump :: LabelMap Int -> Int -> Instr -> UniqSM (Int, [Instr])
+    replace_jump !m !pos instr = do
+      case instr of
+        ANN ann instr -> do
+          (idx,instr':instrs') <- replace_jump m pos instr
+          pure (idx, ANN ann instr':instrs')
+        BCOND cond t
+          -> case target_in_range m t pos of
+              InRange -> pure (pos+long_bc_jump_size,[instr])
+              NotInRange far_target -> do
+                jmp_code <- genCondFarJump cond far_target
+                pure (pos+long_bc_jump_size, fromOL jmp_code)
+        CBZ op t -> long_zero_jump op t EQ
+        CBNZ op t -> long_zero_jump op t NE
+        instr
+          | isMetaInstr instr -> pure (pos,[instr])
+          | otherwise -> pure (pos+1, [instr])
+
+      where
+        -- cmp_op: EQ = CBZ, NEQ = CBNZ
+        long_zero_jump op t cmp_op =
+          case target_in_range m t pos of
+              InRange -> pure (pos+long_bz_jump_size,[instr])
+              NotInRange far_target -> do
+                jmp_code <- genCondFarJump cmp_op far_target
+                -- TODO: Fix zero reg so we can use it here
+                pure (pos + long_bz_jump_size, CMP op (OpImm (ImmInt 0)) : fromOL jmp_code)
+
+
+    target_in_range :: LabelMap Int -> Target -> Int -> BlockInRange
+    target_in_range m target src =
+      case target of
+        (TReg{}) -> InRange
+        (TBlock bid) -> block_in_range m src bid
+        (TLabel clbl)
+          | Just bid <- maybeLocalBlockLabel clbl
+          -> block_in_range m src bid
+          | otherwise
+          -- Maybe we should be pessimistic here, for now just fixing intra proc jumps
+          -> InRange
+
+    block_in_range :: LabelMap Int -> Int -> BlockId -> BlockInRange
+    block_in_range m src_pos dest_lbl =
+      case mapLookup dest_lbl m of
+        Nothing       ->
+          pprTrace "not in range" (ppr dest_lbl) $
+            NotInRange (TBlock dest_lbl)
+        Just dest_pos -> if abs (dest_pos - src_pos) < max_jump_dist
+          then InRange
+          else NotInRange (TBlock dest_lbl)
+
+    calc_lbl_positions :: (Int, LabelMap Int) -> GenBasicBlock Instr -> (Int, LabelMap Int)
+    calc_lbl_positions (pos, m) (BasicBlock lbl instrs)
+      = let !pos' = pos + infoTblSize_maybe lbl
+        in foldl' instr_pos (pos',mapInsert lbl pos' m) instrs
+
+    instr_pos :: (Int, LabelMap Int) -> Instr -> (Int, LabelMap Int)
+    instr_pos (pos, m) instr =
+      case instr of
+        ANN _ann instr -> instr_pos (pos, m) instr
+        NEWBLOCK _bid -> panic "mkFarBranched - unexpected NEWBLOCK" -- At this point there should be no NEWBLOCK
+                                                                     -- in the instruction stream
+                                                                     -- (pos, mapInsert bid pos m)
+        COMMENT{} -> (pos, m)
+        instr
+          | Just jump_size <- is_expandable_jump instr -> (pos+jump_size, m)
+          | otherwise -> (pos+1, m)
+
+    infoTblSize_maybe bid =
+      case mapLookup bid statics of
+        Nothing           -> 0 :: Int
+        Just _info_static -> max_info_size
+
+    -- These jumps have a 19bit immediate as offset which is quite
+    -- limiting so we potentially have to expand them into
+    -- multiple instructions.
+    is_expandable_jump i = case i of
+      CBZ{}   -> Just long_bz_jump_size
+      CBNZ{}  -> Just long_bz_jump_size
+      BCOND{} -> Just long_bc_jump_size
+      _ -> Nothing

compiler/GHC/CmmToAsm/AArch64/Cond.hs

 module GHC.CmmToAsm.AArch64.Cond  where
 
-import GHC.Prelude
+import GHC.Prelude hiding (EQ)
 
 -- https://developer.arm.com/documentation/den0024/a/the-a64-instruction-set/data-processing-instructions/conditional-instructions
 
@@ -60,7 +60,13 @@ data Cond
     | UOGE   -- b.pl
     | UOGT   -- b.hi
     -- others
-    | NEVER  -- b.nv
+    -- NEVER -- b.nv
+             -- I removed never. According to the ARM spec:
+             -- >   The Condition code NV exists only to provide a valid disassembly of
+             -- >   the 0b1111 encoding, otherwise its behavior is identical to AL.
+             -- This can only lead to disaster. Better to not have it than someone
+             -- using it assuming it actually means never.
+
     | VS     -- oVerflow set
     | VC     -- oVerflow clear
     deriving Eq

compiler/GHC/CmmToAsm/AArch64/Instr.hs

@@ -743,6 +743,7 @@ data Target
     = TBlock BlockId
     | TLabel CLabel
     | TReg   Reg
+    deriving (Eq, Ord)
 
 
 -- Extension

compiler/GHC/CmmToAsm/AArch64/Ppr.hs

 {-# OPTIONS_GHC -fno-warn-orphans #-}
 {-# LANGUAGE CPP #-}
 
-module GHC.CmmToAsm.AArch64.Ppr (pprNatCmmDecl, pprInstr) where
+module GHC.CmmToAsm.AArch64.Ppr (pprNatCmmDecl, pprInstr, pprBasicBlock) where
 
 import GHC.Prelude hiding (EQ)
 
@@ -30,10 +30,14 @@ import GHC.Utils.Panic
 
 pprNatCmmDecl :: IsDoc doc => NCGConfig -> NatCmmDecl RawCmmStatics Instr -> doc
 pprNatCmmDecl config (CmmData section dats) =
-  pprSectionAlign config section $$ pprDatas config dats
+  let platform = ncgPlatform config
+  in
+  pprSectionAlign config section $$ pprDatas platform dats
 
 pprNatCmmDecl config proc@(CmmProc top_info lbl _ (ListGraph blocks)) =
-  let platform = ncgPlatform config in
+  let platform = ncgPlatform config
+      with_dwarf = ncgDwarfEnabled config
+  in
   case topInfoTable proc of
     Nothing ->
         -- special case for code without info table:
@@ -41,7 +45,7 @@ pprNatCmmDecl config proc@(CmmProc top_info lbl _ (ListGraph blocks)) =
         -- do not
         -- pprProcAlignment config $$
         pprLabel platform lbl $$ -- blocks guaranteed not null, so label needed
-        vcat (map (pprBasicBlock config top_info) blocks) $$
+        vcat (map (pprBasicBlock platform with_dwarf top_info) blocks) $$
         (if ncgDwarfEnabled config
          then line (pprAsmLabel platform (mkAsmTempEndLabel lbl) <> char ':') else empty) $$
         pprSizeDecl platform lbl
@@ -52,7 +56,7 @@ pprNatCmmDecl config proc@(CmmProc top_info lbl _ (ListGraph blocks)) =
       (if platformHasSubsectionsViaSymbols platform
           then line (pprAsmLabel platform (mkDeadStripPreventer info_lbl) <> char ':')
           else empty) $$
-      vcat (map (pprBasicBlock config top_info) blocks) $$
+      vcat (map (pprBasicBlock platform with_dwarf top_info) blocks) $$
       -- above: Even the first block gets a label, because with branch-chain
       -- elimination, it might be the target of a goto.
       (if platformHasSubsectionsViaSymbols platform
@@ -100,13 +104,13 @@ pprSizeDecl platform lbl
    then line (text "\t.size" <+> pprAsmLabel platform lbl <> text ", .-" <> pprAsmLabel platform lbl)
    else empty
 
-pprBasicBlock :: IsDoc doc => NCGConfig -> LabelMap RawCmmStatics -> NatBasicBlock Instr
+pprBasicBlock :: IsDoc doc => Platform -> {- dwarf enabled -} Bool -> LabelMap RawCmmStatics -> NatBasicBlock Instr
               -> doc
-pprBasicBlock config info_env (BasicBlock blockid instrs)
+pprBasicBlock platform with_dwarf info_env (BasicBlock blockid instrs)
   = maybe_infotable $
     pprLabel platform asmLbl $$
     vcat (map (pprInstr platform) (id {-detectTrivialDeadlock-} optInstrs)) $$
-    (if  ncgDwarfEnabled config
+    (if  with_dwarf
       then line (pprAsmLabel platform (mkAsmTempEndLabel asmLbl) <> char ':')
       else empty
     )
@@ -117,16 +121,15 @@ pprBasicBlock config info_env (BasicBlock blockid instrs)
             f _ = True
 
     asmLbl = blockLbl blockid
-    platform = ncgPlatform config
     maybe_infotable c = case mapLookup blockid info_env of
        Nothing   -> c
        Just (CmmStaticsRaw info_lbl info) ->
           --  pprAlignForSection platform Text $$
            infoTableLoc $$
-           vcat (map (pprData config) info) $$
+           vcat (map (pprData platform) info) $$
            pprLabel platform info_lbl $$
            c $$
-           (if ncgDwarfEnabled config
+           (if with_dwarf
              then line (pprAsmLabel platform (mkAsmTempEndLabel info_lbl) <> char ':')
              else empty)
     -- Make sure the info table has the right .loc for the block
@@ -135,34 +138,31 @@ pprBasicBlock config info_env (BasicBlock blockid instrs)
       (l@LOCATION{} : _) -> pprInstr platform l
       _other             -> empty
 
-pprDatas :: IsDoc doc => NCGConfig -> RawCmmStatics -> doc
+pprDatas :: IsDoc doc => Platform -> RawCmmStatics -> doc
 -- See Note [emit-time elimination of static indirections] in "GHC.Cmm.CLabel".
-pprDatas config (CmmStaticsRaw alias [CmmStaticLit (CmmLabel lbl), CmmStaticLit ind, _, _])
+pprDatas platform (CmmStaticsRaw alias [CmmStaticLit (CmmLabel lbl), CmmStaticLit ind, _, _])
   | lbl == mkIndStaticInfoLabel
   , let labelInd (CmmLabelOff l _) = Just l
         labelInd (CmmLabel l) = Just l
         labelInd _ = Nothing
   , Just ind' <- labelInd ind
   , alias `mayRedirectTo` ind'
-  = pprGloblDecl (ncgPlatform config) alias
-    $$ line (text ".equiv" <+> pprAsmLabel (ncgPlatform config) alias <> comma <> pprAsmLabel (ncgPlatform config) ind')
+  = pprGloblDecl platform alias
+    $$ line (text ".equiv" <+> pprAsmLabel platform alias <> comma <> pprAsmLabel platform ind')
 
-pprDatas config (CmmStaticsRaw lbl dats)
-  = vcat (pprLabel platform lbl : map (pprData config) dats)
-   where
-      platform = ncgPlatform config
+pprDatas platform (CmmStaticsRaw lbl dats)
+  = vcat (pprLabel platform lbl : map (pprData platform) dats)
 
-pprData :: IsDoc doc => NCGConfig -> CmmStatic -> doc
-pprData _config (CmmString str) = line (pprString str)
-pprData _config (CmmFileEmbed path _) = line (pprFileEmbed path)
+pprData :: IsDoc doc => Platform -> CmmStatic -> doc
+pprData _platform (CmmString str) = line (pprString str)
+pprData _platform (CmmFileEmbed path _) = line (pprFileEmbed path)
 
-pprData config (CmmUninitialised bytes)
- = line $ let platform = ncgPlatform config
-          in if platformOS platform == OSDarwin
+pprData platform (CmmUninitialised bytes)
+ = line $ if platformOS platform == OSDarwin
                 then text ".space " <> int bytes
                 else text ".skip "  <> int bytes
 
-pprData config (CmmStaticLit lit) = pprDataItem config lit
+pprData platform (CmmStaticLit lit) = pprDataItem platform lit
 
 pprGloblDecl :: IsDoc doc => Platform -> CLabel -> doc
 pprGloblDecl platform lbl
@@ -196,12 +196,10 @@ pprTypeDecl platform lbl
       then line (text ".type " <> pprAsmLabel platform lbl <> text ", " <> pprLabelType' platform lbl)
       else empty
 
-pprDataItem :: IsDoc doc => NCGConfig -> CmmLit -> doc
-pprDataItem config lit
+pprDataItem :: IsDoc doc => Platform -> CmmLit -> doc
+pprDataItem platform lit
   = lines_ (ppr_item (cmmTypeFormat $ cmmLitType platform lit) lit)
     where
-        platform = ncgPlatform config
-
         imm = litToImm lit
 
         ppr_item II8  _ = [text "\t.byte\t"  <> pprImm platform imm]
@@ -355,7 +353,10 @@ pprInstr platform instr = case instr of
     -> line (text "\t.loc" <+> int file <+> int line' <+> int col)
   DELTA d   -> dualDoc (asmComment $ text "\tdelta = " <> int d) empty
                -- see Note [dualLine and dualDoc] in GHC.Utils.Outputable
-  NEWBLOCK _ -> panic "PprInstr: NEWBLOCK"
+  NEWBLOCK blockid -> -- This is invalid assembly. But NEWBLOCK should never be contained
+                      -- in the final instruction stream. But we still want to be able to
+                      -- print it for debugging purposes.
+                      line (text "BLOCK " <> pprAsmLabel platform (blockLbl blockid))
   LDATA _ _  -> panic "pprInstr: LDATA"
 
   -- Pseudo Instructions -------------------------------------------------------
@@ -569,7 +570,7 @@ pprCond c = case c of
   UGE    -> text "hs" -- Carry set/unsigned higher or same ; Greater than or equal, or unordered
   UGT    -> text "hi" -- Unsigned higher                   ; Greater than, or unordered
 
-  NEVER  -> text "nv" -- Never
+  -- NEVER  -> text "nv" -- Never
   VS     -> text "vs" -- Overflow                          ; Unordered (at least one NaN operand)
   VC     -> text "vc" -- No overflow                       ; Not unordered
 

compiler/GHC/CmmToAsm/BlockLayout.hs

@@ -49,6 +49,7 @@ import Data.STRef
 import Control.Monad.ST.Strict
 import Control.Monad (foldM, unless)
 import GHC.Data.UnionFind
+import GHC.Types.Unique.Supply (UniqSM)
 
 {-
   Note [CFG based code layout]
@@ -794,29 +795,32 @@ sequenceTop
     => NcgImpl statics instr jumpDest
     -> Maybe CFG -- ^ CFG if we have one.
     -> NatCmmDecl statics instr -- ^ Function to serialize
-    -> NatCmmDecl statics instr
-
-sequenceTop _       _           top@(CmmData _ _) = top
-sequenceTop ncgImpl edgeWeights (CmmProc info lbl live (ListGraph blocks))
-  = let
-      config     = ncgConfig ncgImpl
-      platform   = ncgPlatform config
-
-    in CmmProc info lbl live $ ListGraph $ ncgMakeFarBranches ncgImpl info $
-         if -- Chain based algorithm
-            | ncgCfgBlockLayout config
-            , backendMaintainsCfg platform
-            , Just cfg <- edgeWeights
-            -> {-# SCC layoutBlocks #-} sequenceChain info cfg blocks
-
-            -- Old algorithm without edge weights
-            | ncgCfgWeightlessLayout config
-               || not (backendMaintainsCfg platform)
-            -> {-# SCC layoutBlocks #-} sequenceBlocks Nothing info blocks
-
-            -- Old algorithm with edge weights (if any)
-            | otherwise
-            -> {-# SCC layoutBlocks #-} sequenceBlocks edgeWeights info blocks
+    -> UniqSM (NatCmmDecl statics instr)
+
+sequenceTop _       _           top@(CmmData _ _) = pure top
+sequenceTop ncgImpl edgeWeights (CmmProc info lbl live (ListGraph blocks)) = do
+    let config     = ncgConfig ncgImpl
+        platform   = ncgPlatform config
+
+        seq_blocks =
+                  if -- Chain based algorithm
+                      | ncgCfgBlockLayout config
+                      , backendMaintainsCfg platform
+                      , Just cfg <- edgeWeights
+                      -> {-# SCC layoutBlocks #-} sequenceChain info cfg blocks
+
+                      -- Old algorithm without edge weights
+                      | ncgCfgWeightlessLayout config
+                        || not (backendMaintainsCfg platform)
+                      -> {-# SCC layoutBlocks #-} sequenceBlocks Nothing info blocks
+
+                      -- Old algorithm with edge weights (if any)
+                      | otherwise
+                      -> {-# SCC layoutBlocks #-} sequenceBlocks edgeWeights info blocks
+
+    far_blocks <- (ncgMakeFarBranches ncgImpl) platform info seq_blocks
+    pure $ CmmProc info lbl live $ ListGraph far_blocks
+
 
 -- The old algorithm:
 -- It is very simple (and stupid): We make a graph out of

compiler/GHC/CmmToAsm/Monad.hs

@@ -93,7 +93,8 @@ data NcgImpl statics instr jumpDest = NcgImpl {
                               -> UniqSM (NatCmmDecl statics instr, [(BlockId,BlockId)]),
     -- ^ The list of block ids records the redirected jumps to allow us to update
     -- the CFG.
-    ncgMakeFarBranches        :: LabelMap RawCmmStatics -> [NatBasicBlock instr] -> [NatBasicBlock instr],
+    ncgMakeFarBranches        :: Platform -> LabelMap RawCmmStatics -> [NatBasicBlock instr]
+                              -> UniqSM [NatBasicBlock instr],
     extractUnwindPoints       :: [instr] -> [UnwindPoint],
     -- ^ given the instruction sequence of a block, produce a list of
     -- the block's 'UnwindPoint's
@@ -140,7 +141,7 @@ mistake would readily show up in performance tests). -}
 data NatM_State
         = NatM_State {
                 natm_us          :: UniqSupply,
-                natm_delta       :: Int,
+                natm_delta       :: Int, -- ^ Stack offset for unwinding information
                 natm_imports     :: [(CLabel)],
                 natm_pic         :: Maybe Reg,
                 natm_config      :: NCGConfig,

compiler/GHC/CmmToAsm/PPC/Instr.hs

@@ -688,12 +688,13 @@ takeRegRegMoveInstr _  = Nothing
 -- big, we have to work around this limitation.
 
 makeFarBranches
-        :: LabelMap RawCmmStatics
+        :: Platform
+        -> LabelMap RawCmmStatics
         -> [NatBasicBlock Instr]
-        -> [NatBasicBlock Instr]
-makeFarBranches info_env blocks
-    | NE.last blockAddresses < nearLimit = blocks
-    | otherwise = zipWith handleBlock blockAddressList blocks
+        -> UniqSM [NatBasicBlock Instr]
+makeFarBranches _platform info_env blocks
+    | NE.last blockAddresses < nearLimit = return blocks
+    | otherwise = return $ zipWith handleBlock blockAddressList blocks
     where
         blockAddresses = NE.scanl (+) 0 $ map blockLen blocks
         blockAddressList = toList blockAddresses

compiler/GHC/CmmToAsm/X86.hs

@@ -38,7 +38,7 @@ ncgX86_64 config = NcgImpl
    , maxSpillSlots             = X86.maxSpillSlots config
    , allocatableRegs           = X86.allocatableRegs platform
    , ncgAllocMoreStack         = X86.allocMoreStack platform
-   , ncgMakeFarBranches        = const id
+   , ncgMakeFarBranches        = \_p _i bs -> pure bs
    , extractUnwindPoints       = X86.extractUnwindPoints
    , invertCondBranches        = X86.invertCondBranches
    }

compiler/GHC/Core.hs

@@ -42,7 +42,7 @@ module GHC.Core (
         foldBindersOfBindStrict, foldBindersOfBindsStrict,
         collectBinders, collectTyBinders, collectTyAndValBinders,
         collectNBinders, collectNValBinders_maybe,
-        collectArgs, stripNArgs, collectArgsTicks, flattenBinds,
+        collectArgs, collectValArgs, stripNArgs, collectArgsTicks, flattenBinds,
         collectFunSimple,
 
         exprToType,
@@ -1005,6 +1005,60 @@ tail position: A cast changes the type, but the type must be the same. But
 operationally, casts are vacuous, so this is a bit unfortunate! See #14610 for
 ideas how to fix this.
 
+Note [Strict fields in Core]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Evaluating a data constructor worker evaluates its strict fields.
+
+In other words, if `MkT` is strict in its first field and `xs` reduces to
+`error "boom"`, then `MkT xs b` will throw that error.
+Conversely, it is sound to seq the field before the call to the constructor,
+e.g., with `case xs of xs' { __DEFAULT -> MkT xs' b }`.
+Let's call this transformation "field seq insertion".
+
+Note in particular that the data constructor application `MkT xs b` above is
+*not* a value, unless `xs` is!
+
+This has pervasive effect on the Core pipeline:
+
+  * `exprIsHNF`/`exprIsConLike`/`exprOkForSpeculation` need to assert that the
+    strict arguments of a DataCon worker are values/ok-for-spec themselves.
+
+  * `exprIsConApp_maybe` inserts field seqs in the `FloatBind`s it returns, so
+    that the Simplifier, Constant-folding, the pattern-match checker, etc.
+    all see the insert field seqs when they match on strict workers. Often this
+    is just to emphasise strict semantics, but for case-of-known constructor
+    and case-to-let field insertion is *vital*, otherwise these transformations
+    would lose field seqs.
+
+  * The demand signature of a data constructor is strict in strict field
+    position, whereas is it's normally lazy. Likewise the demand *transformer*
+    of a DataCon worker can add stricten up demands on strict field args.
+    See Note [Demand transformer for data constructors].
+
+  * In the absence of `-fpedantic-bottoms`, it is still possible that some seqs
+    are ultimately dropped or delayed due to eta-expansion.
+    See Note [Dealing with bottom].
+
+Strict field semantics is exploited in STG by Note [Tag Inference]:
+It performs field seq insertion to statically guarantee *taggedness* of strict
+fields, establishing the Note [STG Strict Field Invariant]. (Happily, most
+of those seqs are immediately detected as redundant by tag inference and are
+omitted.) From then on, DataCon worker semantics are actually lazy, hence it is
+important that STG passes maintain the Strict Field Invariant.
+
+
+Historical Note:
+The delightfully simple description of strict field semantics is the result of
+a long saga (#20749, the bits about strict data constructors in #21497, #22475),
+where we tried a more lenient (but actually not) semantics first that would
+allow both strict and lazy implementations of DataCon workers. This was favoured
+because the "pervasive effect" throughout the compiler was deemed too large
+(when it really turned out to be very modest).
+Alas, this semantics would require us to implement `exprIsHNF` in *exactly* the
+same way as above, otherwise the analysis would not be conservative wrt. the
+lenient semantics (which includes the strict one). It is also much harder to
+explain and maintain, as it turned out.
+
 ************************************************************************
 *                                                                      *
             In/Out type synonyms
@@ -2091,6 +2145,17 @@ collectArgs expr
     go (App f a) as = go f (a:as)
     go e         as = (e, as)
 
+-- | Takes a nested application expression and returns the function
+-- being applied and the arguments to which it is applied
+collectValArgs :: Expr b -> (Expr b, [Arg b])
+collectValArgs expr
+  = go expr []
+  where
+    go (App f a) as
+      | isValArg a  = go f (a:as)
+      | otherwise   = go f as
+    go e         as = (e, as)
+
 -- | Takes a nested application expression and returns the function
 -- being applied. Looking through casts and ticks to find it.
 collectFunSimple :: Expr b -> Expr b

compiler/GHC/Core/Coercion.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -DDEBUG #-}
 
 {-
 (c) The University of Glasgow 2006
@@ -37,7 +38,7 @@ module GHC.Core.Coercion (
         mkAxInstLHS, mkUnbranchedAxInstLHS,
         mkPiCo, mkPiCos, mkCoCast,
         mkSymCo, mkTransCo,
-        mkSelCo, getNthFun, getNthFromType, mkLRCo,
+        mkSelCo, mkSelCoResRole, getNthFun, selectFromType, mkLRCo,
         mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
         mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
         mkNakedFunCo,
@@ -95,10 +96,10 @@ module GHC.Core.Coercion (
         -- ** Lifting
         liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
         emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope,
-        liftCoSubstVarBndrUsing, isMappedByLC,
+        liftCoSubstVarBndrUsing, isMappedByLC, extendLiftingContextCvSubst,
 
         mkSubstLiftingContext, zapLiftingContext,
-        substForAllCoBndrUsingLC, lcSubst, lcInScopeSet,
+        substForAllCoBndrUsingLC, lcLookupCoVar, lcInScopeSet,
 
         LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
         substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight,
@@ -555,6 +556,10 @@ splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, ForAllTyFlag, ForAllTyFlag, C
 splitForAllCo_maybe (ForAllCo { fco_tcv = tv, fco_visL = vL, fco_visR = vR
                               , fco_kind = k_co, fco_body = co })
   = Just (tv, vL, vR, k_co, co)
+splitForAllCo_maybe co
+  | Just (ty, r)        <- isReflCo_maybe co
+  , Just (Bndr tcv vis, body_ty) <- splitForAllForAllTyBinder_maybe ty
+  = Just (tcv, vis, vis, mkNomReflCo (varType tcv), mkReflCo r body_ty)
 splitForAllCo_maybe _ = Nothing
 
 -- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder
@@ -573,7 +578,6 @@ splitForAllCo_co_maybe co
   = Just stuff
 splitForAllCo_co_maybe _ = Nothing
 
-
 -------------------------------------------------------
 -- and some coercion kind stuff
 
@@ -1114,12 +1118,18 @@ mkUnivCo prov role ty1 ty2
 --   a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@.
 mkSymCo :: Coercion -> Coercion
 
--- Do a few simple optimizations, but don't bother pushing occurrences
--- of symmetry to the leaves; the optimizer will take care of that.
-mkSymCo co | isReflCo co          = co
-mkSymCo    (SymCo co)             = co
-mkSymCo    (SubCo (SymCo co))     = SubCo co
-mkSymCo co                        = SymCo co
+-- Do a few simple optimizations, mainly to expose the underlying
+-- constructors to other 'mk' functions.  E.g.
+--   mkInstCo (mkSymCo (ForAllCo ...)) ty
+-- We want to push the SymCo inside the ForallCo, so that we can instantiate
+-- This can make a big difference.  E.g without coercion optimisation, GHC.Read
+-- totally explodes; but when we push Sym inside ForAll, it's fine.
+mkSymCo co | isReflCo co   = co
+mkSymCo (SymCo co)         = co
+mkSymCo (SubCo (SymCo co)) = SubCo co
+mkSymCo co@(ForAllCo { fco_kind = kco, fco_body = body_co })
+  | isReflCo kco           = co { fco_body = mkSymCo body_co }
+mkSymCo co                 = SymCo co
 
 -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
 --   (co1 ; co2)
@@ -1130,30 +1140,32 @@ mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
   = GRefl r t1 (MCo $ mkTransCo co1 co2)
 mkTransCo co1 co2                = TransCo co1 co2
 
+--------------------
+{- Note [mkSelCo precondition]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+To satisfy the Purely Kinded Type Invariant (PKTI), we require that
+  in any call (mkSelCo cs co)
+  * selectFromType cs (coercionLKind co) works
+  * selectFromType cs (coercionRKind co) works
+  * and hence coercionKind (SelCo cs co) works (PKTI)
+-}
+
 mkSelCo :: HasDebugCallStack
         => CoSel
         -> Coercion
         -> Coercion
+-- See Note [mkSelCo precondition]
 mkSelCo n co = mkSelCo_maybe n co `orElse` SelCo n co
 
 mkSelCo_maybe :: HasDebugCallStack
         => CoSel
         -> Coercion
         -> Maybe Coercion
--- mkSelCo_maybe tries to optimise call to mkSelCo
+-- Note [mkSelCo precondition]
 mkSelCo_maybe cs co
   = assertPpr (good_call cs) bad_call_msg $
     go cs co
   where
-    Pair ty1 ty2 = coercionKind co
-
-    go cs co
-      | Just (ty, _co_role) <- isReflCo_maybe co
-      = let new_role = coercionRole (SelCo cs co)
-        in Just (mkReflCo new_role (getNthFromType cs ty))
-        -- The role of the result (new_role) does not have to
-        -- be equal to _co_role, the role of co, per Note [SelCo].
-        -- This was revealed by #23938.
 
     go SelForAll (ForAllCo { fco_kind = kind_co })
       = Just kind_co
@@ -1173,9 +1185,30 @@ mkSelCo_maybe cs co
     go cs (SymCo co)  -- Recurse, hoping to get to a TyConAppCo or FunCo
       = do { co' <- go cs co; return (mkSymCo co') }
 
-    go _ _ = Nothing
+    go cs co
+      | Just (ty, co_role) <- isReflCo_maybe co
+      = Just (mkReflCo (mkSelCoResRole cs co_role) (selectFromType cs ty))
+        -- mkSelCoreResRole: The role of the result may not be
+        -- be equal to co_role, the role of co, per Note [SelCo].
+        -- This was revealed by #23938.
 
-    -- Assertion checking
+      | Pair ty1 ty2 <- coercionKind co
+      , let sty1    = selectFromType cs ty1
+            sty2    = selectFromType cs ty2
+            co_role = coercionRole co
+      , sty1 `eqType` sty2
+      = Just (mkReflCo (mkSelCoResRole cs co_role) sty1)
+            -- Checking for fully reflexive-ness (by seeing if sty1=sty2)
+            -- is worthwhile, because a non-Refl coercion `co` may well have a
+            -- reflexive (SelCo cs co).
+            -- E.g. co :: Either a b ~ Either a c
+            --      Then (SubCo (SelTyCon 0) co) is reflexive
+
+      | otherwise = Nothing
+
+    ----------- Assertion checking --------------
+    -- NB: using coercionKind requires Note [mkSelCo precondition]
+    Pair ty1 ty2 = coercionKind co
     bad_call_msg = vcat [ text "Coercion =" <+> ppr co
                         , text "LHS ty =" <+> ppr ty1
                         , text "RHS ty =" <+> ppr ty2
@@ -1204,6 +1237,14 @@ mkSelCo_maybe cs co
 
     good_call _ = False
 
+mkSelCoResRole :: CoSel -> Role -> Role
+-- What is the role of (SelCo cs co), if co has role 'r'?
+-- It is not just 'r'!
+-- c.f. the SelCo case of coercionRole
+mkSelCoResRole SelForAll       _ = Nominal
+mkSelCoResRole (SelTyCon _ r') _ = r'
+mkSelCoResRole (SelFun fs)     r = funRole r fs
+
 -- | Extract the nth field of a FunCo
 getNthFun :: FunSel
           -> a    -- ^ multiplicity
@@ -1214,6 +1255,24 @@ getNthFun SelMult mult _   _   = mult
 getNthFun SelArg _     arg _   = arg
 getNthFun SelRes _     _   res = res
 
+selectFromType :: HasDebugCallStack => CoSel -> Type -> Type
+selectFromType (SelFun fs) ty
+  | Just (_af, mult, arg, res) <- splitFunTy_maybe ty
+  = getNthFun fs mult arg res
+
+selectFromType (SelTyCon n _) ty
+  | Just args <- tyConAppArgs_maybe ty
+  = assertPpr (args `lengthExceeds` n) (ppr n $$ ppr ty) $
+    args `getNth` n
+
+selectFromType SelForAll ty       -- Works for both tyvar and covar
+  | Just (tv,_) <- splitForAllTyCoVar_maybe ty
+  = tyVarKind tv
+
+selectFromType cs ty
+  = pprPanic "selectFromType" (ppr cs $$ ppr ty)
+
+--------------------
 mkLRCo :: LeftOrRight -> Coercion -> Coercion
 mkLRCo lr co
   | Just (ty, eq) <- isReflCo_maybe co
@@ -1222,11 +1281,14 @@ mkLRCo lr co
   = LRCo lr co
 
 -- | Instantiates a 'Coercion'.
+-- Works for both tyvar and covar
 mkInstCo :: Coercion -> CoercionN -> Coercion
-mkInstCo (ForAllCo { fco_tcv = tcv, fco_body = body_co }) co
-  | Just (arg, _) <- isReflCo_maybe co
-      -- works for both tyvar and covar
-  = substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
+mkInstCo co_fun co_arg
+  | Just (tcv, _, _, kind_co, body_co) <- splitForAllCo_maybe co_fun
+  , Just (arg, _) <- isReflCo_maybe co_arg
+  = assertPpr (isReflexiveCo kind_co) (ppr co_fun $$ ppr co_arg) $
+       -- If the arg is Refl, then kind_co must be reflexive too
+    substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
 mkInstCo co arg = InstCo co arg
 
 -- | Given @ty :: k1@, @co :: k1 ~ k2@,
@@ -1991,6 +2053,15 @@ extendLiftingContext (LC subst env) tv arg
   | otherwise
   = LC subst (extendVarEnv env tv arg)
 
+-- | Extend the substitution component of a lifting context with
+-- a new binding for a coercion variable. Used during coercion optimisation.
+extendLiftingContextCvSubst :: LiftingContext
+                            -> CoVar
+                            -> Coercion
+                            -> LiftingContext
+extendLiftingContextCvSubst (LC subst env) cv co
+  = LC (extendCvSubst subst cv co) env
+
 -- | Extend a lifting context with a new mapping, and extend the in-scope set
 extendLiftingContextAndInScope :: LiftingContext  -- ^ Original LC
                                -> TyCoVar         -- ^ new variable to map...
@@ -2298,9 +2369,9 @@ liftEnvSubst selector subst lc_env
       where
         equality_ty = selector (coercionKind co)
 
--- | Extract the underlying substitution from the LiftingContext
-lcSubst :: LiftingContext -> Subst
-lcSubst (LC subst _) = subst
+-- | Lookup a 'CoVar' in the substitution in a 'LiftingContext'
+lcLookupCoVar :: LiftingContext -> CoVar -> Maybe Coercion
+lcLookupCoVar (LC subst _) cv = lookupCoVar subst cv
 
 -- | Get the 'InScopeSet' from a 'LiftingContext'
 lcInScopeSet :: LiftingContext -> InScopeSet
@@ -2403,7 +2474,7 @@ coercionLKind co
     go (InstCo aco arg)          = go_app aco [go arg]
     go (KindCo co)               = typeKind (go co)
     go (SubCo co)                = go co
-    go (SelCo d co)              = getNthFromType d (go co)
+    go (SelCo d co)              = selectFromType d (go co)
     go (AxiomInstCo ax ind cos)  = go_ax_inst ax ind (map go cos)
     go (AxiomRuleCo ax cos)      = pFst $ expectJust "coercionKind" $
                                    coaxrProves ax $ map coercionKind cos
@@ -2426,23 +2497,6 @@ coercionLKind co
     go_app (InstCo co arg) args = go_app co (go arg:args)
     go_app co              args = piResultTys (go co) args
 
-getNthFromType :: HasDebugCallStack => CoSel -> Type -> Type
-getNthFromType (SelFun fs) ty
-  | Just (_af, mult, arg, res) <- splitFunTy_maybe ty
-  = getNthFun fs mult arg res
-
-getNthFromType (SelTyCon n _) ty
-  | Just args <- tyConAppArgs_maybe ty
-  = assertPpr (args `lengthExceeds` n) (ppr n $$ ppr ty) $
-    args `getNth` n
-
-getNthFromType SelForAll ty       -- Works for both tyvar and covar
-  | Just (tv,_) <- splitForAllTyCoVar_maybe ty
-  = tyVarKind tv
-
-getNthFromType cs ty
-  = pprPanic "getNthFromType" (ppr cs $$ ppr ty)
-
 coercionRKind :: Coercion -> Type
 coercionRKind co
   = go co
@@ -2464,7 +2518,7 @@ coercionRKind co
     go (InstCo aco arg)          = go_app aco [go arg]
     go (KindCo co)               = typeKind (go co)
     go (SubCo co)                = go co
-    go (SelCo d co)              = getNthFromType d (go co)
+    go (SelCo d co)              = selectFromType d (go co)
     go (AxiomInstCo ax ind cos)  = go_ax_inst ax ind (map go cos)
     go (AxiomRuleCo ax cos)      = pSnd $ expectJust "coercionKind" $
                                    coaxrProves ax $ map coercionKind cos
@@ -2570,9 +2624,7 @@ coercionRole = go
     go (UnivCo _ r _ _)             = r
     go (SymCo co)                   = go co
     go (TransCo co1 _co2)           = go co1
-    go (SelCo SelForAll      _co)   = Nominal
-    go (SelCo (SelTyCon _ r) _co)   = r
-    go (SelCo (SelFun fs)     co)   = funRole (coercionRole co) fs
+    go (SelCo cs co)                = mkSelCoResRole cs (coercionRole co)
     go (LRCo {})                    = Nominal
     go (InstCo co _)                = go co
     go (KindCo {})                  = Nominal

compiler/GHC/Core/Coercion/Opt.hs

@@ -24,10 +24,8 @@ import GHC.Core.Unify
 import GHC.Types.Var
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
-import GHC.Types.Unique.Set
 
 import GHC.Data.Pair
-import GHC.Data.List.SetOps ( getNth )
 
 import GHC.Utils.Outputable
 import GHC.Utils.Constants (debugIsOn)
@@ -132,45 +130,50 @@ optCoercion :: OptCoercionOpts -> Subst -> Coercion -> NormalCo
 optCoercion opts env co
   | optCoercionEnabled opts
   = optCoercion' env co
+
 {-
-  = pprTrace "optCoercion {" (text "Co:" <+> ppr co) $
+  = pprTrace "optCoercion {" (text "Co:" <> ppr (coercionSize co)) $
     let result = optCoercion' env co in
-    pprTrace "optCoercion }" (vcat [ text "Co:" <+> ppr co
-                                   , text "Optco:" <+> ppr result ]) $
+    pprTrace "optCoercion }"
+       (vcat [ text "Co:"    <+> ppr (coercionSize co)
+             , text "Optco:" <+> ppWhen (isReflCo result) (text "(refl)")
+                             <+> ppr (coercionSize result) ]) $
     result
 -}
 
   | otherwise
   = substCo env co
 
-
 optCoercion' :: Subst -> Coercion -> NormalCo
 optCoercion' env co
   | debugIsOn
   = let out_co = opt_co1 lc False co
         (Pair in_ty1  in_ty2,  in_role)  = coercionKindRole co
         (Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
+
+        details = vcat [ text "in_co:" <+> ppr co
+                       , text "in_ty1:" <+> ppr in_ty1
+                       , text "in_ty2:" <+> ppr in_ty2
+                       , text "out_co:" <+> ppr out_co
+                       , text "out_ty1:" <+> ppr out_ty1
+                       , text "out_ty2:" <+> ppr out_ty2
+                       , text "in_role:" <+> ppr in_role
+                       , text "out_role:" <+> ppr out_role
+                       ]
     in
+    warnPprTrace (not (isReflCo out_co) && isReflexiveCo out_co)
+                 "optCoercion: reflexive but not refl" details $
     assertPpr (substTyUnchecked env in_ty1 `eqType` out_ty1 &&
                substTyUnchecked env in_ty2 `eqType` out_ty2 &&
                in_role == out_role)
-              (hang (text "optCoercion changed types!")
-                  2 (vcat [ text "in_co:" <+> ppr co
-                          , text "in_ty1:" <+> ppr in_ty1
-                          , text "in_ty2:" <+> ppr in_ty2
-                          , text "out_co:" <+> ppr out_co
-                          , text "out_ty1:" <+> ppr out_ty1
-                          , text "out_ty2:" <+> ppr out_ty2
-                          , text "in_role:" <+> ppr in_role
-                          , text "out_role:" <+> ppr out_role
-                          , vcat $ map ppr_one $ nonDetEltsUniqSet $ coVarsOfCo co
-                          , text "subst:" <+> ppr env ]))
-               out_co
-
-  | otherwise         = opt_co1 lc False co
+              (hang (text "optCoercion changed types!") 2 details) $
+    out_co
+
+  | otherwise
+  = opt_co1 lc False co
   where
     lc = mkSubstLiftingContext env
-    ppr_one cv = ppr cv <+> dcolon <+> ppr (coVarKind cv)
+--    ppr_one cv = ppr cv <+> dcolon <+> ppr (coVarKind cv)
 
 
 type NormalCo    = Coercion
@@ -201,10 +204,11 @@ opt_co2 :: LiftingContext
         -> Role   -- ^ The role of the input coercion
         -> Coercion -> NormalCo
 opt_co2 env sym Phantom co = opt_phantom env sym co
-opt_co2 env sym r       co = opt_co3 env sym Nothing r co
+opt_co2 env sym r       co = opt_co4_wrap env sym False r co
 
 -- See Note [Optimising coercion optimisation]
--- | Optimize a coercion, knowing the coercion's non-Phantom role.
+-- | Optimize a coercion, knowing the coercion's non-Phantom role,
+--   and with an optional downgrade
 opt_co3 :: LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
 opt_co3 env sym (Just Phantom)          _ co = opt_phantom env sym co
 opt_co3 env sym (Just Representational) r co = opt_co4_wrap env sym True  r co
@@ -215,23 +219,38 @@ opt_co3 env sym _                       r co = opt_co4_wrap env sym False r co
 -- | Optimize a non-phantom coercion.
 opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag
                       -> Role -> Coercion -> NormalCo
--- Precondition: In every call (opt_co4 lc sym rep role co)
---               we should have role = coercionRole co
+-- Precondition:  In every call (opt_co4 lc sym rep role co)
+--                we should have role = coercionRole co
+-- Precondition:  role is not Phantom
+-- Postcondition: The resulting coercion is equivalant to
+--                     wrapsub (wrapsym (mksub co)
+--                 where wrapsym is SymCo if sym=True
+--                       wrapsub is SubCo if rep=True
+
+-- opt_co4_wrap is there just to support tracing, when debugging
+-- Usually it just goes straight to opt_co4
 opt_co4_wrap = opt_co4
 
 {-
 opt_co4_wrap env sym rep r co
   = pprTrace "opt_co4_wrap {"
-    ( vcat [ text "Sym:" <+> ppr sym
-           , text "Rep:" <+> ppr rep
-           , text "Role:" <+> ppr r
-           , text "Co:" <+> ppr co ]) $
-    assert (r == coercionRole co )    $
-    let result = opt_co4 env sym rep r co in
-    pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
-    result
--}
+   ( vcat [ text "Sym:" <+> ppr sym
+          , text "Rep:" <+> ppr rep
+          , text "Role:" <+> ppr r
+          , text "Co:" <+> ppr co ]) $
+   assert (r == coercionRole co )    $
+   let result = opt_co4 env sym rep r co in
+   pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
+   assertPpr (res_role == coercionRole result)
+             (vcat [ text "Role:" <+> ppr r
+                   , text "Result: " <+>  ppr result
+                   , text "Result type:" <+> ppr (coercionType result) ]) $
+   result
 
+  where
+    res_role | rep       = Representational
+             | otherwise = r
+-}
 
 opt_co4 env _   rep r (Refl ty)
   = assertPpr (r == Nominal)
@@ -310,14 +329,15 @@ opt_co4 env sym rep r (FunCo _r afl afr cow co1 co2)
     !(afl', afr') = swapSym sym (afl, afr)
 
 opt_co4 env sym rep r (CoVarCo cv)
-  | Just co <- lookupCoVar (lcSubst env) cv
+  | Just co <- lcLookupCoVar env cv   -- see Note [Forall over coercion] for why
+                                      -- this is the right thing here
   = opt_co4_wrap (zapLiftingContext env) sym rep r co
 
   | ty1 `eqType` ty2   -- See Note [Optimise CoVarCo to Refl]
   = mkReflCo (chooseRole rep r) ty1
 
   | otherwise
-  = assert (isCoVar cv1 )
+  = assert (isCoVar cv1) $
     wrapRole rep r $ wrapSym sym $
     CoVarCo cv1
 
@@ -363,39 +383,15 @@ opt_co4 env sym rep r (TransCo co1 co2)
     co2' = opt_co4_wrap env sym rep r co2
     in_scope = lcInScopeSet env
 
-opt_co4 env _sym rep r (SelCo n co)
-  | Just (ty, _co_role) <- isReflCo_maybe co
-  = liftCoSubst (chooseRole rep r) env (getNthFromType n ty)
-    -- NB: it is /not/ true that r = _co_role
-    --     Rather, r = coercionRole (SelCo n co)
-
-opt_co4 env sym rep r (SelCo (SelTyCon n r1) (TyConAppCo _ _ cos))
-  = assert (r == r1 )
-    opt_co4_wrap env sym rep r (cos `getNth` n)
-
--- see the definition of GHC.Builtin.Types.Prim.funTyCon
-opt_co4 env sym rep r (SelCo (SelFun fs) (FunCo _r2 _afl _afr w co1 co2))
-  = opt_co4_wrap env sym rep r (getNthFun fs w co1 co2)
-
-opt_co4 env sym rep _ (SelCo SelForAll (ForAllCo { fco_kind = eta }))
-      -- works for both tyvar and covar
-  = opt_co4_wrap env sym rep Nominal eta
-
-opt_co4 env sym rep r (SelCo n co)
-  | Just nth_co <- case (co', n) of
-      (TyConAppCo _ _ cos, SelTyCon n _) -> Just (cos `getNth` n)
-      (FunCo _ _ _ w co1 co2, SelFun fs) -> Just (getNthFun fs w co1 co2)
-      (ForAllCo { fco_kind = eta }, SelForAll) -> Just eta
-      _                  -> Nothing
-  = if rep && (r == Nominal)
-      -- keep propagating the SubCo
-    then opt_co4_wrap (zapLiftingContext env) False True Nominal nth_co
-    else nth_co
+opt_co4 env sym rep r (SelCo cs co)
+  -- Historical note 1: we used to check `co` for Refl, TyConAppCo etc
+  -- before optimising `co`; but actually the SelCo will have been built
+  -- with mkSelCo, so these tests always fail.
 
-  | otherwise
-  = wrapRole rep r $ SelCo n co'
-  where
-    co' = opt_co1 env sym co
+  -- Historical note 2: if rep=True and r=Nominal, we used to recursively
+  -- call opt_co4 to re-optimse the result. But (a) that is inefficient
+  -- and (b) wrapRole uses mkSubCo which does much the same job
+  = wrapRole rep r $ mkSelCo cs $ opt_co1 env sym co
 
 opt_co4 env sym rep r (LRCo lr co)
   | Just pr_co <- splitAppCo_maybe co
@@ -414,6 +410,40 @@ opt_co4 env sym rep r (LRCo lr co)
     pick_lr CLeft  (l, _) = l
     pick_lr CRight (_, r) = r
 
+{-
+Note [Forall over coercion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Example:
+  type (:~:) :: forall k. k -> k -> Type
+  Refl :: forall k (a :: k) (b :: k). forall (cv :: (~#) k k a b). (:~:) k a b
+  k1,k2,k3,k4 :: Type
+  eta :: (k1 ~# k2) ~# (k3 ~# k4)    ==    ((~#) Type Type k1 k2) ~# ((~#) Type Type k3 k4)
+  co1_3 :: k1 ~# k3
+  co2_4 :: k2 ~# k4
+  nth 2 eta :: k1 ~# k3
+  nth 3 eta :: k2 ~# k4
+  co11_31 :: <k1> ~# (sym co1_3)
+  co22_24 :: <k2> ~# co2_4
+  (forall (cv :: eta). Refl <Type> co1_3 co2_4 (co11_31 ;; cv ;; co22_24)) ::
+    (forall (cv :: k1 ~# k2). Refl Type k1 k2 (<k1> ;; cv ;; <k2>) ~#
+    (forall (cv :: k3 ~# k4). Refl Type k3 k4
+       (sym co1_3 ;; nth 2 eta ;; cv ;; sym (nth 3 eta) ;; co2_4))
+  co1_2 :: k1 ~# k2
+  co3_4 :: k3 ~# k4
+  co5 :: co1_2 ~# co3_4
+  InstCo (forall (cv :: eta). Refl <Type> co1_3 co2_4 (co11_31 ;; cv ;; co22_24)) co5 ::
+   (Refl Type k1 k2 (<k1> ;; cv ;; <k2>))[cv |-> co1_2] ~#
+   (Refl Type k3 k4 (sym co1_3 ;; nth 2 eta ;; cv ;; sym (nth 3 eta) ;; co2_4))[cv |-> co3_4]
+      ==
+   (Refl Type k1 k2 (<k1> ;; co1_2 ;; <k2>)) ~#
+    (Refl Type k3 k4 (sym co1_3 ;; nth 2 eta ;; co3_4 ;; sym (nth 3 eta) ;; co2_4))
+      ==>
+   Refl <Type> co1_3 co2_4 (co11_31 ;; co1_2 ;; co22_24)
+Conclusion: Because of the way this all works, we want to put in the *left-hand*
+coercion in co5's type. (In the code, co5 is called `arg`.)
+So we extend the environment binding cv to arg's left-hand type.
+-}
+
 -- See Note [Optimising InstCo]
 opt_co4 env sym rep r (InstCo co1 arg)
     -- forall over type...
@@ -425,12 +455,10 @@ opt_co4 env sym rep r (InstCo co1 arg)
                    -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1)
                  sym rep r co_body
 
-    -- forall over coercion...
-  | Just (cv, _visL, _visR, kind_co, co_body) <- splitForAllCo_co_maybe co1
+    -- See Note [Forall over coercion]
+  | Just (cv, _visL, _visR, _kind_co, co_body) <- splitForAllCo_co_maybe co1
   , CoercionTy h1 <- t1
-  , CoercionTy h2 <- t2
-  = let new_co = mk_new_co cv (opt_co4_wrap env sym False Nominal kind_co) h1 h2
-    in opt_co4_wrap (extendLiftingContext env cv new_co) sym rep r co_body
+  = opt_co4_wrap (extendLiftingContextCvSubst env cv h1) sym rep r co_body
 
     -- See if it is a forall after optimization
     -- If so, do an inefficient one-variable substitution, then re-optimize
@@ -441,12 +469,10 @@ opt_co4 env sym rep r (InstCo co1 arg)
                     (mkCoherenceRightCo Nominal t2' (mkSymCo kind_co') arg'))
             False False r' co_body'
 
-    -- forall over coercion...
-  | Just (cv', _visL, _visR, kind_co', co_body') <- splitForAllCo_co_maybe co1'
+    -- See Note [Forall over coercion]
+  | Just (cv', _visL, _visR, _kind_co', co_body') <- splitForAllCo_co_maybe co1'
   , CoercionTy h1' <- t1'
-  , CoercionTy h2' <- t2'
-  = let new_co = mk_new_co cv' kind_co' h1' h2'
-    in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv' new_co)
+  = opt_co4_wrap (extendLiftingContextCvSubst (zapLiftingContext env) cv' h1')
                     False False r' co_body'
 
   | otherwise = InstCo co1' arg'
@@ -467,20 +493,6 @@ opt_co4 env sym rep r (InstCo co1 arg)
     Pair t1  t2  = coercionKind sym_arg
     Pair t1' t2' = coercionKind arg'
 
-    mk_new_co cv kind_co h1 h2
-      = let -- h1 :: (t1 ~ t2)
-            -- h2 :: (t3 ~ t4)
-            -- kind_co :: (t1 ~ t2) ~ (t3 ~ t4)
-            -- n1 :: t1 ~ t3
-            -- n2 :: t2 ~ t4
-            -- new_co = (h1 :: t1 ~ t2) ~ ((n1;h2;sym n2) :: t1 ~ t2)
-            r2  = coVarRole cv
-            kind_co' = downgradeRole r2 Nominal kind_co
-            n1 = mkSelCo (SelTyCon 2 r2) kind_co'
-            n2 = mkSelCo (SelTyCon 3 r2) kind_co'
-         in mkProofIrrelCo Nominal (Refl (coercionType h1)) h1
-                           (n1 `mkTransCo` h2 `mkTransCo` (mkSymCo n2))
-
 opt_co4 env sym _rep r (KindCo co)
   = assert (r == Nominal) $
     let kco' = promoteCoercion co in
@@ -631,8 +643,25 @@ opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] ->
 opt_transList is = zipWithEqual "opt_transList" (opt_trans is)
   -- The input lists must have identical length.
 
-opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
+opt_trans, opt_trans' :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
+
+-- opt_trans just allows us to add some debug tracing
+-- Usually it just goes to opt_trans'
+opt_trans is co1 co2 = opt_trans' is co1 co2
+
+{-
 opt_trans is co1 co2
+  = assertPpr (r1==r2) (vcat [ ppr r1 <+> ppr co1, ppr r2 <+> ppr co2]) $
+    assertPpr (rres == r1) (vcat [ ppr r1 <+> ppr co1, ppr r2 <+> ppr co2, text "res" <+> ppr rres <+> ppr res ]) $
+    res
+  where
+    res = opt_trans' is co1 co2
+    rres = coercionRole res
+    r1 = coercionRole co1
+    r2 = coercionRole co1
+-}
+
+opt_trans' is co1 co2
   | isReflCo co1 = co2
     -- optimize when co1 is a Refl Co
   | otherwise    = opt_trans1 is co1 co2
@@ -806,10 +835,37 @@ opt_trans_rule is co1 co2
 -- Push transitivity inside axioms
 opt_trans_rule is co1 co2
 
+  -- TrPushAxSym/TrPushSymAx
+  -- Put this first!  Otherwise (#23619) we get
+  --    newtype N a = MkN a
+  --    axN :: forall a. N a ~ a
+  -- Now consider (axN ty ; sym (axN ty))
+  -- If we put TrPushSymAxR first, we'll get
+  --    (axN ty ; sym (axN ty)) :: N ty ~ N ty -- Obviously Refl
+  --    --> axN (sym (axN ty))  :: N ty ~ N ty -- Very stupid
+  | Just (sym1, ax1, ind1, cos1) <- isAxiom_maybe co1
+  , Just (sym2, ax2, ind2, cos2) <- isAxiom_maybe co2
+  , ax1 == ax2
+  , ind1 == ind2
+  , sym1 == not sym2
+  , let branch = coAxiomNthBranch ax1 ind1
+        role   = coAxiomRole ax1
+        qtvs   = coAxBranchTyVars branch ++ coAxBranchCoVars branch
+        lhs    = coAxNthLHS ax1 ind1
+        rhs    = coAxBranchRHS branch
+        pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
+  , all (`elemVarSet` pivot_tvs) qtvs
+  = fireTransRule "TrPushAxSym" co1 co2 $
+    if sym2
+       -- TrPushAxSym
+    then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
+       -- TrPushSymAx
+    else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
+
   -- See Note [Push transitivity inside axioms] and
   -- Note [Push transitivity inside newtype axioms only]
   -- TrPushSymAxR
-  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
+  | Just (sym, con, ind, cos1) <- isAxiom_maybe co1
   , isNewTyCon (coAxiomTyCon con)
   , True <- sym
   , Just cos2 <- matchAxiom sym con ind co2
@@ -817,7 +873,7 @@ opt_trans_rule is co1 co2
   = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
 
   -- TrPushAxR
-  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
+  | Just (sym, con, ind, cos1) <- isAxiom_maybe co1
   , isNewTyCon (coAxiomTyCon con)
   , False <- sym
   , Just cos2 <- matchAxiom sym con ind co2
@@ -825,7 +881,7 @@ opt_trans_rule is co1 co2
   = fireTransRule "TrPushAxR" co1 co2 newAxInst
 
   -- TrPushSymAxL
-  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
+  | Just (sym, con, ind, cos2) <- isAxiom_maybe co2
   , isNewTyCon (coAxiomTyCon con)
   , True <- sym
   , Just cos1 <- matchAxiom (not sym) con ind co1
@@ -833,35 +889,13 @@ opt_trans_rule is co1 co2
   = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
 
   -- TrPushAxL
-  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
+  | Just (sym, con, ind, cos2) <- isAxiom_maybe co2
   , isNewTyCon (coAxiomTyCon con)
   , False <- sym
   , Just cos1 <- matchAxiom (not sym) con ind co1
   , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
   = fireTransRule "TrPushAxL" co1 co2 newAxInst
 
-  -- TrPushAxSym/TrPushSymAx
-  | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
-  , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
-  , con1 == con2
-  , ind1 == ind2
-  , sym1 == not sym2
-  , let branch = coAxiomNthBranch con1 ind1
-        qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
-        lhs  = coAxNthLHS con1 ind1
-        rhs  = coAxBranchRHS branch
-        pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
-  , all (`elemVarSet` pivot_tvs) qtvs
-  = fireTransRule "TrPushAxSym" co1 co2 $
-    if sym2
-       -- TrPushAxSym
-    then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
-       -- TrPushSymAx
-    else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
-  where
-    co1_is_axiom_maybe = isAxiom_maybe co1
-    co2_is_axiom_maybe = isAxiom_maybe co2
-    role = coercionRole co1 -- should be the same as coercionRole co2!
 
 opt_trans_rule _ co1 co2        -- Identity rule
   | let ty1 = coercionLKind co1
@@ -1115,11 +1149,13 @@ chooseRole _    r = r
 
 -----------
 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
-isAxiom_maybe (SymCo co)
-  | Just (sym, con, ind, cos) <- isAxiom_maybe co
-  = Just (not sym, con, ind, cos)
-isAxiom_maybe (AxiomInstCo con ind cos)
-  = Just (False, con, ind, cos)
+-- We don't expect to see nested SymCo; and that lets us write a simple,
+-- non-recursive function. (If we see a nested SymCo we'll just fail,
+-- which is ok.)
+isAxiom_maybe (SymCo (AxiomInstCo ax ind cos))
+  = Just (True, ax, ind, cos)
+isAxiom_maybe (AxiomInstCo ax ind cos)
+  = Just (False, ax, ind, cos)
 isAxiom_maybe _ = Nothing
 
 matchAxiom :: Bool -- True = match LHS, False = match RHS

compiler/GHC/Core/DataCon.hs

@@ -49,7 +49,8 @@ module GHC.Core.DataCon (
         dataConIsInfix,
         dataConWorkId, dataConWrapId, dataConWrapId_maybe,
         dataConImplicitTyThings,
-        dataConRepStrictness, dataConImplBangs, dataConBoxer,
+        dataConRepStrictness, dataConRepStrictness_maybe,
+        dataConImplBangs, dataConBoxer,
 
         splitDataProductType_maybe,
 
@@ -60,7 +61,7 @@ module GHC.Core.DataCon (
         isVanillaDataCon, isNewDataCon, isTypeDataCon,
         classDataCon, dataConCannotMatch,
         dataConUserTyVarsNeedWrapper, checkDataConTyVars,
-        isBanged, isMarkedStrict, cbvFromStrictMark, eqHsBang, isSrcStrict, isSrcUnpacked,
+        isBanged, isUnpacked, isMarkedStrict, cbvFromStrictMark, eqHsBang, isSrcStrict, isSrcUnpacked,
         specialPromotedDc,
 
         -- ** Promotion related functions
@@ -97,6 +98,7 @@ import GHC.Types.Unique.FM ( UniqFM )
 import GHC.Types.Unique.Set
 import GHC.Builtin.Uniques( mkAlphaTyVarUnique )
 import GHC.Data.Graph.UnVar  -- UnVarSet and operations
+import GHC.Data.Maybe (orElse)
 
 import {-# SOURCE #-} GHC.Tc.Utils.TcType ( ConcreteTyVars )
 
@@ -524,6 +526,18 @@ data DataCon
                 -- Matches 1-1 with dcOrigArgTys
                 -- Hence length = dataConSourceArity dataCon
 
+        dcImplBangs :: [HsImplBang],
+                -- The actual decisions made (including failures)
+                -- about the original arguments; 1-1 with orig_arg_tys
+                -- See Note [Bangs on data constructor arguments]
+
+        dcStricts :: [StrictnessMark],
+                -- One mark for every field of the DataCon worker;
+                -- if it's empty, then all fields are lazy,
+                -- otherwise it has the same length as dataConRepArgTys.
+                -- See also Note [Strict fields in Core] in GHC.Core
+                -- for the effect on the strictness signature
+
         dcFields  :: [FieldLabel],
                 -- Field labels for this constructor, in the
                 -- same order as the dcOrigArgTys;
@@ -826,13 +840,6 @@ data DataConRep
                                           -- after unboxing and flattening,
                                           -- and *including* all evidence args
 
-        , dcr_stricts :: [StrictnessMark]  -- 1-1 with dcr_arg_tys
-                -- See also Note [Data-con worker strictness]
-
-        , dcr_bangs :: [HsImplBang]  -- The actual decisions made (including failures)
-                                     -- about the original arguments; 1-1 with orig_arg_tys
-                                     -- See Note [Bangs on data constructor arguments]
-
     }
 
 type DataConEnv a = UniqFM DataCon a     -- Keyed by DataCon
@@ -901,43 +908,8 @@ eqSpecPreds spec = [ mkPrimEqPred (mkTyVarTy tv) ty
 instance Outputable EqSpec where
   ppr (EqSpec tv ty) = ppr (tv, ty)
 
-{- Note [Data-con worker strictness]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Notice that we do *not* say the worker Id is strict even if the data
-constructor is declared strict
-     e.g.    data T = MkT ![Int] Bool
-Even though most often the evals are done by the *wrapper* $WMkT, there are
-situations in which tag inference will re-insert evals around the worker.
-So for all intents and purposes the *worker* MkT is strict, too!
-
-Unfortunately, if we exposed accurate strictness of DataCon workers, we'd
-see the following transformation:
-
-  f xs = case xs of xs' { __DEFAULT -> ... case MkT xs b of x { __DEFAULT -> [x] } } -- DmdAnal: Strict in xs
-  ==> { drop-seq, binder swap on xs' }
-  f xs = case MkT xs b of x { __DEFAULT -> [x] } -- DmdAnal: Still strict in xs
-  ==> { case-to-let }
-  f xs = let x = MkT xs' b in [x] -- DmdAnal: No longer strict in xs!
-
-I.e., we are ironically losing strictness in `xs` by dropping the eval on `xs`
-and then doing case-to-let. The issue is that `exprIsHNF` currently says that
-every DataCon worker app is a value. The implicit assumption is that surrounding
-evals will have evaluated strict fields like `xs` before! But now that we had
-just dropped the eval on `xs`, that assumption is no longer valid.
-
-Long story short: By keeping the demand signature lazy, the Simplifier will not
-drop the eval on `xs` and using `exprIsHNF` to decide case-to-let and others
-remains sound.
-
-Similarly, during demand analysis in dmdTransformDataConSig, we bump up the
-field demand with `C_01`, *not* `C_11`, because the latter exposes too much
-strictness that will drop the eval on `xs` above.
-
-This issue is discussed at length in
-"Failed idea: no wrappers for strict data constructors" in #21497 and #22475.
-
-Note [Bangs on data constructor arguments]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Bangs on data constructor arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
   data T = MkT !Int {-# UNPACK #-} !Int Bool
 
@@ -963,8 +935,8 @@ Terminology:
   the flag settings in the importing module.
   Also see Note [Bangs on imported data constructors] in GHC.Types.Id.Make
 
-* The dcr_bangs field of the dcRep field records the [HsImplBang]
-  If T was defined in this module, Without -O the dcr_bangs might be
+* The dcImplBangs field records the [HsImplBang]
+  If T was defined in this module, Without -O the dcImplBangs might be
     [HsStrict _, HsStrict _, HsLazy]
   With -O it might be
     [HsStrict _, HsUnpack _, HsLazy]
@@ -973,6 +945,17 @@ Terminology:
   With -XStrictData it might be
     [HsStrict _, HsUnpack _, HsStrict _]
 
+* Core passes will often need to know whether the DataCon worker or wrapper in
+  an application is strict in some (lifted) field or not. This is tracked in the
+  demand signature attached to a DataCon's worker resp. wrapper Id.
+
+  So if you've got a DataCon dc, you can get the demand signature by
+  `idDmdSig (dataConWorkId dc)` and make out strict args by testing with
+  `isStrictDmd`. Similarly, `idDmdSig <$> dataConWrapId_maybe dc` gives
+  you the demand signature of the wrapper, if it exists.
+
+  These demand signatures are set in GHC.Types.Id.Make.
+
 Note [Detecting useless UNPACK pragmas]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We want to issue a warning when there's an UNPACK pragma in the source code,
@@ -1008,7 +991,6 @@ we consult HsImplBang:
 The boolean flag is used only for this warning.
 See #11270 for motivation.
 
-
 ************************************************************************
 *                                                                      *
 \subsection{Instances}
@@ -1110,6 +1092,11 @@ isBanged (HsUnpack {}) = True
 isBanged (HsStrict {}) = True
 isBanged HsLazy        = False
 
+isUnpacked :: HsImplBang -> Bool
+isUnpacked (HsUnpack {}) = True
+isUnpacked (HsStrict {}) = False
+isUnpacked HsLazy        = False
+
 isSrcStrict :: SrcStrictness -> Bool
 isSrcStrict SrcStrict = True
 isSrcStrict _ = False
@@ -1135,13 +1122,15 @@ cbvFromStrictMark MarkedStrict = MarkedCbv
 
 -- | Build a new data constructor
 mkDataCon :: Name
-          -> Bool           -- ^ Is the constructor declared infix?
-          -> TyConRepName   -- ^  TyConRepName for the promoted TyCon
-          -> [HsSrcBang]    -- ^ Strictness/unpack annotations, from user
-          -> [FieldLabel]   -- ^ Field labels for the constructor,
-                            -- if it is a record, otherwise empty
-          -> [TyVar]        -- ^ Universals.
-          -> [TyCoVar]      -- ^ Existentials.
+          -> Bool               -- ^ Is the constructor declared infix?
+          -> TyConRepName       -- ^  TyConRepName for the promoted TyCon
+          -> [HsSrcBang]        -- ^ Strictness/unpack annotations, from user
+          -> [HsImplBang]       -- ^ Strictness/unpack annotations, as inferred by the compiler
+          -> [StrictnessMark]   -- ^ Strictness marks for the DataCon worker's fields in Core
+          -> [FieldLabel]       -- ^ Field labels for the constructor,
+                                -- if it is a record, otherwise empty
+          -> [TyVar]            -- ^ Universals.
+          -> [TyCoVar]          -- ^ Existentials.
           -> ConcreteTyVars
                                 -- ^ TyVars which must be instantiated with
                                 -- concrete types
@@ -1163,7 +1152,9 @@ mkDataCon :: Name
   -- Can get the tag from the TyCon
 
 mkDataCon name declared_infix prom_info
-          arg_stricts   -- Must match orig_arg_tys 1-1
+          arg_stricts  -- Must match orig_arg_tys 1-1
+          impl_bangs   -- Must match orig_arg_tys 1-1
+          str_marks    -- Must be empty or match dataConRepArgTys 1-1
           fields
           univ_tvs ex_tvs conc_tvs user_tvbs
           eq_spec theta
@@ -1180,6 +1171,8 @@ mkDataCon name declared_infix prom_info
   = con
   where
     is_vanilla = null ex_tvs && null eq_spec && null theta
+    str_marks' | not $ any isMarkedStrict str_marks = []
+               | otherwise                          = str_marks
 
     con = MkData {dcName = name, dcUnique = nameUnique name,
                   dcVanilla = is_vanilla, dcInfix = declared_infix,
@@ -1192,7 +1185,8 @@ mkDataCon name declared_infix prom_info
                   dcStupidTheta = stupid_theta,
                   dcOrigArgTys = orig_arg_tys, dcOrigResTy = orig_res_ty,
                   dcRepTyCon = rep_tycon,
-                  dcSrcBangs = arg_stricts,
+                  dcSrcBangs = arg_stricts, dcImplBangs = impl_bangs,
+                  dcStricts = str_marks',
                   dcFields = fields, dcTag = tag, dcRepType = rep_ty,
                   dcWorkId = work_id,
                   dcRep = rep,
@@ -1436,19 +1430,27 @@ isNullaryRepDataCon :: DataCon -> Bool
 isNullaryRepDataCon dc = dataConRepArity dc == 0
 
 dataConRepStrictness :: DataCon -> [StrictnessMark]
--- ^ Give the demands on the arguments of a
--- Core constructor application (Con dc args)
-dataConRepStrictness dc = case dcRep dc of
-                            NoDataConRep -> [NotMarkedStrict | _ <- dataConRepArgTys dc]
-                            DCR { dcr_stricts = strs } -> strs
+-- ^ Give the demands on the runtime arguments of a Core DataCon worker
+-- application.
+-- The length of the list matches `dataConRepArgTys` (e.g., the number
+-- of runtime arguments).
+dataConRepStrictness dc
+  = dataConRepStrictness_maybe dc
+    `orElse` map (const NotMarkedStrict) (dataConRepArgTys dc)
+
+dataConRepStrictness_maybe :: DataCon -> Maybe [StrictnessMark]
+-- ^ Give the demands on the runtime arguments of a Core DataCon worker
+-- application or `Nothing` if all of them are lazy.
+-- The length of the list matches `dataConRepArgTys` (e.g., the number
+-- of runtime arguments).
+dataConRepStrictness_maybe dc
+  | null (dcStricts dc) = Nothing
+  | otherwise           = Just (dcStricts dc)
 
 dataConImplBangs :: DataCon -> [HsImplBang]
 -- The implementation decisions about the strictness/unpack of each
 -- source program argument to the data constructor
-dataConImplBangs dc
-  = case dcRep dc of
-      NoDataConRep              -> replicate (dcSourceArity dc) HsLazy
-      DCR { dcr_bangs = bangs } -> bangs
+dataConImplBangs dc = dcImplBangs dc
 
 dataConBoxer :: DataCon -> Maybe DataConBoxer
 dataConBoxer (MkData { dcRep = DCR { dcr_boxer = boxer } }) = Just boxer