TAG HEAD merge 6 Aug 06 completed

[ghc-hetmet.git] / compiler / types / TyCon.lhs

diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 99afac9..83cd8f2 100644 (file)
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -238,15 +238,23 @@ The NewTyCon field nt_co is a a TyCon (a coercion constructor in fact)
 which is used for coercing from the representation type of the
 newtype, to the newtype itself. For example,
 
-   newtype T a = MkT [a]
+   newtype T a = MkT (a -> a)
 
-the NewTyCon for T will contain nt_co = CoT where CoT t : [t] :=: T t.
-This TyCon is a CoercionTyCon, so it does not have a kind on its own;
-it basically has its own typing rule for the fully-applied version.
-If the newtype T has k type variables then CoT has arity k.
+the NewTyCon for T will contain nt_co = CoT where CoT t : T t :=: t ->
+t.  This TyCon is a CoercionTyCon, so it does not have a kind on its
+own; it basically has its own typing rule for the fully-applied
+version.  If the newtype T has k type variables then CoT has arity at
+most k.  In the case that the right hand side is a type application
+ending with the same type variables as the left hand side, we
+"eta-contract" the coercion.  So if we had
+
+   newtype S a = MkT [a]
+
+then we would generate the arity 0 coercion CoS : S :=: [].  The
+primary reason we do this is to make newtype deriving cleaner.
 
 In the paper we'd write
-       axiom CoT : (forall t. [t]) :=: (forall t. T t)
+       axiom CoT : (forall t. T t) :=: (forall t. [t])
 and then when we used CoT at a particular type, s, we'd say
        CoT @ s
 which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
@@ -254,10 +262,10 @@ which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
 But in GHC we instead make CoT into a new piece of type syntax
 (like instCoercionTyCon, symCoercionTyCon etc), which must always
 be saturated, but which encodes as
-       TyConAp CoT [s]
+       TyConApp CoT [s]
 In the vocabulary of the paper it's as if we had axiom declarations
 like
-       axiom CoT t : ([t] :=: T t)
+       axiom CoT t :  T t :=: [t]
 
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~