Design decision or implementation detail?

[bennn]

I have a small program where MOVING a type annotation adds a dynamic error.

First, the untyped program:

# 1

def cast(f):
  return f

def identity(x):
  return x

def app(f):
  return cast(f)("NaN")

print(app(identity))

Second, a typed version that does not error:

# 2

def cast(f:Dyn)->Function([String],String):
  return f

def identity(x):
  return x

def app(f:Function([Int],Int))->String:
  return cast(f)("NaN")

print(app(identity))

Third, moving the Function annotation to the definition of identity
makes the program raise a dynamic type error:

# 3

def cast(f:Dyn)->Function([String],String):
  return f

def identity(x:Int)->Int:
  return x

def app(f:Dyn)->String:
  return cast(f)("NaN")

print(app(identity))

This is confusing. I would expect both typed programs to error, but apparently the Function type is weaker than a type given at a function definition.

Why doesn't program 2 raise an exception?
Is there a type-system-design reason, or is the reason because of Reticulated's dynamic semantics?