<div dir="ltr"><div>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:<br><br>withC :: STag t -> (C (Foo t) => r) -> r<br>withC tag k =<br>  case tag of <br>    SA -> k<br>    SB -> k<br><br>(so if you call `withC tag body` you now have the required constraint in `body`<br><br>or you could use the implicit singleton carrying type class:<br><br>instance STagI t => C (Foo t) where<br>  f =<br>    case tagSing of<br>      SA -> f<br>      SB -> f<br><br>and the remaining boilerplate code required:<br><br>data STag t where<br>  SA :: STag A<br>  SB :: STag B<br><br>class STagI t where<br>  tagSing :: STag t<br><br>instance STag A where<br>  tagSing = SA<br><br>instance STag B where<br>  tagSing = SB</div><div><br></div></div>