You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Sep 1, 2020. It is now read-only.
Method signatures can currently only have a single implicit parameter block, which means that explicitly specifying an implicit parameter requires every parameter to be specified, and limits opportunities for the type of one implicit parameter to drive the type inference of another.
Miles:
Arbitrary interleaving of implicit and explicit parameter blocks, a la Agda seems like a good way to go. I don't think there will be any major issues from a typing point of view. The trickiest issue is how this works out a call sites ... Paolo Giarrusso had a nice language extension proposal at some point, introducing a new bracket style for explicitly provided implicit argument lists (again a la Agda) which is probably worth investigating. I'll see if I can dig it out and/or mail him about it.