Explicit type more general than inferred type?

[msaaltink]

Here's an oddity:
some: {n} [n] -> Bit
some x = x != 0
some' x = x != 0

Loading this in Cryptol 2.0.0 gives unexpected results. The definition of 'some' should fail, as the comparison should require that n is finite (as described in "CryptolPrims.pdf", the instance of 'Cmp [n]a' requires 'fin n' and I did not see another matching instance).
Cryptol reports
Main> :t some'
some' : {a} (fin a) => [a] -> Bit
just as expected. But to my surprise the definition of some is accepted.
Main> :t some
some : {n} [n] -> Bit

[LeventErkok]

This is definitely a bug, and Cryptol knows it! Here's what happens when you use your some:

Main> some (zero : [inf])
cryptol: You have encountered a bug in Cryptol's implementation.
*** Please report this problem to [email protected]

%< ---------------------------------------------------
  Revision:  bd578915eaba8c56fadc29fe30f5dcd212c63374
  Branch:    HEAD (non-committed files present during build)
  Location:  [Eval] fromVWord
  Message:   not a word
             [False, False, False, False, False, ...]
%< ---------------------------------------------------

[brianhuffman]

I came across what looks like another instance of the same problem. I wrote the following definition and it typechecked, even though (!) should require a fin n constraint:

last : {n, a} (n >= 1) => [n]a -> a
last xs = xs ! 0

Evaluating last [0 ... ] causes a similar error message:

cryptol: You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/galoisinc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  68b64ab083526a2dced8a78f41dd702a1bb2388b
  Branch:    master (non-committed files present during build)
  Location:  [Eval] indexBack
  Message:   unexpected infinite sequence
%< --------------------------------------------------- 

[yav]

Ah, yeah, I know what that is about: I've actually fixed it and then unfixed it a couple of times :-) I'll have a look at it.

[msaaltink]

I came across another example of this recently. The type of (#) clearly says that front, the length of the first sequence, has to be finite. So, as expected, type checking rejects the expression (zero:[inf]) # zero, failing to satisfy the constraint fin inf. But you can hide it in a function:

bar: {a} [a] -> [inf]
bar x = x # zero

Now the fin a constraint is gone.

Main> :t bar
bar : {a} [a] -> [inf]
Main> bar (zero:[inf])
[False, False, False, False, False, ...]

[yav]

Thanks for your example! This is a known bug in the current constraint solver. We are currently working on a new version of Cryptol's constraint solver that should solve this problem (and, hopefully, others too!).

[weaversa]

With the latest check-in (the same that fixed #140), the fin is inferred for all examples in this thread. Would someone doublecheck?

[brianhuffman]

Yes, it looks like changeset 28fdd44 fixed these examples too: Not only is the "fin" inferred, but a type error occurs if you give a type signature without it. I added some regression tests. Thanks, @elliottt!