State-Dependent Representation Independence

This paper and its related papers shown below, focus on such a problem that, if an general type system can be augmented by local state to further improve it precision without sacrify decidability?

So if this tech is a special case of my idea that combine cheap hinder-milner type system in clasical ML with an expensive counterexample guided refinement based type inference on those potential type error?

For example, a type T has 2 type constructor A and B, for a list of element T, I filter out all those with constructor A, to generate a list l_A, so when enumerating l_A, I only need to process constructor A,not for B.

I general ML, this will raise an incomplete warning, but I can rule it out with refinement.

Ahmed. Step-indexed syntactic logical relations for recursive and quantified types.
Syntactic logical relations for polymorphic and recursive types
Recursive polymorphic types and parametricity in an operational framework.
Typed operational reasoning.
Selective strictness and parametricity in structural operational semantics, inequationally.