In the Curry-Howard isomorphism as applied to Hindley-Milner types, what proposition corresponds to a -> [a]?

Question

(Using Haskell syntax, since the question is inspired by Haskell, but it applies to general Hindley-Milner polymorphic type systems, such as SML or Elm).

If I have a type signature f :: a -> [a], what is the logical proposition encoded by that type signature?

I know that type constructors like ->, (,) correspond to "operations" in your logic: -> corresponds to the "implies" symbol $\rightarrow$.

I assume [] is a type constructor as well, and have a feeling that the answer may have something to do with its recursive definition, which I know could be implemented as something like:

data List a = Cons a (List a) | Nil

but I'm not sure what this means in logic-verse.