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