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 rho
s!
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