Fix large record field types blowing up search for SetterWf instance

[Nils-Lauermann]

Performing cbv in the set_eq case on goals of the form

f (field {| field := r |}) = field {| field := r |} 
→ set field f {| field := r |} = {| field := r |}

blows up for large field types (like r : gmap (bv 64) unit). cbv only seems to be necessary to unfold set. cbn suffices for the outstanding beta reduction of the field projection.

Fixes #46

[tchajed]

Thanks for reporting this issue, tracking it down, and fixing it!

Do you think you can add a test that failed with the old code? Perhaps a field of type Vector.t (factorial 10) nat or something similar? We don't want to create a dependency on stdpp just to use bv 64 in a test. If this is too much work then that's also okay, I'm still happy to merge the fix.

[tchajed]

From the issue thread it sounds like writing a test without depending on stdpp is difficult, so I'll go ahead and merge this. Thanks again!