Having the template haskell generate specializations of explicitMember seems to work really well for a lot of situations.
What if send yielded a tuple of the value and a similar proof forall r. (ExplicitMember r qs) => Member r qs.
Then we'd refactor send's arguments so that instead of using introAnd everywhere, the proof of ownership is paired with the value. Ideally a user would usually not need to unpack the return tuple.
Having the template haskell generate specializations of
explicitMember
seems to work really well for a lot of situations. What if send yielded a tuple of the value and a similar proofforall r. (ExplicitMember r qs) => Member r qs
. Then we'd refactor send's arguments so that instead of usingintroAnd
everywhere, the proof of ownership is paired with the value. Ideally a user would usually not need to unpack the return tuple.