Improve instantiation of datacons
This ticket tracks a possible improvement to
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.