Solver losing assumptions in parameterized modules

[robdockins]

Attempting to load the following file results in an error. It seems like the constraint solver is somehow losing track of some assumptions, because I believe this should be trivial. I can't seem to reproduce this bug without involving module parameters, so there seems to be some interaction there.

module Main where
parameter
    type c : #
    type constraint ( fin c, c >= 1, 64 >= width (c-1) )

dumbHash : {n} (fin n, 64 >= width n) => [n] -> [128]
dumbHash msg = foldl (^) 0 xs
  where
    xs : [(n + 64) /^ 128][128]
    xs = groupBy`{128} (msg # zero # len)

    len = `n : [64]

asdf : {n} (64 >= width (n+192), 64 >= width (128 * c), fin n) => [n] -> [128]
asdf msg = dumbHash (join (drop`{1} ys))
  where
    ys : [c+1][128]
    ys = [ fromInteger 42 ] # [ dumbHash (msg#x#y) | x <- [ 0 .. (c-1):[64] ] | y <- ys ]

[error] at widthbug.cry:1:1--18:90:
  Failed to validate user-specified signature.
    when checking the module's parameters,
    we need to show that
      for any type Main::c
      assuming
        • fin Main::c
        • Main::c >= 1
        • 64 >= width (Main::c - 1)
      the following constraints hold:
        • 64 >= width (128 * Main::c)
            arising from
            use of expression Main::dumbHash
            at widthbug.cry:15:12--15:20

[bboston7]

Here's another simple case for whoever tackles this issue. Take the parameterized module:

module parameterized where

parameter
  type w : #
  type constraint (fin w)

getZeros : [w/8][8]
getZeros = split`{each=8} zero

the instantiated module:

module instantiated = parameterized where

type w = 32

and the importing module:

module importer where

import instantiated

zeros : [4][8]
zeros = getZeros

Crypol will error out on the importing module:

[error] at ./importer.cry:6:9--6:17:
  Unsolved constraints:
    • 4 == instantiated::w / 8
        arising from
        matching types
        at ./importer.cry:6:9--6:17

[yav]

I have a pull request that fixes @bboston7's example, but the issue in the original example is only somewhat related to the module system. Here is an example of the same sort of issue without the module system:

f : {a} a
f = g
  where
  g :  (Literal 1 a) => a
  g = 1

This fails for much the same reason as @robdockins original example:

[error] at test.cry:3:1--6:8:
  Failed to validate user-specified signature.
    in the definition of 'Main::f', at test.cry:3:1--3:2,
    we need to show that
      for any type a
      the following constraints hold:
        • Literal 1 a
            arising from
            use of expression Main::g
            at test.cry:3:5--3:6

Basically the problem is when a schema introduces local assumptions that do not mention any of the schema's variables. The
constraint 64 >= width (128 * c) is just like that in the original example. The confusion arises because, normally, if the definition of a function gives rise to a constraint that does not mention any of the schema's variables we don't try to solve the constraint, but instead "delay" it, in the hopes of more unification variables being instantiated by the time we get to it.

I can see two solutions here:

1. Modify the algorithm to be more aggressive and try to solve goals even if they don't mention any quantified variables, if they do mention some of the "local" constraints. This kind of make sense, especially if the goal doesn't actually have any free unification variables so delaying it doesn't buy us anything.
2. Disallow local constraints that do not mention any of the quantified variables. Generally, such constraints are pretty suspect, I think. For example, in the original example one could instantiate the module with parameters that would make asdf unusable...

@robdockins @brianhuffman thoughts?

[yav]

I ended up doing the more aggressive checking---it was a small change---and now the original example works.

By the way, the example I gave above is not exactly equivalent to Rob's original one, as of course the use of g gives rise to another Literal constraint. A more precise version would be something like this:

f : {a : *} ()
f = ()
  where
  g : (Literal 1 a) => a
  g = 1

[yav]

Should be fixed via #959