Overhaul of the rewrite rules

- Cleaned up and simplified rules
- Added many missing cases
- The rules OccursCheck and swap have been eliminated and integrate with
  the other rules; ie, Subst and Unify perform the occurs check themselves
  and they can deal with left-to-right and right-to-left oriented rewrites.
  This makes the code simpler and more efficient.
- Also added comments.

compiler/typecheck/Inst.lhs

@@ -42,7 +42,8 @@ module Inst (
 	isTyVarDict, isMethodFor, 
 
 	zonkInst, zonkInsts,
-	instToId, instToVar, instType, instName,
+	instToId, instToVar, instType, instName, instToDictBind,
+	addInstToDictBind,
 
 	InstOrigin(..), InstLoc, pprInstLoc,
 
@@ -91,6 +92,7 @@ import PrelNames
 import BasicTypes
 import SrcLoc
 import DynFlags
+import Bag
 import Maybes
 import Util
 import Outputable
@@ -205,6 +207,15 @@ tyVarsOfInst (EqInst {tci_left = ty1, tci_right = ty2}) = tyVarsOfType ty1 `unio
 
 tyVarsOfInsts insts = foldr (unionVarSet . tyVarsOfInst) emptyVarSet insts
 tyVarsOfLIE   lie   = tyVarsOfInsts (lieToList lie)
+
+
+--------------------------
+instToDictBind :: Inst -> LHsExpr TcId -> TcDictBinds
+instToDictBind inst rhs 
+  = unitBag (L (instSpan inst) (VarBind (instToId inst) rhs))
+
+addInstToDictBind :: TcDictBinds -> Inst -> LHsExpr TcId -> TcDictBinds
+addInstToDictBind binds inst rhs = binds `unionBags` instToDictBind inst rhs
 \end{code}
 
 Predicates
@@ -1005,7 +1016,7 @@ mkEqInst (EqPred ty1 ty2) co
 
 mkWantedEqInst :: PredType -> TcM Inst
 mkWantedEqInst pred@(EqPred ty1 ty2)
-  = do { cotv <- newMetaTyVar TauTv (mkCoKind ty1 ty2)
+  = do { cotv <- newMetaCoVar ty1 ty2
        ; mkEqInst pred (Left cotv)
        }
 

compiler/typecheck/TcInstDcls.lhs

@@ -688,23 +688,16 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
     returnM (unitBag main_bind)
 
 mkCoVars :: [PredType] -> TcM [TyVar]
-mkCoVars [] = return []
-mkCoVars (pred:preds) = 
-	do { uniq <- newUnique
-	   ; let name = mkSysTvName uniq FSLIT("mkCoVars")
-	   ; let tv = mkCoVar name (PredTy pred)
-	   ; tvs <- mkCoVars preds
-	   ; return (tv:tvs)
-	   }
+mkCoVars = newCoVars . map unEqPred
+  where
+    unEqPred (EqPred ty1 ty2) = (ty1, ty2)
+    unEqPred _                = panic "TcInstDcls.mkCoVars"
 
 mkMetaCoVars :: [PredType] -> TcM [TyVar]
-mkMetaCoVars [] = return []
-mkMetaCoVars (EqPred ty1 ty2:preds) = 
-	do { tv <- newMetaTyVar TauTv (mkCoKind ty1 ty2) 	  
-	   ; tvs <- mkMetaCoVars preds
-	   ; return (tv:tvs)
-	   }
-
+mkMetaCoVars = mappM eqPredToCoVar
+  where
+    eqPredToCoVar (EqPred ty1 ty2) = newMetaCoVar ty1 ty2
+    eqPredToCoVar _                = panic "TcInstDcls.mkMetaCoVars"
 
 tcMethods origin clas inst_tyvars' dfun_theta' inst_tys' 
 	  avail_insts op_items monobinds uprags

compiler/typecheck/TcMType.lhs

@@ -34,14 +34,14 @@ module TcMType (
 
   --------------------------------
   -- Creating new coercion variables
-  newCoVars,
+  newCoVars, newMetaCoVar,
 
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
   tcInstSigTyVars, zonkSigTyVar,
   tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, 
-  tcSkolSigType, tcSkolSigTyVars,
+  tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
 
   --------------------------------
   -- Checking type validity
@@ -49,7 +49,8 @@ module TcMType (
   SourceTyCtxt(..), checkValidTheta, checkFreeness,
   checkValidInstHead, checkValidInstance, 
   checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
-  validDerivPred, arityErr, 
+  checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
+  unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
 
   --------------------------------
   -- Zonking
@@ -122,6 +123,186 @@ tcInstType inst_tyvars ty
 \end{code}
 
 
+%************************************************************************
+%*									*
+	Updating tau types
+%*									*
+%************************************************************************
+
+Can't be in TcUnify, as we also need it in TcTyFuns.
+
+\begin{code}
+type SwapFlag = Bool
+	-- False <=> the two args are (actual, expected) respectively
+	-- True  <=> the two args are (expected, actual) respectively
+
+checkUpdateMeta :: SwapFlag
+	        -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+-- Update tv1, which is flexi; occurs check is alrady done
+-- The 'check' version does a kind check too
+-- We do a sub-kind check here: we might unify (a b) with (c d) 
+--	where b::*->* and d::*; this should fail
+
+checkUpdateMeta swapped tv1 ref1 ty2
+  = do	{ checkKinds swapped tv1 ty2
+	; updateMeta tv1 ref1 ty2 }
+
+updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+updateMeta tv1 ref1 ty2
+  = ASSERT( isMetaTyVar tv1 )
+    ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
+    do	{ ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
+	; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
+	; writeMutVar ref1 (Indirect ty2) 
+	}
+
+----------------
+checkKinds swapped tv1 ty2
+-- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
+-- ty2 has been zonked at this stage, which ensures that
+-- its kind has as much boxity information visible as possible.
+  | tk2 `isSubKind` tk1 = returnM ()
+
+  | otherwise
+	-- Either the kinds aren't compatible
+	--	(can happen if we unify (a b) with (c d))
+	-- or we are unifying a lifted type variable with an
+	-- 	unlifted type: e.g.  (id 3#) is illegal
+  = addErrCtxtM (unifyKindCtxt swapped tv1 ty2)	$
+    unifyKindMisMatch k1 k2
+  where
+    (k1,k2) | swapped   = (tk2,tk1)
+	    | otherwise = (tk1,tk2)
+    tk1 = tyVarKind tv1
+    tk2 = typeKind ty2
+
+----------------
+checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType
+--    (checkTauTvUpdate tv ty)
+-- We are about to update the TauTv tv with ty.
+-- Check (a) that tv doesn't occur in ty (occurs check)
+--	 (b) that ty is a monotype
+-- Furthermore, in the interest of (b), if you find an
+-- empty box (BoxTv that is Flexi), fill it in with a TauTv
+-- 
+-- Returns the (non-boxy) type to update the type variable with, or fails
+
+checkTauTvUpdate orig_tv orig_ty
+  = go orig_ty
+  where
+    go (TyConApp tc tys)
+	| isSynTyCon tc  = go_syn tc tys
+	| otherwise	 = do { tys' <- mappM go tys; return (TyConApp tc tys') }
+    go (NoteTy _ ty2) 	 = go ty2	-- Discard free-tyvar annotations
+    go (PredTy p)	 = do { p' <- go_pred p; return (PredTy p') }
+    go (FunTy arg res)   = do { arg' <- go arg; res' <- go res; return (FunTy arg' res') }
+    go (AppTy fun arg)	 = do { fun' <- go fun; arg' <- go arg; return (mkAppTy fun' arg') }
+		-- NB the mkAppTy; we might have instantiated a
+		-- type variable to a type constructor, so we need
+		-- to pull the TyConApp to the top.
+    go (ForAllTy tv ty) = notMonoType orig_ty		-- (b)
+
+    go (TyVarTy tv)
+	| orig_tv == tv = occurCheck tv                 -- (a)
+	| isTcTyVar tv  = go_tyvar tv (tcTyVarDetails tv)
+	| otherwise     = return (TyVarTy tv)
+		 -- Ordinary (non Tc) tyvars
+		 -- occur inside quantified types
+
+    go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') }
+    go_pred (IParam n ty)  = do { ty' <- go ty;        return (IParam n ty') }
+    go_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') }
+
+    go_tyvar tv (SkolemTv _) = return (TyVarTy tv)
+    go_tyvar tv (MetaTv box ref)
+	= do { cts <- readMutVar ref
+	     ; case cts of
+		  Indirect ty -> go ty 
+		  Flexi -> case box of
+				BoxTv -> fillBoxWithTau tv ref
+				other -> return (TyVarTy tv)
+	     }
+
+	-- go_syn is called for synonyms only
+	-- See Note [Type synonyms and the occur check]
+    go_syn tc tys
+	| not (isTauTyCon tc)
+	= notMonoType orig_ty	-- (b) again
+	| otherwise
+	= do { (msgs, mb_tys') <- tryTc (mapM go tys)
+	     ; case mb_tys' of
+		Just tys' -> return (TyConApp tc tys')
+				-- Retain the synonym (the common case)
+		Nothing | isOpenTyCon tc
+			  -> notMonoArgs (TyConApp tc tys)
+				-- Synonym families must have monotype args
+			| otherwise
+			  -> go (expectJust "checkTauTvUpdate" 
+					(tcView (TyConApp tc tys)))
+				-- Try again, expanding the synonym
+	     }
+
+    occurCheck tv = occurCheckErr (mkTyVarTy tv) orig_ty
+
+fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType
+-- (fillBoxWithTau tv ref) fills ref with a freshly allocated 
+--  tau-type meta-variable, whose print-name is the same as tv
+-- Choosing the same name is good: when we instantiate a function
+-- we allocate boxy tyvars with the same print-name as the quantified
+-- tyvar; and then we often fill the box with a tau-tyvar, and again
+-- we want to choose the same name.
+fillBoxWithTau tv ref 
+  = do	{ tv' <- tcInstTyVar tv		-- Do not gratuitously forget
+	; let tau = mkTyVarTy tv'	-- name of the type variable
+	; writeMutVar ref (Indirect tau)
+	; return tau }
+\end{code}
+
+Error mesages in case of kind mismatch.
+
+\begin{code}
+unifyKindMisMatch ty1 ty2
+  = zonkTcKind ty1	`thenM` \ ty1' ->
+    zonkTcKind ty2	`thenM` \ ty2' ->
+    let
+	msg = hang (ptext SLIT("Couldn't match kind"))
+		   2 (sep [quotes (ppr ty1'), 
+			   ptext SLIT("against"), 
+			   quotes (ppr ty2')])
+    in
+    failWithTc msg
+
+unifyKindCtxt swapped tv1 ty2 tidy_env	-- not swapped => tv1 expected, ty2 inferred
+	-- tv1 and ty2 are zonked already
+  = returnM msg
+  where
+    msg = (env2, ptext SLIT("When matching the kinds of") <+> 
+		 sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
+
+    (pp_expected, pp_actual) | swapped   = (pp2, pp1)
+		             | otherwise = (pp1, pp2)
+    (env1, tv1') = tidyOpenTyVar tidy_env tv1
+    (env2, ty2') = tidyOpenType  env1 ty2
+    pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
+    pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
+\end{code}
+
+Error message for failure due to an occurs check.
+
+\begin{code}
+occurCheckErr :: TcType -> TcType -> TcM a
+occurCheckErr ty containingTy
+  = do	{ env0 <- tcInitTidyEnv
+	; ty'           <- zonkTcType ty
+	; containingTy' <- zonkTcType containingTy
+	; let (env1, tidy_ty1) = tidyOpenType env0 ty'
+	      (env2, tidy_ty2) = tidyOpenType env1 containingTy'
+	      extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2]
+	; failWithTcM (env2, hang msg 2 extra) }
+  where
+    msg = ptext SLIT("Occurs check: cannot construct the infinite type:")
+\end{code}
+
 %************************************************************************
 %*									*
 	Kind variables
@@ -136,6 +317,9 @@ newCoVars spec
 			   (mkCoKind ty1 ty2)
 		 | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
 
+newMetaCoVar :: TcType -> TcType -> TcM TcTyVar
+newMetaCoVar ty1 ty2 = newMetaTyVar TauTv (mkCoKind ty1 ty2)
+
 newKindVar :: TcM TcKind
 newKindVar = do	{ uniq <- newUnique
 		; ref <- newMutVar Flexi
@@ -886,7 +1070,6 @@ kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of
 \end{code}
 
 
-
 %************************************************************************
 %*									*
 \subsection{Checking a theta or source type}
@@ -1097,6 +1280,21 @@ arityErr kind name n m
 	n_arguments | n == 0 = ptext SLIT("no arguments")
 		    | n == 1 = ptext SLIT("1 argument")
 		    | True   = hsep [int n, ptext SLIT("arguments")]
+
+-----------------
+notMonoType ty
+  = do	{ ty' <- zonkTcType ty
+	; env0 <- tcInitTidyEnv
+	; let (env1, tidy_ty) = tidyOpenType env0 ty'
+	      msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
+	; failWithTcM (env1, msg) }
+
+notMonoArgs ty
+  = do	{ ty' <- zonkTcType ty
+	; env0 <- tcInitTidyEnv
+	; let (env1, tidy_ty) = tidyOpenType env0 ty'
+	      msg = ptext SLIT("Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty)
+	; failWithTcM (env1, msg) }
 \end{code}
 
 

compiler/typecheck/TcRnTypes.lhs

@@ -715,23 +715,22 @@ data Inst
 
   | EqInst {			  -- delayed unification of the form 
 				  --  	co :: ty1 ~ ty2
-	tci_left  :: TcType,      -- ty1
-	tci_right :: TcType,      -- ty2
+	tci_left  :: TcType,      -- ty1    -- both types are...
+	tci_right :: TcType,      -- ty2    -- ...free of boxes
 	tci_co    :: Either    	  -- co
-			TcTyVar	  --	a wanted equation, with a hole, to be 
-				  --      filled with a witness for the equality
-                                  --        for equation generated by the 
-                                  --        unifier, 'ty1' is the actual and
-                                  --        'ty2' the expected type
-			Coercion, --    a given equation, with a coercion
-				  --	  witnessing the equality
-				  --         a coercion that originates from a
-				  --         signature or a GADT is a CoVar, but
-                                  --         after normalisation of coercions,
-				  --         they can be arbitrary Coercions 
-                                  --         involving constructors and 
-                                  --         pseudo-constructors like sym and 
-                                  --         trans.
+			TcTyVar	  --  - a wanted equation, with a hole, to be 
+				  --    filled with a witness for the equality;
+                                  --    for equation arising from deferring
+                                  --    unification, 'ty1' is the actual and
+                                  --    'ty2' the expected type
+			Coercion, --  - a given equation, with a coercion
+				  --	witnessing the equality;
+				  --    a coercion that originates from a
+				  --    signature or a GADT is a CoVar, but
+                                  --    after normalisation of coercions, they
+				  --    can be arbitrary Coercions involving
+                                  --    constructors and pseudo-constructors 
+                                  --    like sym and trans.
 	tci_loc   :: InstLoc,
 
 	tci_name  :: Name	-- Debugging help only: this makes it easier to

compiler/typecheck/TcSimplify.lhs

@@ -1455,7 +1455,8 @@ tcSimplifyRuleLhs wanteds
 				 -- to fromInteger; this looks fragile to me
 	     ; lookup_result <- lookupSimpleInst w'
 	     ; case lookup_result of
-		 GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
+		 GenInst ws' rhs -> 
+                   go dicts (addInstToDictBind binds w rhs) (ws' ++ ws)
 		 NoInstance	 -> pprPanic "tcSimplifyRuleLhs" (ppr w)
 	  }
 \end{code}
@@ -1705,7 +1706,7 @@ reduceContext env wanteds
 	; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
 
 	  -- 1. Normalise the *given* *equality* constraints
-	; (given_eqs, eliminate_skolems) <- normaliseGivens given_eqs0
+	; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0
 
 	  -- 2. Normalise the *given* *dictionary* constraints
 	  --    wrt. the toplevel and given equations
@@ -1713,11 +1714,11 @@ reduceContext env wanteds
                                                             given_dicts0
 
 	  -- 3. Solve the *wanted* *equation* constraints
-	; eq_irreds0 <- solveWanteds given_eqs wanted_eqs 
+	; eq_irreds0 <- solveWantedEqs given_eqs wanted_eqs 
 
 	  -- 4. Normalise the *wanted* equality constraints with respect to
 	  --    each other 
-	; eq_irreds <- normaliseWanteds eq_irreds0
+	; eq_irreds <- normaliseWantedEqs eq_irreds0
 
           -- 5. Build the Avail mapping from "given_dicts"
 	; init_state <- foldlM addGiven emptyAvails given_dicts
@@ -2299,7 +2300,9 @@ extractResults (Avails _ avails) wanteds
 
 	  Just (Given id) 
 		| id == w_id -> go avails binds irreds (w:givens) ws 
-		| otherwise  -> go avails (addBind binds w (nlHsVar id)) irreds (update_id w  id:givens) ws
+		| otherwise  -> 
+                  go avails (addInstToDictBind binds w (nlHsVar id)) irreds 
+                     (update_id w  id:givens) ws
 		-- The sought Id can be one of the givens, via a superclass chain
 		-- and then we definitely don't want to generate an x=x binding!
 
@@ -2311,7 +2314,7 @@ extractResults (Avails _ avails) wanteds
 
 	  Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds givens (ws' ++ ws)
 			     where	
-				new_binds = addBind binds w rhs
+				new_binds = addInstToDictBind binds w rhs
       where
 	w_id = instToId w	
 	update_id m@(Method{}) id = m {tci_id = id}
@@ -2348,7 +2351,7 @@ extractLocalResults (Avails _ avails) wanteds
 
 	  Just (Rhs rhs ws') -> go (add_given avails w) new_binds givens (ws' ++ ws)
 			     where	
-				new_binds = addBind binds w rhs
+				new_binds = addInstToDictBind binds w rhs
       where
 	w_id = instToId w	
 
@@ -2449,6 +2452,7 @@ addAvailAndSCs want_scs avails inst avail
 
     find_all :: IdSet -> Inst -> IdSet
     find_all so_far kid
+      | isEqInst kid                       = so_far
       | kid_id `elemVarSet` so_far	   = so_far
       | Just avail <- findAvail avails kid = findAllDeps so_far' avail
       | otherwise			   = so_far'
@@ -2915,7 +2919,7 @@ report_no_instances tidy_env mb_what insts
        ; mapM_ complain_implic implics
        ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
        ; groupErrs complain_no_inst insts3 
-       ; mapM_ complain_eq eqInsts
+       ; mapM_ eqInstMisMatch eqInsts
        }
   where
     complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
@@ -2925,13 +2929,6 @@ report_no_instances tidy_env mb_what insts
 			  (Just (tci_loc inst, tci_given inst)) 
 			  (tci_wanted inst)
 
-    complain_eq EqInst {tci_left = lty, tci_right = rty, 
-                        tci_loc = InstLoc _ _ ctxt}
-      = do { (env, msg) <- misMatchMsg lty rty
-           ; setErrCtxt ctxt $
-               failWithTcM (env, msg)
-           }
-
     check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
 	-- Right msg  => overlap message
 	-- Left  inst => no instance
@@ -3084,36 +3081,4 @@ reduceDepthErr n stack
 	  nest 4 (pprStack stack)]
 
 pprStack stack = vcat (map pprInstInFull stack)
-
------------------------
-misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
--- Generate the message when two types fail to match,
--- going to some trouble to make it helpful.
--- The argument order is: actual type, expected type
-misMatchMsg ty_act ty_exp
-  = do	{ env0 <- tcInitTidyEnv
-        ; ty_exp <- zonkTcType ty_exp
-        ; ty_act <- zonkTcType ty_act
-	; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
-	; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
-	; return (env2, 
-                  sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp, 
-			    nest 7 $
-                              ptext SLIT("against inferred type") <+> pp_act],
-		       nest 2 (extra_exp $$ extra_act)]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty
-  = do	{ let (env1, tidy_ty) = tidyOpenType env ty
-	; (env2, extra) <- ppr_extra env1 tidy_ty
-	; return (env2, quotes (ppr tidy_ty), extra) }
-
--- (ppr_extra env ty) shows extra info about 'ty'
-ppr_extra env (TyVarTy tv)
-  | isSkolemTyVar tv || isSigTyVar tv
-  = return (env1, pprSkolTvBinding tv1)
-  where
-    (env1, tv1) = tidySkolemTyVar env tv
-
-ppr_extra env ty = return (env, empty)		-- Normal case
 \end{code}

compiler/typecheck/TcUnify.lhs

@@ -22,7 +22,7 @@ module TcUnify (
   unifyType, unifyTypeList, unifyTheta,
   unifyKind, unifyKinds, unifyFunKind, 
   checkExpectedKind, 
-  preSubType, boxyMatchTypes,
+  preSubType, boxyMatchTypes, 
 
   --------------------------------
   -- Holes
@@ -1126,9 +1126,9 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
         -- need to defer unification by generating a wanted equality constraint.
     go1 outer ty1 ty2
       | ty1_is_fun || ty2_is_fun
-      = do { (coi1, ty1') <- if ty1_is_fun then tcNormalizeFamInst ty1 
+      = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1 
                                            else return (IdCo, ty1)
-	   ; (coi2, ty2') <- if ty2_is_fun then tcNormalizeFamInst ty2 
+	   ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2 
                                            else return (IdCo, ty2)
 	   ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2'
 		    then do { -- One type family app can't be reduced yet
@@ -1329,7 +1329,7 @@ uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2
       | isOpenSynTyConApp non_var_ty2
       =           -- 'non_var_ty2's outermost constructor is a type family,
                   -- which we may may be able to normalise
-        do { (coi2, ty2') <- tcNormalizeFamInst non_var_ty2
+        do { (coi2, ty2') <- tcNormaliseFamInst non_var_ty2
            ; case coi2 of
 	       IdCo   ->   -- no progress, but maybe after other instantiations
 		         defer_unification outer swapped (TyVarTy tv1) ps_ty2
@@ -1390,7 +1390,7 @@ defer_unification outer False ty1 ty2
   = do	{ ty1' <- unBox ty1 >>= zonkTcType      -- unbox *and* zonk..
  	; ty2' <- unBox ty2 >>= zonkTcType      -- ..see preceding note
         ; traceTc $ text "deferring:" <+> ppr ty1 <+> text "~" <+> ppr ty2
-	; cotv <- newMetaTyVar TauTv (mkCoKind ty1' ty2')
+	; cotv <- newMetaCoVar ty1' ty2'
 		-- put ty1 ~ ty2 in LIE
 		-- Left means "wanted"
 	; inst <- (if outer then popErrCtxt else id) $
@@ -1503,126 +1503,6 @@ uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
 	-- Try to update sys-y type variables in preference to ones
 	-- gotten (say) by instantiating a polymorphic function with
 	-- a user-written type sig
-	
-----------------
-checkUpdateMeta :: SwapFlag
-	        -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
--- Update tv1, which is flexi; occurs check is alrady done
--- The 'check' version does a kind check too
--- We do a sub-kind check here: we might unify (a b) with (c d) 
---	where b::*->* and d::*; this should fail
-
-checkUpdateMeta swapped tv1 ref1 ty2
-  = do	{ checkKinds swapped tv1 ty2
-	; updateMeta tv1 ref1 ty2 }
-
-updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
-updateMeta tv1 ref1 ty2
-  = ASSERT( isMetaTyVar tv1 )
-    ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
-    do	{ ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
-	; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
-	; writeMutVar ref1 (Indirect ty2) 
-	}
-
-----------------
-checkKinds swapped tv1 ty2
--- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
--- ty2 has been zonked at this stage, which ensures that
--- its kind has as much boxity information visible as possible.
-  | tk2 `isSubKind` tk1 = returnM ()
-
-  | otherwise
-	-- Either the kinds aren't compatible
-	--	(can happen if we unify (a b) with (c d))
-	-- or we are unifying a lifted type variable with an
-	-- 	unlifted type: e.g.  (id 3#) is illegal
-  = addErrCtxtM (unifyKindCtxt swapped tv1 ty2)	$
-    unifyKindMisMatch k1 k2
-  where
-    (k1,k2) | swapped   = (tk2,tk1)
-	    | otherwise = (tk1,tk2)
-    tk1 = tyVarKind tv1
-    tk2 = typeKind ty2
-
-----------------
-checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType
---    (checkTauTvUpdate tv ty)
--- We are about to update the TauTv tv with ty.
--- Check (a) that tv doesn't occur in ty (occurs check)
---	 (b) that ty is a monotype
--- Furthermore, in the interest of (b), if you find an
--- empty box (BoxTv that is Flexi), fill it in with a TauTv
--- 
--- Returns the (non-boxy) type to update the type variable with, or fails
-
-checkTauTvUpdate orig_tv orig_ty
-  = go orig_ty
-  where
-    go (TyConApp tc tys)
-	| isSynTyCon tc  = go_syn tc tys
-	| otherwise	 = do { tys' <- mappM go tys; return (TyConApp tc tys') }
-    go (NoteTy _ ty2) 	 = go ty2	-- Discard free-tyvar annotations
-    go (PredTy p)	 = do { p' <- go_pred p; return (PredTy p') }
-    go (FunTy arg res)   = do { arg' <- go arg; res' <- go res; return (FunTy arg' res') }
-    go (AppTy fun arg)	 = do { fun' <- go fun; arg' <- go arg; return (mkAppTy fun' arg') }
-		-- NB the mkAppTy; we might have instantiated a
-		-- type variable to a type constructor, so we need
-		-- to pull the TyConApp to the top.
-    go (ForAllTy tv ty) = notMonoType orig_ty		-- (b)
-
-    go (TyVarTy tv)
-	| orig_tv == tv = occurCheck tv orig_ty		-- (a)
-	| isTcTyVar tv  = go_tyvar tv (tcTyVarDetails tv)
-	| otherwise     = return (TyVarTy tv)
-		 -- Ordinary (non Tc) tyvars
-		 -- occur inside quantified types
-
-    go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') }
-    go_pred (IParam n ty)  = do { ty' <- go ty;        return (IParam n ty') }
-    go_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') }
-
-    go_tyvar tv (SkolemTv _) = return (TyVarTy tv)
-    go_tyvar tv (MetaTv box ref)
-	= do { cts <- readMutVar ref
-	     ; case cts of
-		  Indirect ty -> go ty 
-		  Flexi -> case box of
-				BoxTv -> fillBoxWithTau tv ref
-				other -> return (TyVarTy tv)
-	     }
-
-	-- go_syn is called for synonyms only
-	-- See Note [Type synonyms and the occur check]
-    go_syn tc tys
-	| not (isTauTyCon tc)
-	= notMonoType orig_ty	-- (b) again
-	| otherwise
-	= do { (msgs, mb_tys') <- tryTc (mapM go tys)
-	     ; case mb_tys' of
-		Just tys' -> return (TyConApp tc tys')
-				-- Retain the synonym (the common case)
-		Nothing | isOpenTyCon tc
-			  -> notMonoArgs (TyConApp tc tys)
-				-- Synonym families must have monotype args
-			| otherwise
-			  -> go (expectJust "checkTauTvUpdate" 
-					(tcView (TyConApp tc tys)))
-				-- Try again, expanding the synonym
-	     }
-
-fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType
--- (fillBoxWithTau tv ref) fills ref with a freshly allocated