• chak@cse.unsw.edu.au.'s avatar
    Type checking for type synonym families · 5822cb8d
    chak@cse.unsw.edu.au. authored
    This patch introduces type checking for type families of which associated
    type synonyms are a special case. E.g.
            type family Sum n m
            type instance Sum Zero n = n
            type instance Sum (Succ n) m = Succ (Sum n m)
            data Zero       -- empty type
            data Succ n     -- empty type
    In addition we support equational constraints of the form:
            ty1 ~ ty2
    (where ty1 and ty2 are arbitrary tau types) in any context where
    type class constraints are already allowed, e.g.
            data Equals a b where
                    Equals :: a ~ b => Equals a b
    The above two syntactical extensions are disabled by default. Enable
    with the -XTypeFamilies flag.
    For further documentation about the patch, see:
            * the master plan
            * the user-level documentation
    The patch is mostly backwards compatible, except for:
            * Some error messages have been changed slightly.
            * Type checking of GADTs now requires a bit more type declarations:
              not only should the type of a GADT case scrutinee be given, but also
              that of any identifiers used in the branches and the return type.
    Please report any unexpected behavior and incomprehensible error message 
    for existing code.
    Contributors (code and/or ideas):
            Tom Schrijvers
            Manuel Chakravarty
            Simon Peyton-Jones
            Martin Sulzmann 
    with special thanks to Roman Leshchinskiy
TcPat.lhs 36.5 KB