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.) type Num a => Point a = (a, a) 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: origin :: Point Integer -- we get Num a => wanted then discharged for free origin = (0, 0) -- although the appearance of zero wants Num a anyway scale :: (Num a) => a -> Point a -> Point a -- seems wrong to give explicit Num a scale w (x,y) = (w*x, w*y) -- the above sig would be inferred anyway The feature disappeared without trace in the next year's Language report. I'm thinking we should be able to write scale :: a -> Point a -> Point a -- get Num a for free by: scale :: a -> (Num a => (a, a)) -> (Num a => (a, a)) -- expand the synonym -- this sig currently illegal scale :: Num a => a -> (a, a) -> (a, a) -- float the constraints out to the implicit forall 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: typePoint :: Num a => (a, a) typePoint = undefined scale w xy = const (undefined `asTypeOf` xy `asTypeOf` typePoint) (w `asTypeOf` fst xy) -- inferred scale :: Num a => a -> (a,a) -> (a,a) (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.) 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. A couple of caveats: * Haskell 1990 didn't have MultiParam Type Classes; * nor existential quant. 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. 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.) Or is there something deeply anti-System FC here? AntC