Interface constraint scoping

[yav]

Consider the following example:

interface I where
   type i: #

interface J where
  type j: #
  type constraint (fin j)

module Fu where
  import I
  import J
  interface constraint (i <= j) 

module F where
  import interface I
  import interface J
  interface constraint (i <= j)
  import interface Fu { I = interface I, J = interface J }
  interface submodule K where
    p: [j]

This reports the following error (error lines omitted):

[error] at F.cry
  Failed to validate user-specified signature.
    when checking the module's parameters,
    we need to show that
      for any type F::I::i, F::J::j
      assuming
        • fin F::J::j
      the following constraints hold:
        • F::I::i <= F::J::j
            arising from
            module instantiation at ./Fu.cry
            at F.cry

However, if you swap the declaration of K and import of Fu things work, which is clearly inconsistent.

The problem is that we don't process declarations in top-to-bottom order---instead the renamer arranges declarations in dependency order when it figures out the names of things. This is nice because the user can declare things in whatever order makes most sense to them. It can do this because it can see where names are used and rearrange things as needed.

interface constraints, however present a problem, because they are not explicitly used so we don't know where to place them. At the moment we do some pretty ad-hoc stuff to try figure out their location, but that's clearly not working well.

We need a different design to work around this. Perhaps interface constraint split the file into chunks and they are only in scope after the declarations, and when we rearrnage things we make sure stuff does not get moved out of its chunk? This requires some more thinking.

[sauclovian-g]

I had to deal with a problem like this at one point (but worse because the scopes were much more complex) -- basically the interface constraint is in scope whenever (as soon as) all the things it mentions are, and it should be possible to use that info to place it.

You can also insert a placeholder marked invalid at the top so that if you get an unsatisfied constraint you can examine the invalid ones to produce a message like "The constraint i <= j is not available here because the variable j is not in scope". This requires a fair amount of machinery though.

The other wrinkle is if you have an interface constraint of the form P /\ Q it might be desirable to split it before doing this processing.