Curiosity related to specialisation and reflection

Consider the following program:

{-# OPTIONS_GHC -ddump-simpl -dno-typeable-binds -fforce-recomp -O -fno-worker-wrapper #-}
module SpecRepro where

import Data.Kind
import Unsafe.Coerce

class Foo t where

class Too where
  too :: Int

class Qux r where
  qux :: r
  boo :: r
  comb :: r -> r -> r

-- This specialises
--instance Qux Int where
-- This does not
instance Too => Qux Int where
  qux = 0
  boo = 1
  comb = (+)

newtype H = H (Int -> Int)

instance Qux H where
  qux = H (\_ -> 0)
  boo = H (\_ -> 1)
  comb (H f) (H g) = H (\x -> f x + g x)

newtype Gift a r = Gift (Too => r)

give :: Int -> (Too => a) -> a
give x f = co f x
  where
    co :: (Too => a) -> (Int -> a)
    co f = unsafeCoerce (Gift f)

-- This does not specialise
a :: Int -> Int
a n = give n (mieux 100)

-- This call specialised to H
b :: Int -> Int
b n = case (mieux 100) of
        H h -> h n

mieux :: Qux a => Int -> a
mieux 0 = boo
mieux n = boo `comb` qux `comb` (mieux (n - 1))

The instances for Too => Q Int and Q H are similar, and both allow the passing of a context (an Int) in the this case to the methods of the function.

They are used in definition of a and b, b is specialised but a is not.

The call to a ends up looking like this:

-- RHS size: {terms: 8, types: 35, coercions: 11, joins: 0/0}
a :: Int -> Int
[GblId,
 Arity=1,
 Str=<A>,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [0] 60 0}]
a = \ (n_axM :: Int) ->
      case unsafeEqualityProof
             @(*) @(Gift GHC.Types.Any Int) @(Int -> Int)
      of
      { UnsafeRefl co_aRm [Dmd=A] ->
      mieux
        @Int
        (SpecRepro.$fQuxInt
           (n_axM
            `cast` (Nth:3
                        (Sub co_aRm
                         ; SpecRepro.N:Gift[0] <GHC.Types.Any>_N <GHC.Types.Any>_P <Int>_N)
                    :: Int ~R# Too)))
        SpecRepro.a1
      }

So we don't specialise it because the fQuxInt dictionary takes n_aXM as an argument so the whole call is discard for specialisation.

We could specialise it however if the n_aXM free variable was abstracted over?

Perhaps @simonpj and @sgraf812 are interested enough to comment.