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

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Georgi Lyubenov // googleson78

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.

Georgi Lyubenov // googleson78

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?

Georgi Lyubenov // googleson78

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)

Asad Saeeduddin

There's this idea about coproducts for instances in, although it didn't work out for my use case when I tried it. It might work for yours though

A syntax for unions of constraints in Haskell. Contribute to rampion/constraint-unions development by creating an account on GitHub.
Sandy Maguire

there is a dumb trick to doing this

Sandy Maguire
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
Sandy Maguire

sfoo is the proof that C is closed for booleans

Georgi Lyubenov // googleson78

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

Georgi Lyubenov // googleson78

I guess this also works:

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