instead of introducing holes in types and contexts to leave parts of a declaration unspecified, why not use type subsumption?
it has been pointed out to me that I should be more specific about what I mean with this suggestion (not least to ensure that I don't suggest to use subsumption the wrong way round, thanks!-): - first, subsumption: (P => t) subsumes (Q => r) iff exists substitution th. (r = th(t) && th(P) |- Q) [where |- is entailment between sets of predicates] in words: a qualified type qt1 is subsumed by a qualified type qt2 (we write: qt1 <= qt2) precisely if qt1 is a substitution instance of qt2 whose constraints are implied by the substition instance of qt2's constraints. - next, its use for partial type declarations: a qualified type is subsumed if its type part is more specific, and its constraint part is implied. so we could declare a qualified type for an expression that, instead of being the precise type of said expression, only has to be subsumed by the inferred expression type: we write (expr :<: qt_partial) iff: (expr :: qt) and (qt_partial <= qt). that means that the precise type can be more specific (variables instantiated), have more constraints (as long as the ones given are implied) and even different constraints (eg., of subclasses, or of other constraints that imply the ones given). this accounts for uses of placeholders (_) in both types and constraints in the alternative option. note that, currently, declarations can already be more specific than the inferred type: f :: Int -> Int -> Int f x y = x+y partial type declarations would permit us to declare types that are more general than the inferred type, allowing us to omit type info that we want to leave inferred (or specifying part of a type without having to specify all of it): f :<: Int -> a -> Int or f :<: Int -> a or f :<: Fractional a => a -> a -> a pro: would easily allow for omission of type details or parts of context (a type with more context, or with more specific type components, is subsumed by the declaration) cons: while this accounts for the explicit parts of the alternative option (_), that option implicitly assumes that other type variables cannot be instantiated, and that contexts without _ cannot be extended. as long as we only specify an one-sided bound, the inferred type could be more specific than we'd like (we can't say that we don't want context, or that some type variable must not be instantiated) hope I got it the right way round this time? claus ps. I can't find the original thread, but this came up again last year, and Oleg suggested, that for the special case of function signatures, the same effect could be had by adding extra fake clauses (similar to fake clauses commonly used for trace or seq): http://haskell.org/pipermail/haskell-cafe/2004-August/006606.html this does not work for other places where type declarations are required, but would be awkward or impossible to give in full, but at least for functions, Oleg's fake clauses might be a possible desugaring (unless our clever optimising compiler removes them as dead code;-): -- f' :: Int -> a -> Int -- f' :: Int -> a -- f' :: Fractional a => a -> a -> a f' :: Eq a => c -> b -> a f' = undefined f x y | False = f' x y f x y = x+y