How precise is the statement "STLC is the internal language of CCCs"?
Cartesian closed categories correspond to the simply typed lambda calculus with products.  Your silly function is just $\lambda x.\lambda y.y$. If you want something that directly corresponds to the simply typed lambda calculus without implying products check out this paper by Bart Jacobs: Simply Typed and Untyped Lambda Calculus Revisited.

Let's instantiate your silly term and spell out what it looks like in type theoretic notation.

First, we're using _[_] at type $(\sigma \vdash \tau \Rightarrow \tau) \to (\Gamma\times\sigma\vdash\sigma) \to (\Gamma\times\sigma\vdash\tau\Rightarrow\tau)$.  As a rule and placing in the terms, we get:
$$\frac{z : \sigma \vdash \lambda y:\tau.y : \tau\Rightarrow\tau \qquad \Gamma, x:\sigma\vdash x:\sigma}{\Gamma,x:\sigma\vdash (\lambda y:\tau.y)[z\mapsto x]:\tau\Rightarrow\tau}$$
where $M[z\mapsto N]$ means "substitute $N$ for $z$ in term $M$".  Of course,  substituting for a variable that doesn't occur does nothing.  So, in type theory, the above is (often by definition of substitution) equivalent to just $\Gamma,x:\sigma\vdash(\lambda y:\tau.y):\tau\Rightarrow\tau$.  (Closely relatedly, weakening is also often transparent in type theory.)  We then lambda abstract to get silly.

As a potential further insight, structural rules like $(\lambda y:\tau.M)[x\mapsto N] \equiv (\lambda y:\tau.M[x\mapsto N])$ with $y$ not free in $N$ come from naturality.  This particular case comes from naturality of currying (if you spell it out, you'll see how the "$y$ not free in $N$" part is handled).

However, in this case it was a bit of a fluke that this worked out.  In general, the second argument to _[_] should be a substitution, i.e. an arrow from contexts to contexts.  In this code, a context is effectively represented by a left nested tuple (ending in an empty tuple).  So if the second argument to _[_] does not return a left nested tuple, then _[_] will not behave like substitution.  For example, the expression var 0 [ var 1 ] does not correspond to $$x:\sigma, y:\sigma \vdash x[x\mapsto y] : \sigma$$ like we might think, but rather to $$x:\sigma\times\sigma, y:\sigma \vdash \mathtt{snd}(x) : \sigma$$
This second interpretation is an artifact of this particular implementation that was exposed by failing to meet the precondition of _[_].  We would get the intended behavior had we written something like var 0 [pair unit (var 1)].  It would be cleaner and closer to typical STLC syntax to have _[_] take a vector of arrows that get tupled together in a left nested manner.

That this confusion between types and contexts is so easy is particular to CCCs.  Most categorical semantics have a strict distinction between types and contexts; they live in separate categories.  This is true of the semantics in the above mentioned Bart Jacobs paper.  However, this conflation of types and contexts in CCCs makes it possible to discuss the categorical semantics without needing to introduce notions like indexed categories or fibrations.