Instantiating a parameterized module results in incorrect operator precedence

[RyanGlScott]

Consider the following parameterized module (B) and instantiation of it (Y):

module B where

parameter
  type a: #

type w = 2 ^^ a
type b = 2 ^^ w

module Y = B where
type a = 0

b should be equivalent to 2 ^^ 2 ^^ 0 which, due to (^^) being right-associative, should be equal to 2 ^^ (2 ^^ 0), i.e., 2. Despite this, b is actually equal to 1, not 2:

Y> :m Y
Loading module Cryptol
Loading module `where` argument of Y
Loading interface module `parameter` interface of B
Loading module B
Loading module Y
Y> `b : Integer
1

Compare this to the output of a variant that does not use parameterized module:

module Z where
type a = 0
type w = 2 ^^ a
type b = 2 ^^ w

Z> :m Z
Loading module Cryptol
Loading module Z
Z> `b : Integer
2

Most likely, the parameterized version is incorrectly using the precedence (2 ^^ 2) ^^ 0, which would explain why it computes 1 instead of 2.

[yav]

I don't think this is an associativity issue. I suspect it's a typo somewhere. If you load with debug you get:

module Main::B
type Main::B::w = 2 ^^ Main::B::`parameter` interface of B::a
type Main::B::b =
  2 ^^ (2 * Main::B::`parameter` interface of B::a)

Note that the exponentiation become multiplication for some reason.

[mccleeary-galois]

Possibly related:

https://github.com/GaloisInc/cryptol/pull/1713/files#diff-ebba50b9686b922abc6310114249d92f721be53f637d9474bfbc01e66e047437R172

[yav]

The problem is in tExp in SimpType, namely this equation is wrong:

 | TCon (TF TCExp) [a,b] <- tNoUser y = tExp x (tMul a b)

This says x ^ (a ^ b) should become x ^ (a * b), which is quite wrong.

[RyanGlScott]

Great sleuthing! Indeed, commenting out that case in tExp fixes the test case above.

The question now is: what should we do about this case? Should we remove it entirely, or is this a case of incorrectly writing down a different, valid simplification rule? (This case was introduced in 984108b — do you recall what the context for this was, @yav?)

[RyanGlScott]

Ah, I suppose the intent could have been to capture this identity of exponentiation:

$$(x^a)^b = x^{ab}$$

Normally, this requires that x is non-zero, but I think this identity still holds in a Cryptol context when x is zero, given that `(0 ^^ 0) : Integer evaluates to 1 in Cryptol.

[yav]

Yes, the intention was to implement this rule, but I matched on the wrong argument, it looks like.