Super-monster patch implementing the new typechecker -- at last

This major patch implements the new OutsideIn constraint solving
algorithm in the typecheker, following our JFP paper "Modular type
inference with local assumptions".  

Done with major help from Dimitrios Vytiniotis and Brent Yorgey.

5 files changed, 101 insertions, 106 deletions

diff --git a/compiler/iface/BuildTyCl.lhs b/compiler/iface/BuildTyCl.lhs
index 8a3dfd79f5..de57feb928 100644
--- a/compiler/iface/BuildTyCl.lhs
+++ b/compiler/iface/BuildTyCl.lhs
@@ -5,10 +5,12 @@
 
 \begin{code}
 module BuildTyCl (
-	buildSynTyCon, buildAlgTyCon, buildDataCon,
+	buildSynTyCon, 
+        buildAlgTyCon, 
+        buildDataCon,
 	TcMethInfo, buildClass,
-	mkAbstractTyConRhs, mkOpenDataTyConRhs, 
-	mkNewTyConRhs, mkDataTyConRhs, setAssocFamilyPermutation
+	mkAbstractTyConRhs, 
+	mkNewTyConRhs, mkDataTyConRhs
     ) where
 
 #include "HsVersions.h"
@@ -27,7 +29,7 @@ import Type
 import Coercion
 
 import TcRnMonad
-import Util		( count )
+import Data.List	( partition )
 import Outputable
 \end{code}
 	
@@ -35,29 +37,22 @@ import Outputable
 \begin{code}
 ------------------------------------------------------
 buildSynTyCon :: Name -> [TyVar] 
-              -> SynTyConRhs 
+              -> SynTyConRhs
 	      -> Kind			-- ^ Kind of the RHS
-	      -> Maybe (TyCon, [Type])  -- ^ family instance if applicable
+	      -> TyConParent
+	      -> Maybe (TyCon, [Type])    -- ^ family instance if applicable
               -> TcRnIf m n TyCon
-
-buildSynTyCon tc_name tvs rhs@(OpenSynTyCon {}) rhs_kind _
-  = let
-      kind = mkArrowKinds (map tyVarKind tvs) rhs_kind
-    in
-    return $ mkSynTyCon tc_name kind tvs rhs NoParentTyCon
-    
-buildSynTyCon tc_name tvs rhs@(SynonymTyCon {}) rhs_kind mb_family
-  = do { -- We need to tie a knot as the coercion of a data instance depends
-	 -- on the instance representation tycon and vice versa.
-       ; tycon <- fixM (\ tycon_rec -> do 
-	 { parent <- mkParentInfo mb_family tc_name tvs tycon_rec
-	 ; let { tycon   = mkSynTyCon tc_name kind tvs rhs parent
-	       ; kind    = mkArrowKinds (map tyVarKind tvs) rhs_kind
-	       }
-         ; return tycon
-         })
-       ; return tycon 
-       }
+buildSynTyCon tc_name tvs rhs rhs_kind parent mb_family 
+  | Just fam_inst_info <- mb_family
+  = ASSERT( isNoParent parent )
+    fixM $ \ tycon_rec -> do 
+    { fam_parent <- mkFamInstParentInfo tc_name tvs fam_inst_info tycon_rec 
+    ; return (mkSynTyCon tc_name kind tvs rhs fam_parent) }
+
+  | otherwise
+  = return (mkSynTyCon tc_name kind tvs rhs parent)
+  where
+    kind = mkArrowKinds (map tyVarKind tvs) rhs_kind
 
 ------------------------------------------------------
 buildAlgTyCon :: Name -> [TyVar] 
@@ -66,23 +61,26 @@ buildAlgTyCon :: Name -> [TyVar]
 	      -> RecFlag
 	      -> Bool			-- ^ True <=> want generics functions
 	      -> Bool			-- ^ True <=> was declared in GADT syntax
+              -> TyConParent
 	      -> Maybe (TyCon, [Type])  -- ^ family instance if applicable
 	      -> TcRnIf m n TyCon
 
 buildAlgTyCon tc_name tvs stupid_theta rhs is_rec want_generics gadt_syn
-	      mb_family
-  = do { -- We need to tie a knot as the coercion of a data instance depends
-	 -- on the instance representation tycon and vice versa.
-       ; tycon <- fixM (\ tycon_rec -> do 
-	 { parent <- mkParentInfo mb_family tc_name tvs tycon_rec
-	 ; let { tycon = mkAlgTyCon tc_name kind tvs stupid_theta rhs
-				    parent is_rec want_generics gadt_syn
-	       ; kind  = mkArrowKinds (map tyVarKind tvs) liftedTypeKind
-	       }
-         ; return tycon
-         })
-       ; return tycon 
-       }
+	      parent mb_family
+  | Just fam_inst_info <- mb_family
+  = -- We need to tie a knot as the coercion of a data instance depends
+     -- on the instance representation tycon and vice versa.
+    ASSERT( isNoParent parent )
+    fixM $ \ tycon_rec -> do 
+    { fam_parent <- mkFamInstParentInfo tc_name tvs fam_inst_info tycon_rec
+    ; return (mkAlgTyCon tc_name kind tvs stupid_theta rhs
+		         fam_parent is_rec want_generics gadt_syn) }
+
+  | otherwise
+  = return (mkAlgTyCon tc_name kind tvs stupid_theta rhs
+	               parent is_rec want_generics gadt_syn)
+  where
+    kind = mkArrowKinds (map tyVarKind tvs) liftedTypeKind
 
 -- | If a family tycon with instance types is given, the current tycon is an
 -- instance of that family and we need to
