Mutual blocks that mix frozen and unfrozen functions can allow quantifiers to escape their scope

[slindley]

Now that we can mark functions as frozen (#688), we can write mutual blocks with one frozen function and one non-frozen function, allowing definitions like:

mutual {
  ~fun f(x) { x }
  fun g(x) { f(x) }
}

This allows quantifiers to escape their scope, similar to #678, meaning f uses the quantifiers bound by g's type.

[jamescheney]

Meeting discussion: as a first step it seems reasonable to disallow mixing frozen and unfrozen things. Alternatively @jstolarek suggests fixing #678 might address this.

Also seems related to #684.

[jamescheney]

@SimonJF we discussed this a bit further today and I think the consensus was:

• if you already had in mind a fix for this that's srtaightforward to do over the next month or so (keeping in mind your other plans) then great
• if not, and you think the right way to fix this is essentially also fix #678, then we suggest closing this for now by making it impossible to mix frozen and unfrozen functions in a mutual block for now and add "fix this the right way so that frozen and unfrozen can be mixed safely" to #678 or a new enhancement issue, and we revisit this and the other FreezeML-related issues (#678, #684) later.

You are away, I am just making this note now.

[jamescheney]

This is milestoned 0.9.2, which we hoped to get released around now. Is it likely to be resolved in the next week or so, or should we postpone it?

(0.9.2 is needed as a bugfix release due to #807 )