Have you seen http://lambda-the-ultimate.org/node/1635 (Lightweight static capabilities)? Author's page: http://okmij.org/ftp/Computation/lightweight-dependent-typin...