@@ -95,27 +93,21 @@ buildAlgTyCon tc_name tvs stupid_theta rhs is_rec want_generics gadt_syn
 -- (2) produce a `TyConParent' value containing the parent and coercion
 --     information.
 --
-mkParentInfo :: Maybe (TyCon, [Type]) 
-             -> Name -> [TyVar] 
-             -> TyCon 
-             -> TcRnIf m n TyConParent
-mkParentInfo Nothing                  _       _   _         =
-  return NoParentTyCon
-mkParentInfo (Just (family, instTys)) tc_name tvs rep_tycon =
-  do { -- Create the coercion
-     ; co_tycon_name <- newImplicitBinder tc_name mkInstTyCoOcc
-     ; let co_tycon = mkFamInstCoercion co_tycon_name tvs
+mkFamInstParentInfo :: Name -> [TyVar] 
+             	    -> (TyCon, [Type]) 
+             	    -> TyCon 
+             	    -> TcRnIf m n TyConParent
+mkFamInstParentInfo tc_name tvs (family, instTys) rep_tycon
+  = do { -- Create the coercion
+       ; co_tycon_name <- newImplicitBinder tc_name mkInstTyCoOcc
+       ; let co_tycon = mkFamInstCoercion co_tycon_name tvs
                                         family instTys rep_tycon
-     ; return $ FamilyTyCon family instTys co_tycon
-     }
+       ; return $ FamInstTyCon family instTys co_tycon }
     
 ------------------------------------------------------
 mkAbstractTyConRhs :: AlgTyConRhs
 mkAbstractTyConRhs = AbstractTyCon
 
-mkOpenDataTyConRhs :: AlgTyConRhs
-mkOpenDataTyConRhs = OpenTyCon Nothing
-
 mkDataTyConRhs :: [DataCon] -> AlgTyConRhs
 mkDataTyConRhs cons
   = DataTyCon {
@@ -182,13 +174,6 @@ mkNewTyConRhs tycon_name tycon con
     eta_reduce tvs ty = (reverse tvs, ty)
 				
 
-setAssocFamilyPermutation :: [TyVar] -> TyThing -> TyThing
-setAssocFamilyPermutation clas_tvs (ATyCon tc) 
-  = ATyCon (setTyConArgPoss clas_tvs tc)
-setAssocFamilyPermutation _clas_tvs other
-  = pprPanic "setAssocFamilyPermutation" (ppr other)
-
-
 ------------------------------------------------------
 buildDataCon :: Name -> Bool
 	    -> [HsBang] 
@@ -249,9 +234,9 @@ mkDataConStupidTheta tycon arg_tys univ_tvs
 type TcMethInfo = (Name, DefMethSpec, Type)  -- A temporary intermediate, to communicate 
 					     -- between tcClassSigs and buildClass
 
-buildClass :: Bool			-- True <=> do not include unfoldings 
-					--	    on dict selectors
-					-- Used when importing a class without -O
+buildClass :: Bool		-- True <=> do not include unfoldings 
+				--	    on dict selectors
+				-- Used when importing a class without -O
 	   -> Name -> [TyVar] -> ThetaType
 	   -> [FunDep TyVar]		   -- Functional dependencies
 	   -> [TyThing]			   -- Associated types
@@ -272,14 +257,14 @@ buildClass no_unf class_name tvs sc_theta fds ats sig_stuff tc_isrec
 	; op_items <- mapM (mk_op_item rec_clas) sig_stuff
 	  		-- Build the selector id and default method id
 
-	; let n_value_preds   = count (not . isEqPred) sc_theta
-	      all_value_preds = n_value_preds == length sc_theta
+	; let (eq_theta, dict_theta) = partition isEqPred sc_theta
+
 	      -- We only make selectors for the *value* superclasses, 
 	      -- not equality predicates 
-
 	; sc_sel_names <- mapM  (newImplicitBinder class_name . mkSuperDictSelOcc) 
-				[1..n_value_preds]
-        ; let sc_sel_ids = [mkDictSelId no_unf sc_name rec_clas | sc_name <- sc_sel_names]
+				[1..length dict_theta]
+        ; let sc_sel_ids = [ mkDictSelId no_unf sc_name rec_clas 
+                           | sc_name <- sc_sel_names]
 	      -- We number off the Dict superclass selectors, 1, 2, 3 etc so that we 
 	      -- can construct names for the selectors. Thus
 	      --      class (C a, C b) => D a b where ...
@@ -287,23 +272,23 @@ buildClass no_unf class_name tvs sc_theta fds ats sig_stuff tc_isrec
 	      --      D_sc1, D_sc2
 	      -- (We used to call them D_C, but now we can have two different
 	      --  superclasses both called C!)
-	      --
 	
-	; let use_newtype = (n_value_preds + length sig_stuff == 1) && all_value_preds
+	; let use_newtype = null eq_theta && (length dict_theta + length sig_stuff == 1)
 		-- Use a newtype if the data constructor has 
 		-- 	(a) exactly one value field
 		--	(b) no existential or equality-predicate fields
 		-- i.e. exactly one operation or superclass taken together
 		-- See note [Class newtypes and equality predicates]
 
-		-- We play a bit fast and loose by treating the superclasses
-		-- as ordinary arguments.  That means that in the case of
+		-- We play a bit fast and loose by treating the dictionary
+		-- superclasses as ordinary arguments.  That means that in 
+                -- the case of
 		--     class C a => D a
 		-- we don't get a newtype with no arguments!
 	      args      = sc_sel_names ++ op_names
-	      arg_tys   = map mkPredTy sc_theta ++ op_tys
 	      op_tys	= [ty | (_,_,ty) <- sig_stuff]
 	      op_names  = [op | (op,_,_) <- sig_stuff]
+	      arg_tys   = map mkPredTy dict_theta ++ op_tys
               rec_tycon = classTyCon rec_clas
                
 	; dict_con <- buildDataCon datacon_name
@@ -311,7 +296,8 @@ buildClass no_unf class_name tvs sc_theta fds ats sig_stuff tc_isrec
 				   (map (const HsNoBang) args)
 				   [{- No fields -}]
 				   tvs [{- no existentials -}]
-                                   [{- No GADT equalities -}] [{- No theta -}]
+                                   [{- No GADT equalities -}] 
+                                   eq_theta
                                    arg_tys
 				   (mkTyConApp rec_tycon (mkTyVarTys tvs))
 				   rec_tycon
@@ -335,7 +321,9 @@ buildClass no_unf class_name tvs sc_theta fds ats sig_stuff tc_isrec
 	      ; atTyCons = [tycon | ATyCon tycon <- ats]
 
 	      ; result = mkClass class_name tvs fds 
-			         sc_theta sc_sel_ids atTyCons
+			         (eq_theta ++ dict_theta)  -- Equalities first
+                                 (length eq_theta)	   -- Number of equalities
+                                 sc_sel_ids atTyCons
 				 op_items tycon
 	      }
 	; traceIf (text "buildClass" <+> ppr tycon) 
diff --git a/compiler/iface/IfaceType.lhs b/compiler/iface/IfaceType.lhs
index 442ecf2e23..47772d7c46 100644
--- a/compiler/iface/IfaceType.lhs
+++ b/compiler/iface/IfaceType.lhs
@@ -265,7 +265,7 @@ instance Outputable IfaceTyCon where
 pprIfaceContext :: IfaceContext -> SDoc
 -- Prints "(C a, D b) =>", including the arrow
 pprIfaceContext []     = empty
-pprIfaceContext theta = ppr_preds theta <+> ptext (sLit "=>")
+pprIfaceContext theta = ppr_preds theta <+> darrow
 
 ppr_preds :: [IfacePredType] -> SDoc
 ppr_preds [pred] = ppr pred	-- No parens
diff --git a/compiler/iface/LoadIface.lhs b/compiler/iface/LoadIface.lhs
index ce08f6d720..31e58754a7 100644
--- a/compiler/iface/LoadIface.lhs
+++ b/compiler/iface/LoadIface.lhs
@@ -31,7 +31,6 @@ import TcRnMonad
 
 import PrelNames
 import PrelInfo
-import PrelRules
 import Rules
 import Annotations
 import InstEnv
diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs
index 5c236b306f..fa9e0ec14c 100644
--- a/compiler/iface/MkIface.lhs
+++ b/compiler/iface/MkIface.lhs
@@ -62,6 +62,7 @@ import Class
 import TyCon
 import DataCon
 import Type
+import Coercion
 import TcType
 import InstEnv
 import FamInstEnv
@@ -318,7 +319,10 @@ mkIface_ hsc_env maybe_old_fingerprint
      le_occ n1 n2 = nameOccName n1 <= nameOccName n2
 
      dflags = hsc_dflags hsc_env
+
+     deliberatelyOmitted :: String -> a
      deliberatelyOmitted x = panic ("Deliberately omitted: " ++ x)
+
      ifFamInstTcName = ifaceTyConName . ifFamInstTyCon
 
      flattenVectInfo (VectInfo { vectInfoVar   = vVar
@@ -1377,14 +1381,14 @@ tyThingToIfaceDecl (ATyCon tycon)
     tyvars = tyConTyVars tycon
     (syn_rhs, syn_ki) 
        = case synTyConRhs tycon of
-	    OpenSynTyCon ki _ -> (Nothing,               toIfaceType ki)
-	    SynonymTyCon ty   -> (Just (toIfaceType ty), toIfaceType (typeKind ty))
+	    SynFamilyTyCon  -> (Nothing,               toIfaceType (synTyConResKind tycon))
+	    SynonymTyCon ty -> (Just (toIfaceType ty), toIfaceType (typeKind ty))
 
     ifaceConDecls (NewTyCon { data_con = con })     = 
       IfNewTyCon  (ifaceConDecl con)
     ifaceConDecls (DataTyCon { data_cons = cons })  = 
       IfDataTyCon (map ifaceConDecl cons)
-    ifaceConDecls OpenTyCon {}                      = IfOpenDataTyCon
+    ifaceConDecls DataFamilyTyCon {}                = IfOpenDataTyCon
     ifaceConDecls AbstractTyCon			    = IfAbstractTyCon
 	-- The last case happens when a TyCon has been trimmed during tidying
 	-- Furthermore, tyThingToIfaceDecl is also used
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 1f846d37fb..83a24584f0 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -414,16 +414,21 @@ the forkM stuff.
 tcIfaceDecl :: Bool	-- True <=> discard IdInfo on IfaceId bindings
 	    -> IfaceDecl
 	    -> IfL TyThing
-
-tcIfaceDecl ignore_prags (IfaceId {ifName = occ_name, ifType = iface_type, 
- 	    		 	   ifIdDetails = details, ifIdInfo = info})
+tcIfaceDecl = tc_iface_decl NoParentTyCon
+
+tc_iface_decl :: TyConParent	-- For nested declarations
+              -> Bool	-- True <=> discard IdInfo on IfaceId bindings
+	      -> IfaceDecl
+	      -> IfL TyThing
+tc_iface_decl _ ignore_prags (IfaceId {ifName = occ_name, ifType = iface_type, 
+ 	                               ifIdDetails = details, ifIdInfo = info})
   = do	{ name <- lookupIfaceTop occ_name
 	; ty <- tcIfaceType iface_type
 	; details <- tcIdDetails ty details
 	; info <- tcIdInfo ignore_prags name ty info
 	; return (AnId (mkGlobalId details name ty info)) }
 
-tcIfaceDecl _ (IfaceData {ifName = occ_name, 
+tc_iface_decl parent _ (IfaceData {ifName = occ_name, 
 			  ifTyVars = tv_bndrs, 
 			  ifCtxt = ctxt, ifGadtSyntax = gadt_syn,
 			  ifCons = rdr_cons, 
@@ -434,34 +439,33 @@ tcIfaceDecl _ (IfaceData {ifName = occ_name,
     { tc_name <- lookupIfaceTop occ_name
     ; tycon <- fixM ( \ tycon -> do
 	    { stupid_theta <- tcIfaceCtxt ctxt
-	    ; mb_fam_inst  <- tcFamInst mb_family
 	    ; cons <- tcIfaceDataCons tc_name tycon tyvars rdr_cons
-	    ; buildAlgTyCon tc_name tyvars stupid_theta
-			    cons is_rec want_generic gadt_syn mb_fam_inst
+	    ; mb_fam_inst  <- tcFamInst mb_family
+	    ; buildAlgTyCon tc_name tyvars stupid_theta cons is_rec
+			    want_generic gadt_syn parent mb_fam_inst
 	    })
     ; traceIf (text "tcIfaceDecl4" <+> ppr tycon)
     ; return (ATyCon tycon) }
 
-tcIfaceDecl _ (IfaceSyn {ifName = occ_name, ifTyVars = tv_bndrs, 
-		         ifSynRhs = mb_rhs_ty,
-		         ifSynKind = kind, ifFamInst = mb_family})
+tc_iface_decl parent _ (IfaceSyn {ifName = occ_name, ifTyVars = tv_bndrs, 
+		         	  ifSynRhs = mb_rhs_ty,
+		         	  ifSynKind = kind, ifFamInst = mb_family})
    = bindIfaceTyVars_AT tv_bndrs $ \ tyvars -> do
-     { tc_name <- lookupIfaceTop occ_name
+     { tc_name  <- lookupIfaceTop occ_name
      ; rhs_kind <- tcIfaceType kind	-- Note [Synonym kind loop]
-     ; ~(rhs, fam) <- forkM (mk_doc tc_name) $ 
-       	      	      do { rhs <- tc_syn_rhs rhs_kind mb_rhs_ty
-			 ; fam <- tcFamInst mb_family
-			 ; return (rhs, fam) }
-     ; tycon <- buildSynTyCon tc_name tyvars rhs rhs_kind fam
-     ; return $ ATyCon tycon
+     ; rhs      <- forkM (mk_doc tc_name) $ 
+       	      	   tc_syn_rhs mb_rhs_ty
+     ; fam_info <- tcFamInst mb_family
+     ; tycon <- buildSynTyCon tc_name tyvars rhs rhs_kind parent fam_info
+     ; return (ATyCon tycon)
      }
    where
      mk_doc n = ptext (sLit "Type syonym") <+> ppr n
-     tc_syn_rhs kind Nothing   = return (OpenSynTyCon kind Nothing)
-     tc_syn_rhs _    (Just ty) = do { rhs_ty <- tcIfaceType ty
-		   		    ; return (SynonymTyCon rhs_ty) }
+     tc_syn_rhs Nothing   = return SynFamilyTyCon
+     tc_syn_rhs (Just ty) = do { rhs_ty <- tcIfaceType ty
+		               ; return (SynonymTyCon rhs_ty) }
 
-tcIfaceDecl ignore_prags
+tc_iface_decl _parent ignore_prags
 	    (IfaceClass {ifCtxt = rdr_ctxt, ifName = occ_name, 
 			 ifTyVars = tv_bndrs, ifFDs = rdr_fds, 
 			 ifATs = rdr_ats, ifSigs = rdr_sigs, 
@@ -473,9 +477,9 @@ tcIfaceDecl ignore_prags
     ; ctxt <- tcIfaceCtxt rdr_ctxt
     ; sigs <- mapM tc_sig rdr_sigs
     ; fds  <- mapM tc_fd rdr_fds
-    ; ats' <- mapM (tcIfaceDecl ignore_prags) rdr_ats
-    ; let ats = map (setAssocFamilyPermutation tyvars) ats'
-    ; cls  <- buildClass ignore_prags cls_name tyvars ctxt fds ats sigs tc_isrec
+    ; cls  <- fixM $ \ cls -> do
+              { ats  <- mapM (tc_iface_decl (AssocFamilyTyCon cls) ignore_prags) rdr_ats
+              ; buildClass ignore_prags cls_name tyvars ctxt fds ats sigs tc_isrec }
     ; return (AClass cls) }
   where
    tc_sig (IfaceClassOp occ dm rdr_ty)
@@ -492,7 +496,7 @@ tcIfaceDecl ignore_prags
 			   ; tvs2' <- mapM tcIfaceTyVar tvs2
 			   ; return (tvs1', tvs2') }
 
-tcIfaceDecl _ (IfaceForeign {ifName = rdr_name, ifExtName = ext_name})
+tc_iface_decl _ _ (IfaceForeign {ifName = rdr_name, ifExtName = ext_name})
   = do	{ name <- lookupIfaceTop rdr_name
 	; return (ATyCon (mkForeignTyCon name ext_name 
 					 liftedTypeKind 0)) }
@@ -507,7 +511,7 @@ tcIfaceDataCons :: Name -> TyCon -> [TyVar] -> IfaceConDecls -> IfL AlgTyConRhs
 tcIfaceDataCons tycon_name tycon _ if_cons
   = case if_cons of
 	IfAbstractTyCon	 -> return mkAbstractTyConRhs
-	IfOpenDataTyCon	 -> return mkOpenDataTyConRhs
+	IfOpenDataTyCon	 -> return DataFamilyTyCon
 	IfDataTyCon cons -> do 	{ data_cons <- mapM tc_con_decl cons
 				; return (mkDataTyConRhs data_cons) }
 	IfNewTyCon con	 -> do 	{ data_con <- tc_con_decl con