<div dir="ltr">There's the makings of a cute feature in a very old Haskell Language report. (With thanks to the 'Partial Type Constructors' 2019 paper for ferreting this out.)<div><br></div><div>    type Num a => Point a = (a, a)</div><div><br></div><div>1990 v1.0 Haskell report. Yes that's a type synonym with a constraint. I'll give their examples, though they don't really demonstrate the potential:</div><div><br></div><div>    origin :: Point Integer                                         -- we get Num a => wanted then discharged for free<br>    origin = (0, 0)                                                       -- although the appearance of zero wants Num a anyway<br><br>    scale :: (Num a) => a -> Point a -> Point a     -- seems wrong to give explicit Num a<br>    scale w (x,y) = (w*x, w*y)                                  -- the above sig would be inferred anyway<br></div><div><br></div><div>The feature disappeared without trace in the next year's Language report.<br></div><div><br></div><div>I'm thinking we should be able to write</div><div><br></div><div>    scale :: a -> Point a -> Point a                             -- get Num a for free by:</div><div>    scale :: a -> (Num a => (a, a)) -> (Num a => (a, a))           -- expand the synonym -- this sig currently illegal</div><div>    scale :: Num a => a -> (a, a) -> (a, a)                  -- float the constraints out to the implicit forall</div><div><br></div><div>So this isn't specific to type synonyms: in general allow prefixing constraints to any sub-term in a type; type inference floats them to the front of the signature. You can kinda get the effect today (so I don't think this is entirely whacky), by cunning use of dummies and term-level combinators:</div><div><span style="font-family:Arial,Helvetica,sans-serif"><br></span></div><div><span style="font-family:Arial,Helvetica,sans-serif">    typePoint :: Num a => (a, a)</span><br></div>    typePoint = undefined<br><div><br></div><div>    scale w xy = const (undefined `asTypeOf` xy `asTypeOf` typePoint) (w `asTypeOf` fst xy)<br></div><div>    -- inferred <span style="font-family:Arial,Helvetica,sans-serif">scale :: Num a => a -> (a,a) -> (a,a)</span></div><div><br></div><div>(Putting a dummy undefined on RHS to show there's nothing up my sleeves, because the actual expression would unify to the right type anyway.)</div><div><br></div><div>You can get maybe cleaner code with PatternSignatures. But it's all workarounds in terms/expressions. I want to do the Right Thing and get it accepted as a stand-alone signature.</div><div><br></div><div>A couple of caveats:</div><div>* Haskell 1990 didn't have MultiParam Type Classes;</div><div>* nor existential quant.</div><div><br></div><div>So if a nested constraint mentions both an existential tyvar with narrow scope and a universally quant'd tyvar, can't float out that constraint, have to reject the sig.</div><div><br></div><div>The constraint in `type Num a => Point a = ...` appearing to the left of the introduced type syn, is also reminiscent of DatatypeContexts, so we could similarly float out the constraints from those appearing within a sig(?) And this would be a way to put constraints on newtypes similarly(?) (Can't put constraints on those currently, because there's not really a data constructor to bind the class dictionary to. Haskell 1990 didn't have newtypes.)</div><div><br></div><div>Or is there something deeply anti-System FC here?</div><div><br></div><div>AntC</div></div>