First of all, very nice example. Thank you for making it so small and easy to work with.
I can see what's happening. The key part is what happens here:
{{{
do_step4 :: (Numerical num) => num -> Box a -> Box a
do_step4 number Box{ func = f, obj = x}
= Box{ func = f, obj = f number x }
}}}
After elaboration (ie making dictionaries explicit) we get this:
{{{
do_step4 dn1 number (Box {func = f, obj = x })
= Box { func = \dn2 -> f ( case dn2 of (f,r) -> f
, case dn2 of (f,r) -> r)
, obj = f dn1 number x }
}}}
That's odd! We expected this:
{{{
do_step4 dn1 number (Box {func = f, obj = x })
= Box { func = f
, obj = f dn1 number x }
}}}
And indeed, the allocation of all those `\dn2` closures is what is causing the problem.
So we are missing this optimisation:
{{{
(case dn2 of (f,r) -> f, case dn2 of (f,r) -> r)
===>
dn2
}}}
If we did this, then the lambda would look like `\dn2 -> f dn2` which could eta-reduce to `f`.
But there are at least three problems:
* The tuple transformation above is hard to spot
* The tuple transformation is not quite semantically right; if `dn2` was bottom, the LHS and RHS are different
* The eta-reduction isn't quite semantically right: if `f` ws bottom, the LHS and RHS are different.
You might argue that the latter two can be ignored because dictionary arguments are special;
indeed we often toy with making them strict.
But perhaps a better way to avoid the tuple-transformation issue would be not to construct that strange expression in the first place. Where is it coming from? It comes from the call to `f` (admittedly applied to no arguments) in `Box { ..., func = f }`. GHC needs a dictionary for `(Numerical dum)` (I changed the name of the type variable in `func`'s type in the definition of `Box`). Since it's just a pair GHC says "fine, I'll build a pair, out of `Fractional dum` and `Real dum`. How does it get those dictionaries? By selecting the components of the `Franctional dum` passed to `f`.
If GHC said instead "I need `Numerical dum` and behold I have one in hand, it'd be much better. It doesn't because tuple constraints are treated specially. But if we adopted the idea in #10362, we would (automatically) get to re-use the `Numerical dum` constraint. That would leave us with eta reduction, which is easier.
As to what will get you rolling, a good solution is `test3`, which saves instantiating and re-generalising `f`. The key thing is to update all the fields ''except'' the polymorphic `func` field. I'm surprised you say that it doesn't work. Can you give a (presumably more complicated) example to demonstrate? Maybe there's a separate bug!