Summary

This is a proposal to support locally scoped type synonyms inside where and let binding lists, with the obvious syntax and semantics.

(Edit: This post was originally written before the polykinds feature was merged. The proposal as previously written didn't interact well with that feature; it has been rewritten to reflect the current consensus based on those interactions, as arrived at in this issue and in associated PR comment chains. Comments here about desugaring by hoisting local type synonyms to the top level are in reference to the original proposal.)

Motivation

There are a few reasons why one might want to define a local type synonym. The simplest is locality itself: sometimes it's desirable to bundle up one or two dozen functions into a ‘submodule‘ consisting of an outer function with a long list of where bindings. If those inner functions reuse a complicated type a few times such that a type synonym would be useful, a synonym defined near to where it's used is more legible than one that's out in the top-level scope, possibly off-screen. Another reason is brevity: a top-level type synonym demands a name that is unambiguous in the context of the entire module, whereas a type synonym scoped only to a single definition can be more succinct without clogging up the outer namespace. My favorite reason, though, is that defining type synonyms for types involving type variables requires you to parameterize the type synonym as well... unless it shares a scope with the type variable. Consider the difference between these two snippets—IMO, the readability gap is obvious, and continues to widen as you imagine the number of type variables involved growing:

type Foo a b c = { alpha :: a, bravo :: b, charlie :: c }
type Paths a b c = Map (Foo a b c) (Set (Foo a b c))

bigFunction :: forall a b c. ...
bigFunction ... = ...
  where
  ...
  computePaths :: ... -> { forward :: Paths a b c, backward :: Paths a b c }
  computePaths = ...

bigFunction :: forall a b c. ...
bigFunction ... = ...
  where
  type Foo = { alpha :: a, bravo :: b, charlie :: c }
  type Paths = Map Foo (Set Foo)
  ...
  computePaths :: ... -> { forward :: Paths, backward :: Paths }
  computePaths = ...

(All of these reasons have their analogs in terms of why let/where bindings for values are useful even though we have top-level value declarations—in principle, many inner bindings could be replaced with a top-level declaration that is likely to suffer from at least one of: being farther away, having a longer name, or needing more parameters. But why suffer?)

Proposal

Syntactically, make type declarations and their associated kind signatures legal inside the binding lists of let expressions, where clauses, and anything parsed similarly. Semantically, these synonyms introduce new types in the same lexical scope as a value binding in the same position. Like other let bindings, local type synonyms can't be exported or used outside of their scope (which does not include the type signature of the value containing the binding—top-level values must be annotated with types visible from the top-level scope), and like regular type synonyms, they can't have instances or cyclic definitions, and their lexical position within the binding list is irrelevant.

Previously, this proposal defined the semantics of local type synonyms in terms of a desugaring transformation; in light of the polykinds feature, this doesn't seem to be the clearest way to express or implement the desired behavior. Instead, I'll just wave my hands a little and say that local type synonyms have the same semantics as top-level type synonyms, with the following differences:

• A local type synonym is only usable in type-level expressions (to wit: type annotations on values, kind annotations on type parameters and type variables, and the bodies of other local type synonyms and their kind signatures) in the lexical scope of its declaration. It is an error to attempt to use the name of a local type synonym outside its lexical scope.
  • As a special case of the above, a local type synonym can't be used in the type signature of a value declaration enclosing the binding list in which the type synonym is declared. So, for example, a top-level type signature can only use top-level types.
  • Many would probably consider this a logical consequence of the above, but to be explicit: a local type synonym can't be exported.
• Local type synonyms and their associated kind signatures can reference type variables introduced by forall in the type signatures of enclosing value declarations, the same way that a type annotation in the same position can.
• Two local type synonyms in non-overlapping lexical scopes can have the same name, and are otherwise not related to each other.
• Types introduced by local type synonym declarations and their associated kind signatures can generally shadow outer types; this should produce a compiler warning. Specifically:
  • When two type declarations in overlapping lexical scopes (equivalently, when one scope contains the other) have the same name, the type synonym in the inner scope shadows the type in the outer scope.
    • As a special case of the above, local type synonyms can shadow top-level types (both synonyms and data types, both declared in the same file and imported).
    • A local type synonym could only possibly shadow an unqualified type. Qualified types are never shadowed, and local type synonyms can't be qualified.
  • When a parameter of a local type synonym has the same name as a type variable in scope at the local type synonym's position, the parameter shadows the type variable within the local type synonym declaration.
  • When a forall appearing in a local type synonym or its kind signature introduces a type variable with the same name as a type variable in scope at the local type synonym's position, the inner type variable shadows the outer one within the scope of its forall.
• Kind inference on local type synonyms does not generalize type parameters that are unconstrained by the body of the synonym. If such a parameter exists, its kind will be inferred, if possible, by the usage of the local type synonym in its scope.
• Errors and warnings mentioning local type synonyms must always refer to the synonym by its name as it is written, and never prefixed by the name of the module in which the local type synonym appears.
• A local type synonym should produce an UnusedName (added in Unused warnings #3819) warning if it is not used (not an UnusedDeclaration, which will only apply to top-level declarations).

This proposal neither includes nor precludes the following potential future extensions/analogous features:

• Local type operators
• Local type operator fixity declarations
• Local data, newtype, class, or instance declarations
• Local imports

Examples

-- none of the below type synonyms would be valid in this signature
foo :: forall a. a -> { left :: Int, right :: a }
foo a = result
  where
  result = result'
    where
    -- `a` here shadows outer `forall a`, but `Alpha` must remain bound to the quantified `a`
    type Bravo a = { left :: a, right :: Alpha }
    result' :: Bravo Int
    result' = { left: 0, right: a }
  type Alpha = a -- type synonyms needn't precede their use in a binding group

-- "anything parsed similarly"
bar :: Effect Int
bar = do
  -- `Alpha` would not be valid here...
  log "hello"
  let type Alpha = Int
  pure (1 :: Alpha) -- ...but it is here!

I have an only-mildly-hackish implementation of this to be offered as a PR shortly; I've been using it locally for a week and this feature has really helped me clean up some nasty signatures.