Propagating fin constraints through /^ operator

[brianhuffman]

Cryptol's type checker fails on something that seems like it should work:

foo : {i, j} (fin i, fin j, j >= 1) => [i /^ j][32]
foo = take [0...]

[error] at ./foo.cry:3:1--3:18:
  Failed to infer the following types:
    • ?back`845, type argument 'back' of 'take' at ./foo.cry:3:7--3:11
  while validating user-specified signature
    in the definition of 'foo', at ./foo.cry:3:1--3:4,
    we need to show that
      for any type i, j
      assuming
        • fin i
        • fin j
        • j >= 1
      the following constraints hold:
        • i /^ j + ?back`845 == inf
            arising from
            matching types
            at ./foo.cry:3:12--3:18

[brianhuffman]

Note that the above example works if /^ is replaced with +, *, /, ^^, min, max, etc. It fails for /^ and %^.

[brianhuffman]

The problem seems to have to do with function tryEqAddInf, which implements the rule (t1 + t2 = Inf, fin t1) ~~> t2 = Inf.

https://github.com/GaloisInc/cryptol/blob/master/src/Cryptol/TypeCheck/Solver/Numeric.hs#L369