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

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 oneI 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 booleansthanks - using the

`Dict`

trick to be able to pattern match on the singleton did the jobI guess this also works: