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

Georgi Lyubenov godzbanebane at gmail.com
Wed Mar 3 07:14:47 UTC 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

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210303/cf072a6b/attachment.html>

More information about the Haskell-Cafe mailing list