on *Tue Sep 1 21:18:40 UTC 2020, Richard Eisenberg wrote:* I see the core idea as a fairly straightforward generalization of the > "Partial Type Constructors" work -- except that I wouldn't phrase any of > this as "floating out".

Thanks Richard, but no: I see this as exploring what was the idea in that brief example in the 1990 Report. (It's very vague, so we're all speculating.) The example there is a type synonym, which the PTC work doesn't consider. And putting the constraint syntactically before the type (synonym/data/new) name suggests to me it's 'outer'. GHC actually can express a bit what I mean by "floating out". I didn't realise that at the time of writing the O.P., so I'll rework the example. I'm correcting it because as you say:

In a few places, you've expanded Point a as Num a => (a, a). But Point a is *not* the same thing as Num a => (a, a). Indeed, you didn't define it that way. ...

The library supplier writes: {#- LANGUAGE RankNTypes #-} type Num a => Point a = (a, a) -- proposed mkPoint :: a -> a -> Point a -- pretend to hide the constructor mkPoint x y = (x, y) -- no using numeric ops/no Num needed The compiler expands the synonym to mkPoint :: a -> a -> Num a => (a, a). Note no parens around the expansion, unlike my O.P. That expansion is not valid H98, but it is valid in GHC with RankNTypes. The docos say it's a Rank-1 type. GHC infers mkPoint :: Num a => a -> a -> (a, a) And that's why I call it "floating out". Longer example below. The idea is the library writer could later change the implementation to a datatype or a newtype, etc; or even add a further constraint. They all carry the constraint(s) 'outer'; the client code doesn't need to know about the change.

Instead, we should understand Point a to expand to (a, a) only when Num a holds.

That might be a valid use case (especially for constrained classes/type families); but it's not the use case I have in mind.

So, the occurrence of Point a causes a Num a constraint to arise. These Num a constraints then get put into the type. No floating.

We all think the 1991 DatatypeContexts design is daft because it raises wanted constraints but doesn't "put" them anywhere, so the client-module programmer has to add them explicitly in signatures. To improve that, where/how should the compiler "put into the type"? The client writes scale :: a -> Point a -> Point a -- expand the synonyms; then float out and squish duplicates -- ===> scale :: a -> Num a => (a, a) -> Num a => (a, a) -- no parens added -- ===> scale :: Num a => a -> (a, a) -> (a, a) The 'no parens' step (different to my O.P.) is valid GHC with RankNTypes; the last step is as GHC infers today, with Num a floated out. (Or if you don't like that phrase: "canonicalises", "simplifies"?)

Note that types like `(Num a => a) -> a` and `Num a => a -> a` (both very valid today) mean quite different things,

Yes; although the first isn't valid H98/wasn't valid in 1990; and I'm struggling to think of a use case for it, noting there's no existential quant inside the parens. (It's not Rank-2, but is it plain Rank-1 or Rank-1-and-a-half?) Anyhoo that was an error on my part.

I think by rephrasing this without floating, we avoid the trouble with existentials, etc., that you are worried about.

I'm not sure on that, but we'll leave it for another day.

Personally, I would tack this onto "Partial Type Constructors" instead of trying to make this happen independently, but the two features would go nicely together.

PTCs introduce a lot of heavy machinery; whereas I'm thinking of this as just-below-the-surface syntactic sugar that gets expanded before type inference. OTOH this doesn't on its own support `instance Functor Point`, treating the type synonym as an unapplied constructor -- which is what the Hughes 1999 paper is tackling. (I have an idea how that could go using this same syntactic expansion idea.) Note BTW, that I didn't add any constraints to the data constructors -- which is all the 1991 design does (and that not consistently). Constructing a `Point` doesn't need any Num ops/methods. But the type is supplying a wanted Num a 'outside', because any expression operating on a Point likely uses arithmetic. Constraints on data constructors (as with GADTs) I see as orthogonal: there will be use cases for one alone, the other alone, or both combined. AntC