Re: [Haskell-cafe] Constraints as a moveable feast?

On Sep 2, 2020, at 10:18 PM, Anthony Clayden wrote:

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". Yes, but what about

pointX :: Point a -> a pointX (x, _) = x

? We don't want that type to expand to (Num a => (a, a)) -> a.

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"?)

Ah. Now I see a bit more of what you're getting at. But I really don't know what it means to expand without adding parens. Expanding a type synonym is an operation on an abstract syntax tree (AST). We often write ASTs by just writing out concrete syntax, and this sometimes requires adding parens. Even so, we're really just operating with ASTs -- and I don't think your "expand without parens" operation is defined on ASTs. For example:

data a + b = Inl a | Inr b foo :: Point a + Point b

I can't imagine we want to expand this to

foo :: Num a => (a, a) + Num b => (b, b)

which, under usual rules of precedence, becomes

foo :: Num a => ((a, a) + Num b) => (b, b)

Note how the + binds tighter than the =>. Richard