Improve instantiation of datacons

This ticket tracks a possible improvement to return_data_con.

When typechecking a datacon T, do we instantiate its arguments? We'd like to avoid instantiation, because it breaks VTA.

Currently, we instantiate levity-polymorphic constructors. Quoting Note [Linear fields generalization]:

A small hitch: if the constructor is levity-polymorphic (unboxed tuples, sums,
certain newtypes with -XUnliftedNewtypes) then this strategy produces

    \r1 r2 a b (x # p :: a) (y # q :: b) -> (# a, b #)

Which has type

    forall r1 r2 a b. a #p-> b #q-> (# a, b #)

Which violates the levity-polymorphism restriction see Note [Levity polymorphism
checking] in DsMonad.

So we really must instantiate r1 and r2 rather than quantify over them.  For
simplicity, we just instantiate the entire type, as described in Note
[Instantiating stupid theta]. It breaks visible type application with unboxed
tuples, sums and levity-polymorphic newtypes, but this doesn't appear to be used
anywhere.

A better plan: let's force all representation variable to be *inferred*, so that
they are not subject to visible type applications. Then we can instantiate
inferred argument eagerly.

The goal of this ticket is to implement the last paragraph.