!7599 unveiled a bug in the Specialiser. * See also #21328 * Test is in `simplCore/should_run/T21229` Back to the Specialiser. Consider ```hs {-# 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.