Skip to content

Change `|-i` to take `psis` instead of a `sigma`

The new judgement should look something like: |-i psis; args ~> Theta ;<Q>; <| exp ; phi |>

As is appearent, instead of taking sigmas, and then returning a rho, we are giving |-i some psis -- that were synthesized using the visible arity of args -- and then not returning any rhos!

This is because we already got the rho when we splitted the sigma at the call-site:

|-arity args ~> nva
|-split nva; sigma ~> psis, rho    -- psis includes invisible ones (as now)
|-i psis; args ~> Theta, Qs, <exp,phi>
Theta(rho)
   ....
------------- INST-CHECK