Hello,

So we need rank-2 type in runST :: (forall s. ST s a) -> a, to prevent s from appearing in a.

I have been thinking about this for a bit, but I failed to come up with a practical situation, where rank-3 types are necessary for safety of some abstraction.

The rank-3 example in here and any other I found, look very synthetic, i.e. limiting computation to id:
https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html

and compared to the runST example of limiting a scope of a type variable for purposes of safety looks unnatural.

Could anyone please point me to a practical example of rank-3 polymorphism, where it is necessary for safety of an abstraction, if it exists?

I suspect there is a situation, where rank-3 is necessary for maintaining abstration exists, but I can't think of any.

Any ideas about such situations and even better situations where this is used on hackage?

Timotej Tomandl