Constraints on type synonyms

[Anthony Clayden]

Consider

>    pattern PPoint :: Floating a => a -> a -> (a, a)   --  => ()
>    pattern PPoint x y = (x, y)
>    originP = PPoint 0 0
>    scaleP w (PPoint x y) = PPoint (w*x) (w*y)

Inferred `scaleP :: Floating a => a -> (a, a) -> (a, a)` -- so more
restrictive than the `Num a` that would be inferred usually for `scaleP`'s
`(*)` operator.

Ok what's the type-level analogue for `PPoint`, so that I can give
signatures, instances, etc for methods using it? The type is not this:

>    type CPoint a = Floating a => (a, a)

(Needs `RankNTypes` to put a constraint in RHS of a type synonym.) This
seems to get accepted:

>     scaleP :: a -> CPoint a -> CPoint a

Inferred `scaleP :: Floating a => a -> CPoint a -> (a, a)` -- that
un-expanded `CPoint a` hints at a lurking danger. I couldn't for example
write the equation for `scaleP` with a type annotation

>    scaleP w (PPoint x y) = PPoint (w*x) (w*y) :: CPoint a

Despite the annotation giving the result type exactly per the signature,
this gives 'rigid type variable' rejections. This works (needs
`ScopedTypeVariables`)

>    scaleP (w :: a) (PPoint x y) = PPoint (w*x) (w*y) :: CPoint a

What I especially want is instances and constraints:

>    instance C1 (CPoint a)              --     * Illegal qualified type:
Floating a => (a, a)
>                                            --     * In the expansion of
type synonym `CPoint'
>    instance (C1 (CPoint a)) => C2 a  --    * Illegal qualified type:
Floating a => (a, a)
>                                            --      GHC doesn't yet
support impredicative polymorphism

(Needs `FlexibleInstances` to appear in the instance head,
`FlexibleContexts` to appear in the constraint.) But I don't want to embed
a qualified type in the instance head nor constraints, I want the expansion
to be

>    instance (Floating a) => C1 (a, a)
>    instance (C1 (a, a), Floating a) => C2 a

It's kinda the constraint is 'outside' the constructed type; as if the
synonym were given by

>    type (Floating a) => CPoint a = (a, a)

With the idea that when the compiler is expanding `CPoint a`, it floats the
associated constraint out to the context the synonym call appears in. That
is, I'm treating the expansion as very early in the compiler pipeline, just
after syntax checking, before type inference/checking.

If that constraint-outside syntax in the type synonym decl seems familiar,
you might have seen it discussed briefly in [Jones, Morris, Eisenberg 2020
Partial Type Constructors], Section 7 Related Work 'Datatype contexts in
Haskell'. Let me emphasise I'm talking here about type synonyms _not_
Datatypes.

That constraint-outside syntax got rejected very early in the history of
Haskell, apparently because nobody could give an adequate specification. Is
my expand-it-as-syntax proposal not viable?

AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20210621/d8166bbf/attachment.html>