Type checking for type synonym families

This patch introduces type checking for type families of which associated
type synonyms are a special case. E.g.

        type family Sum n m

        type instance Sum Zero n = n
        type instance Sum (Succ n) m = Succ (Sum n m)

where

        data Zero       -- empty type
        data Succ n     -- empty type

In addition we support equational constraints of the form:

        ty1 ~ ty2

(where ty1 and ty2 are arbitrary tau types) in any context where
type class constraints are already allowed, e.g.

        data Equals a b where
                Equals :: a ~ b => Equals a b

The above two syntactical extensions are disabled by default. Enable
with the -XTypeFamilies flag.

For further documentation about the patch, see:

        * the master plan
          http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions

        * the user-level documentation
          http://haskell.org/haskellwiki/GHC/Indexed_types

The patch is mostly backwards compatible, except for:

        * Some error messages have been changed slightly.

        * Type checking of GADTs now requires a bit more type declarations:
          not only should the type of a GADT case scrutinee be given, but also
          that of any identifiers used in the branches and the return type.

Please report any unexpected behavior and incomprehensible error message 
for existing code.

Contributors (code and/or ideas):
        Tom Schrijvers
        Manuel Chakravarty
        Simon Peyton-Jones
        Martin Sulzmann 
with special thanks to Roman Leshchinskiy

compiler/NOTES

@@ -1,3 +1,30 @@
+Type functions
+~~~~~~~~~~~~~~
+* A Given inst should be a CoVar, not a coercion
+
+* finaliseEqInst should not need to call zonk
+
+* Why do we need fromGivenEqDict?  How could we construct 	
+	a Dict that had an EqPred?
+	newDictBndr should make an EqInst directly
+
+* tc_co should be accessed only inside Inst
+
+* Inst.mkImplicTy needs a commment about filtering out EqInsts
+  How *do* we deal with wanted equalities?
+
+* Inst.instType behaves inconsistently for EqInsts: it should
+  return an EqPred, like the instType' hack in pprDictsTheta
+
+  Consequences: adjust the uses of instType in TcSimplify
+
+* tcDeref* functions are unused, except in tcGenericNormalizeFamInst, when
+  we can equally well use TcMType.lookupTcTyVar
+
+* Coercion.mkEqPredCoI looks very peculiar.
+
+
+
 
 -------------------------
 *** unexpected failure for jtod_circint(opt)
@@ -46,18 +73,6 @@ Cmm parser notes
   do we need to assign to Node?
 
 
--------------------------
-* Relation between separate type sigs and pattern type sigs
-f :: forall a. a->a
-f :: b->b = e   -- No: monomorphic
-
-f :: forall a. a->a
-f :: forall a. a->a  -- OK
-
-f :: forall a. [a] -> [a]
-f :: forall b. b->b = e  ???
-
-
 -------------------------------
 NB: all floats are let-binds, but some non-rec lets
     may be unlifted (with RHS ok-for-speculation)
@@ -118,46 +133,6 @@ completeLazyBind: 	[given a simplified RHS]
 
 
 
-Right hand sides and arguments
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In many ways we want to treat 
-	(a) the right hand side of a let(rec), and 
-	(b) a function argument
-in the same way.  But not always!  In particular, we would
-like to leave these arguments exactly as they are, so they
-will match a RULE more easily.
-
-	f (g x, h x)	
-	g (+ x)
-
-It's harder to make the rule match if we ANF-ise the constructor,
-or eta-expand the PAP:
-
-	f (let { a = g x; b = h x } in (a,b))
-	g (\y. + x y)
-
-On the other hand if we see the let-defns
-
-	p = (g x, h x)
-	q = + x
-
-then we *do* want to ANF-ise and eta-expand, so that p and q
-can be safely inlined.   
-
-Even floating lets out is a bit dubious.  For let RHS's we float lets
-out if that exposes a value, so that the value can be inlined more vigorously.
-For example
-
-	r = let x = e in (x,x)
-
-Here, if we float the let out we'll expose a nice constructor. We did experiments
-that showed this to be a generally good thing.  But it was a bad thing to float
-lets out unconditionally, because that meant they got allocated more often.
-
-For function arguments, there's less reason to expose a constructor (it won't
-get inlined).  Just possibly it might make a rule match, but I'm pretty skeptical.
-So for the moment we don't float lets out of function arguments either.
-
 
 Eta expansion
 ~~~~~~~~~~~~~~

compiler/basicTypes/DataCon.lhs

