[ ] Make sure unpacking happens after function application. It currently happens inside instantiateSigma which should be called after function application but currently isn't. Possibly a recent regression with the n-ary functions patch.
[ ] Allow more than one implicit argument to dependent pairs, distinguished by name.
[ ] Allow explicit packing and unpacking via named components.
[x] Fix the hack where we special-case UDecl in checkSigma.
[ ] Deprecate the old explicit dependent pair, and perhaps even rule out dependency in data constructors.
[ ] Possibly replace some uses of List in the standard library with implicit dependent pairs.
Still to do:
instantiateSigmawhich should be called after function application but currently isn't. Possibly a recent regression with the n-ary functions patch.UDeclincheckSigma.Listin the standard library with implicit dependent pairs.