wiki:LiberalTypeSynonyms

Version 2 (modified by simonmar@…, 6 years ago) (diff)

document the choice about when kind inference takes place, and add Ross's objections

Liberal Type Synonyms

Brief Explanation

See the GHC Documentation on this extension.

The basic idea is that type validity checking is done after expanding type synonyms. This means that type synonyms can be written unsaturated, as long as the result of expanding synonyms leaves everything saturated. This is sometimes quite useful.

There are also interactions with RankNTypes - a type synonym may expand to a quantified type.

Proposal

Adopt GHC's approach to type synonym expansion.

Design choices

Should kind inference be done before, or after expanding type synonyms? That is, should a type synonym have a fixed kind or not?

Currently GHC does kind inference before expanding type synonyms, and gives each type synonym a fixed kind. The following program is rejected:

type T f a = f a

x :: T (T (,) Int) Float
x = (1,2.0)

gives

syn.hs:5:10:
    `(,)' is not applied to enough type arguments
    Expected kind `* -> *', but `(,)' has kind `* -> * -> *'
    In the type `T (,) Int'
    In the type `T (T (,) Int) Float'
    In the type signature for `x':
      x :: T (T (,) Int) Float 

In favour of GHC's approach is that type errors are more likely to be given in terms of types that the programmer actually wrote. However, this does reject more programs, and perhaps it would be simpler to treat type synonyms uniformly as macros, without kinds?

References

Tickets

#102
add Liberal Type Synonyms

Pros

  • Small generalisation
  • Easily specified
  • Quite handy

Cons

  • It's so ... syntactic.
  • There are the usual worries about deferred checking leading to less informative diagnostics.