|Oh now i see what you mean: consider | f' = abst . (id :: (d->a)->(d->a)) . appl |which GHC understands to mean | f' = abst . (id :: forall d a. (d->a)->(d->a)) . appl | |GHC infers the type | f' :: (Fun d) => Memo d a -> Memo d a |Now you are saying that GHC *could* have figured out that if it added the signature | f' :: forall d a. (Fun d) => Memo d a -> Memo d a |thereby *changing* the scoping of d,a in the buried signature for 'id', doing so would not change whether f' was |typeable or not. Well maybe, but that is way beyond what I have any current plans to do. Indeed!-) I didn't mean to suggest this as a course of action, it was just a way of representing the internal type inference intermediates at source level. Another aspect I would not like about this approach is that renamings of bound type variables would no longer be meaning- preserving (because the signature would be interpreted in the context of the source-code it belongs to) - not good. But the core part of my suggestion (which this example was meant to help explain) remains attractive, at least to me: somewhere during type inference, GHC *does* unify the *apparently free* 'd' with an internal type variable (lets call it 'd1, as in the type error message) that has no explicit counterpart in source code or type signature, so the inferred type should not be f' :: forall d. (Fun d) => Memo d a -> Memo d a -- (1) but rather f' :: forall d. (Fun d,d~d1) => Memo d a -> Memo d a -- (2) That way, the internal dependency would be made explicit in the printed representation of the inferred type signature, and the unknown 'd1' would appear explicitly in the inferred type, not just in the error message (the explicit foralls are needed here to make it clear that 'd1' and by implication, 'd', *cannot* be freely generalized - 'd' is qualified by the equation with the unknown 'd1'). To me, (2) makes more sense as an inferred type for f' than (1), especially as it represents an obviously unusable type signature (we don't know what 'd1' is, and we can't just unify it with anything), whereas (1) suggests a useable type signature, but one that will fail when used: Couldn't match expected type `Memo d1' against inferred type `Memo d'. All I'm suggesting is that the type *printed* by GHCi does not really represent the type *inferred* by GHCi (or else there should not be any attempt to match the *free* 'd' against some unknown 'd1', as the error message says), and that there might be ways to make the discrepancy explicit, by printing the inferred type differently. Claus