You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Symbolic strings defer to the client code the task of interpreting the string (and string interpolation in particular). This allows amongst other things interpolating things which aren't themselves string (like in the motivating Nix example). However, the type-checker expects the interpolated values to be string and complains if they aren't.
To Reproduce
$ nickel eval<<<'foo-s%"Interpolate: %{1}"%'{ fragments = [ "Interpolate: ", 1 ], prefix = 'foo, tag = 'SymbolicString, }
$ nickel eval<<<'foo-s%"Interpolate: %{1}"% : _'error: incompatible types ┌─ <stdin>:1:23 │1 │ foo-s%"Interpolate: %{1}"% : _ │ ^ this expression │ = Expected an expression of type `String` = Found an expression of type `Number` = These types are not compatible
Expected behavior
Don't have the typechecker make any assumption as to the type of what's interpolated and let the user put the needed type assertions.
I wonder what could be a working type annotation, though. Currently there's no obvious way of typing heterogeneous arrays (at least without the subtyping of RFC004):
nickel> ["hello ", {name = "world", drv = null}, "/bin/world"] : Array Dyn
error: incompatible types
┌─ <repl-input-1>:1:2
│
1 │ ["hello ", {name = "world", drv = null}, "/bin/world"] : Array Dyn
│ ^^^^^^^^ this expression
│
= Expected an expression of type `Dyn`
= Found an expression of type `String`
= These types are not compatible
One possibility would be to always set the type of symbolic strings to be Array Dyn, and check each of the interpolated elements separately against a fresh unification variable. So, writing nix-s%"literal1...%{exp1}...literal2" in a statically typed block would be equivalent to ["literal1", (exp1 : _), "literal2"] | Array Dyn. The latter contract can never fail, but it's used to say "this expression has type Array Dyn, just believe me" to the typechecker.
Currently symbolic strings are simply rewritten during parsing, so we either need to add a proper AST node for them, or to perform the proposed desugaring, but the latter requires the parser to know if it's in a typed block or not (which isn't obvious when doing bottom-up parsing).
Describe the bug
Symbolic strings defer to the client code the task of interpreting the string (and string interpolation in particular). This allows amongst other things interpolating things which aren't themselves string (like in the motivating Nix example). However, the type-checker expects the interpolated values to be string and complains if they aren't.
To Reproduce
Expected behavior
Don't have the typechecker make any assumption as to the type of what's interpolated and let the user put the needed type assertions.
Environment
The text was updated successfully, but these errors were encountered: