X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FTyCon.lhs;h=2ec4031c878432feb4d8c68a61e36b4d0ee76b32;hb=b4bf17afb2cf8b6e361cb8715f0de989e939ed1b;hp=09596993569fc1eab3e51e2e734b344f387bdfd2;hpb=b06d623b2e367a572de5daf06d6a0b12c2740471;p=ghc-hetmet.git

diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 0959699..2ec4031 100644
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -95,9 +95,128 @@ import Maybes
 import Outputable
 import FastString
 import Constants
+import Util
+import qualified Data.Data as Data
 import Data.List( elemIndex )
 \end{code}
 
+-----------------------------------------------
+	Notes about type families
+-----------------------------------------------
+
+Type synonym families
+~~~~~~~~~~~~~~~~~~~~~~
+* Type synonym families, also known as "type functions", map directly
+  onto the type functions in FC:
+
+	type family F a :: *
+	type instance F Int = Bool
+	..etc...
+
+* From the user's point of view (F Int) and Bool are simply equivalent
+  types.
+
+* A Haskell 98 type synonym is a degenerate form of a type synonym
+  family.
+
+* Type functions can't appear in the LHS of a type function:
+	type instance F (F Int) = ...	-- BAD!
+
+* In the future we might want to support
+    * closed type families (esp when we have proper kinds)
+    * injective type families (allow decomposition)
+  but we don't at the moment [2010]
+
+Note [Data type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Wrappers for data instance tycons] in MkId.lhs
+
+* Data type families are declared thus
+	data family T a :: *
+	data instance T Int = T1 | T2 Bool
+
+  Here T is the "family TyCon".
+
+* The user does not see any "equivalent types" as he did with type
+  synonym families.  He just sees constructors with types
+	T1 :: T Int
+	T2 :: Bool -> T Int
+
+* Here's the FC version of the above declarations:
+
+	data T a
+	data R:TInt = T1 | T2 Bool
+	axiom ax_ti : T Int ~ R:TInt
+
+  The R:TInt is the "representation TyCons".
+  It has an AlgTyConParent of
+	FamilyTyCon T [Int] ax_ti
+
+* The data contructor T2 has a wrapper (which is what the 
+  source-level "T2" invokes):
+
+	$WT2 :: Bool -> T Int
+	$WT2 b = T2 b `cast` sym ax_ti
+
+* A data instance can declare a fully-fledged GADT:
+
+	data instance T (a,b) where
+          X1 :: T (Int,Bool)
+	  X2 :: a -> b -> T (a,b)
+
+  Here's the FC version of the above declaration:
+
+	data R:TPair a where
+	  X1 :: R:TPair Int Bool
+	  X2 :: a -> b -> R:TPair a b
+  	axiom ax_pr :: T (a,b) ~ R:TPair a b
+
+	$WX1 :: forall a b. a -> b -> T (a,b)
+	$WX1 a b (x::a) (y::b) = X2 a b x y `cast` sym (ax_pr a b)
+
+  The R:TPair are the "representation TyCons".
+  We have a bit of work to do, to unpick the result types of the
+  data instance declaration for T (a,b), to get the result type in the
+  representation; e.g.  T (a,b) --> R:TPair a b
+
+  The representation TyCon R:TList, has an AlgTyConParent of
+
+	FamilyTyCon T [(a,b)] ax_pr
+
+* Notice that T is NOT translated to a FC type function; it just
+  becomes a "data type" with no constructors, which can be coerced inot
+  into R:TInt, R:TPair by the axioms.  These axioms
+  axioms come into play when (and *only* when) you
+  	- use a data constructor
+    	- do pattern matching
+  Rather like newtype, in fact
+
+  As a result
+
+  - T behaves just like a data type so far as decomposition is concerned
+
+  - (T Int) is not implicitly converted to R:TInt during type inference. 
+    Indeed the latter type is unknown to the programmer.
+
+  - There *is* an instance for (T Int) in the type-family instance 
+    environment, but it is only used for overlap checking
+
+  - It's fine to have T in the LHS of a type function:
+    type instance F (T a) = [a]
+
+  It was this last point that confused me!  The big thing is that you
+  should not think of a data family T as a *type function* at all, not
+  even an injective one!  We can't allow even injective type functions
+  on the LHS of a type function:
+  	type family injective G a :: *
+  	type instance F (G Int) = Bool
+  is no good, even if G is injective, because consider
+  	type instance G Int = Bool
+  	type instance F Bool = Char
+
+  So a data type family is not an injective type function. It's just a
+  data type with some axioms that connect it to other data types. 
+
 %************************************************************************
 %*									*
 \subsection{The data type}
