Lambda the Ultimate

Hi,

It's a call for kind help; in the form of more relevant pointers I seemingly have missed so far.

I am looking for authoritative reference materials about what people sometimes people refer to as "precise types" (in the programming languages ontology, preferably).

As most people on these forums I suppose, I believe I have grasped a fair enough notion of what we usually mean by static typing (as opposed to the dynamic side of things). The understanding situation on my end is way less comfortable re: "precise types".

I did try to read quite a bit of resources on typing systems and the corresponding, traditionally associated calculi schemes, and their respective, supporting nomenclatures, and I did stumble a couple times upon various phrasings of what the author is alluding to by his/her "precise types", but without really seeing a blindingly obvious common agreement and shared understanding of what is really meant, unambiguously, in a standard fashion by that : "precise types". It still seems to vary significantly from one author to the other.

For one thing, would that be an absolute notion for the qualifying criteria (like, e.g., when opposing a terminating vs. a non-terminating program, or inhabited vs. non-inhabited types, or confluent vs. non-confluent term rewriting systems, etc) or would that be something relative, with type systems offering features to denote "more or less" precise types ?

For another parallel, the signification of the difference (and implications) between the untyped lambda calculus and the many typed lambda calculi flavors one can devise are well understood today. I was expecting the case to be the same when one speaks of (more or less) strongly type systems, offering static type check convenience features but NOT qualifying as being frameworks for precise types, as opposed to the ones which do so. Therefore : if precise types are well understood today, which are the properties that the meta language / logical framework is supposed to have for one to be able to check about the precise types' inhabitation, its helper algorithms, etc, within the type system being defined or scrutinized ?

Thus, does someone know if "precise types" has been given a clearly delimited (small) set of definitions in the process of converging together, or is it still mostly left open to one's context of work (be it on type inference and/or just type checking, or etc) ?

If my question happens to be too much open for today's state of knowledge, I can provide what I (would like to) understand by the usage of the "precise type" phrase, say, in the specific context of static type inference during some compilation/translation process.

Thank you in advance for any relevant pointers.