Basic type inference outside of statically typed code

[yannham]

Is your feature request related to a problem? Please describe.
At the typechecking phase, the typechecker maintains an environment mapping variables introduced by let expressions to types. Indeed, whether a variable was introduced in a statically typed Promise or outside, it can be used inside a Promise at some point and the typechecker must thus know about its type, or have at least an approximation.

The current rule to determine the type of a variable introduced outside of a Promise is:

• if the variable is annotated, meaning that it is introduced by an expression of the form let var = Assume(type, ...) in ... or let var = Promise(type, ...) in ..., then use the user-defined type.
• otherwise, use the unitype Dyn

This is an understandable rule in general as Nickel is untyped by default: outside of a statically checked Promise block, the typechecker shouldn't - and in general, can't - infer the type of an expression. But assigning the type Dyn to a variable forces the user to resort to explicit type casts (AKA Assumes) when using it inside a Promise:

$nickel <<< 'let magic_number = 2 in
Promise(Num -> Num,
  fun x => x + magic_number
)'
Typechecked: Err("The following types dont match Num -- Dyn")

$nickel <<< 'let base_path = "/home/me/nickel/" in
let full_path = Promise(Str -> Str,
    fun filename => base_path ++ filename ++ ".ncl"
) in
full_path "myfile"'
Typechecked: Err("The following types dont match Str -- Dyn")

Describe the solution you'd like
We could improve a bit the rule above, which determines the type associated to a variable, to accommodate simple common cases as long as the rule stays cheap and simple. For example:

• If the bound term is a constant, as in let x = 1 in or let x = "str" in , deduce its type. This would make the previous examples to be accepted by the typechecker.
• If the bound term is also a variable, as in let x = y, then use the type determined for y.
• and others that we haven't thought of yet.

[aspiwack]

The guiding principle might be: there must not be a recursion in the right-hand term. And the type must be the most general type possible. Under this principle we could also mark syntactic functions as Dyn -> Dyn. Don't know if it'd be useful.

[yannham]

Closed #273.