SpecConstr reboxes inside loops

Compile the following program with -O2 -fno-liberate-case:

f :: (Int, Int) -> Int -> Int
f _ 0 = 0
f p n = length (go n) + f p (n-1)
  where
    go 0 = []
    go n = case p of (x,y) -> (p,x+y) : go (n-1)

main = print $ f (1,2) 10000

For me, it takes about 6.8GB of memory to run the resulting binary. If I also pass -fno-spec-constr, it only takes 5.6GB and is a bit faster.

(No liberate case is material, otherwise the case will just be floated out.)

Here's the simplified Core with SpecConstr:

Rec {
-- RHS size: {terms: 44, types: 36, coercions: 0, joins: 0/1}
Main.main_$s$wf [Occ=LoopBreaker]
  :: Int -> Int -> GHC.Prim.Int# -> GHC.Prim.Int#
[GblId, Arity=3, Str=<L><L><1L>, Unf=OtherCon []]
Main.main_$s$wf
  = \ (sc_s2dV :: Int)
      (sc1_s2dW :: Int)
      (ww_s2dz :: GHC.Prim.Int#) ->
      case ww_s2dz of ds_X1 {
        __DEFAULT ->
          letrec {
            $wgo_s2du [InlPrag=[2], Occ=LoopBreaker, Dmd=SC(S,L)]
              :: GHC.Prim.Int# -> [((Int, Int), Int)]
            [LclId, Arity=1, Str=<1L>, Unf=OtherCon []]
            $wgo_s2du
              = \ (ww1_s2dr :: GHC.Prim.Int#) ->
                  case ww1_s2dr of wild_X1F {
                    __DEFAULT ->
                      GHC.Types.:
                        @((Int, Int), Int)
                        ((sc_s2dV, sc1_s2dW), GHC.Num.$fNumInt_$c+ sc_s2dV sc1_s2dW)
                        ($wgo_s2du (GHC.Prim.-# wild_X1F 1#));
                    0# -> GHC.Types.[] @((Int, Int), Int)
                  }; } in
          case GHC.List.$wlenAcc @((Int, Int), Int) ($wgo_s2du ds_X1) 0#
          of ww1_a2dn
          { __DEFAULT ->
          case Main.main_$s$wf sc_s2dV sc1_s2dW (GHC.Prim.-# ds_X1 1#)
          of ww2_s2dH
          { __DEFAULT ->
          GHC.Prim.+# ww1_a2dn ww2_s2dH
          }
          };
        0# -> 0#
      }
end Rec }

Note the reboxing of (sc_s2dV, sc1_s2dW) inside the loop $wgo. Bad bad bad!

It's all due to SpecConstr substituting (sc_s2dV, sc1_s2dW) for the pair p instead of merely binding let-binding it in $s$wf. It would be reasonable for SpecConstr to do the latter. It can still do case-of-known-con via its sc_val env, I think.