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 familyF :: Bool -> Type
.I have instances of
C
for bothF 'False
andF '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
andTrue
, whereas an instance forC (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 overBool
G
- type family, associated with a type class - don't have "control" over this oneI know that
G (F 'False)
is the same asG (F 'True)
Can I show that
C (G (F b))
?I don't think so, unless
G
somehow makes a singleton onb
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 likeF
to make the small bits different)but
G (F 'False)
==G (F 'True)
, andG
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: