Parameterized modules, types and type definitions.

[linesthatinterlace]

I came upon this bug in a larger context - I've boiled it down to what I think is a minimum working example:
testp.zip

We have two files: test.cry:

module test where
parameter
    type a : #
    type constraint (fin a) 

type b = (2^^a - 1)

f : [b] -> [3*b]
f x = x # x # x

and test_parameters.cry:

module test_parameters = test where
    type a             = 2

When you try to load test_parameters.cry, you get the following error:

Cryptol> :l test_parameters.cry
Loading module Cryptol
Loading module test

[error] at ./test.cry:1:1--9:16:
  Failed to validate user-specified signature.
    when checking the module's parameters,
    we need to show that
      for any type test::a
      assuming
        • fin test::a
      the following constraints hold:
        • 3 * test::b == test::b + 2 * test::b
            arising from
            matching types
            at ./test.cry:9:7--9:16

However, if we de-parameterize, thus:

module test where
type a             = 2

type b = (2^^a)

f : [b] -> [3*b]
f x = x # x # x

Then test.cry loads.

Something is breaking somewhere involving:

• The parameterization.
• The use of exponentials and subtraction in the definition of b.
• The typechecker's understanding of associativit or addition of types.

Obviously this is a pretty specialised example - but it did come up naturally for me, and I think it is a bug?

[robdockins]

Just tried to reproduce this behavior. The printing has changed a bit, but the problem is otherwise unchanged.

Loading module Cryptol
Loading module test
[error] at ./test.cry:1:1--10:16:
  Failed to validate user-specified signature.
    when checking the module's parameters,
    we need to show that
      for any type test::a
      assuming
        • fin test::a
      the following constraints hold:
        • 3 * 2 ^^ test::a - 1 == 2 ^^ test::a - 1 + 2 * 2 ^^ test::a - 1
            arising from
            matching types
            at ./test.cry:10:7--10:16

It seems like the problem is related to the subtraction operator. If I remove it or replace it with (+ 1), the module loads. Likewise, if I replace - 1 with / 2 I get a similar problem. So, partial type functions seem implicated here.

[robdockins]

We should also fix the pretty-printer here, as it seems to be getting operator precedence wrong.

[robdockins]

Indeed, it doesn't seem related to parameterized modules, really. I can produce essentially the same problem directly.

module test where

f : {a} (fin a) => [2^^a -1] -> [3*(2^^a - 1)]
f x = x # x # x

[error] at test2.cry:4:1--4:16:
  Failed to validate user-specified signature.
    in the definition of 'test::f', at test2.cry:4:1--4:2,
    we need to show that
      for any type a
      assuming
        • fin a
      the following constraints hold:
        • 3 * (2 ^^ a - 1) == 2 ^^ a - 1 + 2 * (2 ^^ a - 1)
            arising from
            matching types
            at test2.cry:4:7--4:16

[robdockins]

Worth noting, the following program is accepted without complaint:

module test where

f : {a} (fin a) => [2^^a - 1] -> [2*(2^^a - 1)]
f x = x # x