Define Σ as a partial application of Sigma

[RyanGlScott]

Having to create defunctionalization symbols for Σ is annoying since morally, Σ ought to be defined as a simple partial application of Sigma, like so:

type Σ = Sigma

Until recently, I thought doing so was impossible due to GHC restrictions (see Trac #13408). But as it turns out, I was mistaken. There is actually an extremely straightforward way to make the above definition kind-check: just enable ImpredicativeTypes!

This patch implements that suggestion, and since the defunctionalization symbols for Σ are no longer necessary, I have removed them. In the event that someone ever fixes Trac #13408, we can remove the use of ImpredicativeTypes, so I have added a Note reminding us to do so should the time ever come.

[goldfirere]

Σ will also be able to be written once forall ... -> syntax is supported.

Sadly, until then, I agree that this should be merged, just to allow forward movement.