Can't infer Arith ([inf]a) from Arith a

[brianhuffman]

When loading the following file

foo : {a} (Arith a) => [inf]a -> [inf]a -> [inf]a
foo x y = x + y

I get the following error message:

Loading module Main
[error] at ./arithinf.cry:2:1--2:16:
  Failed to validate user-specified signature.
    in the definition of 'Main::foo', at ./arithinf.cry:2:1--2:4,
    we need to show that
      for any type a
      assuming
        • Arith a
      the following constraints hold:
        • Arith ([inf]a)
            arising from
            use of expression (Cryptol::+)
            at ./arithinf.cry:2:11--2:16

I would expect Cryptol to be able to infer Arith ([inf]a) from Arith a.

[yav]

Interesting---currently we are not reducing this because we are waiting to see if a might be bit or not. However, if we know that the sequence length is inf we could reduce to Arith a as we know that in that case the Word-based operations would not apply. I just made the change.