Changes between Version 25 and Version 26 of TypeFunctionsTypeChecking


Ignore:
Timestamp:
Aug 22, 2006 7:30:10 PM (8 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsTypeChecking

    v25 v26  
    5858data AlgTyConParent = NoParentTyCon 
    5959                    | ClassTyCon    Class 
    60                     | FamilyTyCon   TyCon 
     60                    | FamilyTyCon   TyCon     -- family tycon 
     61                                    TyCon     -- representation coercion 
    6162}}} 
    62 which is a generalisation of the old field `algTcClass` of the internal representation for datatypes, `TyCon.AlgTyCon`.  In contrast to the old `algTcClass` field, the new field also appears in `IfaceSyn.IfaceDecl`.  However, it does so as `Maybe IfaceTyCon` as we still do not want to represent class parent information in interfaces. 
     63which is a generalisation of the old field `algTcClass` of the internal representation for datatypes, `TyCon.AlgTyCon`.  In contrast to the old `algTcClass` field, the new field also appears in `IfaceSyn.IfaceDecl`.  However, it does so as `Maybe IfaceTyCon` as we still do not want to represent class parent information in interfaces and we only record the family tycon in interfaces, not the coercion.  (The latter is implicitly reconstructed upon loading an interface.) 
     64 
     65NB: The type argument variables of the representation tycon are the free variables of the instance types; i.e., the representation data type is an ordinary data type, it is neither indexed nor open.  The only give away of its special purpose is the value in `algTcParent`. 
    6366 
    6467==== The `DataCon`s of the variants of an instance ==== 
     
    7073the instance types are `[(a, b), v]`.  Whenever the field `dcInstTys` of a `DataCon` is not `Nothing`, the field `algTcParent` of its `TyCon` must be of the form `FamilyTyCon famTyCon`, where `famTyCon` is the `TyCon` of the data family to which the instance belongs.  The exact same information goes into the interface representation `IfaceSyn.IfaceConDecl` with the new field `ifConInstTys`. 
    7174 
    72 ==== The equality axiom identifying family instance and representation type ==== 
     75==== The coercion identifying family instance and representation type ==== 
    7376 
    74 === Representation of type equation axioms === 
     77As each `data instance` is ''represented'' by its own `TyCon`, we need to be able to move between the type of the family instance and that of the representation.  We do so by an adaptation of the same method used to implement newtypes with coercions (c.f., IntermediateTypes).  Newtypes store the coercion moving between representation and abstract type in the field `nt_co` of the `NewTyCon` variant of `TyCon.AlgTyConRhs`, whereas representation types for indexed data types use `algTcParent` (see above).  Newtype coercions are constructed by `Coercion.mkNewTypeCoercion`, whereas representation types for indexed data types use a similar function `Coercion.mkDataInstCoercion`, which is invoked by `BuildTyCl.buildAlgTyCon` iff it is passed family and type instance information. 
     78 
     79=== Representation of equality axioms === 
    7580 
    7681Type functions have a number of properties in common with class instances; in particular, they require a machinery for matching type patterns against types, as instance heads do during context simplification.  Hence, we probably want some structure similar to `InstEnv.Instance` for type functions - for instances this is maintained in the field `iSpec` of `TcEnv.InstInfo` (for type functions we don't need anything like `iBinds` as they are pure type-level entities).  If possible, it would be ideal if we can reuse (or generalise) some of the matching machinery for instance heads.