X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FTyCon.lhs;h=c80e3a7dc7c8b3b818104eb3f39595e44e13a776;hb=5653634ead7a7f31f1a584483e53b23e78b047c2;hp=479ea7c110a81070d00e1042767629020b70bfc8;hpb=c76c69c5b62f1ca4fa52d75b0dfbd37b7eddbb09;p=ghc-hetmet.git

diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 479ea7c..c80e3a7 100644
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -252,6 +252,20 @@ 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.
 
+In the paper we'd write
+	axiom CoT : (forall t. [t]) :=: (forall t. 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])
+
+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]
+In the vocabulary of the paper it's as if we had axiom declarations
+like
+	axiom CoT t : ([t] :=: T t)
+
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~
 Consider