Top-down typing strategy - is there a name for this?

In most statically typed languages, each expression has an intrinsic type. E.g. in Java, 3 is an int, 3.0 is a double, 3+3.0 is also a double. Types do not depend on the context of the expression.

However, in the CSS type system described in the spec, some expressions have a type depending on the context. For example, the red token can be a `, a , or an , depending on the context in which it is used.

I want to build a type system for a CSS-based programming langauge. In this type system, I want to use a typing strategy that does not go from the bottom up (starting from the leaves in the AST), but top down (starting from the root of the AST).

For example, when the compiler needs to derive that the linear(red, yellow) expression inhabits the type, it would do the following derivation:

we want to derive that
  linear(red, yellow) ::    
 is defined as  | linear(, ), so
  linear(red, yellow) ::  | linear(, )
let us try the second branch
  linear(red, yellow) :: linear(, )
let us check sub-expressions
  red :: 
  yellow :: 
everything fine, OK

Can you point me to scholarly articles where this kind of typing strategy is discussed?

P.s. I don't know of other languages where a type of the expression depends on the context, except for Perl. In Perl, ("a","b")` can be interpreted as either a list or an integer (its length), depending on the context:

print ("a","b") # => ab
print 0+("a","b") # => 2

There is no top-down or bottom-up typing strategy when defining a language. It is an implementation issue. A type system will
only define operator operand constraints on your AST. The kind
constraints is fixed by the type system and is part of the design of
the language. It can be very simple as in older languages, or be a
sophisticated logical system. Even when simple, it can be seen as a
logical system. Your AST may be seen as a proof tree in that logical
system, where the nodes are to be decorated by types, that may be seen as logical
propositions proved by by the sub-tree dominated by that node . For example, the type int found for an expression is
a predicate satisfied by the expression.

So you can associate type inference rules to the operators of your
AST. For example if you have an AST operator + with two operands,
you can associate (among others) the inference rule:
$X::int \,\wedge\, Y::int \;\Rightarrow\; X+Y::int$

Defining the type system of a language amount to defining such rules
for all AST operators where that make sense, i.e. involved with the
type system.

Type checking your program consists in finding a type for each
(relevant) AST node, such that that there is an inference
rule (associated to the operator of that node) that is satisfied by
the node type and the types of its operands.

This can be done with top-down or bottom-up algorithms, or any
mix. That is only a matter of finding efficient algorithms. But the
checking strategy is an implementation issue, not a language
definition issue. However, it is advisable to choose a type system
that allows for a tractable type checking strategy.

Note that the types may not be all completely defined by the type system,
and the checking strategy may actually infer the "details" of these
types, in particular by means of unification techniques.

The above description may not seem too complex (I hope). One hidden
aspect, that makes the whole thing a lot more interesting, is that
in static typing (particularly) all occurences of the same variable
must have the same type, which introduces additional constraints.
But getting into the details is too much for a normally sized answer.

For more about this, you should look for type inference.

StackExchange Computer Science Q#43461, answer score: 4