Re: [Haskell-cafe] data kinds and exhaustiveness of typeclass instances

3 Mar 2021


      To "more directly" do the same thing as in coq, you can also take the
singletons approach, and either explicitly use a "proof providing" function:

withC :: STag t -> (C (Foo t) => r) -> r
withC tag k =
  case tag of
    SA -> k
    SB -> k

(so if you call `withC tag body` you now have the required constraint in
`body`

or you could use the implicit singleton carrying type class:

instance STagI t => C (Foo t) where
  f =
    case tagSing of
      SA -> f
      SB -> f

and the remaining boilerplate code required:

data STag t where
  SA :: STag A
  SB :: STag B

class STagI t where
  tagSing :: STag t

instance STag A where
  tagSing = SA

instance STag B where
  tagSing = SB

Re: [Haskell-cafe] data kinds and exhaustiveness of typeclass instances

Georgi Lyubenov