Changes between Version 33 and Version 34 of TypeFunctionsTypeChecking


Ignore:
Timestamp:
Sep 1, 2006 4:09:00 AM (8 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsTypeChecking

    v33 v34  
    8787=== Representation of newtype instances === 
    8888 
    89 We handle newtype instances similar to data instances.  However, newtypes have no separate worker and wrapper, but only a hybrid that is categorised as a worker (see `MkIds.mkDataConIds`).  In particular, this worker gets the wrapper signature as well as an unfolding.  The wrapper signature ensures that the result type of the constructor mentions the family constructor (and not the instance representation constructor).  The body of an ordinary newtype applies the newtype coercion to move from abstract to concrete type.  In the case of a family instance, we compose the newtype coercion with the family coercion to directly move from the abstract family instance to the concrete type.  We apply the same idea in the opposite direction; cf. `MkIds.unwrapNewTypeBody`. 
     89We handle newtype instances similar to data instances.  However, newtypes have no separate worker and wrapper, but only a hybrid that is categorised as a worker (see `MkIds.mkDataConIds`).  In particular, this worker gets the wrapper signature as well as an unfolding.  The wrapper signature ensures that the result type of the constructor mentions the family constructor (and not the instance representation constructor).  The body of an ordinary newtype applies the newtype coercion to move from abstract to concrete type.  In the case of a family instance, we compose the newtype coercion with the family coercion to directly move from the abstract family instance to the concrete type.  We don't do the same in the opposite direction - i.e., in `MkIds.unwrapNewTypeBody` - as computing the right type arguments is more complicated than a simple tycon split.  Instead, we use the same mechanism in `TcPat.tcConPat` as for pattern matching, and hence elimination, of data constructors. 
     90 
     91NB: It is necessary to refine the `TyCon.isNewTyCon` predicate by introducing `TyCon.isClosedNewTyCon` and using it in all places where the predicate is used to determine whether a newtype can be expanded to its right hand side.  In principle, this is also possible for families, but only in dependence on the concrete type arguments (and newtype instances in scope), so it would be much harder to check.  Hence, for now, newtype families are opaque. 
    9092 
    9193=== Representation of equality axioms ===