…f type variables during singling]

Now that goldfirere/th-desugar#199 has been fixed,
`singletons-th` can always guarantee that the type variable specificities that
it reifies will be accurate. As such, all of wrinkle 2 in `Note [Preserve the
order of type variables during singling]` is moot, so this PR deletes this
wrinkle entirely. Wrinkle 3 has now been renamed to wrinkle 2.

What was formerly known as wrinkle 3 is mostly kept the same, although I have
expanded upon it a little to clarify what we single data constructors such as
`Nothing :: forall a. Maybe a` to `SNothing :: forall a. SMaybe (Nothing ::
Maybe a)` rather than, say, `SNothing :: forall a. SMaybe (Nothing @A)`. For
instance, imagine if `a` was inferred rather than specified!

I have added a `T565` test case which ensures that `singletons-th` generates
valid code for the case when a data constructor uses an inferred type variable
binder. I have also added an addendum to the `README` noting that
`singletons-th` does not currently support `AllowAmbiguousTypes` at all, which
would be perhaps the one convincing argument in favor of using explicit kind
applications when singling return types (rather than explicit return kinds).

Fixes #565.