Inlining DFuns leads to an unsound interaction with Specialise

!7599 (merged) unveiled a bug in the Specialiser.

• See also #21328 (closed)
• Test is in simplCore/should_run/T21229

Back to the Specialiser. Consider

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

data B = T | F deriving Show

class Sing (b :: B) where sing :: B
instance Sing 'T where sing = T
instance Sing 'F where sing = F

f :: forall a. Sing a => Int -> (Int -> B -> B) -> B
f 0 g = g 0 (sing @a)
f n g = f @a (n-1) g

h :: forall a. Sing a => Int -> (Int -> B -> B) -> B
h = case sing @a of
      T -> f @'T
      F -> f @a
{-# NOINLINE h #-}

main = print $ h @'T 0 (\ _ a -> a)

With -O0, this prints T, as expected, because h will ultimately call its supplied argument once with T.

But with -O, I get F. Why is that? The reason is we ultimately get the following specialisation for the second call to f:

 RULES: "SPEC f @a"
            forall (@(a_aXu :: B)) ($dSing_s1OW :: Sing a_aXu).
              f @a_aXu $dSing_s1OW
              = $sf_s1OX @a_aXu]

and this specialisation (for when $dSing_s1OW is F) somehow also applies at f @'T.

FTR, here is the output of the pprTrace "spec_call" in Specialise:

spec_call
  call info:  CI{SpecType a_aXu
                 SpecDict F `cast` (Sym (N:Sing[0] <a_aXu>_N) :: B ~R# Sing a_aXu)}
  useful:     True
  rule_bndrs: [a_aXu, $dSing_s1OW]
  lhs_args:   [TYPE: a_aXu, $dSing_s1OW]
  spec_bndrs: [a_aXu]
  spec_args:  [TYPE: a_aXu,
               F `cast` (Sym (N:Sing[0] <a_aXu>_N) :: B ~R# Sing a_aXu)]
  dx_binds:   []
  rhs_env2:   <InScope = {main g_aC8 a_aXu $cshowsPrec_aY5 $cshow_aYd
                          $cshowList_aYl $krep_aZ1 $krep_aZ2 $krep_aZ3 $krep_aZ4 $krep_aZ5
                          $krep_aZ6 ds_dZX main $fShowB $fSingF F $fSingT $tc'C:Sing
                          $trModule $tc'F $tc'T $tcB $tcSing f h main_s19F main_s19G
                          main_s1OF $trModule_s1OG $trModule_s1OH $trModule_s1OI
                          $trModule_s1OJ $krep_s1OK $tcB_s1OL $tcB_s1OM $tc'T_s1ON $tc'T_s1OO
                          $tc'F_s1OP $tc'F_s1OQ $tcSing_s1OR $tcSing_s1OS $krep_s1OT
                          $tc'C:Sing_s1OU $tc'C:Sing_s1OV}
               IdSubst   = [aKV :-> F
                                    `cast` (Sym (N:Sing[0] <a_aXu>_N) :: B ~R# Sing a_aXu)]
               TvSubst   = [aKU :-> a_aXu]
               CvSubst   = []>
  []

How did it come to this?! For that we have to look at the Core of h that Specialise sees:

h = \ (@(a_aWY :: B))
      ($dSing_aWZ :: Sing a_aWY)
      (eta_B0 :: Int)
      (eta_B1 :: Int -> B -> B) ->
      case $dSing_aWZ
           `cast` (Main.N:Sing[0] <a_aWY>_N :: Sing a_aWY ~R# B)
      of {
        T ->
          f @'T
            (Main.T `cast` (Sym (Main.N:Sing[0] <'T>_N) :: B ~R# Sing 'T))
            eta_B0
            eta_B1;
        F ->
          f @a_aWY
            (Main.F
             `cast` (Sym (Main.N:Sing[0] <a_aWY>_N) :: B ~R# Sing a_aWY))
            eta_B0
            eta_B1
      }

Note the second call to f. The type argument a_aWY is passed, as well as Main.F as the dictionary. That's strange! We should know statically that a_aWY must be F. (In fact, Main.F `cast` (Sym (Main.N:Sing[0] <a_aWY>_N) :: B ~R# Sing a_aWY) is unsound if a_aWY is instantiated to T, which would perhaps happen if we floated that expression out of the F case. I guess it doesn't matter much, at least not to this ticket.)

How did we get this code? After desugaring, we still have

h = \ (@(a_aXu :: B)) ($dSing_aXv :: Sing a_aXu) ->
      case sing @a_aXu $dSing_aXv of {
        T -> f @'T Main.$fSingT;
        F -> f @a_aXu $dSing_aXv
      }

But then gentle simplification inlines sing and sees that $dSing_aXv is F in the F case, performs a binder swap and successively inlines F (at least that's what I believe the Simplifier does).

Then the Specialiser can't connect F to the arguments $dSing_aXv or the type arg a and somehow bogs up. I suspect this happens in specHeader, but actually I'm not completely sure.

I couldn't reproduce with GHC 9.2 and any prior release. I see that we get the same Core pre-Specialise, but it is handled soundly there and we only get a specialisation for T. So perhaps we want to fix this before 9.4.