fix type inference non-propagation thru InterchangeEntrys

[mhuesch]

see https://asciinema.org/a/vRaEh4GeSvhVGNaqbu4lQwnUV.

we should be able to infer that we only want Bools, after a function Bool -> Bool was selected as the function in the higher-order application.

at least, I think this should be doable. we prob are just dropping type info instead of propagating the env across entries.

[mhuesch]

I believe that this is caused by using not storing & integrating the Substs (which occur in inference of the distinct intermediate IEs) into inference of subsequent IEs.

it's possible we'll need to store the Subst in the IE. but I am not sure.

doing this right will require understanding HM inference over function applications, and then recreating that at the level of IEs.

[mhuesch]

replication scenarion

as of 8cc86c, the scenario from https://asciinema.org/a/vRaEh4GeSvhVGNaqbu4lQwnUV is still an issue.

sequence of events:

• create not IE (which has scheme (Bool -> Bool))
• create true IE (which has scheme Bool)
• create 1 IE (which has scheme Int)
• input expr (but don't create yet): (lam [f x] (f x))
  • observe scheme forall t4 t3. ((t3 -> t4) -> (t3 -> t4))
  • observer that selector suggests the correct IE of not, which unifies with the arrow type (t3 ~ Bool & t4 ~ Bool)
  • press s to select not
  • observe 3 suggested IEs in the selector - not, true, 1. nothing is excluded, even tho if we propagate inference info correctly we should know that t3 ~ Booland therefore we want something which unifies withBool, and true` is the only such option.

expected behavior:

• in the last step, we should only see 1 IE, corresponding to true. not and 1 should be filtered out because they do not unify.

next actions

• look at how inference works for applications in rep_lang.
  • we are recreating an application here, but it is "exogenous" - via the interchange, which has access to internals of rep_lang. presumably we messed something up and aren't faithfully recreating application
• look at how Substs are managed in rep_lang
• look at howSubsts are managed in rep_interchange
  • I suspect we discard them, and we may want to not do that.