Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
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
F :: Bool -> Type
(how) Can I show ghc that there is an always an instance for C (F b)?
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))?
G (F 'False)
G (F 'True)
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
data SBool a where
STrue :: SBool 'True
SFalse :: SBool 'False
data Dict c where
Dict :: c => Dict c
sfoo :: SBool a -> Dict (C a)
sfoo STrue = Dict
sfoo SFalse = Dict
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