Disable elimination-based instantiation by default

[SquidDev]

Given ids : [forall a, e::Row. (a) -e-> a], one may currently write hd(ids)(2). However, under FreezeML this should strictly be a type error (one must write hd(ids)@2).

We should probably add a flag to be able to switch between the current behaviour and that of FreezeML, and potentially use FreezeML's behaviour by default.

[jamescheney]

The title of this issue is confusing. I think this is a "question" rather than a "bug". The things to discuss first are:

• is it ever actually wrong to implicitly instantiate a function argument? i.e. is there any downside to the current approach? For example, I could imagine it making IR generation a little more complicated.
• what are the consequences of disabling this implicit instantiation? Do we need to many changes (to insert @'s) or just a handful?

As a first step, adding code that just prints a debug message whenever this happens would be useful, so that we can understand (2). Understanding (1) I think amounts to adding this to the FreezeML system/inference algorothm and convincing ourselves it doesn't break anything.

Ultimately, I think we should decide on one behavior rather than add yet another flag that enables or disables it.

[slindley]

I discussed this with @SquidDev and I explicitly told him that we should have a flag for this, and I stand by this. It is an experimental feature that it is useful to be able to switch on and off.

The current behaviour is always sound (the only sensible interpretation of placing a quantified type in an elimination position is to instantiate all of the quantifiers), but I would prefer to default to the standard FreezeML behaviour until we have a better understanding of the pros and cons of alternative strategies. Some minor changes will need to be made to desugaring, but I expect they will be entirely straightforward.

[jamescheney]

OK