"Annotation vs. Internal Annotation" is essentially variable shadowing (and the solution is to disallow it)

[mskiptr]

This is something to consider for the next release.

While browsing the documentation I encountered this paragraph:

Annotation vs. Internal Annotation

A quite tricky case is when an outer type annotation clashes with an inner type annotation. Here is an example of this:

filter : (a -> Bool) -> List a -> List a
filter isOkay list =
  let
    keepIfOkay : a -> Maybe a
    keepIfOkay x =
      if isOkay x then Just x else Nothing
  in
    List.filterMap keepIfOkay list

This case is very unfortunate because all the type annotations are correct, but there is a detail of how type inference works right now that user-defined type variables are not shared between annotations. This can lead to probably the worst type error messages we have because the problem here is that a in the outer annotation does not equal a in the inner annotation.

For now the best route is to leave off the inner annotation. It is unfortunate, and hopefully we will be able to do a nicer thing in future releases.

Here, the top-level type annotation implicitly binds the name a, and uses it three times to construct a type. To make what this means slightly clearer, here are examples in Haskell and Idris that do so explicitly:

• filter :: forall a. (a -> Bool) -> [a] -> [a]
• filter : {a : Type} -> (a -> Bool) -> List a -> List a

At call site, a concrete value of a is passed as a hidden argument to filter and then used to instantiate a concrete type signature (like (Int -> Bool) -> List Int -> List Int).

The problem, as described in the above snippet, is that the a used in the inner type annotation is a brand new a. In Haskell binding a variable explicitly disables shadowing and lets us re-use it in any nested definitions while in Idris this a is readily available in the entire body of filter even when the binding is left implicit.

A good solution would be to let the (implicitly-bound) type variables be available in any nested type annotations and not do any variable shadowing at the type level. In case the user truly wants a new type variable, they can just use a different name. This would of course be a breaking change, but I think doing so to get rid of confusing behavior is absolutely worth it.

The only potential problem I see is that the opposite situation might become confusing. But that depends on whether we can have a good error message there. (I guess an if (a type variable is re-used) and (there is a type unification error with it) then (warn about shadowing) might be a good heuristic.)