Changes between Version 45 and Version 46 of TypeFunctionsTypeChecking


Ignore:
Timestamp:
Jan 4, 2007 10:43:06 PM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsTypeChecking

    v45 v46  
    33== Kind checking indexed type families == 
    44 
    5 The workhorse of kind checking type and class declarations is `TcTyClDecls.kcTyClDecls`, which is invoked by `TcTyClDecls.tcTyClDecls` once per binding group.  It handles type synonyms different from algebraic data type declarations and classes, as synonyms have a richer kind structure (making kind checking harder), but cannot be recursive (which makes kind checking easier).  We handle kind signatures (of both type functions and indexed data types) in the same way as algebraic data type declarations.  More precisely, kind signatures participate in the construction of the initial kind environment (as performed by `getInitialKind`). 
     5The workhorse of kind checking type and class declarations is `TcTyClDecls.kcTyClDecls`. It is invoked by `TcTyClDecls.tcTyClDecls` once per binding group.  It handles type synonyms different from data/newtype declarations and classes; this is as synonyms have a richer kind structure (making kind checking harder), but cannot be recursive (which makes kind checking easier).  Somehwat in contrast, we handle all flavours of family declarations in the same way as algebraic data type declarations.  More precisely, family declarations participate in the construction of the initial kind environment (as performed by `getInitialKind`). 
    66 
    7 In contrast, instances of indexed types are not processed by `TcTyClDecls.tcTyClDecls`, but by `TcInstDcls.tcInstDecls1`, which handles the heads of class instance declarations.  However, the later invokes `TcTyClDecls.tcIdxTyInstDecl` (both directly and indirectly via `IcInstDcls.tcLocalInstDecl1`, the later for associated types).  The function `tcIdxTyInstDecl` shares a lot of code with the `TcTyClDecls.kcTyClDecls` and `TcTyClDecls.tcTyClDecl`. 
     7In contrast, family instances are not processed by `TcTyClDecls.tcTyClDecls`, but by `TcInstDcls.tcInstDecls1`, which handles the heads of class instance declarations.  However, the later invokes `TcTyClDecls.tcFamInstDecl` (both directly and indirectly via `TcInstDcls.tcLocalInstDecl1`, the later for associated types).  The function `tcFamInstDecl` shares a lot of code with the `TcTyClDecls.kcTyClDecls` and `TcTyClDecls.tcTyClDecl`. 
    88 
    99== Type checking indexed type families == 
    1010 
    11 Type checking in the presence of only indexed data and newtypes is much simpler than in the presence of type functions as type equality remains purely syntactic (i.e., we do not need to change the unification procedure).  However, we need to check that the alternatives of a case expression inspecting an indexed data type contains only constructors of one member of the family.  (To relax this restriction, we would need a story for compiling open data types.) 
     11Type checking in the presence of only data and newtype families is much simpler than in the presence of type synonym families as type equality remains purely syntactic (i.e., we do not need to change the unification procedure).  However, we need to check that the alternatives of a case expression inspecting an indexed data/newtype family contains only constructors of one member of the family.  (To relax this restriction, we would need a story for compiling open data types.) 
    1212 
    13 However, this difference in complexity applies only to the type checking of expression whose types involve indexed data types and type functions, respectively.  The type checking of the declaration forms is not that different; in fact, indexed data type declarations require more effort as they introduce data type constructors, which need to behandled as well.  However, a lot of machinery can be re-used from vanilla algebraic data types. 
     13However, this difference in complexity applies only to the type checking of expression whose types involve data and type synonym families, respectively.  Type checking of the declarations themselves is not that different; in fact, data/newtype family declarations require more effort as they introduce data type constructors, which need to be handled as well.  However, a lot of machinery can be re-used from vanilla algebraic data types. 
    1414 
    15 === Type checking signatures and instances of indexed types === 
     15=== Type checking family declarations and family instances === 
    1616 
    17 Kind signatures are handled by `TcTyClsDecls.tcTyClsDecl` together with all other type and class declarations.  Within class declarations, we invoke the functions recursively to process associated types. 
     17Family declarations are handled by `TcTyClsDecls.tcTyClsDecl` together with all other type and class declarations.  Within class declarations, we invoke the function recursively to process associated types. 
    1818 
    19 Instances of indexed types are type checked by `TcTyClDecls.tcIdxTyInstDecl`; i.e., the same functions that performs their kind checking.  Kind checking and type checking of instances of indexed types can be combined, as we don't need to worry as much about recursive dependencies as we have to for standard type declarations.  In particular, the kinds of indexed types are declared by their signature and we don't have to compute any recursiveness information, as we never know whether we reached a fixed point for open types.  (Hence, we conservatively assume indexed types to be always `Recursive`.  This is safe as they are implicit loop breakers due to to implying coercions.) 
     19Family instances are type checked by `TcTyClDecls.tcFamInstDecl`; i.e., the same function that performs their kind checking.  Kind checking and type checking of family instances can be combined, as we don't need to worry as much about recursive dependencies as we have to for standard type declarations.  In particular, the kinds of families are declared by their signature and we don't have to compute any recursiveness information, as we never know whether we reached a fixed point for open types.  (Hence, we conservatively assume families and their instances to be always `Recursive`.  This is safe as they are implicit loop breakers due to implying coercions.) 
    2020 
    2121=== Deriving clauses at data instances === 
     
    3838                 | SynonymTyCon Type    -- rhs of ordinary synonym 
    3939}}} 
    40 Consequently, all functions that dependent on this field need to be extended.  In particular, `TcType.isTauTyCon` regards applications of type family constructors as ''tau types'', which is why we need to require that the right hand side of each `type instance` declaration is also a tau type.  As a result, `BuildTyCls.buildSynTyCon`'s last argument now also takes a value of type `SynTyConRhs`. 
     40Consequently, all functions that dependent on this field had to be extended.  In particular, `TcType.isTauTyCon` regards applications of type family constructors as ''tau types'', which is why we need to require that the right hand side of each `type instance` declaration is also a tau type.  As a result, `BuildTyCls.buildSynTyCon`'s last argument now also takes a value of type `SynTyConRhs`. 
    4141 
    4242=== Associated types === 
     
    5757The GHC API has a new predicate `isOpenTyCon` with the understanding that it is illegal to invoke `synTyConDefn`, `synTyConRhs`, and `tyConDataCons` on type constructors that fulfil `isOpenTyCon`. 
    5858 
    59 == Core representation of instances of indexed types == 
     59== Core representation of family instances == 
    6060 
    6161=== Representation of data instances ===