Make desugaring/elaboration of interfaces, interface implementations,
records, and parameter blocks take into account the pragma
%unbound_implicits off.
Main changes:
(a) Execute the pragma also during desugaring
(b) Check whether isUnboundImplicits is on at each desugaring step
Alternatives I didn't take:
(1) Changing findBindableNames to effectfully check the flag.
Rationale:
Apart from turning a pure function into an effectful one, this
would mean repeatedly calling findBindableNames, only to do
nothing once the flag is read.
(2) Adding another function that takes multiple places (list of terms)
that might contain bindable names, and before dispatching
findBindableNames on each term, checking the flag.
Rationale: I didn't want to add another abstraction, as that would
also require further changes inside TTImp. (weak rationale)
@edwinb @gallais : if you prefer (2), I can do that.
ohad
commented
4 years ago
Fix for #269
Make desugaring/elaboration of interfaces, interface implementations, records, and parameter blocks take into account the pragma
%unbound_implicits off.Main changes:
(a) Execute the pragma also during desugaring (b) Check whether
isUnboundImplicitsis on at each desugaring stepAlternatives I didn't take:
(1) Changing
findBindableNamesto effectfully check the flag.Rationale: Apart from turning a pure function into an effectful one, this would mean repeatedly calling
findBindableNames, only to do nothing once the flag is read.(2) Adding another function that takes multiple places (list of terms) that might contain bindable names, and before dispatching
findBindableNameson each term, checking the flag.Rationale: I didn't want to add another abstraction, as that would also require further changes inside TTImp. (weak rationale)
@edwinb @gallais : if you prefer (2), I can do that.