[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 5 commits: gitlab-ci: Bump docker images

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Wed Feb 12 10:22:16 UTC 2025



Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC


Commits:
a566da92 by Ben Gamari at 2025-02-10T03:21:49-05:00
gitlab-ci: Bump docker images

Closes #25693.

- - - - -
a7e23f01 by Ben Gamari at 2025-02-10T03:21:49-05:00
hadrian: Drop uses of head/tail

To silence warnings with GHC 9.10

- - - - -
12752f0c by Ben Gamari at 2025-02-10T03:21:49-05:00
hadrian: Disable x-data-list-nonempty-unzip warning

- - - - -
e22a14fc by Simon Peyton Jones at 2025-02-11T16:21:10+00:00
Deal correctly with Given CallStack constraints

As #25675 showed, the CallStack solving mechanism was failing
to account for Given CallStack constraints.

This small patch fixes it and improves the Notes.

Small improvement to GHCi debugger output in break011, break024,
which is discussed on the MR !13883

- - - - -
a3bbd4bf by Simon Peyton Jones at 2025-02-12T05:21:45-05:00
Fix inlineBoringOk again

This MR fixes #25713, which turned out to be a consequence of not
completing #17182.

I think I have now gotten it right.  See the new
  Note [inlineBoringOk]

- - - - -


21 changed files:

- .gitlab-ci.yml
- compiler/GHC/Core/Opt/SetLevels.hs
- compiler/GHC/Core/Unfold.hs
- compiler/GHC/Core/Unfold/Make.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Types.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Types/Origin.hs
- hadrian/src/Hadrian/Utilities.hs
- hadrian/src/Oracles/ModuleFiles.hs
- hadrian/src/Rules/Dependencies.hs
- hadrian/src/Settings/Parser.hs
- testsuite/tests/ghci.debugger/scripts/break011.stdout
- testsuite/tests/ghci.debugger/scripts/break024.stdout
- + testsuite/tests/profiling/should_run/T25675.hs
- + testsuite/tests/profiling/should_run/T25675.stdout
- testsuite/tests/profiling/should_run/all.T
- testsuite/tests/simplCore/should_compile/T22375DataFamily.stderr
- + testsuite/tests/simplCore/should_compile/T25713.hs
- + testsuite/tests/simplCore/should_compile/T25713.stderr
- testsuite/tests/simplCore/should_compile/all.T


Changes:

=====================================
.gitlab-ci.yml
=====================================
@@ -2,7 +2,7 @@ variables:
   GIT_SSL_NO_VERIFY: "1"
 
   # Commit of ghc/ci-images repository from which to pull Docker images
-  DOCKER_REV: eb4d3389fd62e4f7321a0c8799014ec1f4da0708
+  DOCKER_REV: 94df7d589f0ded990826bc7a4d7f5a40d6055a4f
 
   # Sequential version number of all cached things.
   # Bump to invalidate GitLab CI cache.


=====================================
compiler/GHC/Core/Opt/SetLevels.hs
=====================================
@@ -1203,8 +1203,8 @@ Note [Floating applications to coercions]
 We don’t float out variables applied only to type arguments, since the
 extra binding would be pointless: type arguments are completely erased.
 But *coercion* arguments aren’t (see Note [Coercion tokens] in
-"GHC.CoreToStg" and Note [Count coercion arguments in boring contexts] in
-"GHC.Core.Unfold"), so we still want to float out variables applied only to
+"GHC.CoreToStg" and Note [inlineBoringOk] in"GHC.Core.Unfold"),
+so we still want to float out variables applied only to
 coercion arguments.
 
 


=====================================
compiler/GHC/Core/Unfold.hs
=====================================
@@ -213,34 +213,110 @@ let-bound things that are dead are usually caught by preInlineUnconditionally
 ************************************************************************
 -}
 
