unbound symbol error when symbol is actually bound

[weaversa]

G = [1, 2, 3, 4]
G' = [ x | x <- [0 .. width(G)-1]]

cryptol> :r
Loading module Cryptol
Loading module Main

[error] unbound symbol: (at test.cry:2:29--2:30, G)

[brianhuffman]

I think this is because width(G)-1 in your example is parsed as a type instead of an expression. G is not in scope as a type variable, so we get the unbound symbol error.

We could definitely improve the error message in this case, perhaps saying "unbound type name" instead of just "unbound symbol". Or we could have a special message just for cases like this where the symbol is in scope as an expression variable but not a type variable.

[weaversa]

I feel that even giving a better error message here would be misleading. That is, I find it confusing that sometimes I can use width and sometimes I can't. I now understand you've placed a restriction on it's use, but I wish it wasn't there.

The main use of width is to get the length of something when a type variable isn't lying around. Even though width takes a value definition as an argument, the length can always be determined at compile time because the value of the definition doesn't matter, only it's type.

What would it take to get the version of width in the type world to provide the length of value definitions?

[dylanmc]

The error message is much better. Aaron suggests "typeof" to take a value and produce a type, so we could do something like:

width(typeof(G))

in this case. Rob pointed out that we could define a type alias for G, and use that everywhere, but maybe not as satisfying. Yav?