The idea of treating !S as a subtype of S and then relying on the potential for new impredicativity machinery to let us just talk about how !S <= S makes me really happy.
data Nat = Z | S !Nat
Pattern matching on S could give back the tighter type !Nat rather than Nat for the argument, and if we ever have to show that to a user, the 'approximation' machinery would show it to users as Nat, concealing this implementation detail. Similarly matching with an as-pattern as part of a pattern that evaluates could do the same.
The constructor is a bit messier. It should really give back S :: Nat -> Nat as what the constructor should behave as rather than S :: !Nat -> Nat, because this will match existing behavior. Then the exposed constructor would force the argument before storing it away, just like we do today and we could recover via a sort of peephole optimization the elimination of the jump into the closure to evaluate when it is fed something known to be of type !Nat by some kind of "case/(!)-coercion" rule in the optimizer.
I'm partial to those parts of the idea and think it works pretty well.
I'm not sure how well it mixes with all the other discussions on levity polymorphism though. Notably: Trying to get to having !Nat live in an Unlifted kind, while Nat has a different kind seems likely to cause all sorts of headaches. =/
-Edward