My proof-of-concept for this as of last year was flaky. I think I've now
got it robust:
- all DatatypeContexts apply for all constructors, irrespective of which
type params the constructor mentions;
- If a data constructor+fields appears in a pattern match, no constraints
inferred;
- whether using positional or labelled field syntax;
- using field labels as selectors also doesn't infer constraints (they're
as-if pattern matching);
- numeric literals in patterns do raise a Num/Integral/Fractional
constraint ...
- ... even if nested inside a data constructor. (That's something I broke
back in October.)
It turned out to only need a few lines of code added to the compiler. It
was finding _where_ to position them that needed a huge amount of trial and
error.
Back to the glorious GHC 1999 (and even pre-1991) future! And "Bleah!"
right back to Wadler.
AntC
On Mon, 11 Oct 2021 at 19:40, Anthony Clayden
There's a discussion in May 1999 pointing out the H98 Report is "inexplicit" wrt the semantics of pattern matching on datatypes with a context.
http://web.archive.org/web/20151208175102/http://code.haskell.org/~dons/hask..., 'Contexts on datatype declarations', starting at SPJ's opener.
The Report has this example, section 4.2.1:
data Eq a => Set a = NilSet | ConsSet a (Set a) -- with inferred types -- NilSet :: forall a. Set a -- ConsSet :: forall a. Eq a => a -> Set a -> a
(If, per Wadler's response, he thinks "a type will make no sense without the constraints", what sense is there in having a `NilSet` without constraints?)
Ref the q SPJ poses, it's _not_ the case that a selector function always gets the constraint inferred. (As of Hugs 2006 and GHC 8.10.)
If a selector function pattern matches on `ConsSet`, `Eq a =>` is indeed inferred. But if matching on only `NilSet`, or only on a bare var/wildcard pattern, no constraint. (In practice of course you would be matching on `ConsSet`, so this point is purely academic.)
Anyhoo, this behaviour doesn't deliver Wadler's objective. And I find it weird you have to look at the term level to explain the type. Since `data Eq a => ...` prefixes the type and constructors, I'd expect the behaviour to apply at _type_ level.
If I bend Hugs to behave same as-was GHC (no constraint inferred if purely matching), I get the benefit I can declare instances for constructor classes (including Foldable) over type constructor `Set`. Whereas the post-May 199 behaviour disallows this: pattern matching in the method decls wants an `Eq a =>`, but there's no means to pass in a dictionary.
I can't declare a Functor instance, because building the result applies the data constructors, so does want a dictionary; again there's no means to pass one in. I can simulate `fmap` via Foldable's `foldMap`, because that wants a Monoid instance for the builder, and that does see the element type as well as the constructor. (The builder can squish out resulting duplicates, so preserving the invariant of `Set`.) Not being able to declare `Set` an instance of Functor is a Good Thing. Nor of Monad https://mail.haskell.org/pipermail/haskell-cafe/2004-March/005995.html
As SPJ points out later in the 1999 thread
But when you take a constructor *apart*, the invariant must hold by construction: you couldn't have built the thing you are taking apart unless invariant held. So enforcing the invariant again is redundant; and in addition it pollutes the type of selectors.
(I note GHC's Pattern Synonyms seem to have fallen into the same hephalump trap of polluting constraints for matching with constraints needed only for building.)
If you're thinking "but hasn't GHC solved all this with GADTs?" I say no: their sweet spot is where there's different constraints down the structure; you can't help but hold a different dictionary at each node and 'Provide' it on pattern matching. Whereas for `Set` it's crucial you have exactly the same constraint 'all the way down', and all nodes type `Set a`.
I can (just about) see use cases for datatypes that both have global contexts and GADT constructors.
AntC