Can't use generate for length 2^^n with index [n]

[brianhuffman]

I was trying to use left-hand-side indexing to define a list of length 2^^n using a perfectly-sized index of type [n]. Here's a simplified version of my function definition:

table : {n, a} (fin n) => ([n] -> a) -> [2^^n]a
table f @ i = f i

But cryptol rejects this with a type error message:

[error] at Temp.cry:2:1--2:18:
  Failed to validate user-specified signature.
    in the definition of 'Main::table', at Temp.cry:2:1--2:6,
    we need to show that
      for any type n, a
      assuming
        • fin n
      the following constraints hold:
        • n >= width (max 1 (2 ^^ n) - 1)
            arising from
            use of expression generate
            at Temp.cry:2:1--2:18

Using perfectly-sized index types like this is one of the reasons for introducing left-hand-side indexing in the first place. We should make this work.

[brianhuffman]

#704 seems related.

[brianhuffman]

By the way, it seems like the type checker ought to be able to simplify max 1 (2 ^^ n) to just 2 ^^ n.