Add support for equalities between sigmas

Currently Ct is just a Q tagged with a flavour, and the constraint solver can only handle equalities between Qs (taus). This is very limiting and wouldn't let us infer a rho for multiple match-expressions. Example:

-- f : Bool -> (forall a. a -> a -> a) -> Bool -> Int -> Bool
f True  = \(x :: forall a. a -> a -> a) -> \y           -> \(z :: Int) -> True
f False = \(x :: forall a. a -> a -> a) -> \(y :: Bool) -> \z          -> True

The above example should be accepted, which will only happen if we make Cts more expressive.

Have a look at: Allow multiple case branches to have a higher rank type