I don't have terribly much to add, but I do want to counter one point:
On Oct 28, 2015, at 5:48 AM, Edward Kmett
There are situations where we are truly polymorphic in lifting, e.g. (==) from Eq and compare from Ord don't care if the arguments of type 'a' are lifted or not.
But these do, I think. In running code, if (==) is operating over a lazy type, it has to check if the pointer points to a thunk. If (==) is operating over a strict one, it can skip the check. This is not a big difference, but it *is* a difference. A little more thinking about this has led here: The distinction isn't really forall vs. pi. That is, in the cases where the levity matters, we don't really need to pi-quantify. Instead, it's exactly like type classes. Imagine, for a moment, that we have an alternate universe where strict is the default, and we have
data Lazy a = Thunk (() -> a) | WHNF a
The WHNF is a bit of a lie, because this representation would mean that the contents of a WHNF are fully evaluated. But let's not get hung up on that point. Then, we have
type family BaseType a where BaseType (Lazy a) = a BaseType a = a
class Forceable a where force :: a -> BaseType a
instance Forceable a where force = id
instance Forceable (Lazy a) where force (Thunk f) = f () force (WHNF a) = a
Things that need to behave differently depending on strictness just take a dictionary of the Forceable class. Equivalently, they make a runtime decision of whether to force or not. So we don't need an exponential number of maps. We need a map that makes some runtime decisions. And the optimizer can be taught that specializing these decisions may be helpful. Of course, none of this would be exposed. And I'm not suggesting that we need to make the core language strict-by-default. But it clarified things, for me at least, when I realized this is regular old ad-hoc polymorphism, not something fancier. Richard