On Fri, Sep 11, 2020 at 6:19 PM Anthony Clayden < anthony_clayden@clear.net.nz> wrote:
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):
{-# LANGUAGE GADTs #-}
data SetG a where NilSetG :: Eq a => SetG a ConsSetG :: Eq a => a -> SetG a -> SetG a
elemSG x NilSetG = False elemSG x (ConsSetG y ys) | x == y = True | otherwise = elemSG x ys -- ===> elemSG :: a -> SetG a -> Bool -- no Eq a inferred
The elem pattern matching test makes use of ConsSetG's Eq instance, but doesn't expose that in the inferred type. Whereas:
headS (ConsSetG x _) = x -- hide the pattern match tailS (ConsSetG _ xs) = xs
elemSh x NilSetG = False elemSh x yss | x == headS yss = True | otherwise = elemSG x $ tailS yss -- ==> elemSh :: Eq a => a -> SetG a -> Bool -- Eq a inferred
It seems you can get there with PatternSynonyms, using an explicit signature with 'required' constraints: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... pattern ConsSetPS x yss = ConsSetG x yss -- inferred pattern ConsSetPS :: () => Eq a => a -> SetP a -> SetP a -- that is, if no sig given 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 pattern ConsSetPS :: Eq a => a -> SetG a -> SetG a -- longhand :: Eq a => () => a -> SetG a -> SetG a The 'required' `Eq a` is exposed, so `elemSG` gets the same signature as `elemSh` above. 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. 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. AntC