I also like the proposal; however, I think it only makes sense if the set of unbound variables with the same name is treated as referring to the same identifier. This was, after all, the main reason for named holes. Roman expected this, and I think everybody who uses the feature will expect it. It would be endlessly confusing to have identifiers that look the same but aren't. I agree that occurrences of an unbound variable with the same name can be thought of as being the same identifier -- but I do not agree that means that each occurrence need have the same type. Consider f x = (undefined && True, ord undefined) There are two occurrences of 'undefined', but one has type Bool, and the other has type Char. is that endlessly confusing? I think that each hole *must* be independent, and effectively must have type (forall a.a), just like undefined. Otherwise you get into real difficulties about how polymorphism is affected because we don't know how far out the sharing happens. I don't think type sharing is a good reason for named holes -- indeed I think that trying to specify what sharing might mean would be plain confusing. Instead, I'm proposing this simple design * If there is no binding for "x", "_x" or "foo_x" then they are unbound variables * With a suitable flag, any unbound variable is treated as a hole, with each occurrence having a separate type. That is, it's just as if there was a top level binding for the variable saying foo_x :: forall a. a; foo_x = error "foo_x is undefined", except that the compiler reports the type of each occurrence of a hole. * Our current holes "_" are just a degenerate case of the above. Simple, uniform, explainable. Simon