... | ... | @@ -120,7 +120,10 @@ As each `data instance` is *represented* by its own `TyCon`, we need to be able |
|
|
### Representation of newtype instances
|
|
|
|
|
|
|
|
|
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`.
|
|
|
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 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.
|
|
|
|
|
|
|
|
|
NB: 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.
|
|
|
|
|
|
### Representation of equality axioms
|
|
|
|
... | ... | |