+{- Note [inlineBoringOk]
+~~~~~~~~~~~~~~~~~~~~~~~~
+See Note [INLINE for small functions]
+
+The function `inlineBoringOk` returns True (boringCxtOk) if the supplied
+unfolding, which looks like (\x y z. body), is such that the result of
+inlining a saturated call is no bigger than `body`.  Some wrinkles:
+
+(IB1) An important case is
+    - \x. (x `cast` co)
+
+(IB2) If `body` looks like a data constructor worker, we become keener
+  to inline, by ignoring the number of arguments; we just insist they
+  are all trivial.  Reason: in a call like `f (g x y)`, if `g` unfolds
+  to a data construtor, we can allocate a data constructor instead of
+  a thunk (g x y).
+
+  A case in point where a GADT data constructor failed to inline (#25713)
+      $WK = /\a \x. K @a <co> x
+  We really want to inline a boring call to $WK so that we allocate
+  a data constructor not a thunk ($WK @ty x).
+
+  But not for nullary constructors!  We don't want to turn
+     f ($WRefl @ty)
+  into
+     f (Refl @ty <co>)
+   because the latter might allocate, whereas the former shares.
+   (You might wonder if (Refl @ty <co>) should allocate, but I think
+   that currently it does.)  So for nullary constructors, `inlineBoringOk`
+   returns False.
+
+(IB3) Types and coercions do not count towards the expression size.
+      They are ultimately erased.
+
+(IB4) If there are no value arguments, `inlineBoringOk` we have to be
+  careful (#17182).  If we have
+      let y = x @Int in f y y
+  there’s no reason not to inline y at both use sites — no work is
+  actually duplicated.
+
+  But not so for coercion arguments! Unlike type arguments, which have
+  no runtime representation, coercion arguments *do* have a runtime
+  representation (albeit the zero-width VoidRep, see Note [Coercion
+  tokens] in "GHC.CoreToStg").  For example:
+       let y = g @Int <co> in g y y
+  Here `co` is a value argument, and calling it twice might duplicate
+  work.
+
+  Even if `g` is a data constructor, so no work is duplicated,
+  inlining `y` might duplicate allocation of a data constructor object
+  (#17787). See also (IB2).
+
+  TL;DR: if `is_fun` is False, so we have no value arguments, we /do/
+  count coercion arguments, despite (IB3).
+
+(IB5) You might wonder about an unfolding like  (\x y z -> x (y z)),
+  whose body is, in some sense, just as small as (g x y z).
+  But `inlineBoringOk` doesn't attempt anything fancy; it just looks
+  for a function call with trivial arguments, Keep it simple.
+-}
+
 inlineBoringOk :: CoreExpr -> Bool
--- See Note [INLINE for small functions]
 -- True => the result of inlining the expression is
 --         no bigger than the expression itself
 --     eg      (\x y -> f y x)
--- This is a quick and dirty version. It doesn't attempt
--- to deal with  (\x y z -> x (y z))
--- The really important one is (x `cast` c)
+-- See Note [inlineBoringOk]
 inlineBoringOk e
   = go 0 e
   where
+    is_fun = isValFun e
+
     go :: Int -> CoreExpr -> Bool
-    go credit (Lam x e) | isId x           = go (credit+1) e
-                        | otherwise        = go credit e
-        -- See Note [Count coercion arguments in boring contexts]
-    go credit (App f (Type {}))            = go credit f
-    go credit (App f a) | credit > 0
-                        , exprIsTrivial a  = go (credit-1) f
-    go credit (Tick _ e)                   = go credit e -- dubious
-    go credit (Cast e _)                   = go credit e
+    go credit (Lam x e) | isRuntimeVar x  = go (credit+1) e
+                        | otherwise       = go credit e      -- See (IB3)
+
+    go credit (App f (Type {}))           = go credit f      -- See (IB3)
+    go credit (App f (Coercion {}))
+      | is_fun                            = go credit f      -- See (IB3)
+      | otherwise                         = go (credit-1) f  -- See (IB4)
+    go credit (App f a) | exprIsTrivial a = go (credit-1) f
+
     go credit (Case e b _ alts)
       | null alts
       = go credit e   -- EmptyCase is like e
       | Just rhs <- isUnsafeEqualityCase e b alts
       = go credit rhs -- See Note [Inline unsafeCoerce]
-    go _      (Var {})                     = boringCxtOk
-    go _      (Lit l)                      = litIsTrivial l && boringCxtOk
-    go _      _                            = boringCxtNotOk
+
+    go credit (Tick _ e) = go credit e      -- dubious
+    go credit (Cast e _) = go credit e      -- See (IB3)
+
+    go _      (Lit l)    = litIsTrivial l && boringCxtOk
+
+      -- We assume credit >= 0; literals aren't functions
+    go credit (Var v) | isDataConWorkId v, is_fun = boringCxtOk  -- See (IB2)
+                      | credit >= 0               = boringCxtOk
+                      | otherwise                 = boringCxtNotOk
+    go _      _                                   = boringCxtNotOk
+
+isValFun :: CoreExpr -> Bool
+-- True of functions with at least
+-- one top-level value lambda
+isValFun (Lam b e) | isRuntimeVar b = True
+                   | otherwise      = isValFun e
+isValFun _                          = False
 
 calcUnfoldingGuidance
         :: UnfoldingOpts
@@ -398,29 +474,6 @@ Things to note:
     NB: you might think that PostInlineUnconditionally would do this
     but it doesn't fire for top-level things; see GHC.Core.Opt.Simplify.Utils
     Note [Top level and postInlineUnconditionally]
-
-Note [Count coercion arguments in boring contexts]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In inlineBoringOK, we ignore type arguments when deciding whether an
-expression is okay to inline into boring contexts. This is good, since
-if we have a definition like
-
-  let y = x @Int in f y y
-
-there’s no reason not to inline y at both use sites — no work is
-actually duplicated. It may seem like the same reasoning applies to
-coercion arguments, and indeed, in #17182 we changed inlineBoringOK to
-treat coercions the same way.
-
-However, this isn’t a good idea: unlike type arguments, which have
-no runtime representation, coercion arguments *do* have a runtime
-representation (albeit the zero-width VoidRep, see Note [Coercion tokens]
-in "GHC.CoreToStg"). This caused trouble in #17787 for DataCon wrappers for
-nullary GADT constructors: the wrappers would be inlined and each use of
-the constructor would lead to a separate allocation instead of just
-sharing the wrapper closure.
-
-The solution: don’t ignore coercion arguments after all.
 -}
 
 uncondInline :: Bool -> CoreExpr -> [Var] -> Arity -> CoreExpr -> Int -> Bool


=====================================
compiler/GHC/Core/Unfold/Make.hs
=====================================
@@ -97,7 +97,10 @@ mkDataConUnfolding expr
   where
     guide = UnfWhen { ug_arity     = manifestArity expr
                     , ug_unsat_ok  = unSaturatedOk
-                    , ug_boring_ok = False }
+                    , ug_boring_ok = inlineBoringOk expr }
+            -- inineBoringOk; sometimes wrappers are very simple, like
+            --    \@a p q. K @a <coercion> p q
+            -- and then we definitely want to inline it #25713
 
 mkWrapperUnfolding :: SimpleOpts -> CoreExpr -> Arity -> Unfolding
 -- Make the unfolding for the wrapper in a worker/wrapper split


=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -140,7 +140,7 @@ canDictCt ev cls tys
 
   | CtWanted { ctev_rewriters = rewriters } <- ev
   , Just ip_name <- isCallStackPred cls tys
-  , isPushCallStackOrigin orig
+  , Just fun_fs  <- isPushCallStackOrigin_maybe orig
   -- If we're given a CallStack constraint that arose from a function
   -- call, we need to push the current call-site onto the stack instead
   -- of solving it directly from a given.
@@ -159,8 +159,7 @@ canDictCt ev cls tys
 
          -- Then we solve the wanted by pushing the call-site
          -- onto the newly emitted CallStack
-       ; let ev_cs = EvCsPushCall (callStackOriginFS orig)
-                                  (ctLocSpan loc) (ctEvExpr new_ev)
+       ; let ev_cs = EvCsPushCall fun_fs (ctLocSpan loc) (ctEvExpr new_ev)
        ; solveCallStack ev ev_cs
 
        ; continueWith (DictCt { di_ev = new_ev, di_cls = cls


=====================================
compiler/GHC/Tc/Solver/Types.hs
=====================================
@@ -134,7 +134,7 @@ emptyDictMap = emptyTcAppMap
 findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
 findDict m loc cls tys
   | Just {} <- isCallStackPred cls tys
-  , isPushCallStackOrigin (ctLocOrigin loc)
+  , Just {} <- isPushCallStackOrigin_maybe (ctLocOrigin loc)
   = Nothing             -- See Note [Solving CallStack constraints]
 
   | otherwise
@@ -156,7 +156,7 @@ foldDicts = foldTcAppMap
 
 {- Note [Solving CallStack constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See also Note [Overview of implicit CallStacks] in GHc.Tc.Types.Evidence.
+See Note [Overview of implicit CallStacks] in GHc.Tc.Types.Evidence.
 
 Suppose f :: HasCallStack => blah.  Then
 


=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -655,7 +655,6 @@ Conclusion: a new wanted coercion variable should be made mutable.
 [Notice though that evidence variables that bind coercion terms
  from super classes will be "given" and hence rigid]
 
-
 Note [Overview of implicit CallStacks]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 (See https://gitlab.haskell.org/ghc/ghc/wikis/explicit-call-stack/implicit-locations)
@@ -667,12 +666,13 @@ to constraints of type GHC.Stack.Types.HasCallStack, an alias
 
   type HasCallStack = (?callStack :: CallStack)
 
-Implicit parameters of type GHC.Stack.Types.CallStack (the name is not
-important) are solved in three steps:
+Implicit parameters of type GHC.Stack.Types.CallStack (the /name/ of the
+implicit parameter is not important, see (CS5) below) are solved as follows:
 
-1. Explicit, user-written occurrences of `?stk :: CallStack`
-   which have IPOccOrigin, are solved directly from the given IP,
-   just like a regular IP; see GHC.Tc.Solver.Dict.tryInertDicts.
+1. Plan NORMAL. Explicit, user-written occurrences of `?stk :: CallStack`, which
+   have IPOccOrigin, are solved directly from the given IP, just like any other
+   implicit-parameter constraint; see GHC.Tc.Solver.Dict.tryInertDicts. We can
+   solve it from a Given or from another Wanted, if the two have the same type.
 
    For example, the occurrence of `?stk` in
 
@@ -681,44 +681,35 @@ important) are solved in three steps:
 
    will be solved for the `?stk` in `error`s context as before.
 
-2. In a function call, instead of simply passing the given IP, we first
-   append the current call-site to it. For example, consider a
-   call to the callstack-aware `error` above.
-
-     foo :: (?stk :: CallStack) => a
-     foo = error "undefined!"
-
-   Here we want to take the given `?stk` and append the current
-   call-site, before passing it to `error`. In essence, we want to
-   rewrite `foo "undefined!"` to
+2. Plan PUSH.  A /function call/ with a CallStack constraint, such as
+   a call to `foo` where
+        foo :: (?stk :: CallStack) => a
+   will give rise to a Wanted constraint
+        [W] d :: (?stk :: CallStack)    CtOrigin = OccurrenceOf "foo"
 
-     let ?stk = pushCallStack <foo's location> ?stk
-     in foo "undefined!"
+   We do /not/ solve this constraint from Givens, or from other
+   Wanteds.  Rather, have a built-in mechanism in that solves it thus:
+        d := EvCsPushCall "foo" <details of call-site of `foo`> d2
+        [W] d2 :: (?stk :: CallStack)    CtOrigin = IPOccOrigin
 
-   We achieve this as follows:
+   That is, `d` is a call-stack that has the `foo` call-site pushed on top of
+   `d2`, which can now be solved normally (as in (1) above).  This is done in two
+   places:
+     - In GHC.Tc.Solver.Dict.canDictNC we do the pushing.
+     - In GHC.Tc.Solver.Types.findDict we arrrange /not/ to solve a plan-PUSH
+       constraint by forcing a "miss" in the lookup in the inert set
 
-   * At a call of foo :: (?stk :: CallStack) => blah
-     we emit a Wanted
-        [W] d1 : IP "stk" CallStack
-     with CtOrigin = OccurrenceOf "foo"
+3. For a CallStack constraint, we choose how to solve it based on its CtOrigin:
 
-   * We /solve/ this constraint, in GHC.Tc.Solver.Dict.canDictNC
-     by emitting a NEW Wanted
-        [W] d2 :: IP "stk" CallStack
-     with CtOrigin = IPOccOrigin
+     * solve it normally (plan NORMAL above)
+         - IPOccOrigin (discussed above)
+         - GivenOrigin (see (CS1) below)
 
-     and solve d1 = EvCsPushCall "foo" <foo's location> (EvId d1)
+     * push an item on the stack and emit a new constraint (plan PUSH above)
+         - OccurrenceOf "foo" (discused above)
+         - anything else      (see (CS1) below)
 
-   * The new Wanted, for `d2` will be solved per rule (1), ie as a regular IP.
-
-3. We use the predicate isPushCallStackOrigin to identify whether we
-   want to do (1) solve directly, or (2) push and then solve directly.
-   Key point (see #19918): the CtOrigin where we want to push an item on the
-   call stack can include IfThenElseOrigin etc, when RebindableSyntax is
-   involved.  See the defn of fun_orig in GHC.Tc.Gen.App.tcInstFun; it is
-   this CtOrigin that is pinned on the constraints generated by functions
-   in the "expansion" for rebindable syntax. c.f. GHC.Rename.Expr
-   Note [Handling overloaded and rebindable constructs]
+   This choice is by the predicate isPushCallStackOrigin_maybe
 
 4. We default any insoluble CallStacks to the empty CallStack. Suppose
    `undefined` did not request a CallStack, ie
@@ -754,21 +745,38 @@ and the call to `error` in `undefined`, but *not* the call to `head`
 in `g`, because `head` did not explicitly request a CallStack.
 
 
-Important Details:
-- GHC should NEVER report an insoluble CallStack constraint.
+Wrinkles
+
+(CS1) Which CtOrigins should qualify for plan PUSH?  Certainly ones that arise
+   from a function call like (f a b).
 
-- GHC should NEVER infer a CallStack constraint unless one was requested
+   But (see #19918) when RebindableSyntax is involved we can function call whose
+   CtOrigin is somethign like `IfThenElseOrigin`. See the defn of fun_orig in
+   GHC.Tc.Gen.App.tcInstFun; it is this CtOrigin that is pinned on the
+   constraints generated by functions in the "expansion" for rebindable
+   syntax. c.f. GHC.Rename.Expr Note [Handling overloaded and rebindable
+   constructs].
+
+   So isPushCallStackOrigin_maybe has a fall-through for "anything else", and
+   assumes that we should adopt plan PUSH for it.
+
+   However we should /not/ take this fall-through for Given constraints
+   (#25675).  So isPushCallStackOrigin_maybe identifies Givens as plan NORMAL.
+
+(CS2) GHC should NEVER report an insoluble CallStack constraint.
+
+(CS3) GHC should NEVER infer a CallStack constraint unless one was requested
   with a partial type signature (See GHC.Tc.Solver..pickQuantifiablePreds).
 
-- A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
+(CS4)- A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
   where the String is the name of the binder that is used at the
   SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the
   package/module/file name, as well as the full source-span. Both
   CallStack and SrcLoc are kept abstract so only GHC can construct new
   values.
 
-- We will automatically solve any wanted CallStack regardless of the
-  name of the IP, i.e.
+(CS5) We will automatically solve any wanted CallStack regardless of the
+  /name/ of the IP, i.e.
 
     f = show (?stk :: CallStack)
     g = show (?loc :: CallStack)
@@ -782,17 +790,16 @@ Important Details:
   the printed CallStack will NOT include head's call-site. This reflects the
   standard scoping rules of implicit-parameters.
 
-- An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
+(CS6) An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
   The desugarer will need to unwrap the IP newtype before pushing a new
   call-site onto a given stack (See GHC.HsToCore.Binds.dsEvCallStack)
 
-- When we emit a new wanted CallStack from rule (2) we set its origin to
+(CS7) When we emit a new wanted CallStack in plan PUSH we set its origin to
   `IPOccOrigin ip_name` instead of the original `OccurrenceOf func`
   (see GHC.Tc.Solver.Dict.tryInertDicts).
 
   This is a bit shady, but is how we ensure that the new wanted is
   solved like a regular IP.
-
 -}
 
 mkEvCast :: EvExpr -> TcCoercion -> EvTerm


=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -27,7 +27,7 @@ module GHC.Tc.Types.Origin (
   TypedThing(..), TyVarBndrs(..),
 
   -- * CallStack
-  isPushCallStackOrigin, callStackOriginFS,
+  isPushCallStackOrigin_maybe,
 
   -- * FixedRuntimeRep origin
   FixedRuntimeRepOrigin(..),
@@ -984,18 +984,22 @@ pprNonLinearPatternReason OtherPatternReason = empty
 *                                                                      *
 ********************************************************************* -}
 
-isPushCallStackOrigin :: CtOrigin -> Bool
--- Do we want to solve this IP constraint directly (return False)
--- or push the call site (return True)
--- See Note [Overview of implicit CallStacks] in GHc.Tc.Types.Evidence
-isPushCallStackOrigin (IPOccOrigin {}) = False
-isPushCallStackOrigin _                = True
-
-
-callStackOriginFS :: CtOrigin -> FastString
--- This is the string that appears in the CallStack
-callStackOriginFS (OccurrenceOf fun) = occNameFS (getOccName fun)
-callStackOriginFS orig               = mkFastString (showSDocUnsafe (pprCtO orig))
+isPushCallStackOrigin_maybe :: CtOrigin -> Maybe FastString
+-- Do we want to solve this IP constraint normally (return Nothing)
+-- or push the call site (returning the name of the function being called)
+-- See Note [Overview of implicit CallStacks] esp (CS1) in GHC.Tc.Types.Evidence
+isPushCallStackOrigin_maybe (GivenOrigin {})   = Nothing
+isPushCallStackOrigin_maybe (GivenSCOrigin {}) = Nothing
+isPushCallStackOrigin_maybe (IPOccOrigin {})   = Nothing
+isPushCallStackOrigin_maybe (OccurrenceOf fun) = Just (occNameFS (getOccName fun))
+isPushCallStackOrigin_maybe orig               = Just orig_fs
+  -- This fall-through case is important to deal with call stacks
+  --      that arise from rebindable syntax (#19919)
+  -- Here the "name of the function being called" is approximated as
+  --      the result of prettty-printing the CtOrigin; a bit messy,
+  --      but we can perhaps improve it in the light of user feedback
+  where
+    orig_fs = mkFastString (showSDocUnsafe (pprCtO orig))
 
 {-
 ************************************************************************


=====================================
hadrian/src/Hadrian/Utilities.hs
=====================================
@@ -149,7 +149,10 @@ as /c/foo, while it occasionally falls over on paths of the form C:\foo.
 --
 -- See Note [Absolute paths and MSYS].
 (-/-) :: FilePath -> FilePath -> FilePath
-_  -/- b | isAbsolute b && not (isAbsolute $ tail b) = b
+_  -/- b
+    | isAbsolute b
+    , _:b' <- b
+    , not (isAbsolute b') = b
 "" -/- b = b
 a  -/- b
     | last a == '/' = a ++       b
@@ -636,7 +639,8 @@ renderLibrary name lib synopsis = renderBox $
 -- | ipsum    |
 -- \----------/
 renderBox :: [String] -> String
-renderBox ls = tail $ concatMap ('\n' :) (boxTop : map renderLine ls ++ [boxBot])
+renderBox ls =
+    drop 1 $ concatMap ('\n' :) (boxTop : map renderLine ls ++ [boxBot])
   where
     -- Minimum total width of the box in characters
     minimumBoxWidth = 32


=====================================
hadrian/src/Oracles/ModuleFiles.hs
=====================================
@@ -169,10 +169,12 @@ moduleFilesOracle = void $ do
 
         let pairs = sort $ mainpairs ++ [ (encodeModule d f, f) | (fs, d) <- result, f <- fs ]
             multi = [ (m, f1, f2) | (m, f1):(n, f2):_ <- tails pairs, m == n ]
-        unless (null multi) $ do
-            let (m, f1, f2) = head multi
-            error $ "Module " ++ m ++ " has more than one source file: "
-                ++ f1 ++ " and " ++ f2 ++ "."
+
+        case multi of
+            [] -> return ()
+            (m, f1, f2) : _ ->
+              fail $ "Module " ++ m ++ " has more than one source file: "
+                  ++ f1 ++ " and " ++ f2 ++ "."
         return $ lookupAll modules pairs
 
     -- Optimisation: we discard Haskell files here, because they are never used


=====================================
hadrian/src/Rules/Dependencies.hs
=====================================
@@ -1,4 +1,5 @@
 {-# OPTIONS_GHC -Wno-deprecations #-}
+{-# OPTIONS_GHC -Wno-x-data-list-nonempty-unzip #-}
 
 module Rules.Dependencies (buildPackageDependencies) where
 


=====================================
hadrian/src/Settings/Parser.hs
=====================================
@@ -184,14 +184,11 @@ instance Match SettingsM where
 matchStringSettingsM :: String -> SettingsM ()
 matchStringSettingsM s = do
   ks <- State.get
-  if null ks
-    then throwError $ "expected " ++ show s ++ ", got nothing"
-    else go (head ks)
-
-  where go k
-          | k == s = State.modify tail
-          | otherwise = throwError $
-              "expected " ++ show s ++ ", got " ++ show k
+  case ks of
+    []            -> throwError $ "expected " ++ show s ++ ", got nothing"
+    k:_
+      | k == s    -> State.modify (drop 1)
+      | otherwise -> throwError $ "expected " ++ show s ++ ", got " ++ show k
 
 matchOneOfSettingsM :: [SettingsM a] -> SettingsM a
 matchOneOfSettingsM acts = StateT $ \k -> do


=====================================
testsuite/tests/ghci.debugger/scripts/break011.stdout
=====================================
@@ -29,9 +29,9 @@ HasCallStack backtrace:
   error, called at Test7.hs:2:18 in main:Main
 
 Stopped in <exception thrown>, <unknown>
-_exception :: e = _
+_exception :: e = SomeException (ErrorCall "foo")
 Stopped in <exception thrown>, <unknown>
-_exception :: e = _
+_exception :: e = SomeException (ErrorCall "foo")
 *** Exception: foo
 
 HasCallStack backtrace:


=====================================
testsuite/tests/ghci.debugger/scripts/break024.stdout
=====================================
@@ -17,7 +17,9 @@ _exception = SomeException
                   Nothing GHC.Internal.IO.Exception.UserError [] "error" Nothing
                   Nothing)
 Stopped in <exception thrown>, <unknown>
-_exception :: e = _
+_exception :: e = SomeException
+                    (GHC.Internal.IO.Exception.IOError
+                       Nothing GHC.Internal.IO.Exception.UserError ....)
 Stopped in <exception thrown>, <unknown>
 _exception :: e = _
 _exception = SomeException


=====================================
testsuite/tests/profiling/should_run/T25675.hs
=====================================
@@ -0,0 +1,21 @@
+{-# LANGUAGE ImplicitParams #-}
+
+module Main where
+
+import Data.Maybe
+import Debug.Trace
+import GHC.IsList
+import GHC.Stack
+
+hd (c:cs) = c
+hd [] = error "urk"
+
+what :: (HasCallStack) => Int
+what =
+  let cs = getCallStack callStack
+   in srcLocStartCol (snd (hd cs))
+
+main :: IO ()
+main =
+  let ?callStack = fromList []
+   in print (what, what)


=====================================
testsuite/tests/profiling/should_run/T25675.stdout
=====================================
@@ -0,0 +1 @@
+(14,20)


=====================================
testsuite/tests/profiling/should_run/all.T
=====================================
@@ -232,3 +232,5 @@ test('scc-prof-overloaded-calls002',
      # Need optimizations to get rid of unwanted overloaded calls
      ['-O -fno-prof-auto -fprof-late-overloaded-calls']
 )
+
+test('T25675', [], compile_and_run, ['-dcore-lint'])


=====================================
testsuite/tests/simplCore/should_compile/T22375DataFamily.stderr
=====================================
@@ -8,7 +8,7 @@ T22375DataFamily.$WA [InlPrag=INLINE[final] CONLIKE] :: X ()
 [GblId[DataConWrapper],
  Unf=Unf{Src=StableSystem, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 T22375DataFamily.$WA
   = T22375DataFamily.A
     `cast` (Sym T22375DataFamily.D:R:XUnit0
@@ -19,7 +19,7 @@ T22375DataFamily.$WB [InlPrag=INLINE[final] CONLIKE] :: X ()
 [GblId[DataConWrapper],
  Unf=Unf{Src=StableSystem, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 T22375DataFamily.$WB
   = T22375DataFamily.B
     `cast` (Sym T22375DataFamily.D:R:XUnit0
@@ -30,7 +30,7 @@ T22375DataFamily.$WC [InlPrag=INLINE[final] CONLIKE] :: X ()
 [GblId[DataConWrapper],
  Unf=Unf{Src=StableSystem, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 T22375DataFamily.$WC
   = T22375DataFamily.C
     `cast` (Sym T22375DataFamily.D:R:XUnit0
@@ -41,7 +41,7 @@ T22375DataFamily.$WD [InlPrag=INLINE[final] CONLIKE] :: X ()
 [GblId[DataConWrapper],
  Unf=Unf{Src=StableSystem, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 T22375DataFamily.$WD
   = T22375DataFamily.D
     `cast` (Sym T22375DataFamily.D:R:XUnit0
@@ -52,7 +52,7 @@ T22375DataFamily.$WE [InlPrag=INLINE[final] CONLIKE] :: X ()
 [GblId[DataConWrapper],
  Unf=Unf{Src=StableSystem, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 T22375DataFamily.$WE
   = T22375DataFamily.E
     `cast` (Sym T22375DataFamily.D:R:XUnit0
@@ -63,7 +63,7 @@ T22375DataFamily.$WF [InlPrag=INLINE[final] CONLIKE] :: X ()
 [GblId[DataConWrapper],
  Unf=Unf{Src=StableSystem, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 T22375DataFamily.$WF
   = T22375DataFamily.F
     `cast` (Sym T22375DataFamily.D:R:XUnit0
@@ -74,7 +74,7 @@ T22375DataFamily.$WG [InlPrag=INLINE[final] CONLIKE] :: X ()
 [GblId[DataConWrapper],
  Unf=Unf{Src=StableSystem, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 T22375DataFamily.$WG
   = T22375DataFamily.G
     `cast` (Sym T22375DataFamily.D:R:XUnit0
@@ -85,7 +85,7 @@ T22375DataFamily.$WH [InlPrag=INLINE[final] CONLIKE] :: X ()
 [GblId[DataConWrapper],
  Unf=Unf{Src=StableSystem, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 T22375DataFamily.$WH
   = T22375DataFamily.H
     `cast` (Sym T22375DataFamily.D:R:XUnit0
@@ -96,7 +96,7 @@ T22375DataFamily.$WI [InlPrag=INLINE[final] CONLIKE] :: X ()
 [GblId[DataConWrapper],
  Unf=Unf{Src=StableSystem, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 T22375DataFamily.$WI
   = T22375DataFamily.I
     `cast` (Sym T22375DataFamily.D:R:XUnit0
@@ -107,7 +107,7 @@ T22375DataFamily.$WJ [InlPrag=INLINE[final] CONLIKE] :: X ()
 [GblId[DataConWrapper],
  Unf=Unf{Src=StableSystem, TopLvl=True,
          Value=True, ConLike=True, WorkFree=True, Expandable=True,
-         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)}]
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 T22375DataFamily.$WJ
   = T22375DataFamily.J
     `cast` (Sym T22375DataFamily.D:R:XUnit0


=====================================
testsuite/tests/simplCore/should_compile/T25713.hs
=====================================
@@ -0,0 +1,49 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving  #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE TypeApplications    #-}
+
+module Ifoldl (module Ifoldl) where
+
+import Data.Kind (Type)
+import Data.Type.Equality
+import Prelude hiding (reverse)
+
+data Nat = Z | S Nat
+
+data Vec n a where
+    Nil  :: Vec 'Z a
+    (:::) :: a -> Vec n a -> Vec ('S n) a
+
+infixr 5 :::
+
+deriving instance Show a => Show (Vec n a)
+
+type family a + b where
+  Z + b = b
+  S a + b = S (a + b)
+
+newtype Wonk k w = Wonk (S k + S w :~: S (S k) + w)
+
+upWonk :: Wonk k w -> Wonk (S k) w
+upWonk (Wonk Refl) = Wonk Refl
+
+ifoldlRec :: forall b n a. (forall m. b m -> a -> b ('S m)) -> b 'Z -> Vec n a -> b n
+ifoldlRec f = go Refl Refl (Wonk Refl)
+  where
+    go :: forall k m. k + Z :~: k -> k + m :~: n -> (forall w. Wonk k w) -> b k -> Vec m a -> b n
+    go Refl Refl (Wonk Refl) bk Nil = bk
+    go Refl Refl !pf bk (a ::: (as :: Vec pm a)) = go @(S k) Refl
+      (case pf :: Wonk k pm of Wonk Refl -> Refl) (upWonk pf) (f bk a) as
+{-# INLINE ifoldlRec #-}
+
+newtype Flip f y x = Flip
+    { unFlip :: f x y
+    }
+
+reverseVec :: Vec n a -> Vec n a
+reverseVec = unFlip . ifoldlRec (\(Flip xs) x -> Flip $ x ::: xs) (Flip Nil)


=====================================
testsuite/tests/simplCore/should_compile/T25713.stderr
=====================================
@@ -0,0 +1,1267 @@
+
+==================== Tidy Core ====================
+Result size of Tidy Core
+  = {terms: 480, types: 774, coercions: 434, joins: 1/1}
+
+-- RHS size: {terms: 2, types: 3, coercions: 1, joins: 0/0}
+Ifoldl.$WNil [InlPrag=INLINE[final] CONLIKE] :: forall a. Vec Z a
+[GblId[DataConWrapper],
+ Unf=Unf{Src=StableSystem, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=False)
+         Tmpl= \ (@a_akj) ->
+                 Ifoldl.Nil @Z @a_akj @~(<Z>_N :: Z GHC.Internal.Prim.~# Z)}]
+Ifoldl.$WNil
+  = \ (@a_akj) ->
+      Ifoldl.Nil @Z @a_akj @~(<Z>_N :: Z GHC.Internal.Prim.~# Z)
+
+-- RHS size: {terms: 7, types: 10, coercions: 2, joins: 0/0}
+Ifoldl.$W::: [InlPrag=INLINE[final] CONLIKE]
+  :: forall a (n :: Nat). a %1 -> Vec n a %1 -> Vec (S n) a
+[GblId[DataConWrapper],
+ Arity=2,
+ Str=<L><L>,
+ Unf=Unf{Src=StableSystem, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=True)
+         Tmpl= \ (@a_akk)
+                 (@(n_X0 :: Nat))
+                 (conrep_aHU [Occ=Once1] :: a_akk)
+                 (conrep1_aHV [Occ=Once1] :: Vec n_X0 a_akk) ->
+                 Ifoldl.:::
+                   @(S n_X0)
+                   @a_akk
+                   @n_X0
+                   @~(<S n_X0>_N :: S n_X0 GHC.Internal.Prim.~# S n_X0)
+                   conrep_aHU
+                   conrep1_aHV}]
+Ifoldl.$W:::
+  = \ (@a_akk)
+      (@(n_X0 :: Nat))
+      (conrep_aHU [Occ=Once1] :: a_akk)
+      (conrep1_aHV [Occ=Once1] :: Vec n_X0 a_akk) ->
+      Ifoldl.:::
+        @(S n_X0)
+        @a_akk
+        @n_X0
+        @~(<S n_X0>_N :: S n_X0 GHC.Internal.Prim.~# S n_X0)
+        conrep_aHU
+        conrep1_aHV
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+lvl_r1n5 :: Int
+[GblId, Unf=OtherCon []]
+lvl_r1n5 = GHC.Internal.Types.I# 6#
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+lvl1_r1n6 :: GHC.Internal.Prim.Addr#
+[GblId, Unf=OtherCon []]
+lvl1_r1n6 = "Nil"#
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+lvl2_r1n7 :: GHC.Internal.Prim.Addr#
+[GblId, Unf=OtherCon []]
+lvl2_r1n7 = " ::: "#
+
+Rec {
+-- RHS size: {terms: 48, types: 39, coercions: 0, joins: 0/0}
+Ifoldl.$fShowVec_$cshowsPrec [Occ=LoopBreaker]
+  :: forall a (n :: Nat). Show a => Int -> Vec n a -> ShowS
+[GblId,
+ Arity=4,
+ Str=<LP(SC(S,C(1,C(1,L))),A,A)><ML><1L><L>,
+ Unf=OtherCon []]
+Ifoldl.$fShowVec_$cshowsPrec
+  = \ (@a_a11n)
+      (@(n_a11o :: Nat))
+      ($dShow_a11p :: Show a_a11n)
+      (ds_d1gq :: Int)
+      (ds1_d1gr :: Vec n_a11o a_a11n)
+      (eta_B0 :: String) ->
+      case ds1_d1gr of {
+        Nil co_a11w [Dmd=B] ->
+          GHC.Internal.CString.unpackAppendCString# lvl1_r1n6 eta_B0;
+        ::: @n1_a11A co_a11B [Dmd=B] b1_aJu b2_aJv ->
+          case ds_d1gq of { GHC.Internal.Types.I# x_a1kQ ->
+          case GHC.Internal.Prim.>=# x_a1kQ 6# of {
+            __DEFAULT ->
+              showsPrec
+                @a_a11n
+                $dShow_a11p
+                lvl_r1n5
+                b1_aJu
+                (GHC.Internal.CString.unpackAppendCString#
+                   lvl2_r1n7
+                   (Ifoldl.$fShowVec_$cshowsPrec
+                      @a_a11n @n1_a11A $dShow_a11p lvl_r1n5 b2_aJv eta_B0));
+            1# ->
+              GHC.Internal.Types.:
+                @Char
+                GHC.Internal.Show.$fShowCallStack3
+                (showsPrec
+                   @a_a11n
+                   $dShow_a11p
+                   lvl_r1n5
+                   b1_aJu
+                   (GHC.Internal.CString.unpackAppendCString#
+                      lvl2_r1n7
+                      (Ifoldl.$fShowVec_$cshowsPrec
+                         @a_a11n
+                         @n1_a11A
+                         $dShow_a11p
+                         lvl_r1n5
+                         b2_aJv
+                         (GHC.Internal.Types.:
+                            @Char GHC.Internal.Show.$fShowCallStack2 eta_B0))))
+          }
+          }
+      }
+end Rec }
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$fShowVec1 :: Int
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$fShowVec1 = GHC.Internal.Types.I# 0#
+
+-- RHS size: {terms: 11, types: 14, coercions: 0, joins: 0/0}
+Ifoldl.$fShowVec_$cshowList
+  :: forall a (n :: Nat). Show a => [Vec n a] -> ShowS
+[GblId,
+ Arity=3,
+ Str=<LP(SC(S,C(1,C(1,L))),A,A)><1L><L>,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [0 0 0] 70 0}]
+Ifoldl.$fShowVec_$cshowList
+  = \ (@a_a11n)
+      (@(n_a11o :: Nat))
+      ($dShow_a11p :: Show a_a11n)
+      (ls_a1hi :: [Vec n_a11o a_a11n])
+      (s_a1hj :: String) ->
+      GHC.Internal.Show.showList__
+        @(Vec n_a11o a_a11n)
+        (Ifoldl.$fShowVec_$cshowsPrec
+           @a_a11n @n_a11o $dShow_a11p Ifoldl.$fShowVec1)
+        ls_a1hi
+        s_a1hj
+
+-- RHS size: {terms: 9, types: 10, coercions: 0, joins: 0/0}
+Ifoldl.$fShowVec_$cshow
+  :: forall a (n :: Nat). Show a => Vec n a -> String
+[GblId,
+ Arity=2,
+ Str=<LP(SC(S,C(1,C(1,L))),A,A)><1L>,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [0 0] 50 0}]
+Ifoldl.$fShowVec_$cshow
+  = \ (@a_a11n)
+      (@(n_a11o :: Nat))
+      ($dShow_a11p :: Show a_a11n)
+      (x_a1hf :: Vec n_a11o a_a11n) ->
+      Ifoldl.$fShowVec_$cshowsPrec
+        @a_a11n
+        @n_a11o
+        $dShow_a11p
+        Ifoldl.$fShowVec1
+        x_a1hf
+        (GHC.Internal.Types.[] @Char)
+
+-- RHS size: {terms: 10, types: 13, coercions: 0, joins: 0/0}
+Ifoldl.$fShowVec [InlPrag=CONLIKE]
+  :: forall a (n :: Nat). Show a => Show (Vec n a)
+[GblId[DFunId],
+ Arity=1,
+ Str=<LP(LC(L,C(1,C(1,L))),A,A)>,
+ Unf=DFun: \ (@a_aAd) (@(n_aAe :: Nat)) (v_B1 :: Show a_aAd) ->
+       GHC.Internal.Show.C:Show TYPE: Vec n_aAe a_aAd
+                                Ifoldl.$fShowVec_$cshowsPrec @a_aAd @n_aAe v_B1
+                                Ifoldl.$fShowVec_$cshow @a_aAd @n_aAe v_B1
+                                Ifoldl.$fShowVec_$cshowList @a_aAd @n_aAe v_B1]
+Ifoldl.$fShowVec
+  = \ (@a_a11n) (@(n_a11o :: Nat)) ($dShow_a11p :: Show a_a11n) ->
+      GHC.Internal.Show.C:Show
+        @(Vec n_a11o a_a11n)
+        (Ifoldl.$fShowVec_$cshowsPrec @a_a11n @n_a11o $dShow_a11p)
+        (Ifoldl.$fShowVec_$cshow @a_a11n @n_a11o $dShow_a11p)
+        (Ifoldl.$fShowVec_$cshowList @a_a11n @n_a11o $dShow_a11p)
+
+-- RHS size: {terms: 7, types: 13, coercions: 0, joins: 0/0}
+Ifoldl.unFlip1
+  :: forall k1 k2 (f :: k1 -> k2 -> *) (y :: k2) (x :: k1).
+     Flip f y x -> Flip f y x
+[GblId,
+ Arity=1,
+ Str=<1L>,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
+Ifoldl.unFlip1
+  = \ (@k_aJb)
+      (@k1_aJc)
+      (@(f_aJd :: k_aJb -> k1_aJc -> *))
+      (@(y_aJe :: k1_aJc))
+      (@(x_aJf :: k_aJb))
+      (ds_d1go :: Flip f_aJd y_aJe x_aJf) ->
+      ds_d1go
+
+-- RHS size: {terms: 1, types: 0, coercions: 26, joins: 0/0}
+unFlip
+  :: forall {k1} {k2} (f :: k1 -> k2 -> *) (y :: k2) (x :: k1).
+     Flip f y x -> f x y
+[GblId[[RecSel]],
+ Arity=1,
+ Str=<1L>,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
+unFlip
+  = Ifoldl.unFlip1
+    `cast` (forall (k :: <*>_N) (k1 :: <*>_N) (f :: <k
+                                                     -> k1 -> *>_N) (y :: <k1>_N) (x :: <k>_N).
+            <Flip f y x>_R
+            %<Many>_N ->_R Ifoldl.N:Flip <k>_N <k1>_N <f>_R <y>_N <x>_N
+            :: (forall k k1 (f :: k -> k1 -> *) (y :: k1) (x :: k).
+                Flip f y x -> Flip f y x)
+               ~R# (forall k k1 (f :: k -> k1 -> *) (y :: k1) (x :: k).
+                    Flip f y x -> f x y))
+
+-- RHS size: {terms: 7, types: 37, coercions: 63, joins: 0/0}
+upWonk :: forall (k :: Nat) (w :: Nat). Wonk k w -> Wonk (S k) w
+[GblId,
+ Arity=1,
+ Str=<1!P(L)>,
+ Cpr=1,
+ Unf=Unf{Src=StableSystem, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)
+         Tmpl= \ (@(k_aXP :: Nat))
+                 (@(w_aXQ :: Nat))
+                 (ds_d1f6 [Occ=Once1!] :: Wonk k_aXP w_aXQ) ->
+                 case ds_d1f6
+                      `cast` (Ifoldl.N:Wonk <k_aXP>_N <w_aXQ>_N
+                              :: Wonk k_aXP w_aXQ
+                                 ~R# ((S k_aXP + S w_aXQ) :~: (S (S k_aXP) + w_aXQ)))
+                 of
+                 { Refl co_aXU ->
+                 (GHC.Internal.Data.Type.Equality.$WRefl
+                    @Nat @(S (S (S (k_aXP + w_aXQ)))))
+                 `cast` (((:~:)
+                            <Nat>_N
+                            ((S ((S (Sym (Ifoldl.D:R:+[1] <k_aXP>_N <w_aXQ>_N)
+                                     ; SelCo:Tc(0,N)
+                                           (Sym (Ifoldl.D:R:+[1] <S k_aXP>_N <w_aXQ>_N)
+                                            ; co_aXU
+                                            ; Ifoldl.D:R:+[1] <k_aXP>_N <S w_aXQ>_N)))_N
+                                 ; Sym (Ifoldl.D:R:+[1] <k_aXP>_N <S w_aXQ>_N)))_N
+                             ; Sym (Ifoldl.D:R:+[1] <S k_aXP>_N <S w_aXQ>_N))
+                            ((S ((S (Sym (Ifoldl.D:R:+[1] <k_aXP>_N <w_aXQ>_N)))_N
+                                 ; Sym (Ifoldl.D:R:+[1] <S k_aXP>_N <w_aXQ>_N)))_N
+                             ; Sym (Ifoldl.D:R:+[1] <S (S k_aXP)>_N <w_aXQ>_N)))_R
+                         ; Sym (Ifoldl.N:Wonk <S k_aXP>_N <w_aXQ>_N)
+                         :: (S (S (S (k_aXP + w_aXQ))) :~: S (S (S (k_aXP + w_aXQ))))
+                            ~R# Wonk (S k_aXP) w_aXQ)
+                 }}]
+upWonk
+  = \ (@(k_aXP :: Nat))
+      (@(w_aXQ :: Nat))
+      (ds_d1f6 :: Wonk k_aXP w_aXQ) ->
+      case ds_d1f6
+           `cast` (Ifoldl.N:Wonk <k_aXP>_N <w_aXQ>_N
+                   :: Wonk k_aXP w_aXQ
+                      ~R# ((S k_aXP + S w_aXQ) :~: (S (S k_aXP) + w_aXQ)))
+      of
+      { Refl co_aXU ->
+      (GHC.Internal.Data.Type.Equality.$WRefl
+         @Nat @(S (S (S (k_aXP + w_aXQ)))))
+      `cast` (((:~:)
+                 <Nat>_N
+                 ((S ((S (Sym (Ifoldl.D:R:+[1] <k_aXP>_N <w_aXQ>_N)
+                          ; SelCo:Tc(0,N)
+                                (Sym (Ifoldl.D:R:+[1] <S k_aXP>_N <w_aXQ>_N)
+                                 ; co_aXU
+                                 ; Ifoldl.D:R:+[1] <k_aXP>_N <S w_aXQ>_N)))_N
+                      ; Sym (Ifoldl.D:R:+[1] <k_aXP>_N <S w_aXQ>_N)))_N
+                  ; Sym (Ifoldl.D:R:+[1] <S k_aXP>_N <S w_aXQ>_N))
+                 ((S ((S (Sym (Ifoldl.D:R:+[1] <k_aXP>_N <w_aXQ>_N)))_N
+                      ; Sym (Ifoldl.D:R:+[1] <S k_aXP>_N <w_aXQ>_N)))_N
+                  ; Sym (Ifoldl.D:R:+[1] <S (S k_aXP)>_N <w_aXQ>_N)))_R
+              ; Sym (Ifoldl.N:Wonk <S k_aXP>_N <w_aXQ>_N)
+              :: (S (S (S (k_aXP + w_aXQ))) :~: S (S (S (k_aXP + w_aXQ))))
+                 ~R# Wonk (S k_aXP) w_aXQ)
+      }
+
+-- RHS size: {terms: 43, types: 198, coercions: 150, joins: 1/1}
+ifoldlRec [InlPrag=INLINE (sat-args=1)]
+  :: forall (b :: Nat -> *) (n :: Nat) a.
+     (forall (m :: Nat). b m -> a -> b (S m)) -> b Z -> Vec n a -> b n
+[GblId,
+ Arity=3,
+ Str=<LC(S,C(1,L))><L><1L>,
+ Unf=Unf{Src=StableUser, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=1,unsat_ok=False,boring_ok=False)
+         Tmpl= \ (@(b_aY8 :: Nat -> *))
+                 (@(n_aY9 :: Nat))
+                 (@a_aYa)
+                 (f_azT [Occ=OnceL1!]
+                    :: forall (m :: Nat). b_aY8 m -> a_aYa -> b_aY8 (S m))
+                 (eta_B0 [Occ=Once1] :: b_aY8 Z)
+                 (eta1_B1 [Occ=Once1] :: Vec n_aY9 a_aYa) ->
+                 joinrec {
+                   go_azU [Occ=LoopBreakerT[7]]
+                     :: forall (k :: Nat) (m :: Nat).
+                        ((k + Z) :~: k)
+                        -> ((k + m) :~: n_aY9)
+                        -> (forall (w :: Nat). Wonk k w)
+                        -> b_aY8 k
+                        -> Vec m a_aYa
+                        -> b_aY8 n_aY9
+                   [LclId[JoinId(7)(Nothing)],
+                    Arity=5,
+                    Str=<L><L><L><L><L>,
+                    Unf=OtherCon []]
+                   go_azU (@(k_aYT :: Nat))
+                          (@(m_aYU :: Nat))
+                          (ds_d1fg [Occ=Once1!] :: (k_aYT + Z) :~: k_aYT)
+                          (ds1_d1fh [Occ=Once1!] :: (k_aYT + m_aYU) :~: n_aY9)
+                          (ds2_d1fi :: forall (w :: Nat). Wonk k_aYT w)
+                          (bk_azY [Occ=Once2] :: b_aY8 k_aYT)
+                          (ds3_d1fj [Occ=Once1!] :: Vec m_aYU a_aYa)
+                     = case ds_d1fg of { Refl co_aYX ->
+                       case ds1_d1fh of { Refl co1_aYZ ->
+                       case (ds2_d1fi @(GHC.Internal.Types.ZonkAny 0))
+                            `cast` (Ifoldl.N:Wonk <k_aYT>_N <GHC.Internal.Types.ZonkAny 0>_N
+                                    :: Wonk k_aYT (GHC.Internal.Types.ZonkAny 0)
+                                       ~R# ((S k_aYT + S (GHC.Internal.Types.ZonkAny 0))
+                                            :~: (S (S k_aYT) + GHC.Internal.Types.ZonkAny 0)))
+                       of
+                       { Refl _ [Occ=Dead] ->
+                       case ds3_d1fj of {
+                         Nil co3_aZ5 ->
+                           bk_azY
+                           `cast` (<b_aY8>_R (co_aYX
+                                              ; (<k_aYT>_N + Sym co3_aZ5)_N
+                                              ; Sym co1_aYZ)
+                                   :: b_aY8 k_aYT ~R# b_aY8 n_aY9);
+                         ::: @ipv_s1jk ipv1_s1jl ipv2_s1jm [Occ=Once1]
+                             ipv3_s1jn [Occ=Once1] ->
+                           case ds2_d1fi of ds4_X5 { __DEFAULT ->
+                           jump go_azU
+                             @(S k_aYT)
+                             @ipv_s1jk
+                             ((GHC.Internal.Data.Type.Equality.$WRefl @Nat @(S k_aYT))
+                              `cast` (((:~:)
+                                         <Nat>_N
+                                         ((S co_aYX)_N
+                                          ; Sym (Ifoldl.D:R:+[1] <k_aYT>_N <Z>_N))
+                                         <S k_aYT>_N)_R
+                                      :: (S k_aYT :~: S k_aYT) ~R# ((S k_aYT + Z) :~: S k_aYT)))
+                             (case (ds4_X5 @ipv_s1jk)
+                                   `cast` (Ifoldl.N:Wonk <k_aYT>_N <ipv_s1jk>_N
+                                           :: Wonk k_aYT ipv_s1jk
+                                              ~R# ((S k_aYT + S ipv_s1jk)
+                                                   :~: (S (S k_aYT) + ipv_s1jk)))
+                              of
+                              { Refl co3_aZJ ->
+                              (GHC.Internal.Data.Type.Equality.$WRefl @Nat @n_aY9)
+                              `cast` (((:~:)
+                                         <Nat>_N
+                                         (co1_aYZ
+                                          ; (<k_aYT>_N + ipv1_s1jl)_N
+                                          ; SelCo:Tc(0,N)
+                                                (Sym (Ifoldl.D:R:+[1] <k_aYT>_N <S ipv_s1jk>_N)
+                                                 ; Sym co3_aZJ
+                                                 ; Ifoldl.D:R:+[1] <S k_aYT>_N <ipv_s1jk>_N))
+                                         <n_aY9>_N)_R
+                                      :: (n_aY9 :~: n_aY9) ~R# ((S k_aYT + ipv_s1jk) :~: n_aY9))
+                              })
+                             (\ (@(w_aZP :: Nat)) ->
+                                case (ds4_X5 @w_aZP)
+                                     `cast` (Ifoldl.N:Wonk <k_aYT>_N <w_aZP>_N
+                                             :: Wonk k_aYT w_aZP
+                                                ~R# ((S k_aYT + S w_aZP) :~: (S (S k_aYT) + w_aZP)))
+                                of
+                                { Refl co3_aXU ->
+                                (GHC.Internal.Data.Type.Equality.$WRefl
+                                   @Nat @(S (S (S (k_aYT + w_aZP)))))
+                                `cast` (((:~:)
+                                           <Nat>_N
+                                           ((S ((S (Sym (Ifoldl.D:R:+[1] <k_aYT>_N <w_aZP>_N)
+                                                    ; SelCo:Tc(0,N)
+                                                          (Sym (Ifoldl.D:R:+[1]
+                                                                    <S k_aYT>_N <w_aZP>_N)
+                                                           ; co3_aXU
+                                                           ; Ifoldl.D:R:+[1]
+                                                                 <k_aYT>_N <S w_aZP>_N)))_N
+                                                ; Sym (Ifoldl.D:R:+[1] <k_aYT>_N <S w_aZP>_N)))_N
+                                            ; Sym (Ifoldl.D:R:+[1] <S k_aYT>_N <S w_aZP>_N))
+                                           ((S ((S (Sym (Ifoldl.D:R:+[1] <k_aYT>_N <w_aZP>_N)))_N
+                                                ; Sym (Ifoldl.D:R:+[1] <S k_aYT>_N <w_aZP>_N)))_N
+                                            ; Sym (Ifoldl.D:R:+[1] <S (S k_aYT)>_N <w_aZP>_N)))_R
+                                        ; Sym (Ifoldl.N:Wonk <S k_aYT>_N <w_aZP>_N)
+                                        :: (S (S (S (k_aYT + w_aZP))) :~: S (S (S (k_aYT + w_aZP))))
+                                           ~R# Wonk (S k_aYT) w_aZP)
+                                })
+                             (f_azT @k_aYT bk_azY ipv2_s1jm)
+                             ipv3_s1jn
+                           }
+                       }
+                       }
+                       }
+                       }; } in
+                 jump go_azU
+                   @Z
+                   @n_aY9
+                   ((GHC.Internal.Data.Type.Equality.$WRefl @Nat @Z)
+                    `cast` (((:~:) <Nat>_N (Sym (Ifoldl.D:R:+[0] <Z>_N)) <Z>_N)_R
+                            :: (Z :~: Z) ~R# ((Z + Z) :~: Z)))
+                   ((GHC.Internal.Data.Type.Equality.$WRefl @Nat @n_aY9)
+                    `cast` (((:~:)
+                               <Nat>_N (Sym (Ifoldl.D:R:+[0] <n_aY9>_N)) <n_aY9>_N)_R
+                            :: (n_aY9 :~: n_aY9) ~R# ((Z + n_aY9) :~: n_aY9)))
+                   ((\ (@(w_a10g :: Nat)) ->
+                       GHC.Internal.Data.Type.Equality.$WRefl @Nat @(S (S w_a10g)))
+                    `cast` (forall (w :: <Nat>_N).
+                            ((:~:)
+                               <Nat>_N
+                               ((S (Sym (Ifoldl.D:R:+[0] <S w>_N)))_N
+                                ; Sym (Ifoldl.D:R:+[1] <Z>_N <S w>_N))
+                               ((S ((S (Sym (Ifoldl.D:R:+[0] <w>_N)))_N
+                                    ; Sym (Ifoldl.D:R:+[1] <Z>_N <w>_N)))_N
+                                ; Sym (Ifoldl.D:R:+[1] <S Z>_N <w>_N)))_R
+                            ; Sym (Ifoldl.N:Wonk <Z>_N <w>_N)
+                            :: (forall (w :: Nat). S (S w) :~: S (S w))
+                               ~R# (forall (w :: Nat). Wonk Z w)))
+                   eta_B0
+                   eta1_B1}]
+ifoldlRec
+  = \ (@(b_aY8 :: Nat -> *))
+      (@(n_aY9 :: Nat))
+      (@a_aYa)
+      (f_azT :: forall (m :: Nat). b_aY8 m -> a_aYa -> b_aY8 (S m))
+      (eta_B0 :: b_aY8 Z)
+      (eta1_B1 :: Vec n_aY9 a_aYa) ->
+      joinrec {
+        $wgo_s1lY [InlPrag=[2],
+                   Occ=LoopBreaker,
+                   Dmd=SC(S,C(1,C(1,C(1,C(1,L)))))]
+          :: forall (k :: Nat) (m :: Nat).
+             (k GHC.Internal.Prim.~# (k + Z),
+              n_aY9 GHC.Internal.Prim.~# (k + m)) =>
+             (forall (w :: Nat). Wonk k w)
+             -> b_aY8 k -> Vec m a_aYa -> b_aY8 n_aY9
+        [LclId[JoinId(7)(Just [~, ~, !, ~, !])],
+         Arity=5,
+         Str=<L><L><SL><L><1L>,
+         Unf=OtherCon []]
+        $wgo_s1lY (@(k_s1lK :: Nat))
+                  (@(m_s1lL :: Nat))
+                  (ww_s1lT :: k_s1lK GHC.Internal.Prim.~# (k_s1lK + Z))
+                  (ww1_s1lW :: n_aY9 GHC.Internal.Prim.~# (k_s1lK + m_s1lL))
+                  (ds_s1lO :: forall (w :: Nat). Wonk k_s1lK w)
+                  (bk_s1lP :: b_aY8 k_s1lK)
+                  (ds1_s1lQ :: Vec m_s1lL a_aYa)
+          = case (ds_s1lO @(GHC.Internal.Types.ZonkAny 0))
+                 `cast` (Ifoldl.N:Wonk <k_s1lK>_N <GHC.Internal.Types.ZonkAny 0>_N
+                         :: Wonk k_s1lK (GHC.Internal.Types.ZonkAny 0)
+                            ~R# ((S k_s1lK + S (GHC.Internal.Types.ZonkAny 0))
+                                 :~: (S (S k_s1lK) + GHC.Internal.Types.ZonkAny 0)))
+            of
+            { Refl co_aZ3 [Dmd=A] ->
+            case ds1_s1lQ of {
+              Nil co1_aZ5 [Dmd=S] ->
+                bk_s1lP
+                `cast` (<b_aY8>_R (ww_s1lT
+                                   ; (<k_s1lK>_N + Sym co1_aZ5)_N
+                                   ; Sym ww1_s1lW)
+                        :: b_aY8 k_s1lK ~R# b_aY8 n_aY9);
+              ::: @ipv_s1jf ipv1_s1jg [Dmd=S] ipv2_s1jh ipv3_s1ji ->
+                case ds_s1lO of ds2_X5 { __DEFAULT ->
+                case (ds2_X5 @ipv_s1jf)
+                     `cast` (Ifoldl.N:Wonk <k_s1lK>_N <ipv_s1jf>_N
+                             :: Wonk k_s1lK ipv_s1jf
+                                ~R# ((S k_s1lK + S ipv_s1jf) :~: (S (S k_s1lK) + ipv_s1jf)))
+                of
+                { Refl co1_aZJ ->
+                jump $wgo_s1lY
+                  @(S k_s1lK)
+                  @ipv_s1jf
+                  @~((S ww_s1lT)_N
+                     ; Sym (Ifoldl.D:R:+[1] <k_s1lK>_N <Z>_N)
+                     :: S k_s1lK GHC.Internal.Prim.~# (S k_s1lK + Z))
+                  @~(ww1_s1lW
+                     ; (<k_s1lK>_N + ipv1_s1jg)_N
+                     ; SelCo:Tc(0,N)
+                           (Sym (Ifoldl.D:R:+[1] <k_s1lK>_N <S ipv_s1jf>_N)
+                            ; Sym co1_aZJ
+                            ; Ifoldl.D:R:+[1] <S k_s1lK>_N <ipv_s1jf>_N)
+                     :: n_aY9 GHC.Internal.Prim.~# (S k_s1lK + ipv_s1jf))
+                  (\ (@(w_aZP :: Nat)) ->
+                     case (ds2_X5 @w_aZP)
+                          `cast` (Ifoldl.N:Wonk <k_s1lK>_N <w_aZP>_N
+                                  :: Wonk k_s1lK w_aZP
+                                     ~R# ((S k_s1lK + S w_aZP) :~: (S (S k_s1lK) + w_aZP)))
+                     of
+                     { Refl co2_aXU ->
+                     (GHC.Internal.Data.Type.Equality.$WRefl
+                        @Nat @(S (S (S (k_s1lK + w_aZP)))))
+                     `cast` (((:~:)
+                                <Nat>_N
+                                ((S ((S (Sym (Ifoldl.D:R:+[1] <k_s1lK>_N <w_aZP>_N)
+                                         ; SelCo:Tc(0,N)
+                                               (Sym (Ifoldl.D:R:+[1] <S k_s1lK>_N <w_aZP>_N)
+                                                ; co2_aXU
+                                                ; Ifoldl.D:R:+[1] <k_s1lK>_N <S w_aZP>_N)))_N
+                                     ; Sym (Ifoldl.D:R:+[1] <k_s1lK>_N <S w_aZP>_N)))_N
+                                 ; Sym (Ifoldl.D:R:+[1] <S k_s1lK>_N <S w_aZP>_N))
+                                ((S ((S (Sym (Ifoldl.D:R:+[1] <k_s1lK>_N <w_aZP>_N)))_N
+                                     ; Sym (Ifoldl.D:R:+[1] <S k_s1lK>_N <w_aZP>_N)))_N
+                                 ; Sym (Ifoldl.D:R:+[1] <S (S k_s1lK)>_N <w_aZP>_N)))_R
+                             ; Sym (Ifoldl.N:Wonk <S k_s1lK>_N <w_aZP>_N)
+                             :: (S (S (S (k_s1lK + w_aZP))) :~: S (S (S (k_s1lK + w_aZP))))
+                                ~R# Wonk (S k_s1lK) w_aZP)
+                     })
+                  (f_azT @k_s1lK bk_s1lP ipv2_s1jh)
+                  ipv3_s1ji
+                }
+                }
+            }
+            }; } in
+      jump $wgo_s1lY
+        @Z
+        @n_aY9
+        @~(Sym (Ifoldl.D:R:+[0] <Z>_N) :: Z GHC.Internal.Prim.~# (Z + Z))
+        @~(Sym (Ifoldl.D:R:+[0] <n_aY9>_N)
+           :: n_aY9 GHC.Internal.Prim.~# (Z + n_aY9))
+        ((\ (@(w_a10g :: Nat)) ->
+            GHC.Internal.Data.Type.Equality.$WRefl @Nat @(S (S w_a10g)))
+         `cast` (forall (w :: <Nat>_N).
+                 ((:~:)
+                    <Nat>_N
+                    ((S (Sym (Ifoldl.D:R:+[0] <S w>_N)))_N
+                     ; Sym (Ifoldl.D:R:+[1] <Z>_N <S w>_N))
+                    ((S ((S (Sym (Ifoldl.D:R:+[0] <w>_N)))_N
+                         ; Sym (Ifoldl.D:R:+[1] <Z>_N <w>_N)))_N
+                     ; Sym (Ifoldl.D:R:+[1] <S Z>_N <w>_N)))_R
+                 ; Sym (Ifoldl.N:Wonk <Z>_N <w>_N)
+                 :: (forall (w :: Nat). S (S w) :~: S (S w))
+                    ~R# (forall (w :: Nat). Wonk Z w)))
+        eta_B0
+        eta1_B1
+
+Rec {
+-- RHS size: {terms: 33, types: 159, coercions: 128, joins: 0/0}
+Ifoldl.$wpoly_go [InlPrag=[2], Occ=LoopBreaker]
+  :: forall a (n :: Nat) (k :: Nat) (m :: Nat).
+     (k GHC.Internal.Prim.~# (k + Z), n GHC.Internal.Prim.~# (k + m)) =>
+     (forall (w :: Nat). Wonk k w)
+     -> Flip Vec a k -> Vec m a -> Flip Vec a n
+[GblId[StrictWorker([~, ~, !, ~, !])],
+ Arity=5,
+ Str=<L><L><SL><L><1L>,
+ Unf=OtherCon []]
+Ifoldl.$wpoly_go
+  = \ (@a_s1m1)
+      (@(n_s1m2 :: Nat))
+      (@(k_s1m3 :: Nat))
+      (@(m_s1m4 :: Nat))
+      (ww_s1mc :: k_s1m3 GHC.Internal.Prim.~# (k_s1m3 + Z))
+      (ww1_s1mf :: n_s1m2 GHC.Internal.Prim.~# (k_s1m3 + m_s1m4))
+      (ds_s1m7 :: forall (w :: Nat). Wonk k_s1m3 w)
+      (bk_s1m8 :: Flip Vec a_s1m1 k_s1m3)
+      (ds1_s1m9 :: Vec m_s1m4 a_s1m1) ->
+      case (ds_s1m7 @(GHC.Internal.Types.ZonkAny 0))
+           `cast` (Ifoldl.N:Wonk <k_s1m3>_N <GHC.Internal.Types.ZonkAny 0>_N
+                   :: Wonk k_s1m3 (GHC.Internal.Types.ZonkAny 0)
+                      ~R# ((S k_s1m3 + S (GHC.Internal.Types.ZonkAny 0))
+                           :~: (S (S k_s1m3) + GHC.Internal.Types.ZonkAny 0)))
+      of
+      { Refl co_aZ3 [Dmd=A] ->
+      case ds1_s1m9 of {
+        Nil co1_aZ5 [Dmd=S] ->
+          bk_s1m8
+          `cast` ((Flip
+                     <Nat>_N
+                     <*>_N
+                     <Vec>_R
+                     <a_s1m1>_N
+                     (ww_s1mc
+                      ; (<k_s1m3>_N + Sym co1_aZ5)_N
+                      ; Sym ww1_s1mf))_R
+                  :: Flip Vec a_s1m1 k_s1m3 ~R# Flip Vec a_s1m1 n_s1m2);
+        ::: @ipv_s1jk ipv1_s1jl [Dmd=S] ipv2_s1jm ipv3_s1jn ->
+          case ds_s1m7 of ds2_X5 { __DEFAULT ->
+          case (ds2_X5 @ipv_s1jk)
+               `cast` (Ifoldl.N:Wonk <k_s1m3>_N <ipv_s1jk>_N
+                       :: Wonk k_s1m3 ipv_s1jk
+                          ~R# ((S k_s1m3 + S ipv_s1jk) :~: (S (S k_s1m3) + ipv_s1jk)))
+          of
+          { Refl co1_aZJ ->
+          Ifoldl.$wpoly_go
+            @a_s1m1
+            @n_s1m2
+            @(S k_s1m3)
+            @ipv_s1jk
+            @~((S ww_s1mc)_N
+               ; Sym (Ifoldl.D:R:+[1] <k_s1m3>_N <Z>_N)
+               :: S k_s1m3 GHC.Internal.Prim.~# (S k_s1m3 + Z))
+            @~(ww1_s1mf
+               ; (<k_s1m3>_N + ipv1_s1jl)_N
+               ; SelCo:Tc(0,N)
+                     (Sym (Ifoldl.D:R:+[1] <k_s1m3>_N <S ipv_s1jk>_N)
+                      ; Sym co1_aZJ
+                      ; Ifoldl.D:R:+[1] <S k_s1m3>_N <ipv_s1jk>_N)
+               :: n_s1m2 GHC.Internal.Prim.~# (S k_s1m3 + ipv_s1jk))
+            (\ (@(w_aZP :: Nat)) ->
+               case (ds2_X5 @w_aZP)
+                    `cast` (Ifoldl.N:Wonk <k_s1m3>_N <w_aZP>_N
+                            :: Wonk k_s1m3 w_aZP
+                               ~R# ((S k_s1m3 + S w_aZP) :~: (S (S k_s1m3) + w_aZP)))
+               of
+               { Refl co2_aXU ->
+               (GHC.Internal.Data.Type.Equality.$WRefl
+                  @Nat @(S (S (S (k_s1m3 + w_aZP)))))
+               `cast` (((:~:)
+                          <Nat>_N
+                          ((S ((S (Sym (Ifoldl.D:R:+[1] <k_s1m3>_N <w_aZP>_N)
+                                   ; SelCo:Tc(0,N)
+                                         (Sym (Ifoldl.D:R:+[1] <S k_s1m3>_N <w_aZP>_N)
+                                          ; co2_aXU
+                                          ; Ifoldl.D:R:+[1] <k_s1m3>_N <S w_aZP>_N)))_N
+                               ; Sym (Ifoldl.D:R:+[1] <k_s1m3>_N <S w_aZP>_N)))_N
+                           ; Sym (Ifoldl.D:R:+[1] <S k_s1m3>_N <S w_aZP>_N))
+                          ((S ((S (Sym (Ifoldl.D:R:+[1] <k_s1m3>_N <w_aZP>_N)))_N
+                               ; Sym (Ifoldl.D:R:+[1] <S k_s1m3>_N <w_aZP>_N)))_N
+                           ; Sym (Ifoldl.D:R:+[1] <S (S k_s1m3)>_N <w_aZP>_N)))_R
+                       ; Sym (Ifoldl.N:Wonk <S k_s1m3>_N <w_aZP>_N)
+                       :: (S (S (S (k_s1m3 + w_aZP))) :~: S (S (S (k_s1m3 + w_aZP))))
+                          ~R# Wonk (S k_s1m3) w_aZP)
+               })
+            ((Ifoldl.:::
+                @(S k_s1m3)
+                @a_s1m1
+                @k_s1m3
+                @~(<S k_s1m3>_N :: S k_s1m3 GHC.Internal.Prim.~# S k_s1m3)
+                ipv2_s1jm
+                (bk_s1m8
+                 `cast` (Ifoldl.N:Flip <Nat>_N <*>_N <Vec>_R <a_s1m1>_N <k_s1m3>_N
+                         :: Flip Vec a_s1m1 k_s1m3 ~R# Vec k_s1m3 a_s1m1)))
+             `cast` (Sym (Ifoldl.N:Flip
+                              <Nat>_N <*>_N <Vec>_R <a_s1m1>_N <S k_s1m3>_N)
+                     :: Vec (S k_s1m3) a_s1m1 ~R# Flip Vec a_s1m1 (S k_s1m3)))
+            ipv3_s1jn
+          }
+          }
+      }
+      }
+end Rec }
+
+-- RHS size: {terms: 8, types: 15, coercions: 49, joins: 0/0}
+Ifoldl.reverseVec_g
+  :: forall {n :: Nat} {a}. Vec n a -> Flip Vec a n
+[GblId,
+ Arity=1,
+ Str=<1L>,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [0] 40 60}]
+Ifoldl.reverseVec_g
+  = \ (@(n_a10v :: Nat)) (@a_a10w) (eta_B1 :: Vec n_a10v a_a10w) ->
+      Ifoldl.$wpoly_go
+        @a_a10w
+        @n_a10v
+        @Z
+        @n_a10v
+        @~(Sym (Ifoldl.D:R:+[0] <Z>_N) :: Z GHC.Internal.Prim.~# (Z + Z))
+        @~(Sym (Ifoldl.D:R:+[0] <n_a10v>_N)
+           :: n_a10v GHC.Internal.Prim.~# (Z + n_a10v))
+        ((\ (@(w_a10g :: Nat)) ->
+            GHC.Internal.Data.Type.Equality.$WRefl @Nat @(S (S w_a10g)))
+         `cast` (forall (w :: <Nat>_N).
+                 ((:~:)
+                    <Nat>_N
+                    ((S (Sym (Ifoldl.D:R:+[0] <S w>_N)))_N
+                     ; Sym (Ifoldl.D:R:+[1] <Z>_N <S w>_N))
+                    ((S ((S (Sym (Ifoldl.D:R:+[0] <w>_N)))_N
+                         ; Sym (Ifoldl.D:R:+[1] <Z>_N <w>_N)))_N
+                     ; Sym (Ifoldl.D:R:+[1] <S Z>_N <w>_N)))_R
+                 ; Sym (Ifoldl.N:Wonk <Z>_N <w>_N)
+                 :: (forall (w :: Nat). S (S w) :~: S (S w))
+                    ~R# (forall (w :: Nat). Wonk Z w)))
+        ((Ifoldl.$WNil @a_a10w)
+         `cast` (Sym (Ifoldl.N:Flip <Nat>_N <*>_N <Vec>_R <a_a10w>_N <Z>_N)
+                 :: Vec Z a_a10w ~R# Flip Vec a_a10w Z))
+        eta_B1
+
+-- RHS size: {terms: 1, types: 0, coercions: 15, joins: 0/0}
+reverseVec :: forall (n :: Nat) a. Vec n a -> Vec n a
+[GblId,
+ Arity=1,
+ Str=<1L>,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
+reverseVec
+  = Ifoldl.reverseVec_g
+    `cast` (forall (n[infrd]~[spec] :: <Nat>_N) (a[infrd]~[spec] :: <*>_N).
+            <Vec n a>_R
+            %<Many>_N ->_R Ifoldl.N:Flip <Nat>_N <*>_N <Vec>_R <a>_N <n>_N
+            :: (forall {n :: Nat} {a}. Vec n a -> Flip Vec a n)
+               ~R# (forall (n :: Nat) a. Vec n a -> Vec n a))
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$trModule4 :: GHC.Internal.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 20 0}]
+Ifoldl.$trModule4 = "main"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$trModule3 :: GHC.Internal.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$trModule3 = GHC.Internal.Types.TrNameS Ifoldl.$trModule4
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$trModule2 :: GHC.Internal.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 30 0}]
+Ifoldl.$trModule2 = "Ifoldl"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$trModule1 :: GHC.Internal.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$trModule1 = GHC.Internal.Types.TrNameS Ifoldl.$trModule2
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$trModule :: GHC.Internal.Types.Module
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$trModule
+  = GHC.Internal.Types.Module Ifoldl.$trModule3 Ifoldl.$trModule1
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+$krep_r1n8 :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep_r1n8 = GHC.Internal.Types.KindRepVar 1#
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep1_r1n9 :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep1_r1n9
+  = GHC.Internal.Types.KindRepFun
+      $krep_r1n8 GHC.Internal.Types.krep$*
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+$krep2_r1na :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep2_r1na = GHC.Internal.Types.KindRepVar 0#
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep3_r1nb :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep3_r1nb = GHC.Internal.Types.KindRepFun $krep2_r1na $krep1_r1n9
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep4_r1nc :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep4_r1nc
+  = GHC.Internal.Types.KindRepFun
+      $krep2_r1na GHC.Internal.Types.krep$*
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep5_r1nd :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep5_r1nd = GHC.Internal.Types.KindRepFun $krep_r1n8 $krep4_r1nc
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcFlip1 [InlPrag=[~]] :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+Ifoldl.$tcFlip1
+  = GHC.Internal.Types.KindRepFun $krep3_r1nb $krep5_r1nd
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+$krep6_r1ne :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep6_r1ne = GHC.Internal.Types.KindRepVar 2#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+$krep7_r1nf :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep7_r1nf = GHC.Internal.Types.KindRepVar 3#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+$krep8_r1ng :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep8_r1ng = GHC.Internal.Types.KindRepVar 4#
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep9_r1nh :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep9_r1nh = GHC.Internal.Types.KindRepApp $krep6_r1ne $krep8_r1ng
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep10_r1ni :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep10_r1ni
+  = GHC.Internal.Types.KindRepApp $krep9_r1nh $krep7_r1nf
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcNat2 :: GHC.Internal.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 20 0}]
+Ifoldl.$tcNat2 = "Nat"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcNat1 :: GHC.Internal.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tcNat1 = GHC.Internal.Types.TrNameS Ifoldl.$tcNat2
+
+-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcNat :: GHC.Internal.Types.TyCon
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tcNat
+  = GHC.Internal.Types.TyCon
+      18236869020729724782#Word64
+      4245855676397049056#Word64
+      Ifoldl.$trModule
+      Ifoldl.$tcNat1
+      0#
+      GHC.Internal.Types.krep$*
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Z1 [InlPrag=[~]] :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+Ifoldl.$tc'Z1
+  = GHC.Internal.Types.KindRepTyConApp
+      Ifoldl.$tcNat (GHC.Internal.Types.[] @GHC.Internal.Types.KindRep)
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Z3 :: GHC.Internal.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 20 0}]
+Ifoldl.$tc'Z3 = "'Z"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Z2 :: GHC.Internal.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tc'Z2 = GHC.Internal.Types.TrNameS Ifoldl.$tc'Z3
+
+-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Z :: GHC.Internal.Types.TyCon
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tc'Z
+  = GHC.Internal.Types.TyCon
+      12150613558191457985#Word64
+      17820276006185949984#Word64
+      Ifoldl.$trModule
+      Ifoldl.$tc'Z2
+      0#
+      Ifoldl.$tc'Z1
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+$krep11_r1nj :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep11_r1nj
+  = GHC.Internal.Types.KindRepTyConApp
+      Ifoldl.$tc'Z (GHC.Internal.Types.[] @GHC.Internal.Types.KindRep)
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcVec1 [InlPrag=[~]] :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+Ifoldl.$tcVec1
+  = GHC.Internal.Types.KindRepFun
+      Ifoldl.$tc'Z1 GHC.Internal.Types.krep$*Arr*
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep12_r1nk :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep12_r1nk
+  = GHC.Internal.Types.KindRepFun
+      Ifoldl.$tc'Z1 GHC.Internal.Types.krep$*
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcWonk1 [InlPrag=[~]] :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+Ifoldl.$tcWonk1
+  = GHC.Internal.Types.KindRepFun Ifoldl.$tc'Z1 $krep12_r1nk
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'S1 [InlPrag=[~]] :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+Ifoldl.$tc'S1
+  = GHC.Internal.Types.KindRepFun Ifoldl.$tc'Z1 Ifoldl.$tc'Z1
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'S3 :: GHC.Internal.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 20 0}]
+Ifoldl.$tc'S3 = "'S"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'S2 :: GHC.Internal.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tc'S2 = GHC.Internal.Types.TrNameS Ifoldl.$tc'S3
+
+-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'S :: GHC.Internal.Types.TyCon
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tc'S
+  = GHC.Internal.Types.TyCon
+      11382371654426533936#Word64
+      12395597000343428369#Word64
+      Ifoldl.$trModule
+      Ifoldl.$tc'S2
+      0#
+      Ifoldl.$tc'S1
+
+-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
+$krep13_r1nl :: [GHC.Internal.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep13_r1nl
+  = GHC.Internal.Types.:
+      @GHC.Internal.Types.KindRep
+      $krep_r1n8
+      (GHC.Internal.Types.[] @GHC.Internal.Types.KindRep)
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep14_r1nm :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep14_r1nm
+  = GHC.Internal.Types.KindRepTyConApp Ifoldl.$tc'S $krep13_r1nl
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcVec3 :: GHC.Internal.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 20 0}]
+Ifoldl.$tcVec3 = "Vec"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcVec2 :: GHC.Internal.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tcVec2 = GHC.Internal.Types.TrNameS Ifoldl.$tcVec3
+
+-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcVec :: GHC.Internal.Types.TyCon
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tcVec
+  = GHC.Internal.Types.TyCon
+      14854607458058977841#Word64
+      8374922991311866538#Word64
+      Ifoldl.$trModule
+      Ifoldl.$tcVec2
+      0#
+      Ifoldl.$tcVec1
+
+-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
+$krep15_r1nn :: [GHC.Internal.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep15_r1nn
+  = GHC.Internal.Types.:
+      @GHC.Internal.Types.KindRep
+      $krep2_r1na
+      (GHC.Internal.Types.[] @GHC.Internal.Types.KindRep)
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+$krep16_r1no :: [GHC.Internal.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep16_r1no
+  = GHC.Internal.Types.:
+      @GHC.Internal.Types.KindRep $krep_r1n8 $krep15_r1nn
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep17_r1np :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep17_r1np
+  = GHC.Internal.Types.KindRepTyConApp Ifoldl.$tcVec $krep16_r1no
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+$krep18_r1nq :: [GHC.Internal.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep18_r1nq
+  = GHC.Internal.Types.:
+      @GHC.Internal.Types.KindRep $krep14_r1nm $krep15_r1nn
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep19_r1nr :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep19_r1nr
+  = GHC.Internal.Types.KindRepTyConApp Ifoldl.$tcVec $krep18_r1nq
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep20_r1ns :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep20_r1ns
+  = GHC.Internal.Types.KindRepFun $krep17_r1np $krep19_r1nr
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc':::1 [InlPrag=[~]] :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+Ifoldl.$tc':::1
+  = GHC.Internal.Types.KindRepFun $krep2_r1na $krep20_r1ns
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc':::3 :: GHC.Internal.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 20 0}]
+Ifoldl.$tc':::3 = "':::"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc':::2 :: GHC.Internal.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tc':::2 = GHC.Internal.Types.TrNameS Ifoldl.$tc':::3
+
+-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'::: :: GHC.Internal.Types.TyCon
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tc':::
+  = GHC.Internal.Types.TyCon
+      334686219684160234#Word64
+      3014902632845087398#Word64
+      Ifoldl.$trModule
+      Ifoldl.$tc':::2
+      2#
+      Ifoldl.$tc':::1
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+$krep21_r1nt :: [GHC.Internal.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep21_r1nt
+  = GHC.Internal.Types.:
+      @GHC.Internal.Types.KindRep $krep11_r1nj $krep15_r1nn
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Nil1 [InlPrag=[~]] :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+Ifoldl.$tc'Nil1
+  = GHC.Internal.Types.KindRepTyConApp Ifoldl.$tcVec $krep21_r1nt
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Nil3 :: GHC.Internal.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 20 0}]
+Ifoldl.$tc'Nil3 = "'Nil"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Nil2 :: GHC.Internal.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tc'Nil2 = GHC.Internal.Types.TrNameS Ifoldl.$tc'Nil3
+
+-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Nil :: GHC.Internal.Types.TyCon
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tc'Nil
+  = GHC.Internal.Types.TyCon
+      6632636372057876164#Word64
+      13532705703229277899#Word64
+      Ifoldl.$trModule
+      Ifoldl.$tc'Nil2
+      1#
+      Ifoldl.$tc'Nil1
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcWonk3 :: GHC.Internal.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 20 0}]
+Ifoldl.$tcWonk3 = "Wonk"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcWonk2 :: GHC.Internal.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tcWonk2 = GHC.Internal.Types.TrNameS Ifoldl.$tcWonk3
+
+-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcWonk :: GHC.Internal.Types.TyCon
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tcWonk
+  = GHC.Internal.Types.TyCon
+      2107340412666559272#Word64
+      605784541161197679#Word64
+      Ifoldl.$trModule
+      Ifoldl.$tcWonk2
+      0#
+      Ifoldl.$tcWonk1
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcFlip3 :: GHC.Internal.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 20 0}]
+Ifoldl.$tcFlip3 = "Flip"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcFlip2 :: GHC.Internal.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tcFlip2 = GHC.Internal.Types.TrNameS Ifoldl.$tcFlip3
+
+-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tcFlip :: GHC.Internal.Types.TyCon
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tcFlip
+  = GHC.Internal.Types.TyCon
+      562740838472115680#Word64
+      15461924706169976739#Word64
+      Ifoldl.$trModule
+      Ifoldl.$tcFlip2
+      2#
+      Ifoldl.$tcFlip1
+
+-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
+$krep22_r1nu :: [GHC.Internal.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep22_r1nu
+  = GHC.Internal.Types.:
+      @GHC.Internal.Types.KindRep
+      $krep8_r1ng
+      (GHC.Internal.Types.[] @GHC.Internal.Types.KindRep)
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+$krep23_r1nv :: [GHC.Internal.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep23_r1nv
+  = GHC.Internal.Types.:
+      @GHC.Internal.Types.KindRep $krep7_r1nf $krep22_r1nu
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+$krep24_r1nw :: [GHC.Internal.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep24_r1nw
+  = GHC.Internal.Types.:
+      @GHC.Internal.Types.KindRep $krep6_r1ne $krep23_r1nv
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+$krep25_r1nx :: [GHC.Internal.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep25_r1nx
+  = GHC.Internal.Types.:
+      @GHC.Internal.Types.KindRep $krep_r1n8 $krep24_r1nw
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+$krep26_r1ny :: [GHC.Internal.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep26_r1ny
+  = GHC.Internal.Types.:
+      @GHC.Internal.Types.KindRep $krep2_r1na $krep25_r1nx
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+$krep27_r1nz :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep27_r1nz
+  = GHC.Internal.Types.KindRepTyConApp Ifoldl.$tcFlip $krep26_r1ny
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Flip1 [InlPrag=[~]] :: GHC.Internal.Types.KindRep
+[GblId, Unf=OtherCon []]
+Ifoldl.$tc'Flip1
+  = GHC.Internal.Types.KindRepFun $krep10_r1ni $krep27_r1nz
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Flip3 :: GHC.Internal.Prim.Addr#
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 30 0}]
+Ifoldl.$tc'Flip3 = "'Flip"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Flip2 :: GHC.Internal.Types.TrName
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tc'Flip2 = GHC.Internal.Types.TrNameS Ifoldl.$tc'Flip3
+
+-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
+Ifoldl.$tc'Flip :: GHC.Internal.Types.TyCon
+[GblId,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [] 10 10}]
+Ifoldl.$tc'Flip
+  = GHC.Internal.Types.TyCon
+      7623277265010559423#Word64
+      16926366384040641029#Word64
+      Ifoldl.$trModule
+      Ifoldl.$tc'Flip2
+      5#
+      Ifoldl.$tc'Flip1
+
+
+


=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -532,3 +532,4 @@ test('T24725a', [ grep_errmsg(r'testedRule')], compile, ['-O -ddump-rule-firings
 test('T25033', normal, compile, ['-O'])
 test('T25160', normal, compile, ['-O -ddump-rules'])
 test('T25197', [req_th, extra_files(["T25197_TH.hs"]), only_ways(['optasm'])], multimod_compile, ['T25197', '-O2 -v0'])
+test('T25713', [grep_errmsg('W:::')], compile, ['-O -ddump-simpl'])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a25e56da97cd9ad15b78e30b898aa230571c1df7...a3bbd4bf450c532f1bd11a9ef9d9885099b0e0b4

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a25e56da97cd9ad15b78e30b898aa230571c1df7...a3bbd4bf450c532f1bd11a9ef9d9885099b0e0b4
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/20250212/effe2018/attachment-0001.html>


More information about the ghc-commits mailing list