<div dir="ltr"><div dir="ltr"><br></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Sep 11, 2020 at 6:19 PM Anthony Clayden <<a href="mailto:anthony_clayden@clear.net.nz">anthony_clayden@clear.net.nz</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div><font face="monospace"><br></font></div><div><font face="monospace">So it's the same type `a` all the way down, and therefore the same instance for the constraint(s). Consider (adapted from the H98 Report for DatatypeContexts):</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">    {-# LANGUAGE  GADTs    #-}</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">    data SetG a  where<br>      NilSetG  :: Eq a => SetG a<br>      ConsSetG :: Eq a => a -> SetG a -> SetG a<br></font></div><div><font face="monospace"><br></font></div><div><br></div><div><font face="monospace">    elemSG x NilSetG                     = False<br>    elemSG x (ConsSetG y ys) | x == y    = True<br>                             | otherwise = elemSG x ys<br></font></div><div><font face="monospace">      -- ===> elemSG :: a -> SetG a -> Bool           -- no Eq a inferred<br></font></div><div><font face="monospace"><br></font></div><div><font face="monospace">The elem pattern matching test makes use of ConsSetG's Eq instance, but doesn't expose that in the inferred type. Whereas:</font></div><div><font face="monospace"><br></font></div><font face="monospace">    headS (ConsSetG x _) = x         -- hide the pattern match<br>    tailS (ConsSetG _ xs) = xs<br></font><div><font face="monospace"><br></font></div><div><font face="monospace">    elemSh x NilSetG                     = False<br>    elemSh x yss        | x == headS yss = True<br>                        | otherwise      = elemSG x $ tailS yss<br></font></div><div><font face="monospace">      -- ==> elemSh :: Eq a => a -> SetG a -> Bool        -- Eq a inferred<br></font></div><div><font face="monospace"><br></font></div><div><br></div></div></blockquote><div><br></div><div>It seems you can get there with PatternSynonyms, using an explicit signature with 'required' constraints:</div><div><a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms">https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms</a><br></div><div><br></div><div>    pattern ConsSetPS x yss = ConsSetG x yss<br>    -- inferred pattern ConsSetPS :: () => Eq a => a -> SetP a -> SetP a  -- that is, if no sig given<br></div><div><br></div><div>Using `ConsSetPS` as the pattern in `elemSG` with that default/inferred signature gives the same typing as using the GADT constructor. But with explicit signature</div><div><br></div><div>    pattern ConsSetPS :: Eq a => a -> SetG a -> SetG a</div><div>    --                      longhand :: Eq a => () => a -> SetG a -> SetG a</div><div><br></div><div>The 'required' `Eq a` is exposed, so `elemSG` gets the same signature as `elemSh` above.</div><div><br></div><div>After all, if you're trying to maintain an invariant, you'd be using a PatternSynonym as 'smart constructor' to validate uniqueness; so giving it a signature (and hiding the GADT constructor) is easy enough.</div><div><br></div><div>Would be nice to be able to give pattern-style signatures for GADT constructors. Unfortunately, the sigs for `ConsSetG` and `ConsSetPS` look the same but mean the opposite way round.</div><div><br></div><div><br></div><div>AntC</div></div></div>