Compiler: share type variables between nested type annotations

[evancz]

Right now you can write things like this:

id : a -> a
id x =
  let
    y : a
    y = x
  in
    y

This code is "obviously correct" but right now type variables are not shared between sub annotations. That means the y : a is talking about a fresh type variable, not the one that appears in id : a -> a. This is confusing.

Maybe it'd be good to figure out how to share them. Are there any problems that may come from this? I believe OCaml does it with no issues. Can anyone confirm or deny that?

[jvoigtlaender]

I cannot speak about OCaml, but Haskell has this feature. You have to explicitly turn it on there: https://wiki.haskell.org/Scoped_type_variables.

[jvoigtlaender]

Let me add that I don't think we want this to be a feature you have to explicitly turn on, like in Haskell. Instead, it should always be turned on. (It would be better if it were always turned on in Haskell.)

[evancz]

Yeah, I have seen how it works in Haskell. I'm just wondering if there are any nice principled reasons for having the default behavior of Haskell. I don't know of any, and I'm like 99% certain OCaml does what you'd expect. I just feel like maybe there is a good reason that I don't know about.

[mgold]

I'm in favor of this, since you cannot currently write some type annotations.

To capture the desired behavior: "let-bound type annotations have in scope type variables from the top-level definition and any parent let-expressions." Because these type variables are "in scope", they are not "fresh", and therefore should unify.

[thSoft]

I was just bitten by this, getting The type annotation does not match its definition. ... Hint: A type annotation is clashing with itself or with a sub-annotation., which hints in this direction, but does not make it obvious that the cause of the problem is this issue. (Then I remembered. :))

[sgraf812]

I was bitten by the same error as @thSoft. In Haskell, the type variable would at least have a different name (e.g. a1). This may be confusing, too (after all, where would a1 come from in your code?), so I'll suggest to emit a warning when there's a scoped type signature. Or just change to the ScopedTypeSignatures behavior.

[evancz]

This works in the latest version of the dev branch.