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

links-lang / links

Links: Linking Theory to Practice for the Web

http://www.links-lang.org

Other

330 stars 42 forks source link

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

Open slindley opened 5 years ago

slindley commented 5 years ago

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 commented 4 years ago

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 commented 4 years ago

@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 commented 4 years ago

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 )