@@ -138,12 +257,11 @@ data TyCon
 	tyConArity  :: Arity,
 
 	tyConTyVars :: [TyVar],		-- ^ The type variables used in the type constructor.
+                                        -- Invariant: length tyvars = arity
 	                                -- Precisely, this list scopes over:
 	                                --
 	                                -- 1. The 'algTcStupidTheta'
-	                                --
 					-- 2. The cached types in 'algTyConRhs.NewTyCon'
-					-- 
 					-- 3. The family instance types if present
 					--
 					-- Note that it does /not/ scope over the data constructors.
@@ -363,17 +481,11 @@ data TyConParent
   --
   --  3) A 'CoTyCon' identifying the representation
   --  type with the type instance family
-  | FamilyTyCon
+  | FamilyTyCon	  -- See Note [Data type families]
 	TyCon
 	[Type]
 	TyCon  -- c.f. Note [Newtype coercions]
 
-	--
-	-- E.g.  data intance T [a] = ...
-	-- gives a representation tycon:
-	--	data :R7T a = ...
-	-- 	axiom co a :: T [a] ~ :R7T a
-	-- with :R7T's algTcParent = FamilyTyCon T [a] co
 
 -- | Checks the invariants of a 'TyConParent' given the appropriate type class name, if any
 okParent :: Name -> TyConParent -> Bool
@@ -483,39 +595,6 @@ so the coercion tycon CoT must have
  and	arity:   0
 
 
-Note [Indexed data types] (aka data type families)
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-   See also Note [Wrappers for data instance tycons] in MkId.lhs
-
-Consider
-	data family T a
-
-	data instance T (b,c) where
-	  T1 :: b -> c -> T (b,c)
-
-Then
-  * T is the "family TyCon"
-
-  * We make "representation TyCon" :R1T, thus:
-	data :R1T b c where
-	  T1 ::	forall b c. b -> c -> :R1T b c
-
-  * It has a top-level coercion connecting it to the family TyCon
-
-	axiom :Co:R1T b c : T (b,c) ~ :R1T b c
-
-  * The data contructor T1 has a wrapper (which is what the source-level
-    "T1" invokes):
-
-	$WT1 :: forall b c. b -> c -> T (b,c)
-	$WT1 b c (x::b) (y::c) = T1 b c x y `cast` sym (:Co:R1T b c)
-
-  * The representation TyCon :R1T has an AlgTyConParent of
-
-	FamilyTyCon T [(b,c)] :Co:R1T
-
-
-
 %************************************************************************
 %*									*
 \subsection{PrimRep}
@@ -609,7 +688,7 @@ mkAlgTyCon name kind tyvars stupid rhs parent is_rec gen_info gadt_syn
   = AlgTyCon {	
 	tyConName 	 = name,
 	tyConUnique	 = nameUnique name,
-	tc_kind	 = kind,
+	tc_kind	         = kind,
 	tyConArity	 = length tyvars,
 	tyConTyVars	 = tyvars,
 	algTcStupidTheta = stupid,
@@ -617,7 +696,7 @@ mkAlgTyCon name kind tyvars stupid rhs parent is_rec gen_info gadt_syn
 	algTcParent	 = ASSERT( okParent name parent ) parent,
 	algTcRec	 = is_rec,
 	algTcGadtSyntax  = gadt_syn,
-	hasGenerics = gen_info
+	hasGenerics      = gen_info
     }
 
 -- | Simpler specialization of 'mkAlgTyCon' for classes
@@ -836,7 +915,7 @@ isOpenSynTyCon :: TyCon -> Bool
 isOpenSynTyCon tycon = isSynTyCon tycon && isOpenTyCon tycon
 
 isDecomposableTyCon :: TyCon -> Bool
--- True iff we can deocmpose (T a b c) into ((T a b) c)
+-- True iff we can decompose (T a b c) into ((T a b) c)
 -- Specifically NOT true of synonyms (open and otherwise) and coercions
 isDecomposableTyCon (SynTyCon {}) = False
 isDecomposableTyCon (CoTyCon {})  = False
@@ -1251,4 +1330,13 @@ instance Outputable TyCon where
 
 instance NamedThing TyCon where
     getName = tyConName
+
+instance Data.Typeable TyCon where
+    typeOf _ = Data.mkTyConApp (Data.mkTyCon "TyCon") []
+
+instance Data.Data TyCon where
+    -- don't traverse?
+    toConstr _   = abstractConstr "TyCon"
+    gunfold _ _  = error "gunfold"
+    dataTypeOf _ = mkNoRepType "TyCon"
 \end{code}