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.