Duplicating a function causes failure

[weaversa]

perm : {m, n} (fin m, fin n) => [n] -> [lg2 m][lg2 n] -> [lg2 m]
perm a b = a @@	b

perm2 : {m, n} (fin m, fin n) => [n] -> [lg2 m][lg2 n] -> [lg2 m]
perm2 a	b = perm a b

perm works fine. perm2 fails to type check. Maybe related to #389 ?

[error]
  Failed to validate user-specified signature.
    In the definition of 'Main::perm2'
      for any type m, n
        fin m
        fin n
      =>
      width (max 1 m - 1) == width (max 1 ?m`973 - 1)
        arising from
        matching types
      width (max 1 ?m`973 - 1) == width (max 1 m - 1)
        arising from
        matching types
      fin ?m`973
        arising from
        use of expression Main::perm
  where
  ?m`973 is type argument 'm' of 'Main::perm'

However, changing the lg2 m to m removes the issue.

perm : {m, n} (fin m, fin n) => [n] -> [m][lg2 n] -> [m]
perm a b = a @@	b

perm2 : {m, n} (fin m, fin n) => [n] -> [m][lg2 n] -> [m]
perm2 a	b = perm a b

[yav]

TLDR: The issue here is that lg2 is not an injective function, which is why Cryptol cannot infer what type to use for m on the call to perm.

Here are the types of the two functions, renaming the one to avoid confusion:

perm   : {m, n} (fin m, fin n) => [n] -> [lg2 m][lg2 n] -> [lg2 m] 

perm2 : {x, y} (fin x, fin y) => [y] -> [lg2 x][lg2 y] -> [lg2 x]
perm2  a b = perm a b

perm2 makes a call to perm, so Cryptol needs to figure out what type parameters to choose for m and n, and also check that all types match, which results in the following goals (after a bit of simplifcation)

1. n = y
2. lg2 m = lg2 x
3. lg2 n = lg2 y

Clearly there is only one possible way to solve 1, which allows Cryptol to infer that type n must be equal to y, which makes goal 1 and 3 trivial. However, Cryptol is stuck on goal 2 because there is no unique way to solve it---choosing x for m is one way to do it, but since lg2 is not injective, other answers are also possible, and Cryptol does not make arbitrary choices when inferring types.

Now, in this case one could argue that there is only possible "reasonable" solution, and Cryptol should pick x for m. We would have to come up with some sort of definition for "reasonable" though.

Perhaps some sort of defaulting, if there is only one possible variable around, and choosing it would solve everything.

[brianhuffman]

I discussed this issue with @yav, and we identified a case where the "Failed to validate user-specified signature" error message is particularly misleading.

If type checking results in one or more unsolved constraints, which also include one or more unbound unification variables, then we have a situation where the constraints might be solvable if we only knew how to instantiate the variables.

In this case, the error message should not say that the type checking definitely "failed"; instead it should highlight the remaining unification variables, possibly suggesting that the user could add explicit type applications or type signatures.

[yav]

I've updated the error messages to make it a bit more obvious what went wrong:

 Failed to infer the following types:
    • ?m`861, type argument 'm' of 'Main::perm' at ./test.cry:5:13--5:17
  while validating user-specified signature
    in the definition of 'Main::perm2', at ./test.cry:5:1--5:6,
    we need to show that
      for any type m, n
      assuming
        • fin m
        • fin n
      the following constraints hold:
        • width (max 1 m - 1) == width (max 1 ?m`861 - 1)
            arising from
            matching types
            at ./test.cry:5:13--5:17
        • width (max 1 ?m`861 - 1) == width (max 1 m - 1)
            arising from
            matching types
            at ./test.cry:5:20--5:21
        • fin ?m`861
            arising from
            use of expression Main::perm
            at ./test.cry:5:13--5:17

[brianhuffman]

Is there anything left to do here, or should we close the ticket?

[brianhuffman]

With the improved error messages, I think we're done here.