GitLab

!SpecConstr creates the following rules, with the right cajoling. (I've used unboxed integers merely to avoid w/w, which only adds noise in this example.)

(See ticket:13014#comment:129293 for a Minimal Working Example.)

data VL :: [k] -> * where
  VLZ :: VL '[]
  VLS :: VL as -> VL (a ': as)

lengthVL :: GHC.Types.SPEC -> VL as -> Int#
{-# INLINABLE lengthVL #-}
lengthVL !sPEC VLZ = 0#
lengthVL !sPEC (VLS vl) = 1# +# lengthVL sPEC vl

==================== Tidy Core rules ====================
"SC:lengthVL0" [ALWAYS]
    forall (@ a) (@ (as :: [*])) (sc :: VL as).
      lengthVL @ (a : as)
               SPEC
               (VLS
                  @ * @ (a : as) @ as @ a @~ (<a : as>_N :: (a : as) ~ (a : as)) sc)
      = lengthVL_$slengthVL1 @ a @ as sc
"SC:lengthVL1" [ALWAYS]
    forall (sc :: VL '[]).
      lengthVL @ '[] SPEC sc
      = lengthVL_$slengthVL sc

But the cons-case specialization, lengthVL_$slengthVL1, is marked as a loopbreaker. Consider the following idiomatic usage to see why that is problematic.

class KnownSpine (as :: [k]) where sing :: VL as
instance KnownSpine '[] where   -- '
  {-# INLINE sing #-}
  sing = VLZ
instance KnownSpine as => KnownSpine (a ': as) where   -- '
  {-# INLINE sing #-}
  sing = VLS sing

example :: Int
example = I# $ lengthVL SPEC (sing :: VL '[Int,Char,Bool])

The right-hand side of example would ideally be simplified to 3. It's not, ultimately because the specialization is marked as a loopbreaker.

I switched on -dverbose-core2core to track the simplification of the right-hand side of example. 1) The sing dictionary is unfolded to constructor applications. 2) Those are floated out but then pre-inlined-unconditionally right back in before CSE gets a chance to spoil it. 3) Thus the VLS rule fires. But it only fires once, because of the loopbreaker designation!

I have not yet investigated why the specialization in the cons-case is marked a loopbreaker.

(Even if the specialization wasn't being considered a loopbreaker --- which immediately makes this approach to optimization a dead-end --- I don't know with any certainty how to force the specialization to be inlined in those cases where its right-hand side was relatively large.)