@@ -12,9 +12,10 @@ module DataCon (
 	dataConRepType, dataConSig, dataConFullSig,
 	dataConName, dataConIdentity, dataConTag, dataConTyCon, dataConUserType,
 	dataConUnivTyVars, dataConExTyVars, dataConAllTyVars, 
-	dataConEqSpec, eqSpecPreds, dataConTheta, dataConStupidTheta, 
+	dataConEqSpec, eqSpecPreds, dataConEqTheta, dataConDictTheta, dataConStupidTheta, 
 	dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy,
-	dataConInstOrigArgTys, dataConRepArgTys, 
+	dataConInstOrigArgTys, dataConInstOrigDictsAndArgTys,
+	dataConRepArgTys, 
 	dataConFieldLabels, dataConFieldType,
 	dataConStrictMarks, dataConExStricts,
 	dataConSourceArity, dataConRepArity,
@@ -48,6 +49,7 @@ import Module
 
 import Data.Char
 import Data.Word
+import Data.List ( partition )
 \end{code}
 
 
@@ -224,27 +226,28 @@ data DataCon
 	--
 	-- 	*** As declared by the user
 	--  data T a where
-	--    MkT :: forall x y. (Ord x) => x -> y -> T (x,y)
+	--    MkT :: forall x y. (x~y,Ord x) => x -> y -> T (x,y)
 
 	-- 	*** As represented internally
 	--  data T a where
-	--    MkT :: forall a. forall x y. (a:=:(x,y), Ord x) => x -> y -> T a
+	--    MkT :: forall a. forall x y. (a:=:(x,y),x~y,Ord x) => x -> y -> T a
 	-- 
 	-- The next six fields express the type of the constructor, in pieces
 	-- e.g.
 	--
 	--	dcUnivTyVars  = [a]
 	--	dcExTyVars    = [x,y]
 	--	dcEqSpec      = [a:=:(x,y)]
-	--	dcTheta       = [Ord x]
+	--	dcEqTheta     = [x~y]	
+	--	dcDictTheta   = [Ord x]
 	--	dcOrigArgTys  = [a,List b]
 	--	dcRepTyCon       = T
 
 	dcVanilla :: Bool,	-- True <=> This is a vanilla Haskell 98 data constructor
 				--	    Its type is of form
 				--	        forall a1..an . t1 -> ... tm -> T a1..an
 				-- 	    No existentials, no coercions, nothing.
-				-- That is: dcExTyVars = dcEqSpec = dcTheta = []
+				-- That is: dcExTyVars = dcEqSpec = dcEqTheta = dcDictTheta = []
 		-- NB 1: newtypes always have a vanilla data con
 		-- NB 2: a vanilla constructor can still be declared in GADT-style 
 		--	 syntax, provided its type looks like the above.
@@ -272,11 +275,14 @@ data DataCon
 		-- Each equality is of the form (a :=: ty), where 'a' is one of 
 		-- the universally quantified type variables
 					
-	dcTheta  :: ThetaType,		-- The context of the constructor
+		-- The next two fields give the type context of the data constructor
+		-- 	(aside from the GADT constraints, 
+		--	 which are given by the dcExpSpec)
 		-- In GADT form, this is *exactly* what the programmer writes, even if
 		-- the context constrains only universally quantified variables
-		--	MkT :: forall a. Eq a => a -> T a
-		-- It may contain user-written equality predicates too
+		--	MkT :: forall a b. (a ~ b, Ord b) => a -> T a b
+	dcEqTheta   :: ThetaType,  -- The *equational* constraints
+	dcDictTheta :: ThetaType,  -- The *type-class and implicit-param* constraints
 
 	dcStupidTheta :: ThetaType,	-- The context of the data type declaration 
 					--	data Eq a => T a = ...
@@ -460,7 +466,7 @@ mkDataCon name declared_infix
 -- so the error is detected properly... it's just that asaertions here
 -- are a little dodgy.
 
-  = ASSERT( not (any isEqPred theta) )
+  = -- ASSERT( not (any isEqPred theta) )
 	-- We don't currently allow any equality predicates on
 	-- a data constructor (apart from the GADT ones in eq_spec)
     con
@@ -470,7 +476,8 @@ mkDataCon name declared_infix
 		  dcVanilla = is_vanilla, dcInfix = declared_infix,
 	  	  dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, 
 		  dcEqSpec = eq_spec, 
-		  dcStupidTheta = stupid_theta, dcTheta = theta,
+		  dcStupidTheta = stupid_theta, 
+		  dcEqTheta = eq_theta, dcDictTheta = dict_theta,
 		  dcOrigArgTys = orig_arg_tys, dcOrigResTy = orig_res_ty,
 		  dcRepTyCon = tycon, 
 		  dcRepArgTys = rep_arg_tys,
@@ -486,9 +493,10 @@ mkDataCon name declared_infix
 	-- The 'arg_stricts' passed to mkDataCon are simply those for the
 	-- source-language arguments.  We add extra ones for the
 	-- dictionary arguments right here.
-    dict_tys     = mkPredTys theta
-    real_arg_tys = dict_tys                      ++ orig_arg_tys
-    real_stricts = map mk_dict_strict_mark theta ++ arg_stricts
+    (eq_theta,dict_theta)  = partition isEqPred theta
+    dict_tys     	   = mkPredTys dict_theta
+    real_arg_tys 	   = dict_tys ++ orig_arg_tys
+    real_stricts 	   = map mk_dict_strict_mark dict_theta ++ arg_stricts
 
 	-- Example
 	--   data instance T (b,c) where 
@@ -497,6 +505,7 @@ mkDataCon name declared_infix
 	-- The representation tycon looks like this:
 	--   data :R7T b c where 
 	--	TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
+	-- In this case orig_res_ty = T (e,e)
     orig_res_ty = mkFamilyTyConApp tycon (substTyVars (mkTopTvSubst eq_spec) univ_tvs)
 
 	-- Representation arguments and demands
@@ -506,6 +515,7 @@ mkDataCon name declared_infix
     tag = assoc "mkDataCon" (tyConDataCons tycon `zip` [fIRST_TAG..]) con
     ty  = mkForAllTys univ_tvs $ mkForAllTys ex_tvs $ 
 	  mkFunTys (mkPredTys (eqSpecPreds eq_spec)) $
+	  mkFunTys (mkPredTys eq_theta) $
 		-- NB:	the dict args are already in rep_arg_tys
 		--	because they might be flattened..
 		--	but the equality predicates are not
@@ -548,8 +558,11 @@ dataConAllTyVars (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs })
 dataConEqSpec :: DataCon -> [(TyVar,Type)]
 dataConEqSpec = dcEqSpec
 
