
3 Mar
2021
3 Mar
'21
7:14 a.m.
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