Overly-strick typechecking of symbolic strings

[thufschmitt]

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

$ 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.

Environment

• OS name + version:
• Version of the code: 28672ee45bfe78dc3dc828ac1fe4fa40f99965e9

[yannham]

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).