-dataConTheta :: DataCon -> ThetaType
-dataConTheta = dcTheta
+dataConEqTheta :: DataCon -> ThetaType
+dataConEqTheta = dcEqTheta
+
+dataConDictTheta :: DataCon -> ThetaType
+dataConDictTheta = dcDictTheta
 
 dataConWorkId :: DataCon -> Id
 dataConWorkId dc = case dcIds dc of
@@ -585,7 +598,7 @@ dataConStrictMarks = dcStrictMarks
 dataConExStricts :: DataCon -> [StrictnessMark]
 -- Strictness of *existential* arguments only
 -- Usually empty, so we don't bother to cache this
-dataConExStricts dc = map mk_dict_strict_mark (dcTheta dc)
+dataConExStricts dc = map mk_dict_strict_mark $ dcDictTheta dc
 
 dataConSourceArity :: DataCon -> Arity
 	-- Source-level arity of the data constructor
@@ -608,14 +621,14 @@ dataConRepStrictness dc = dcRepStrictness dc
 
 dataConSig :: DataCon -> ([TyVar], ThetaType, [Type], Type)
 dataConSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
-		    dcTheta  = theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
-  = (univ_tvs ++ ex_tvs, eqSpecPreds eq_spec ++ theta, arg_tys, res_ty)
+		    dcEqTheta  = eq_theta, dcDictTheta = dict_theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
+  = (univ_tvs ++ ex_tvs, eqSpecPreds eq_spec ++ eq_theta ++ dict_theta, arg_tys, res_ty)
 
 dataConFullSig :: DataCon 
-	       -> ([TyVar], [TyVar], [(TyVar,Type)], ThetaType, [Type], Type)
+	       -> ([TyVar], [TyVar], [(TyVar,Type)], ThetaType, ThetaType, [Type], Type)
 dataConFullSig (MkData {dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
-			dcTheta  = theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
-  = (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty)
+			dcEqTheta = eq_theta, dcDictTheta = dict_theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty})
+  = (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, res_ty)
 
 dataConOrigResTy :: DataCon -> Type
 dataConOrigResTy dc = dcOrigResTy dc
@@ -633,10 +646,11 @@ dataConUserType :: DataCon -> Type
 -- mentions the family tycon, not the internal one.
 dataConUserType  (MkData { dcUnivTyVars = univ_tvs, 
 			   dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
-			   dcTheta = theta, dcOrigArgTys = arg_tys,
+			   dcEqTheta = eq_theta, dcDictTheta = dict_theta, dcOrigArgTys = arg_tys,
 			   dcOrigResTy = res_ty })
   = mkForAllTys ((univ_tvs `minusList` map fst eq_spec) ++ ex_tvs) $
-    mkFunTys (mkPredTys theta) $
+    mkFunTys (mkPredTys eq_theta) $
+    mkFunTys (mkPredTys dict_theta) $
     mkFunTys arg_tys $
     res_ty
 
@@ -671,6 +685,21 @@ dataConInstOrigArgTys dc@(MkData {dcOrigArgTys = arg_tys,
     map (substTyWith tyvars inst_tys) arg_tys
   where
     tyvars = univ_tvs ++ ex_tvs
+
+dataConInstOrigDictsAndArgTys 
+	:: DataCon	-- Works for any DataCon
+	-> [Type]	-- Includes existential tyvar args, but NOT
+			-- equality constraints or dicts
+	-> [Type]	-- Returns just the instsantiated dicts and *value* arguments
+dataConInstOrigDictsAndArgTys dc@(MkData {dcOrigArgTys = arg_tys,
+				  dcDictTheta = dicts,       
+			          dcUnivTyVars = univ_tvs, 
+			          dcExTyVars = ex_tvs}) inst_tys
+  = ASSERT2( length tyvars == length inst_tys
+          , ptext SLIT("dataConInstOrigDictsAndArgTys") <+> ppr dc $$ ppr tyvars $$ ppr inst_tys )
+    map (substTyWith tyvars inst_tys) (mkPredTys dicts ++ arg_tys)
+  where
+    tyvars = univ_tvs ++ ex_tvs
 \end{code}
 
 These two functions get the real argument types of the constructor,