bug, in splitAtV?

[msaaltink]

With this pointless definition

bar: {a, b} [a+b] -> [a] -> [b]
bar x y = take x

we can trigger a bug:

Main> bar (zero:[inf]) 0xf
cryptol: You have encountered a bug in Cryptol's implementation.
%< --------------------------------------------------- 
  Revision:  0352dca57a32ef79a0575c97047a405b99d49c84
  Branch:    master (non-committed files present during build)
  Location:  [Eval] splitAtV
  Message:   invalid `front` len
%< --------------------------------------------------- 

[weaversa]

You're a man after my own heart!

[brianhuffman]

This definition of bar should cause a type error. The type of take is

take : {front, back, elem} (fin front) => [front + back]elem -> [front]elem

so the type of bar should be required to have a fin b constraint:

bar : {a, b} fin b => [a+b] -> [a] -> [b]

I suspect this is related to #58.