Show the existence of an instance for a total type family - Haskell

I have a type class C and a total closed type family F :: Bool -> Type.
I have instances of C for both F 'False and F 'True

(how) Can I show ghc that there is an always an instance for C (F b)?

You can't in general because there is different code for False and True, whereas an instance for C (F b) would have to be the same code for both.

Ah, thanks, that's obvious in hindsight.

But I realised my question was "wrong" - I actually have:
F - type family, closed and total over Bool
G - type family, associated with a type class - don't have "control" over this one
I know that G (F 'False) is the same as G (F 'True)
Can I show that C (G (F b))?

I don't think so, unless G somehow makes a singleton on b available. If it truly is the same code, why would the case split be necessary in the first place?

F 'False /= F 'True, and I do use this (a lot of types are the same except for small bits, and I use type families like F to make the small bits different)
but G (F 'False) == G (F 'True), and G isn't a constant for all types in general (and I can't touch it, it's in a library)

There's this idea about coproducts for instances in https://github.com/rampion/constraint-unions, although it didn't work out for my use case when I tried it. It might work for yours though

there is a dumb trick to doing this

sfoo is the proof that C is closed for booleans

thanks - using the Dict trick to be able to pattern match on the singleton did the job

I guess this also works:

withSBool :: SBool b -> (C (F b) => r) -> r
withSBool sing k =
  case sing of
    STrue -> k
    SFalse -> k