Type schema shown with :t doesn't match the declaration

[brianhuffman]

If a Cryptol file contains a declaration with an explicit signature, I would expect :t to show the exact same signature. However, it seems that there is some preprocessing going on. For example

foo : {n} (fin n, n == 2 * (n / 2)) => [n]
foo = undefined

bar : {n} (fin n, n + 1 - 1 == n) => [n]
bar = undefined

Main> :t foo
foo : {n} (fin n, n == n - n % 2) => [n]
Main> :t bar
bar : {n} (fin n, True) => [n]

Granted, these new type signatures are logically equivalent to the ones I provided; but I still find this quite surprising. Is this intended behavior?

[brianhuffman]

Here's an even weirder one:

baz : {i, j, k} (fin (i + j + k)) => [i][j][k]
baz = undefined

Main> :t baz
baz : {i, j, k} ((&&) (&&) fin i fin j fin k) => [i][j][k]

[yav]

Argh, this is just wrong, the (&&) should never show up anywhere. I'll have a look

[yav]

Ok, so I fixed some of the issues (you shouldn't see (&&) and True anymore). However the main issue remains---we do simplify user written signatures.

What's happening is that when we check a definition with a signature, after we are done checking things, we apply a substitution to the inferred signatures (so that we can fill in _, if there are any). However, our code for applying substitutions also automatically simplifies things---reduces type functions and simplified predicates, which is what's changing the signatures here.

This automatic simplification on substitution is quite convenient, but perhaps we should try to separate the two, although we'd have to work out some invariants about when to simplify things.

[brianhuffman]

If the signature has no underscores, then the substitution applied at the end would be empty, wouldn't it? If so, then couldn't we just skip doing the substitution in that case?

[yav]

Yes, we could do that. The constraints would still get simplified in some cases (i.e., when there are _) but perhaps we can explain that by "this is a partial signature anyway", so we "fixed" it for you :-) I'll do that for now

[yav]

Ok, so it is a more tricky than I thought, as we also normalize types when we kind check them (i.e., when they are imported from the parsed to the typechecker AST). We do this, so that things are always in the normal form we expect when we write simplification rules. While this makes sense, perhaps this normalization should happen at a different time, but the change is non-trivial, so I'll leave this open for now.

[brianhuffman]

Should we just decide that type signatures will always be normalized, and mark this one as won't fix?