Question: Is forcing this value in WHNF avoidable?

Summary

In containers we have

data Map k a = Bin !Int !k a !(Map k a) !(Map k a)
             | Tip

And we can find the minimum value in the map as follows.

data KV k a = KV !k a

lookupMin :: Map k a -> Maybe (KV k a)
lookupMin Tip = Nothing
lookupMin (Bin _ k x l _) = Just $! lookupMinSure k x l

lookupMinSure :: k -> a -> Map k a -> KV k a
lookupMinSure k x Tip = KV k x
lookupMinSure _ _ (Bin _ k x l _) = lookupMinSure k x l

This leads to this core for lookupMinSure.

Rec {
-- RHS size: {terms: 19, types: 26, coercions: 0, joins: 0/0}
SetMin.$wlookupMinSure [InlPrag=[2], Occ=LoopBreaker]
  :: forall {k} {a}. k -> a -> Map k a -> (# k, a #)
[GblId[StrictWorker([~, ~, !])],
 Arity=3,
 Str=<ML><L><1L>,
 Unf=OtherCon []]
SetMin.$wlookupMinSure
  = \ (@k) (@a) (k1 :: k) (x :: a) (ds :: Map k a) ->
      case ds of {
        Bin bx k2 x1 l ds1 -> SetMin.$wlookupMinSure @k @a k2 x1 l;
        Tip -> case k1 of conrep { __DEFAULT -> (# conrep, x #) }
      }
end Rec }

Notice that there is a case k1 of conrep which forces the key. This should not be necessary, since the map is strict in the key.

@treeowl suggested trying this alternative:

data UBox :: Type -> UnliftedType where
  UBox :: !a -> UBox a

lookupMin' :: Map k a -> Maybe (KV k a)
lookupMin' Tip = Nothing
lookupMin' (Bin _ k x l _) = Just $! lookupMinSure' (UBox k) x l

lookupMinSure' :: UBox k -> a -> Map k a -> KV k a
lookupMinSure' (UBox k) x Tip = KV k x
lookupMinSure' _ _ (Bin _ k x l _) = lookupMinSure' (UBox k) x l

This generates the core

Rec {
-- RHS size: {terms: 19, types: 26, coercions: 0, joins: 0/0}
SetMin.$wlookupMinSure' [InlPrag=[2], Occ=LoopBreaker]
  :: forall {k} {a}. k -> a -> Map k a -> (# k, a #)
[GblId[StrictWorker([!, ~, !])],
 Arity=3,
 Str=<1L><L><1L>,
 Unf=OtherCon []]
SetMin.$wlookupMinSure'
  = \ (@k) (@a) (ww :: k) (x :: a) (ds :: Map k a) ->
      case ww of ww1 { __DEFAULT ->
      case ds of {
        Bin ipv ipv1 ipv2 ipv3 ipv4 ->
          SetMin.$wlookupMinSure' @k @a ipv1 ipv2 ipv3;
        Tip -> (# ww1, x #)
      }
      }
end Rec }

This still forces the key, but now on every iteration.

Questions:

• Why does the UBox version force the key on every iteration?
• Is it possible to implement this in a way that GHC realizes that forcing they key is not necessary?

Original discussion on containers for reference: #976.

Steps to reproduce

Compile the code above.

Environment

• GHC version used: 9.6.3