compiler/typecheck/TcEvidence.lhs

@@ -36,7 +36,7 @@ import Var
 import PprCore ()   -- Instance OutputableBndr TyVar
 import TypeRep  -- Knows type representation
 import TcType
-import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe, getEqPredTys )
+import Type( tyConAppArgN, tyConAppTyCon_maybe, getEqPredTys )
 import TysPrim( funTyCon )
 import TyCon
 import PrelNames
@@ -114,7 +114,7 @@ isEqVar v = case tyConAppTyCon_maybe (varType v) of
 
 isTcReflCo_maybe :: TcCoercion -> Maybe TcType
 isTcReflCo_maybe (TcRefl ty) = Just ty
-isTcReflCo_maybe _             = Nothing
+isTcReflCo_maybe _           = Nothing
 
 isTcReflCo :: TcCoercion -> Bool
 isTcReflCo (TcRefl {}) = True
@@ -185,13 +185,12 @@ mkTcInstCos co tys          = foldl TcInstCo co tys
 
 mkTcCoVarCo :: EqVar -> TcCoercion
 -- ipv :: s ~ t  (the boxed equality type)
-mkTcCoVarCo ipv
-  | ty1 `eqType` ty2 = TcRefl ty1
-  | otherwise        = TcCoVarCo ipv
-  where
-    (ty1, ty2) = case getEqPredTys_maybe (varType ipv) of
-        Nothing  -> pprPanic "mkCoVarLCo" (ppr ipv)
-        Just tys -> tys
+mkTcCoVarCo ipv = TcCoVarCo ipv
+  -- Previously I checked for (ty ~ ty) and generated Refl,
+  -- but in fact ipv may not even (visibly) have a (t1 ~ t2) type, because
+  -- the constraint solver does not substitute in the types of
+  -- evidence variables as it goes.  In any case, the optimisation
+  -- will be done in the later zonking phase
 \end{code}
 
 \begin{code}
@@ -245,11 +244,9 @@ coVarsOfTcCo tc_co
     go (TcLetCo {}) = emptyVarSet    -- Harumph. This does legitimately happen in the call
                                      -- to evVarsOfTerm in the DEBUG check of setEvBind
 
-    -- We expect only coercion bindings
+    -- We expect only coercion bindings, so use evTermCoercion 
     go_bind :: EvBind -> VarSet
-    go_bind (EvBind _ (EvCoercion co)) = go co
-    go_bind (EvBind _ (EvId v))        = unitVarSet v
-    go_bind other = pprPanic "coVarsOfTcCo:Bind" (ppr other)
+    go_bind (EvBind _ tm) = go (evTermCoercion tm)
 
     get_bndrs :: Bag EvBind -> VarSet
     get_bndrs = foldrBag (\ (EvBind b _) bs -> extendVarSet bs b) emptyVarSet 
@@ -493,28 +490,28 @@ data EvLit
 
 \end{code}
 
-Note [Coecion evidence terms]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Notice that a coercion variable (v :: t1 ~ t2) can be represented as an EvTerm
-in two different ways:
-   EvId v
-   EvCoercion (TcCoVarCo v)
-
-An alternative would be 
-
-* To establish the invariant that coercions are represented only 
-   by EvCoercion
-
-* To maintain the invariant by smart constructors.  Eg
-     mkEvCast (EvCoercion c1) c2 = EvCoercion (TcCastCo c1 c2)
-     mkEvCast t c = EvCast t c
+Note [Coercion evidence terms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A "coercion evidence term" takes one of these forms
+   co_tm ::= EvId v           where v :: t1 ~ t2
+           | EvCoercion co
+           | EvCast co_tm co
 
 We do quite often need to get a TcCoercion from an EvTerm; see
-'evTermCoercion'.  Notice that as well as EvId and EvCoercion it may see
-an EvCast.
-
-I don't think it matters much... but maybe we'll find a good reason to
-do one or the other.
+'evTermCoercion'.
+
+INVARIANT: The evidence for any constraint with type (t1~t2) is 
+a coercion evidence term.  Consider for example
+    [G] g :: F Int a
+If we have
+    ax7 a :: F Int a ~ (a ~ Bool)
+then we do NOT generate the constraint
+    [G} (g |> ax7 a) :: a ~ Bool
+because that does not satisfy the invariant.  Instead we make a binding
+    g1 :: a~Bool = g |> ax7 a
+and the constraint
+    [G] g1 :: a~Bool
+See Trac [7238]
 
 Note [EvKindCast] 
 ~~~~~~~~~~~~~~~~~ 

compiler/typecheck/TcHsSyn.lhs

@@ -29,7 +29,7 @@ module TcHsSyn (
 	zonkTopDecls, zonkTopExpr, zonkTopLExpr, 
 	zonkTopBndrs, zonkTyBndrsX,
         emptyZonkEnv, mkEmptyZonkEnv, mkTyVarZonkEnv, 
-        zonkTcTypeToType, zonkTcTypeToTypes
+        zonkTcTypeToType, zonkTcTypeToTypes, zonkTyVarOcc,
   ) where
 
 #include "HsVersions.h"
@@ -1158,26 +1158,25 @@ zonkEvBinds env binds
 
 zonkEvBind :: ZonkEnv -> EvBind -> TcM EvBind
 zonkEvBind env (EvBind var term)
-  -- This function has some special cases for avoiding re-zonking the
-  -- same types many types. See Note [Optimized Evidence Binding Zonking]
   = case term of 
-      -- Fast path for reflexivity coercions:
+      -- Special-case fast paths for small coercions
+      -- NB: could be optimized further! (e.g. SymCo cv)
+      -- See Note [Optimized Evidence Binding Zonking]
       EvCoercion co 
         | Just ty <- isTcReflCo_maybe co
-        ->
-          do { zty  <- zonkTcTypeToType env ty
-             ; let var' = setVarType var (mkEqPred zty zty)
-             ; return (EvBind var' (EvCoercion (mkTcReflCo zty))) }
+        -> do { zty  <- zonkTcTypeToType env ty
+              ; let var' = setVarType var (mkEqPred zty zty)
+                  -- Here we save the task of zonking var's type, 
+                  -- because we know just what it is!
+              ; return (EvBind var' (EvCoercion (mkTcReflCo zty))) }
 
-      -- Fast path for variable-variable bindings 
-      -- NB: could be optimized further! (e.g. SymCo cv)
         | Just cv <- getTcCoVar_maybe co 
         -> do { let cv'   = zonkIdOcc env cv -- Just lazily look up
                     term' = EvCoercion (TcCoVarCo cv')
                     var'  = setVarType var (varType cv')
               ; return (EvBind var' term') }
 
-      -- Ugly safe and slow path
+      -- The default path
       _ -> do { var'  <- {-# SCC "zonkEvBndr" #-} zonkEvBndr env var
               ; term' <- zonkEvTerm env term 
               ; return (EvBind var' term')
@@ -1238,29 +1237,16 @@ not the ill-kinded Any BOX).
 
 Note [Optimized Evidence Binding Zonking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-When optimising evidence binds we may come accross situations where 
-a coercion is just reflexivity: 
+When optimising evidence binds we may come across situations where 
+a coercion looks like
       cv = ReflCo ty
-In such a case it is a waste of time to zonk both ty and the type 
-of the coercion, especially if the types involved are huge. For this
-reason this case is optimized to only zonk 'ty' and set the type of 
-the variable to be that zonked type.
-
-Another case that hurts a lot are simple coercion bindings of the form:
-      cv1 = cv2
-      cv3 = cv1
-      cv4 = cv2 
-etc. In all such cases it is very easy to just get the zonked type of 
-cv2 and use it to set the type of the LHS coercion variable without zonking
-twice. Though this case is funny, it can happen due the way that evidence 
-from spontaneously solved goals is now used.
-See Note [Optimizing Spontaneously Solved Goals] about this.
-
-NB: That these optimizations are independently useful, regardless of the 
-constraint solver strategy.
-
-DV, TODO: followup on this note mentioning new examples I will add to perf/
+or    cv1 = cv2
+where the type 'ty' is big.  In such cases it is a waste of time to zonk both 
+  * The variable on the LHS
+  * The coercion on the RHS
+Rather, we can zonk the coercion, take its type and use that for 
+the variable.  For big coercions this might be a lose, though, so we
+just have a fast case for a couple of special cases.
 
 
 \begin{code}

compiler/typecheck/TcHsType.lhs

@@ -48,7 +48,6 @@ import {-# SOURCE #-}	TcSplice( tcSpliceType )
 import HsSyn
 import TcHsSyn ( zonkTcTypeToType, emptyZonkEnv )
 import TcRnMonad
-import RnEnv   ( dataKindsErr )
 import TcEvidence( HsWrapper )
 import TcEnv
 import TcMType
@@ -70,13 +69,14 @@ import TysWiredIn
 import BasicTypes
 import SrcLoc
 import DynFlags ( ExtensionFlag( Opt_DataKinds ) )
+import Unique
 import UniqSupply
 import Outputable
 import FastString
 import Util
 
 import Control.Monad ( unless, when, zipWithM )
-import PrelNames(ipClassName)
+import PrelNames( ipClassName, funTyConKey )
 \end{code}
 
 
@@ -317,12 +317,28 @@ tc_lhs_type (L span ty) exp_kind
 tc_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [TcType]
 tc_lhs_types tys_w_kinds = mapM (uncurry tc_lhs_type) tys_w_kinds
 
+------------------------------------------
+tc_fun_type :: HsType Name -> LHsType Name -> LHsType Name -> ExpKind -> TcM TcType
+-- We need to recognise (->) so that we can construct a FunTy, 
+-- *and* we need to do by looking at the Name, not the TyCon
+-- (see Note [Zonking inside the knot]).  For example,
+-- consider  f :: (->) Int Int  (Trac #7312)
+tc_fun_type ty ty1 ty2 exp_kind@(EK _ ctxt)
+  = do { ty1' <- tc_lhs_type ty1 (EK openTypeKind ctxt)
+       ; ty2' <- tc_lhs_type ty2 (EK openTypeKind ctxt)
+       ; checkExpectedKind ty liftedTypeKind exp_kind
+       ; return (mkFunTy ty1' ty2') }
+
 ------------------------------------------
 tc_hs_type :: HsType Name -> ExpKind -> TcM TcType
 tc_hs_type (HsParTy ty)        exp_kind = tc_lhs_type ty exp_kind
 tc_hs_type (HsDocTy ty _)      exp_kind = tc_lhs_type ty exp_kind
 tc_hs_type (HsQuasiQuoteTy {}) _ = panic "tc_hs_type: qq"	-- Eliminated by renamer
-tc_hs_type (HsBangTy {})       _ = panic "tc_hs_type: bang"   -- Unwrapped by con decls
+tc_hs_type ty@(HsBangTy {})    _
+    -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
+    -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
+    -- bangs are invalid, so fail. (#7210)
+    = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
 tc_hs_type (HsRecTy _)         _ = panic "tc_hs_type: record" -- Unwrapped by con decls
       -- Record types (which only show up temporarily in constructor 
       -- signatures) should have been removed by now
@@ -333,24 +349,30 @@ tc_hs_type hs_ty@(HsTyVar name) exp_kind
        ; checkExpectedKind hs_ty k exp_kind
        ; return ty }
 
-tc_hs_type ty@(HsFunTy ty1 ty2) exp_kind@(EK _ ctxt)
-  = do { ty1' <- tc_lhs_type ty1 (EK openTypeKind ctxt)
-       ; ty2' <- tc_lhs_type ty2 (EK openTypeKind ctxt)
-       ; checkExpectedKind ty liftedTypeKind exp_kind
-       ; return (mkFunTy ty1' ty2') }
+tc_hs_type ty@(HsFunTy ty1 ty2) exp_kind
+  = tc_fun_type ty ty1 ty2 exp_kind
 
 tc_hs_type hs_ty@(HsOpTy ty1 (_, l_op@(L _ op)) ty2) exp_kind
+  | op `hasKey` funTyConKey
+  = tc_fun_type hs_ty ty1 ty2 exp_kind
+  | otherwise
   = do { (op', op_kind) <- tcTyVar op
        ; tys' <- tcCheckApps hs_ty l_op op_kind [ty1,ty2] exp_kind
        ; return (mkNakedAppTys op' tys') }
          -- mkNakedAppTys: see Note [Zonking inside the knot]
 
 tc_hs_type hs_ty@(HsAppTy ty1 ty2) exp_kind
-  = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
-       ; (fun_ty', fun_kind) <- tc_infer_lhs_type fun_ty
+  | L _ (HsTyVar fun) <- fun_ty
+  , fun `hasKey` funTyConKey
+  , [fty1,fty2] <- arg_tys
+  = tc_fun_type hs_ty fty1 fty2 exp_kind
+  | otherwise
+  = do { (fun_ty', fun_kind) <- tc_infer_lhs_type fun_ty
        ; arg_tys' <- tcCheckApps hs_ty fun_ty fun_kind arg_tys exp_kind
        ; return (mkNakedAppTys fun_ty' arg_tys') }
          -- mkNakedAppTys: see Note [Zonking inside the knot]
+  where
+    (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
 
 --------- Foralls
 tc_hs_type (HsForAllTy _ hs_tvs context ty) exp_kind
@@ -405,8 +427,8 @@ tc_hs_type hs_ty@(HsExplicitListTy _k tys) exp_kind
        ; checkExpectedKind hs_ty (mkPromotedListTy kind) exp_kind
        ; return (foldr (mk_cons kind) (mk_nil kind) taus) }
   where
-    mk_cons k a b = mkTyConApp (buildPromotedDataCon consDataCon) [k, a, b]
-    mk_nil  k     = mkTyConApp (buildPromotedDataCon nilDataCon) [k]
+    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
+    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
 
 tc_hs_type hs_ty@(HsExplicitTupleTy _ tys) exp_kind
   = do { tks <- mapM tc_infer_lhs_type tys
@@ -567,7 +589,12 @@ tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
        ; thing <- tcLookup name
        ; traceTc "lk2" (ppr name <+> ppr thing)
        ; case thing of
-           ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
+           ATyVar _ tv 
+              | isKindVar tv
+              -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr tv)
+                             <+> ptext (sLit "used as a type"))
+              | otherwise
+              -> return (mkTyVarTy tv, tyVarKind tv)
 
            AThing kind -> do { tc <- get_loopy_tc name
                              ; inst_tycon (mkNakedTyConApp tc) kind }
@@ -576,12 +603,10 @@ tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
            AGlobal (ATyCon tc) -> inst_tycon (mkTyConApp tc) (tyConKind tc)
 
            AGlobal (ADataCon dc)
-             | isPromotableType ty -> inst_tycon (mkTyConApp tc) (tyConKind tc)
+             | Just tc <- promoteDataCon_maybe dc
+             -> inst_tycon (mkTyConApp tc) (tyConKind tc)
              | otherwise -> failWithTc (quotes (ppr dc) <+> ptext (sLit "of type")
-                            <+> quotes (ppr ty) <+> ptext (sLit "is not promotable"))
-             where
-               ty = dataConUserType dc
-               tc = buildPromotedDataCon dc
+                            <+> quotes (ppr (dataConUserType dc)) <+> ptext (sLit "is not promotable"))
 
            APromotionErr err -> promotionErr name err
 
@@ -1347,7 +1372,7 @@ tc_lhs_kind (L span ki) = setSrcSpan span (tc_hs_kind ki)
 
 -- The main worker
 tc_hs_kind :: HsKind Name -> TcM Kind
-tc_hs_kind k@(HsTyVar _)   = tc_kind_app k []
+tc_hs_kind (HsTyVar tc)    = tc_kind_var_app tc []
 tc_hs_kind k@(HsAppTy _ _) = tc_kind_app k []
 
 tc_hs_kind (HsParTy ki) = tc_lhs_kind ki
@@ -1402,7 +1427,7 @@ tc_kind_var_app name arg_kis
   	           ; unless data_kinds $ addErr (dataKindsErr name)
   	     	   ; case isPromotableTyCon tc of
   	     	       Just n | n == length arg_kis ->
-  	     	         return (mkTyConApp (buildPromotedTyCon tc) arg_kis)
+  	     	         return (mkTyConApp (promoteTyCon tc) arg_kis)
   	     	       Just _  -> tycon_err tc "is not fully applied"
   	     	       Nothing -> tycon_err tc "is not promotable" }
 
@@ -1437,6 +1462,11 @@ tc_kind_var_app name arg_kis
    tycon_err tc msg = failWithTc (quotes (ppr tc) <+> ptext (sLit "of kind")
                                   <+> quotes (ppr (tyConKind tc)) <+> ptext (sLit msg))
 
+dataKindsErr :: Name -> SDoc
+dataKindsErr name
+  = hang (ptext (sLit "Illegal kind:") <+> quotes (ppr name))
+       2 (ptext (sLit "Perhaps you intended to use -XDataKinds"))
+
 promotionErr :: Name -> PromotionErr -> TcM a
 promotionErr name err
   = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> ptext (sLit "cannot be used here"))

compiler/typecheck/TcInstDcls.lhs

@@ -432,7 +432,7 @@ addFamInsts :: [FamInst] -> TcM a -> TcM a
 --        (b) the type envt with stuff from data type decls
 addFamInsts fam_insts thing_inside
   = tcExtendLocalFamInstEnv fam_insts $ 
-    tcExtendGlobalEnvImplicit things  $ 
+    tcExtendGlobalEnv things $
     do { traceTc "addFamInsts" (pprFamInsts fam_insts)
        ; tcg_env <- tcAddImplicits things
        ; setGblEnv tcg_env thing_inside }

compiler/typecheck/TcInteract.lhs

@@ -47,7 +47,6 @@ import Control.Monad ( foldM )
 
 import VarEnv
 import qualified Data.Traversable as Traversable
-import Data.Maybe ( isJust )
 
 import Control.Monad( when, unless )
 import Pair ()
@@ -763,19 +762,6 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
                                   , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 }) 
                     wi@(CFunEqCan { cc_ev = fl2, cc_fun = tc2
                                   , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
-{-  ToDo: Check with Dimitrios
-  | lhss_match  
-  , isSolved fl1 -- Inert is solved and we can simply ignore it
-                 -- when workitem is given/solved
-  , isGiven fl2
-  = irInertConsumed "FunEq/FunEq"
-  | lhss_match
-  , isSolved fl2 -- Workitem is solved and we can ignore it when
-                 -- the inert is given/solved
-  , isGiven fl1                 
-  = irWorkItemConsumed "FunEq/FunEq" 
--}
-
   | fl1 `canSolve` fl2 && lhss_match
   = do { traceTcS "interact with inerts: FunEq/FunEq" $ 
          vcat [ text "workItem =" <+> ppr wi
@@ -934,12 +920,6 @@ solveOneFromTheOther info ifl workItem
 		  -- so it's safe to continue on from this point
   = irInertConsumed ("Solved[DI] " ++ info)
   
-{-  ToDo: Check with Dimitrios
-  | isSolved ifl, isGiven wfl
-    -- Same if the inert is a GivenSolved -- just get rid of it
-  = irInertConsumed ("Solved[SI] " ++ info)
--}
-
   | otherwise
   = ASSERT( ifl `canSolve` wfl )
       -- Because of Note [The Solver Invariant], plus Derived dealt with
@@ -1443,16 +1423,32 @@ doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
 --   (b) See Note [Given constraint that matches an instance declaration] 
 --       for some design decisions for given dictionaries. 
 
-doTopReact inerts workItem@(CDictCan { cc_ev = fl
-                                     , cc_class = cls, cc_tyargs = xis, cc_depth = depth })
+doTopReact inerts workItem
   = do { traceTcS "doTopReact" (ppr workItem)
-       ; instEnvs <- getInstEnvs 
-       ; let fd_eqns = improveFromInstEnv instEnvs (mkClassPred cls xis, arising_sdoc)
+       ; case workItem of
+      	   CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis
+      	            , cc_depth = d }
+      	      -> doTopReactDict inerts workItem fl cls xis d
+
+      	   CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args
+      	             , cc_rhs = xi, cc_depth = d }
+      	      -> doTopReactFunEq fl tc args xi d
+
+      	   _  -> -- Any other work item does not react with any top-level equations
+      	         return NoTopInt  }
+
+--------------------
+doTopReactDict :: InertSet -> WorkItem -> CtEvidence -> Class -> [Xi]
+               -> SubGoalDepth -> TcS TopInteractResult
+doTopReactDict inerts workItem fl cls xis depth
+  = do { instEnvs <- getInstEnvs 
+       ; let fd_eqns = improveFromInstEnv instEnvs 
+                           (mkClassPred cls xis, arising_sdoc)
              
        ; m <- rewriteWithFunDeps fd_eqns xis fl
        ; case m of
            Just (_xis',fd_work) ->
-               do { emitFDWorkAsDerived fd_work (cc_depth workItem)
+               do { emitFDWorkAsDerived fd_work depth
                   ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
                                       , tir_new_item = ContinueWith workItem } }
            Nothing 
@@ -1493,106 +1489,54 @@ doTopReact inerts workItem@(CDictCan { cc_ev = fl
                SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
                           , tir_new_item = Stop } }
 
-
--- Otherwise, it's a Given, Derived, or Wanted
-doTopReact _inerts workItem@(CFunEqCan { cc_ev = fl, cc_depth = d
-                                       , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
-  = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far 
+--------------------
+doTopReactFunEq :: CtEvidence -> TyCon -> [Xi] -> Xi
+                -> SubGoalDepth -> TcS TopInteractResult
+doTopReactFunEq fl tc args xi d
+  = ASSERT (isSynFamilyTyCon tc) -- No associated data families have 
+                                 -- reached that far 
+
+    -- First look in the cache of solved funeqs
+    do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
+       ; case lookupFamHead fun_eq_cache (mkTyConApp tc args) of {
+            Just ctev -> ASSERT( not (isDerived ctev) )
+                         ASSERT( isEqPred (ctEvPred ctev) )
+                         succeed_with (evTermCoercion (ctEvTerm ctev)) 
+                                      (snd (getEqPredTys (ctEvPred ctev))) ;
+            Nothing -> 
+
+    -- No cached solved, so look up in top-level instances
     do { match_res <- matchFam tc args   -- See Note [MATCHING-SYNONYMS]
-       ; case match_res of
-           Nothing -> return NoTopInt 
-           Just (famInst, rep_tys)
-             -> do { mb_already_solved <- lkpSolvedFunEqCache (mkTyConApp tc args)
-                   ; traceTcS "doTopReact: Family instance matches" $ 
-                     vcat [ text "solved-fun-cache" <+> if isJust mb_already_solved 
-                                                        then text "hit" else text "miss"
-                          , text "workItem =" <+> ppr workItem ]
-                   ; let (coe,rhs_ty) 
-                           | Just ctev <- mb_already_solved
-                           , not (isDerived ctev)
-                           = ASSERT( isEqPred (ctEvPred ctev) )
-                             (evTermCoercion (ctEvTerm ctev), snd (getEqPredTys (ctEvPred ctev)))
-                           | otherwise 
-                           = let coe_ax = famInstAxiom famInst
-                             in (mkTcAxInstCo coe_ax rep_tys, 
-                                              mkAxInstRHS coe_ax rep_tys)
-                                
-                         xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)]
-                         xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x)
-                         xcomp _   = panic "No more goals!"
-                         
-                         xev = XEvTerm xcomp xdecomp
-                   ; ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
-                   ; case ctevs of
-                       [ctev] -> updWorkListTcS $ extendWorkListEq $
-                                 CNonCanonical { cc_ev = ctev
-                                               , cc_depth  = d+1 }
-                       ctevs -> -- No subgoal (because it's cached)
-                                ASSERT( null ctevs) return () 
-
-                   ; unless (isDerived fl) $
-                     do { addSolvedFunEq fl
-                        ; addToSolved fl }
-                   ; return $ SomeTopInt { tir_rule = "Fun/Top"
-                                       , tir_new_item = Stop } } }
-            
--- Any other work item does not react with any top-level equations
-doTopReact _inerts _workItem = return NoTopInt 
-
-
-lkpSolvedFunEqCache :: TcType -> TcS (Maybe CtEvidence)
-lkpSolvedFunEqCache fam_head 
-  = do { (_subst,_inscope) <- getInertEqs 
-       ; fun_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
-       ; traceTcS "lkpFunEqCache" $ vcat [ text "fam_head    =" <+> ppr fam_head
-                                         , text "funeq cache =" <+> ppr fun_cache ]
-       ; return (lookupFamHead fun_cache fam_head) }
-
-{-             ToDo; talk to Dimitrios.  I have no idea what is happening here
-
-       ; rewrite_cached (lookupFamHead fun_cache fam_head) }
--- The two different calls do not seem to make a significant difference in 
--- terms of hit/miss rate for many memory-critical/performance tests but the
--- latter blows up the space on the heap somehow ... It maybe the niFixTvSubst.
--- So, I am simply disabling it for now, until we investigate a bit more.
---       lookupTypeMap_mod subst cc_rhs fam_head (unCtFamHeadMap fun_cache) }
- 
-  where rewrite_cached Nothing = return Nothing
-        rewrite_cached (Just ct@(CFunEqCan { cc_ev = fl, cc_depth = d
-                                           , cc_fun = tc, cc_tyargs = xis
-                                           , cc_rhs = xi}))
-          = do { (xis_subst,cos) <- flattenMany d FMFullFlatten fl xis 
-                                    -- cos :: xis_subst ~ xis 
-               ; (xi_subst,co) <- flatten d FMFullFlatten fl xi
-                                    -- co :: xi_subst ~ xi
-               ; let flat_fam_head = mkTyConApp tc xis_subst 
-
-               ; unless (flat_fam_head `eqType` fam_head) $ 
-                        pprPanic "lkpFunEqCache" (vcat [ text "Cached (solved) constraint =" <+> ppr ct
-                                                       , text "Flattened constr. head     =" <+> ppr flat_fam_head ])
-               ; traceTcS "lkpFunEqCache" $ text "Flattened constr. rhs = " <+> ppr xi_subst 
-                                                  
-
-               ; let new_pty = mkTcEqPred (mkTyConApp tc xis_subst) xi_subst
-                     new_co  = mkTcTyConAppCo eqTyCon [ mkTcReflCo (defaultKind $ typeKind xi_subst)
-                                                      , mkTcTyConAppCo tc cos
-                                                      , co ]
-                               -- new_co :: (F xis_subst ~  xi_subst) ~ (F xis ~ xi)
-                               -- new_co = (~) <k> (F cos) co
-               ; new_fl <- rewriteCtFlavor fl new_pty new_co 
-               ; case new_fl of
-                    Nothing 
-                      -> return Nothing -- Strange: cached?
-                    Just fl' 
-                      -> return $ 
-                         Just (CFunEqCan { cc_ev = fl'
-                                         , cc_depth = d
-                                         , cc_fun = tc
-                                         , cc_tyargs = xis_subst
-                                         , cc_rhs = xi_subst }) }
-        rewrite_cached (Just other_ct) 
-          = pprPanic "lkpFunEqCache:not family equation!" $ ppr other_ct
--}
+       ; case match_res of {
+           Nothing -> return NoTopInt ;
+           Just (famInst, rep_tys) -> 
+
+    -- Found a top-level instance
+    do {    -- Add it to the solved goals
+         unless (isDerived fl) $
+         do { addSolvedFunEq fl            
+            ; addToSolved fl }
+
+       ; let coe_ax = famInstAxiom famInst 
+       ; succeed_with (mkTcAxInstCo coe_ax rep_tys)
+                      (mkAxInstRHS coe_ax rep_tys) } } } } }
+  where
+    succeed_with :: TcCoercion -> TcType -> TcS TopInteractResult
+    succeed_with coe rhs_ty 
+      = do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
+           ; case ctevs of
+               [ctev] -> updWorkListTcS $ extendWorkListEq $
+                         CNonCanonical { cc_ev = ctev
+                                       , cc_depth  = d+1 }
+               ctevs -> -- No subgoal (because it's cached)
+                        ASSERT( null ctevs) return () 
+           ; return $ SomeTopInt { tir_rule = "Fun/Top"
+                                 , tir_new_item = Stop } }
+      where
+        xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)]
+        xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x)
+        xcomp _   = panic "No more goals!"
+        xev = XEvTerm xcomp xdecomp
 \end{code}
 
 

compiler/typecheck/TcMType.lhs

@@ -55,7 +55,7 @@ module TcMType (
   checkValidInstHead, checkValidInstance, validDerivPred,
   checkInstTermination, checkValidFamInst, checkTyFamFreeness, 
   arityErr, 
-  growPredTyVars, growThetaTyVars, 
+  growThetaTyVars, quantifyPred,
 
   --------------------------------
   -- Zonking
@@ -113,7 +113,7 @@ import Data.List        ( (\\), partition, mapAccumL )
 
 \begin{code}
 newMetaKindVar :: TcM TcKind
-newMetaKindVar = do { uniq <- newUnique
+newMetaKindVar = do { uniq <- newMetaUnique
 		    ; ref <- newMutVar Flexi
 		    ; return (mkTyVarTy (mkMetaKindVar uniq ref)) }
 
@@ -593,14 +593,17 @@ skolemiseSigTv tv
 
 \begin{code}
 zonkImplication :: Implication -> TcM Implication
-zonkImplication implic@(Implic { ic_given = given 
+zonkImplication implic@(Implic { ic_skols  = skols
+                               , ic_given = given 
                                , ic_wanted = wanted
                                , ic_loc = loc })
-  = do {    -- No need to zonk the skolems
+  = do { skols'  <- mapM zonkTcTyVarBndr skols  -- Need to zonk their kinds!
+                                                -- as Trac #7230 showed
        ; given'  <- mapM zonkEvVar given
        ; loc'    <- zonkGivenLoc loc
        ; wanted' <- zonkWC wanted
-       ; return (implic { ic_given = given'
+       ; return (implic { ic_skols = skols'
+                        , ic_given = given'
                         , ic_wanted = wanted'
                         , ic_loc = loc' }) }
 
@@ -765,10 +768,18 @@ zonkTcType ty
 		       | otherwise	 = TyVarTy <$> updateTyVarKindM go tyvar
 		-- Ordinary (non Tc) tyvars occur inside quantified types
 
-    go (ForAllTy tyvar ty) = ASSERT2( isImmutableTyVar tyvar, ppr tyvar ) do
-                             ty' <- go ty
-                             tyvar' <- updateTyVarKindM go tyvar
-                             return (ForAllTy tyvar' ty')
+    go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
+                             ; ty' <- go ty
+                             ; return (ForAllTy tv' ty') }
+
+zonkTcTyVarBndr :: TcTyVar -> TcM TcTyVar
+-- A tyvar binder is never a unification variable (MetaTv),
+-- rather it is always a skolems.  BUT it may have a kind 
+-- that has not yet been zonked, and may include kind
+-- unification variables.
+zonkTcTyVarBndr tyvar
+  = ASSERT2( isImmutableTyVar tyvar, ppr tyvar ) do
+    updateTyVarKindM zonkTcType tyvar
 
 zonkTcTyVar :: TcTyVar -> TcM TcType
 -- Simply look through all Flexis
@@ -1305,9 +1316,9 @@ Is every call to 'g' ambiguous?  After all, we might have
    intance C [a] where ...
 at the call site.  So maybe that type is ok!  Indeed even f's
 quintessentially ambiguous type might, just possibly be callable: 
-with -XUndecidableInstances we could have
+with -XFlexibleInstances we could have
   instance C a where ...
-and now a call could be legal after all!  (But only with  -XUndecidableInstances!)
+and now a call could be legal after all!  (But only with  -XFlexibleInstances!)
 
 What about things like this:
    class D a b | a -> b where ..
@@ -1333,7 +1344,7 @@ where
   * The constraints in 'Cambig' are all of form (C a b c) 
     where a,b,c are type variables
   * 'Cambig' is non-empty
-  * '-XUndecidableInstances' is not on.
+  * '-XFlexibleInstances' is not on.
 
 And that is what checkAmbiguity does.  See Trac #6134.
 
@@ -1375,8 +1386,8 @@ so we can take their type variables into account as part of the
 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 -- Note [The ambiguity check for type signatures]
 checkAmbiguity forall_tyvars theta tau_tyvars
-  = do { undecidable_instances <- xoptM Opt_UndecidableInstances
-       ; unless undecidable_instances $
+  = do { flexible_instances <- xoptM Opt_FlexibleInstances
+       ; unless flexible_instances $
          mapM_  ambigErr (filter is_ambig candidates) }
   where
 	-- See Note [Implicit parameters and ambiguity] in TcSimplify
@@ -1408,7 +1419,38 @@ Note [Growing the tau-tvs using constraints]
 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
 Then grow precs tvs = {a,b,c}
 
+Note [Inheriting implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this:
+
+	f x = (x::Int) + ?y
+
+where f is *not* a top-level binding.
+From the RHS of f we'll get the constraint (?y::Int).
+There are two types we might infer for f:
+
+	f :: Int -> Int
+
+(so we get ?y from the context of f's definition), or
+
+	f :: (?y::Int) => Int -> Int
+
+At first you might think the first was better, becuase then
+?y behaves like a free variable of the definition, rather than
+having to be passed at each call site.  But of course, the WHOLE
+IDEA is that ?y should be passed at each call site (that's what
+dynamic binding means) so we'd better infer the second.
+
+BOTTOM LINE: when *inferring types* you *must* quantify 
+over implicit parameters. See the predicate isFreeWhenInferring.
+
 \begin{code}
+quantifyPred :: TyVarSet      -- Quantifying over these
+	     -> PredType -> Bool	    -- True <=> quantify over this wanted
+quantifyPred qtvs pred
+  | isIPPred pred = True  -- Note [Inheriting implicit parameters]
+  | otherwise	  = tyVarsOfType pred `intersectsVarSet` qtvs
+
 growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
 -- See Note [Growing the tau-tvs using constraints]
 growThetaTyVars theta tvs
@@ -1422,6 +1464,7 @@ growPredTyVars :: TcPredType
                -> TyVarSet	-- The set to extend
 	       -> TyVarSet	-- TyVars of the predicate if it intersects the set, 
 growPredTyVars pred tvs 
+   | isIPPred pred                   = pred_tvs   -- Always quantify over implicit parameers
    | pred_tvs `intersectsVarSet` tvs = pred_tvs
    | otherwise                       = emptyVarSet
   where

compiler/typecheck/TcRnDriver.lhs

@@ -63,7 +63,6 @@ import CoreSyn
 import ErrUtils
 import Id
 import VarEnv
-import Var
 import Module
 import UniqFM
 import Name
@@ -726,15 +725,12 @@ checkBootTyCon tc1 tc2
 
   | Just c1 <- tyConClass_maybe tc1
   , Just c2 <- tyConClass_maybe tc2
-  = let
-       (clas_tyvars1, clas_fds1, sc_theta1, _, ats1, op_stuff1)
+  , let (clas_tvs1, clas_fds1, sc_theta1, _, ats1, op_stuff1)
           = classExtraBigSig c1
-       (clas_tyvars2, clas_fds2, sc_theta2, _, ats2, op_stuff2)
+        (clas_tvs2, clas_fds2, sc_theta2, _, ats2, op_stuff2)
           = classExtraBigSig c2
-
-       env0 = mkRnEnv2 emptyInScopeSet
-       env = rnBndrs2 env0 clas_tyvars1 clas_tyvars2
-
+  , Just env <- eqTyVarBndrs emptyRnEnv2 clas_tvs1 clas_tvs2
+  = let
        eqSig (id1, def_meth1) (id2, def_meth2)
          = idName id1 == idName id2 &&
            eqTypeX env op_ty1 op_ty2 &&
@@ -751,18 +747,15 @@ checkBootTyCon tc1 tc2
 
        -- Ignore the location of the defaults
        eqATDef (ATD tvs1 ty_pats1 ty1 _loc1) (ATD tvs2 ty_pats2 ty2 _loc2)
-         = eqListBy same_kind tvs1 tvs2 &&
-           eqListBy (eqTypeX env) ty_pats1 ty_pats2 &&
+         | Just env <- eqTyVarBndrs emptyRnEnv2 tvs1 tvs2
+         = eqListBy (eqTypeX env) ty_pats1 ty_pats2 &&
            eqTypeX env ty1 ty2
-         where env = rnBndrs2 env0 tvs1 tvs2
+         | otherwise = False
 
        eqFD (as1,bs1) (as2,bs2) =
          eqListBy (eqTypeX env) (mkTyVarTys as1) (mkTyVarTys as2) &&
          eqListBy (eqTypeX env) (mkTyVarTys bs1) (mkTyVarTys bs2)
-
-       same_kind tv1 tv2 = eqKind (tyVarKind tv1) (tyVarKind tv2)
     in
-       eqListBy same_kind clas_tyvars1 clas_tyvars2 &&
              -- Checks kind of class
        eqListBy eqFD clas_fds1 clas_fds2 &&
        (null sc_theta1 && null op_stuff1 && null ats1
@@ -772,23 +765,20 @@ checkBootTyCon tc1 tc2
         eqListBy eqAT ats1 ats2)
 
   | isSynTyCon tc1 && isSynTyCon tc2
+  , Just env <- eqTyVarBndrs emptyRnEnv2 (tyConTyVars tc1) (tyConTyVars tc2)
   = ASSERT(tc1 == tc2)
-    let tvs1 = tyConTyVars tc1; tvs2 = tyConTyVars tc2
-        env = rnBndrs2 env0 tvs1 tvs2
-
-        eqSynRhs SynFamilyTyCon SynFamilyTyCon
+    let eqSynRhs SynFamilyTyCon SynFamilyTyCon
             = True
         eqSynRhs (SynonymTyCon t1) (SynonymTyCon t2)
             = eqTypeX env t1 t2
         eqSynRhs _ _ = False
     in
-    equalLength tvs1 tvs2 &&
     eqSynRhs (synTyConRhs tc1) (synTyConRhs tc2)
 
   | isAlgTyCon tc1 && isAlgTyCon tc2
+  , Just env <- eqTyVarBndrs emptyRnEnv2 (tyConTyVars tc1) (tyConTyVars tc2)
   = ASSERT(tc1 == tc2)
-    eqKind (tyConKind tc1) (tyConKind tc2) &&
-    eqListBy eqPred (tyConStupidTheta tc1) (tyConStupidTheta tc2) &&
+    eqListBy (eqPredX env) (tyConStupidTheta tc1) (tyConStupidTheta tc2) &&
     eqAlgRhs (algTyConRhs tc1) (algTyConRhs tc2)
 
   | isForeignTyCon tc1 && isForeignTyCon tc2
@@ -797,8 +787,6 @@ checkBootTyCon tc1 tc2
 
   | otherwise = False
   where
-        env0 = mkRnEnv2 emptyInScopeSet
-
         eqAlgRhs (AbstractTyCon dis1) rhs2
           | dis1      = isDistinctAlgRhs rhs2   --Check compatibility
           | otherwise = True
@@ -816,6 +804,9 @@ checkBootTyCon tc1 tc2
           && dataConFieldLabels c1 == dataConFieldLabels c2
           && eqType (dataConUserType c1) (dataConUserType c2)
 
+emptyRnEnv2 :: RnEnv2
+emptyRnEnv2 = mkRnEnv2 emptyInScopeSet
+
 ----------------
 missingBootThing :: Name -> String -> SDoc
 missingBootThing name what

compiler/typecheck/TcRnTypes.lhs

@@ -857,8 +857,8 @@ type SubGoalDepth = Int -- An ever increasing number used to restrict
 data Ct
   -- Atomic canonical constraints 
   = CDictCan {  -- e.g.  Num xi
-      cc_ev :: CtEvidence, 
-      cc_class  :: Class, 
+      cc_ev :: CtEvidence,   -- See Note [Ct/evidence invariant]
+      cc_class  :: Class,   
       cc_tyargs :: [Xi],
 
       cc_depth  :: SubGoalDepth -- Simplification depth of this constraint
@@ -866,7 +866,7 @@ data Ct
     }
 
   | CIrredEvCan {  -- These stand for yet-unknown predicates
-      cc_ev :: CtEvidence,
+      cc_ev :: CtEvidence,   -- See Note [Ct/evidence invariant]
       cc_ty     :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin)
                        -- Since, if it were a type constructor application, that'd make the
                        -- whole constraint a CDictCan, or CTyEqCan. And it can't be
@@ -880,7 +880,7 @@ data Ct
        --   * typeKind xi `compatKind` typeKind tv
        --       See Note [Spontaneous solving and kind compatibility]
        --   * We prefer unification variables on the left *JUST* for efficiency
-      cc_ev :: CtEvidence, 
+      cc_ev :: CtEvidence,    -- See Note [Ct/evidence invariant]
       cc_tyvar  :: TcTyVar, 
       cc_rhs    :: Xi,
 
@@ -890,7 +890,7 @@ data Ct
   | CFunEqCan {  -- F xis ~ xi  
                  -- Invariant: * isSynFamilyTyCon cc_fun 
                  --            * typeKind (F xis) `compatKind` typeKind xi
-      cc_ev :: CtEvidence, 
+      cc_ev :: CtEvidence,      -- See Note [Ct/evidence invariant]
       cc_fun    :: TyCon,	-- A type function
       cc_tyargs :: [Xi],	-- Either under-saturated or exactly saturated
       cc_rhs    :: Xi,      	--    *never* over-saturated (because if so
@@ -904,9 +904,16 @@ data Ct
       cc_ev :: CtEvidence, 
       cc_depth  :: SubGoalDepth
     }
-
 \end{code}
 
+Note [Ct/evidence invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If  ct :: Ct, then extra fields of 'ct' cache precisely the ctev_pred field
+of (cc_ev ct).   Eg for CDictCan, 
+   ctev_pred (cc_ev ct) = (cc_class ct) (cc_tyargs ct)
+This holds by construction; look at the unique place where CDictCan is
+built (in TcCanonical)
+
 \begin{code}
 mkNonCanonical :: CtEvidence -> Ct
 mkNonCanonical flav = CNonCanonical { cc_ev = flav, cc_depth = 0}
@@ -915,6 +922,7 @@ ctEvidence :: Ct -> CtEvidence
 ctEvidence = cc_ev
 
 ctPred :: Ct -> PredType 
+-- See Note [Ct/evidence invariant]
 ctPred ct = ctEvPred (cc_ev ct)
 
 keepWanted :: Cts -> Cts
@@ -922,18 +930,6 @@ keepWanted = filterBag isWantedCt
     -- DV: there used to be a note here that read: 
     -- ``Important: use fold*r*Bag to preserve the order of the evidence variables'' 
     -- DV: Is this still relevant? 
-
--- ToDo Check with Dimitrios
-{-
-ctPred (CNonCanonical { cc_ev = fl }) = ctEvPred fl
-ctPred (CDictCan { cc_class = cls, cc_tyargs = xis }) 
-  = mkClassPred cls xis
-ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) 
-  = mkTcEqPred (mkTyVarTy tv) xi
-ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 }) 
-  = mkTcEqPred (mkTyConApp fn xis1) xi2
-ctPred (CIrredEvCan { cc_ty = xi }) = xi
--}
 \end{code}
 
 
@@ -1197,6 +1193,12 @@ At the end, we will hopefully have substituted uf1 := F alpha, and we
 will be able to report a more informative error:
     'Can't construct the infinite type beta ~ F alpha beta'
 
+Insoluble constraints *do* include Derived constraints. For example,
+a functional dependency might give rise to [D] Int ~ Bool, and we must
+report that.  If insolubles did not contain Deriveds, reportErrors would
+never see it.
+
+
 %************************************************************************
 %*									*
             Pretty printing
@@ -1233,14 +1235,12 @@ ctev_evar; instead we look at the cte_pred field.  The evtm/evar field
 may be un-zonked.
 
 \begin{code}
-data CtEvidence   -- Rename to CtEvidence
+data CtEvidence 
   = Given { ctev_gloc :: GivenLoc
           , ctev_pred :: TcPredType
           , ctev_evtm :: EvTerm }          -- See Note [Evidence field of CtEvidence]
     -- Truly given, not depending on subgoals
     -- NB: Spontaneous unifications belong here
-    -- DV TODOs: (i)  Consider caching actual evidence _term_
-    --           (ii) Revisit Note [Optimizing Spontaneously Solved Coercions]
     
   | Wanted { ctev_wloc :: WantedLoc
            , ctev_pred :: TcPredType

compiler/typecheck/TcSMonad.lhs

@@ -140,7 +140,7 @@ import Digraph
 import Maybes ( orElse, catMaybes )
 
 
-import Control.Monad( when, zipWithM )
+import Control.Monad( unless, when, zipWithM )
 import StaticFlags( opt_PprStyle_Debug )
 import Data.IORef
 import TrieMap
@@ -171,7 +171,6 @@ mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
 
 Note [WorkList]
 ~~~~~~~~~~~~~~~
-
 A WorkList contains canonical and non-canonical items (of all flavors). 
 Notice that each Ct now has a simplification depth. We may 
 consider using this depth for prioritization as well in the future. 
@@ -496,8 +495,10 @@ The reason for all this is simply to avoid re-solving goals we have solved alrea
 
 * A solved Given is just given
 
-* A solved Derived is possible; purpose is to avoid creating tons of identical
-  Derived goals.
+* A solved Derived in inert_solved is possible; purpose is to avoid
+  creating tons of identical Derived goals.
+
+  But there are no solved Deriveds in inert_solved_funeqs
 
 
 \begin{code}
@@ -516,7 +517,9 @@ data InertSet
               -- Key is by family head. We use this field during flattening only
               -- Not necessarily inert wrt top-level equations (or inert_cans)
 
-       , inert_solved_funeqs :: FamHeadMap CtEvidence  -- Of form co :: F xis ~ xi
+       , inert_solved_funeqs :: FamHeadMap CtEvidence  -- Of form co :: F xis ~ xi 
+                                                       -- No Deriveds 
+
        , inert_solved        :: PredMap    CtEvidence  -- All others
        	      -- These two fields constitute a cache of solved (only!) constraints
               -- See Note [Solved constraints]
@@ -1123,11 +1126,16 @@ emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
 emitFrozenError fl depth 
   = do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
        ; inert_ref <- getTcSInertsRef 
-       ; inerts <- wrapTcS (TcM.readTcRef inert_ref)
-       ; let ct = CNonCanonical { cc_ev = fl
-                                , cc_depth = depth } 
-             inerts_new = inerts { inert_frozen = extendCts (inert_frozen inerts) ct } 
-       ; wrapTcS (TcM.writeTcRef inert_ref inerts_new) }
+       ; wrapTcS $ do
+       { inerts <- TcM.readTcRef inert_ref
+       ; let old_insols = inert_frozen inerts
+             ct = CNonCanonical { cc_ev = fl, cc_depth = depth } 
+             inerts_new = inerts { inert_frozen = extendCts old_insols ct } 
+             this_pred = ctEvPred fl
+             already_there = not (isWanted fl) && anyBag (eqType this_pred . ctPred) old_insols
+	     -- See Note [Do not add duplicate derived insolubles]
+       ; unless already_there $
+         TcM.writeTcRef inert_ref inerts_new } }
 
 instance HasDynFlags TcS where
     getDynFlags = wrapTcS getDynFlags
@@ -1184,52 +1192,8 @@ setWantedTyBind tv ty
 
 
 \end{code}
-Note [Optimizing Spontaneously Solved Coercions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
-
-Spontaneously solved coercions such as alpha := tau used to be bound as everything else
-in the evidence binds. Subsequently they were used for rewriting other wanted or solved
-goals. For instance: 
-
-WorkItem = [S] g1 : a ~ tau
-Inerts   = [S] g2 : b ~ [a]
-           [S] g3 : c ~ [(a,a)]
-
-Would result, eventually, after the workitem rewrites the inerts, in the
-following evidence bindings:
-
-        g1 = ReflCo tau
-        g2 = ReflCo [a]
-        g3 = ReflCo [(a,a)]
-        g2' = g2 ; [g1] 
-        g3' = g3 ; [(g1,g1)]
-
-This ia annoying because it puts way too much stress to the zonker and
-desugarer, since we /know/ at the generation time (spontaneously
-solving) that the evidence for a particular evidence variable is the
-identity.
-
-For this reason, our solution is to cache inside the GivenSolved
-flavor of a constraint the term which is actually solving this
-constraint. Whenever we perform a setEvBind, a new flavor is returned
-so that if it was a GivenSolved to start with, it remains a
-GivenSolved with a new evidence term inside. Then, when we use solved
-goals to rewrite other constraints we simply use whatever is in the
-GivenSolved flavor and not the constraint cc_id.
-
-In our particular case we'd get the following evidence bindings, eventually: 
-
-       g1 = ReflCo tau
-       g2 = ReflCo [a]
-       g3 = ReflCo [(a,a)]
-       g2'= ReflCo [a]
-       g3'= ReflCo [(a,a)]
-
-Since we use smart constructors to get rid of g;ReflCo t ~~> g etc.
 
 \begin{code}
-
-
 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
 warnTcS loc warn_if doc 
   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
@@ -1285,6 +1249,52 @@ isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
 
 \end{code}
 
+Note [Do not add duplicate derived insolubles]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In general we do want to add an insoluble (Int ~ Bool) even if there is one
+such there already, because they may come from distinct call sites.  But for
+*derived* insolubles, we only want to report each one once.  Why?
+
+(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
+    equality many times, as the original constraint is sucessively rewritten.
+
+(b) Ditto the successive iterations of the main solver itself, as it traverses
+    the constraint tree. See example below.
+
+Also for *given* insolubles we may get repeated errors, as we
+repeatedly traverse the constraint tree.  These are relatively rare
+anyway, so removing duplicates seems ok.  (Alternatively we could take
+the SrcLoc into account.)
+
+Note that the test does not need to be particularly efficient because
+it is only used if the program has a type error anyway.
+
+Example of (b): assume a top-level class and instance declaration:
+
+  class D a b | a -> b 
+  instance D [a] [a] 
+
+Assume we have started with an implication:
+
+  forall c. Eq c => { wc_flat = D [c] c [W] }
+
+which we have simplified to:
+
+  forall c. Eq c => { wc_flat = D [c] c [W]
+                    , wc_insols = (c ~ [c]) [D] }
+
+For some reason, e.g. because we floated an equality somewhere else,
+we might try to re-solve this implication. If we do not do a
+keepWanted, then we will end up trying to solve the following
+constraints the second time:
+
+  (D [c] c) [W]
+  (c ~ [c]) [D]
+
+which will result in two Deriveds to end up in the insoluble set:
+
+  wc_flat   = D [c] c [W]
+  wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
 
 Note [Touchable meta type variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1468,6 +1478,20 @@ Example
                                      , ev_decomp = \c. [nth 1 c, nth 2 c] })
               (\fresh-goals.  stuff)
 
+Note [Bind new Givens immediately]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For Givens we make new EvVars and bind them immediately. We don't worry
+about caching, but we don't expect complicated calculations among Givens.
+It is important to bind each given:
+      class (a~b) => C a b where ....
+      f :: C a b => ....
+Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
+But that superclass selector can't (yet) appear in a coercion
+(see evTermCoercion), so the easy thing is to bind it to an Id.
+
+See Note [Coercion evidence terms] in TcEvidence.
+
+
 \begin{code}
 xCtFlavor :: CtEvidence              -- Original flavor   
           -> [TcPredType]          -- New predicate types
@@ -1484,14 +1508,7 @@ xCtFlavor_cache :: Bool            -- True = if wanted add to the solved bag!
 xCtFlavor_cache _ (Given { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
   = ASSERT( equalLength ptys (ev_decomp xev tm) )
     zipWithM (newGivenEvVar gl) ptys (ev_decomp xev tm)
-    -- For Givens we make new EvVars and bind them immediately. We don't worry
-    -- about caching, but we don't expect complicated calculations among Givens.
-    -- It is important to bind each given:
-    --       class (a~b) => C a b where ....
-    --       f :: C a b => ....
-    -- Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
-    -- But that superclass selector can't (yet) appear in a coercion
-    -- (see evTermCoercion), so the easy thing is to bind it to an Id
+    -- See Note [Bind new Givens immediately]
   
 xCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev
   = do { new_evars <- mapM (newWantedEvVar wl) ptys
@@ -1550,7 +1567,8 @@ rewriteCtFlavor_cache _cache (Derived { ctev_wloc = wl }) pty_new _co
   = newDerived wl pty_new
         
 rewriteCtFlavor_cache _cache (Given { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co
-  = return (Just (Given { ctev_gloc = gl, ctev_pred = pty_new, ctev_evtm = new_tm }))
+  = do { new_ev <- newGivenEvVar gl pty_new new_tm  -- See Note [Bind new Givens immediately]
+       ; return (Just new_ev) }
   where
     new_tm = mkEvCast old_tm (mkTcSymCo co)  -- mkEvCase optimises ReflCo
   
@@ -1681,25 +1699,6 @@ getCtCoercion :: EvBindMap -> Ct -> TcCoercion
 getCtCoercion _bs ct 
   = ASSERT( not (isDerivedCt ct) )
     evTermCoercion (ctEvTerm (ctEvidence ct))
-{-       ToDo: check with Dimitrios that we can dump this stuff
-         WARNING: if we *do* need this stuff, we need to think again about cyclic bindings.
-  = case lookupEvBind bs cc_id of
-        -- Given and bound to a coercion term
-      Just (EvBind _ (EvCoercion co)) -> co
-                -- NB: The constraint could have been rewritten due to spontaneous 
-                -- unifications but because we are optimizing away mkRefls the evidence
-                -- variable may still have type (alpha ~ [beta]). The constraint may 
-                -- however have a more accurate type (alpha ~ [Int]) (where beta ~ Int has
-                -- been previously solved by spontaneous unification). So if we are going 
-                -- to use the evidence variable for rewriting other constraints, we'd better 
-                -- make sure it's of the right type!
-                -- Always the ctPred type is more accurate, so we just pick that type
-
-      _ -> mkTcCoVarCo (setVarType cc_id (ctPred ct))
-      
-  where 
-    cc_id = ctId ct
--}
 \end{code}
 
 

compiler/typecheck/TcSimplify.lhs

@@ -148,7 +148,9 @@ More details in Note [DefaultTyVar].
 simplifyAmbiguityCheck :: Name -> WantedConstraints -> TcM (Bag EvBind)
 simplifyAmbiguityCheck name wanteds
   = traceTc "simplifyAmbiguityCheck" (text "name =" <+> ppr name) >> 
-    simplifyCheck wanteds
+    simplifyTop wanteds  -- NB: must be simplifyTop not simplifyCheck, so that we
+                         --     do ambiguity resolution.  
+                         -- See Note [Impedence matching] in TcBinds.
  
 ------------------
 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
@@ -388,10 +390,12 @@ simplifyInfer _top_lvl apply_mr name_taus (untch,wanteds)
                                   , wc_insol = emptyBag }
 
               -- Step 6) Final candidates for quantification                
-       ; let final_quant_candidates :: Bag PredType
-             final_quant_candidates = mapBag ctPred $ 
+       ; let final_quant_candidates :: [PredType]
+             final_quant_candidates = map ctPred $ bagToList $
                                       keepWanted (wc_flat quant_candidates_transformed)
              -- NB: Already the fixpoint of any unifications that may have happened
+             -- But need to zonk out the flatten-skolems
+       ; final_quant_candidates <- mapM zonkTcType final_quant_candidates
                   
        ; gbl_tvs        <- tcGetGlobalTyVars -- TODO: can we just use untch instead of gbl_tvs?
        ; zonked_tau_tvs <- zonkTyVarsAndFV zonked_tau_tvs
@@ -401,25 +405,27 @@ simplifyInfer _top_lvl apply_mr name_taus (untch,wanteds)
               , ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
               , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs ]
          
-       ; let init_tvs 	     = zonked_tau_tvs `minusVarSet` gbl_tvs
-             poly_qtvs       = growPreds gbl_tvs id final_quant_candidates init_tvs
-             
-             pbound          = filterBag (quantifyMe poly_qtvs id) final_quant_candidates
+       ; let init_tvs  = zonked_tau_tvs `minusVarSet` gbl_tvs
+             poly_qtvs = growThetaTyVars final_quant_candidates init_tvs 
+                         `minusVarSet` gbl_tvs
+             pbound    = filter (quantifyPred poly_qtvs) final_quant_candidates
              
        ; traceTc "simplifyWithApprox" $
-         vcat [ ptext (sLit "pbound =") <+> ppr pbound ]
+         vcat [ ptext (sLit "pbound =") <+> ppr pbound
+              , ptext (sLit "init_qtvs =") <+> ppr init_tvs 
+              , ptext (sLit "poly_qtvs =") <+> ppr poly_qtvs ]
          
 	     -- Monomorphism restriction
        ; let mr_qtvs  	     = init_tvs `minusVarSet` constrained_tvs
-             constrained_tvs = tyVarsOfBag tyVarsOfType final_quant_candidates
-	     mr_bites        = apply_mr && not (isEmptyBag pbound)
+             constrained_tvs = tyVarsOfTypes final_quant_candidates
+	     mr_bites        = apply_mr && not (null pbound)
 
              (qtvs, bound)
-                | mr_bites  = (mr_qtvs,   emptyBag)
+                | mr_bites  = (mr_qtvs,   [])
                 | otherwise = (poly_qtvs, pbound)
              
 
-       ; if isEmptyVarSet qtvs && isEmptyBag bound
+       ; if isEmptyVarSet qtvs && null bound
          then do { traceTc "} simplifyInfer/no quantification" empty                   
                  ; emitConstraints wanted_transformed
                     -- Includes insolubles (if -fdefer-type-errors)
@@ -431,7 +437,7 @@ simplifyInfer _top_lvl apply_mr name_taus (untch,wanteds)
          ptext (sLit "bound are =") <+> ppr bound 
          
             -- Step 4, zonk quantified variables 
-       ; let minimal_flat_preds = mkMinimalBySCs $ bagToList bound
+       ; let minimal_flat_preds = mkMinimalBySCs bound
              skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
                                    | (name, ty) <- name_taus ]
                         -- Don't add the quantified variables here, because
@@ -467,8 +473,8 @@ simplifyInfer _top_lvl apply_mr name_taus (untch,wanteds)
 \end{code}
 
 
-Note [Note [Default while Inferring]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Default while Inferring]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Our current plan is that defaulting only happens at simplifyTop and
 not simplifyInfer.  This may lead to some insoluble deferred constraints
 Example:
@@ -514,10 +520,7 @@ from superclass selection from Ord alpha. This minimization is what
 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
 to check the original wanted.
 
-
 \begin{code}
-
-
 approximateWC :: WantedConstraints -> Cts
 -- Postcondition: Wanted or Derived Cts 
 approximateWC wc = float_wc emptyVarSet wc
@@ -539,27 +542,6 @@ approximateWC wc = float_wc emptyVarSet wc
         
     do_bag :: (a -> Bag c) -> Bag a -> Bag c
     do_bag f = foldrBag (unionBags.f) emptyBag
-
-
-\end{code}
-
-\begin{code}
-growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
-growPreds gbl_tvs get_pred items tvs
-  = foldrBag extend tvs items
-  where
-    extend item tvs = tvs `unionVarSet`
-                      (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
-
---------------------
-quantifyMe :: TyVarSet      -- Quantifying over these
-	   -> (a -> PredType)
-	   -> a -> Bool	    -- True <=> quantify over this wanted
-quantifyMe qtvs toPred ct
-  | isIPPred pred = True  -- Note [Inheriting implicit parameters]
-  | otherwise	  = tyVarsOfType pred `intersectsVarSet` qtvs
-  where
-    pred = toPred ct
 \end{code}
 
 Note [Avoid unecessary constraint simplification]
@@ -586,32 +568,6 @@ the contraints before simplifying.
 This only half-works, but then let-generalisation only half-works.
 
 
-Note [Inheriting implicit parameters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this:
-
-	f x = (x::Int) + ?y
-
-where f is *not* a top-level binding.
-From the RHS of f we'll get the constraint (?y::Int).
-There are two types we might infer for f:
-
-	f :: Int -> Int
-
-(so we get ?y from the context of f's definition), or
-
-	f :: (?y::Int) => Int -> Int
-
-At first you might think the first was better, becuase then
-?y behaves like a free variable of the definition, rather than
-having to be passed at each call site.  But of course, the WHOLE
-IDEA is that ?y should be passed at each call site (that's what
-dynamic binding means) so we'd better infer the second.
-
-BOTTOM LINE: when *inferring types* you *must* quantify 
-over implicit parameters. See the predicate isFreeWhenInferring.
-
-
 *********************************************************************************
 *                                                                                 * 
 *                             RULES                                               *
@@ -771,10 +727,10 @@ solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols
 
          -- Try the flat bit, including insolubles. Solving insolubles a 
          -- second time round is a bit of a waste but the code is simple 
-         -- and the program is wrong anyway. 
-         -- Why keepWanted insols? See Note [KeepWanted in SolveWanteds] 
-       ; let all_flats = flats `unionBags` keepWanted insols
-             -- DV: Used to be 'keepWanted insols' but just insols is
+         -- and the program is wrong anyway, and we don't run the danger 
+         -- of adding Derived insolubles twice; see 
+         -- TcSMonad Note [Do not add duplicate derived insolubles] 
+       ; let all_flats = flats `unionBags` insols
                          
        ; impls_from_flats <- solveInteractCts $ bagToList all_flats
 
@@ -917,10 +873,7 @@ solveImplication tcs_untouchables
        ; let (res_flat_free, res_flat_bound)
                  = floatEqualities skols givens unsolved_flats
 
-       ; let res_wanted = WC { wc_flat  = keepWanted $ res_flat_bound
-                               -- I think this keepWanted must eventually go away, but it is
-                               -- a real code-breaking change. 
-                               -- See Note [KeepWanted in SolveImplication]
+       ; let res_wanted = WC { wc_flat  = res_flat_bound
                              , wc_impl  = unsolved_implics
                              , wc_insol = insols }
 
@@ -940,81 +893,8 @@ solveImplication tcs_untouchables
 
 \end{code}
 
-Note [KeepWanted in SolveWanteds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Why do we have:
-   let all_flats = flats `unionBags` keepWanted insols
-instead of the simpler:
-   let all_flats = flats `unionBags` insols
-in solve_wanteds?
-
-Assume a top-level class and instance declaration:
-
-  class D a b | a -> b 
-  instance D [a] [a] 
-
-Assume we have started with an implication:
-
-  forall c. Eq c => { wc_flat = D [c] c [W] }
-
-which we have simplified to:
-
-  forall c. Eq c => { wc_flat = D [c] c [W]
-                    , wc_insols = (c ~ [c]) [D] }
-
-For some reason, e.g. because we floated an equality somewhere else,
-we might try to re-solve this implication. If we do not do a
-keepWanted, then we will end up trying to solve the following
-constraints the second time:
-
-  (D [c] c) [W]
-  (c ~ [c]) [D]
-
-which will result in two Deriveds to end up in the insoluble set:
-
-  wc_flat   = D [c] c [W]
-  wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
-
-which can result in reporting the same error twice.  
-
-So, do we /lose/ some potentially useful information by doing this? 
-
-No, because the insoluble Derived/Given are going to be equalities, 
-which are going to be derivable anyway from the rest of the flat 
-constraints. 
-
-
-Note [KeepWanted in SolveImplication]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Here is a real example, 
-stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs
-
-  class C a b | a -> b
-  g :: C a b => a -> b -> () 
-  f :: C a b => a -> b -> () 
-  f xa xb = 
-      let loop = g xa 
-      in loop xb
-
-We will first try to infer a type for loop, and we will succeed:
-    C a b' => b' -> ()
-Subsequently, we will type check (loop xb) and all is good. But, 
-recall that we have to solve a final implication constraint: 
-    C a b => (C a b' => .... cts from body of loop .... )) 
-And now we have a problem as we will generate an equality b ~ b' and fail to 
-solve it. 
-
-I actually think this is a legitimate behaviour (to fail). After all, if we had 
-given the inferred signature to foo we would have failed as well, but we have to 
-find a workaround because library code breaks.
-
-For now I keep the 'keepWanted' though it seems problematic e.g. we might discard 
-a useful Derived!
 
 \begin{code}
-
-
 floatEqualities :: [TcTyVar] -> [EvVar] -> Cts -> (Cts, Cts)
 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
 -- and come from the input wanted ev vars or deriveds 

compiler/typecheck/TcSplice.lhs

@@ -349,22 +349,22 @@ tcBracket brack res_ty
           -- We build a single implication constraint with a BracketSkol;
           -- that in turn tells simplifyCheck to report only definite
           -- errors
-       ; (_,lie) <- captureConstraints $
-                    newImplication BracketSkol [] [] $
-                    setStage brack_stage $
-                    do { meta_ty <- tc_bracket cur_stage brack
-                       ; unifyType meta_ty res_ty }
+       ; ((_binds1, meta_ty), lie) <- captureConstraints $
+                          newImplication BracketSkol [] [] $
+                          setStage brack_stage $
+                          tc_bracket cur_stage brack
 
           -- It's best to simplify the constraint now, even though in
           -- principle some later unification might be useful for it,
           -- because we don't want these essentially-junk TH implication
           -- contraints floating around nested inside other constraints
           -- See for example Trac #4949
-       ; _ <- simplifyTop lie
+       ; _binds2 <- simplifyTop lie
 
         -- Return the original expression, not the type-decorated one
        ; pendings <- readMutVar pending_splices
-       ; return (noLoc (HsBracketOut brack pendings)) }
+       ; co <- unifyType meta_ty res_ty
+       ; return (noLoc (mkHsWrapCo co (HsBracketOut brack pendings))) }
 
 tc_bracket :: ThStage -> HsBracket Name -> TcM TcType
 tc_bracket outer_stage br@(VarBr _ name)     -- Note [Quoting names]
@@ -496,6 +496,12 @@ tcTopSpliceExpr :: TcM (LHsExpr Id) -> TcM (LHsExpr Id)
 tcTopSpliceExpr tc_action
   = checkNoErrs $  -- checkNoErrs: must not try to run the thing
                    -- if the type checker fails!
+    unsetDOptM Opt_DeferTypeErrors $
+                   -- Don't defer type errors.  Not only are we
+                   -- going to run this code, but we do an unsafe
+                   -- coerce, so we get a seg-fault if, say we
+                   -- splice a type into a place where an expression
+                   -- is expected (Trac #7276)
     setStage Splice $
     do {    -- Typecheck the expression
          (expr', lie) <- captureConstraints tc_action

compiler/typecheck/TcTyClsDecls.lhs

@@ -147,11 +147,12 @@ tcTyClGroup boot_details tyclds
            -- expects well-formed TyCons
        ; tcExtendGlobalEnv tyclss $ do
        { traceTc "Starting validity check" (ppr tyclss)
-       ; mapM_ (recoverM (return ()) . addLocM checkValidTyCl) 
+       ; checkNoErrs $
+         mapM_ (recoverM (return ()) . addLocM checkValidTyCl) 
                (flattenTyClDecls tyclds)
            -- We recover, which allows us to report multiple validity errors
-           -- even from successive groups.  But we stop after all groups are
-           -- processed if we find any errors.
+           -- but we then fail if any are wrong.  Lacking the checkNoErrs
+           -- we get Trac #7175
 
            -- Step 4: Add the implicit things;
            -- we want them in the environment because
@@ -568,12 +569,15 @@ tcTyClDecl1 _parent calc_isrec
 
           ; ctxt' <- tcHsContext ctxt
           ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'  
-                     -- Squeeze out any kind unification variables
-
+                  -- Squeeze out any kind unification variables
           ; fds'  <- mapM (addLocM tc_fundep) fundeps
           ; (sig_stuff, gen_dm_env) <- tcClassSigs class_name sigs meths
+          ; env <- getLclTypeEnv
+          ; traceTc "tcClassDecl" (ppr fundeps $$ ppr tvs' $$ ppr fds' $$  ppr env)
           ; return (tvs', ctxt', fds', sig_stuff, gen_dm_env) }
 
+
+
   ; clas <- fixM $ \ clas -> do
 	    { let 	-- This little knot is just so we can get
 			-- hold of the name of the class TyCon, which we
@@ -602,9 +606,17 @@ tcTyClDecl1 _parent calc_isrec
       --     tying the the type and class declaration type checking knot.
   }
   where
-    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tcLookupTyVar tvs1 ;
-				; tvs2' <- mapM tcLookupTyVar tvs2 ;
+    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tc_fd_tyvar tvs1 ;
+				; tvs2' <- mapM tc_fd_tyvar tvs2 ;
 				; return (tvs1', tvs2') }
+    tc_fd_tyvar name   -- Scoped kind variables are bound to unification variables
+                       -- which are now fixed, so we can zonk
+      = do { tv <- tcLookupTyVar name
+           ; ty <- zonkTyVarOcc emptyZonkEnv tv
+                  -- Squeeze out any kind unification variables
+           ; case getTyVar_maybe ty of
+               Just tv' -> return tv'
+               Nothing  -> pprPanic "tc_fd_tyvar" (ppr name $$ ppr tv $$ ppr ty) }
 
 tcTyClDecl1 _ _
   (ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
@@ -1030,7 +1042,9 @@ tcConArg new_or_data bty
   = do  { traceTc "tcConArg 1" (ppr bty)
         ; arg_ty <- tcHsConArgType new_or_data bty
         ; traceTc "tcConArg 2" (ppr bty)
-        ; strict_mark <- chooseBoxingStrategy arg_ty (getBangStrictness bty)
+        ; dflags <- getDynFlags
+        ; let strict_mark = chooseBoxingStrategy dflags arg_ty (getBangStrictness bty)
+                              -- Must be computed lazily
 	; return (arg_ty, strict_mark) }
 
 tcConRes :: ResType (LHsType Name) -> TcM (ResType Type)
@@ -1166,28 +1180,34 @@ conRepresentibleWithH98Syntax
 --
 -- We have turned off unboxing of newtypes because coercions make unboxing 
 -- and reboxing more complicated
-chooseBoxingStrategy :: TcType -> HsBang -> TcM HsBang
-chooseBoxingStrategy arg_ty bang
-  = case bang of
-	HsNoBang -> return HsNoBang
-	HsStrict -> do { unbox_strict <- doptM Opt_UnboxStrictFields
-                       ; if unbox_strict then return (can_unbox HsStrict arg_ty)
-                                         else return HsStrict }
-	HsNoUnpack -> return HsStrict
-	HsUnpack -> do { omit_prags <- doptM Opt_OmitInterfacePragmas
-                       ; let bang = can_unbox HsUnpackFailed arg_ty
-                       ; if omit_prags && bang == HsUnpack
-                            then return HsStrict
-                            else return bang }
-            -- Do not respect UNPACK pragmas if OmitInterfacePragmas is on
-	    -- See Trac #5252: unpacking means we must not conceal the
-	    --                 representation of the argument type
-            -- However: even when OmitInterfacePragmas is on, we still want
-            -- to know if we have HsUnpackFailed, because we omit a
-            -- warning in that case (#3966)
-        HsUnpackFailed -> pprPanic "chooseBoxingStrategy" (ppr arg_ty)
-		       	  -- Source code never has shtes
+chooseBoxingStrategy :: DynFlags -> TcType -> HsBang -> HsBang
+chooseBoxingStrategy dflags arg_ty bang
+  = case choice of
+      HsUnpack | dopt Opt_OmitInterfacePragmas dflags
+               -> HsStrict
+      _other   -> choice
   where
+    choice :: HsBang
+    choice = case bang of
+      HsNoBang -> HsNoBang
+      HsStrict -> let unbox_strict = dopt Opt_UnboxStrictFields dflags
+                  in if unbox_strict then (can_unbox HsStrict arg_ty)
+                                     else HsStrict
+      HsNoUnpack -> HsStrict
+      HsUnpack -> let omit_prags = dopt Opt_OmitInterfacePragmas dflags
+                      bang = can_unbox HsUnpackFailed arg_ty
+                  in if omit_prags && bang == HsUnpack
+                     then HsStrict
+                     else bang
+          -- Do not respect UNPACK pragmas if OmitInterfacePragmas is on
+          -- See Trac #5252: unpacking means we must not conceal the
+          --                 representation of the argument type
+          -- However: even when OmitInterfacePragmas is on, we still want
+          -- to know if we have HsUnpackFailed, because we omit a
+          -- warning in that case (#3966)
+      HsUnpackFailed -> pprPanic "chooseBoxingStrategy" (ppr arg_ty)
+                        -- Source code never has shtes
+
     can_unbox :: HsBang -> TcType -> HsBang
     -- Returns   HsUnpack  if we can unpack arg_ty
     -- 		 fail_bang if we know what arg_ty is but we can't unpack it

compiler/typecheck/TcUnify.lhs

@@ -1059,18 +1059,21 @@ happy to have types of kind Constraint on either end of an arrow.
 matchExpectedFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
 -- Like unifyFunTy, but does not fail; instead just returns Nothing
 
-matchExpectedFunKind (TyVarTy kvar) = do
-    maybe_kind <- readMetaTyVar kvar
-    case maybe_kind of
-      Indirect fun_kind -> matchExpectedFunKind fun_kind
-      Flexi ->
-          do { arg_kind <- newMetaKindVar
-             ; res_kind <- newMetaKindVar
-             ; writeMetaTyVar kvar (mkArrowKind arg_kind res_kind)
-             ; return (Just (arg_kind,res_kind)) }
-
-matchExpectedFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))
-matchExpectedFunKind _                         = return Nothing
+matchExpectedFunKind (FunTy arg_kind res_kind) 
+  = return (Just (arg_kind,res_kind))
+
+matchExpectedFunKind (TyVarTy kvar) 
+  | isTcTyVar kvar, isMetaTyVar kvar
+  = do { maybe_kind <- readMetaTyVar kvar
+       ; case maybe_kind of
+            Indirect fun_kind -> matchExpectedFunKind fun_kind
+            Flexi ->
+                do { arg_kind <- newMetaKindVar
+                   ; res_kind <- newMetaKindVar
+                   ; writeMetaTyVar kvar (mkArrowKind arg_kind res_kind)
+                   ; return (Just (arg_kind,res_kind)) } }
+
+matchExpectedFunKind _ = return Nothing
 
 -----------------  
 unifyKind :: TcKind           -- k1 (actual)
@@ -1162,17 +1165,20 @@ uUnboundKVar kv1 k2@(TyVarTy kv2)
 
 uUnboundKVar kv1 non_var_k2
   = do  { k2' <- zonkTcKind non_var_k2
-        ; kindOccurCheck kv1 k2'
         ; let k2'' = defaultKind k2'
                 -- MetaKindVars must be bound only to simple kinds
+        ; kindUnifCheck kv1 k2''
         ; writeMetaTyVar kv1 k2'' }
 
 ----------------
-kindOccurCheck :: TyVar -> Type -> TcM ()
-kindOccurCheck kv1 k2   -- k2 is zonked
-  = if elemVarSet kv1 (tyVarsOfType k2)
-    then failWithTc (kindOccurCheckErr kv1 k2)
-    else return ()
+kindUnifCheck :: TyVar -> Type -> TcM ()
+kindUnifCheck kv1 k2   -- k2 is zonked
+  | elemVarSet kv1 (tyVarsOfType k2)
+  = failWithTc (kindOccurCheckErr kv1 k2)
+  | isSigTyVar kv1
+  = failWithTc (kindSigVarErr kv1 k2)
+  | otherwise
+  = return ()
 
 mkKindErrorCtxt :: Type -> Type -> Kind -> Kind -> TidyEnv -> TcM (TidyEnv, SDoc)
 mkKindErrorCtxt ty1 ty2 k1 k2 env0
@@ -1204,4 +1210,9 @@ kindOccurCheckErr :: Var -> Type -> SDoc
 kindOccurCheckErr tyvar ty
   = hang (ptext (sLit "Occurs check: cannot construct the infinite kind:"))
        2 (sep [ppr tyvar, char '=', ppr ty])
+
+kindSigVarErr :: Var -> Type -> SDoc
+kindSigVarErr tv ty
+  = hang (ptext (sLit "Cannot unify the kind variable") <+> quotes (ppr tv))
+       2 (ptext (sLit "with the kind") <+> quotes (ppr ty))
 \end{code}

compiler/types/TyCon.lhs

@@ -595,7 +595,7 @@ via the PromotedTyCon alternative in TyCon.
   kind signature on the forall'd variable; so the tc_kind field of
   PromotedTyCon is not identical to the dataConUserType of the
   DataCon.  But it's the same modulo changing the variable kinds,
-  done by Kind.promoteType.
+  done by DataCon.promoteType.
 
 * Small note: We promote the *user* type of the DataCon.  Eg
      data T = MkT {-# UNPACK #-} !(Bool, Bool)

compiler/types/Type.lhs

@@ -93,7 +93,7 @@ module Type (
 
 	-- * Type comparison
         eqType, eqTypeX, eqTypes, cmpType, cmpTypes, 
-	eqPred, eqPredX, cmpPred, eqKind,
+	eqPred, eqPredX, cmpPred, eqKind, eqTyVarBndrs,
 
 	-- * Forcing evaluation of types
         seqType, seqTypes,
@@ -611,14 +611,14 @@ newtype at outermost level; and bale out if we see it again.
 
 Note [Nullary unboxed tuple]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We represent the nullary unboxed tuple as the unary (but void) type
+State# RealWorld.  The reason for this is that the ReprArity is never
+less than the Arity (as it would otherwise be for a function type like
+(# #) -> Int).
 
-We represent the nullary unboxed tuple as the unary (but void) type State# RealWorld.
-The reason for this is that the ReprArity is never less than the Arity (as it would
-otherwise be for a function type like (# #) -> Int).
-
-As a result, ReprArity is always strictly positive if Arity is. This is important
-because it allows us to distinguish at runtime between a thunk and a function
- takes a nullary unboxed tuple as an argument!
+As a result, ReprArity is always strictly positive if Arity is. This
+is important because it allows us to distinguish at runtime between a
+thunk and a function takes a nullary unboxed tuple as an argument!
 
 \begin{code}
 type UnaryType = Type
@@ -1178,6 +1178,17 @@ eqPred = eqType
 
 eqPredX :: RnEnv2 -> PredType -> PredType -> Bool
 eqPredX env p1 p2 = isEqual $ cmpTypeX env p1 p2
+
+eqTyVarBndrs :: RnEnv2 -> [TyVar] -> [TyVar] -> Maybe RnEnv2
+-- Check that the tyvar lists are the same length
+-- and have matching kinds; if so, extend the RnEnv2
+-- Returns Nothing if they don't match
+eqTyVarBndrs env [] []
+ = Just env
+eqTyVarBndrs env (tv1:tvs1) (tv2:tvs2)
+ | eqTypeX env (tyVarKind tv1) (tyVarKind tv2)
+ = eqTyVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
+eqTyVarBndrs _ _ _= Nothing
 \end{code}
 
 Now here comes the real worker
@@ -1208,7 +1219,8 @@ cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
 -- So the RHS has a data type
 
 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
-cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
+cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX env (tyVarKind tv1) (tyVarKind tv1)
+                                                       `thenCmp` cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2

configure.ac

@@ -13,7 +13,7 @@ dnl
 # see what flags are available. (Better yet, read the documentation!)
 #
 
-AC_INIT([The Glorious Glasgow Haskell Compilation System], [7.5], [glasgow-haskell-bugs@haskell.org], [ghc])
+AC_INIT([The Glorious Glasgow Haskell Compilation System], [7.6.1], [glasgow-haskell-bugs@haskell.org], [ghc])
 
 # Set this to YES for a released version, otherwise NO
 : ${RELEASE=NO}

docs/users_guide/7.6.1-notes.xml

@@ -17,9 +17,32 @@
 
     <itemizedlist>
       <listitem>
-          <para>
-              TODO
-          </para>
+        <para>
+          Polymorphic kinds and data promotion are now fully implemented and
+          supported features: <xref linkend="kind-polymorphism" />.
+        </para>
+      </listitem>
+
+      <listitem>
+        <para>
+          Windows 64bit is now a supported platform.
+        </para>
+      </listitem>
+
+      <listitem>
+        <para>
+          It is now possible to defer type errors until runtime using the
+          <literal>-fdefer-type-errors</literal> flag: <xref
+              linkend="defer-type-errors" />.
+        </para>
+      </listitem>
+
+      <listitem>
+        <para>
+          The RTS now supports changing the number of capabilities at runtime
+          with <literal>Control.Concurrent.setNumCapabilities</literal>: <xref
+            linkend="parallel-options" />.
+        </para>
       </listitem>
     </itemizedlist>
   </sect2>
@@ -29,85 +52,302 @@
     <sect3>
         <title>Language</title>
         <itemizedlist>
-            <listitem>
-                <para>
-                    TODO
-                </para>
-            </listitem>
+          <listitem>
+            <para>
+              There is a new extension <literal>ExplicitNamespaces</literal>
+              that allows to qualify the export of a type with the
+              <literal>type</literal> keyword.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              The behavior of the <literal>TypeOperator</literal> extension has
+              changed: previously, only type operators starting with ":" were
+              considered type constructors, and other operators were treated as
+              type variables. Now type operators are always constructors.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              It is now possible to explicitly annotate types with kind
+              variables (<ulink
+                url="http://hackage.haskell.org/trac/ghc/ticket/5862">#5862</ulink>).
+              You can now write, for example:
+<programlisting>
+class Category (c :: k -> k -> *) where
+  type Ob c :: k -> Constraint
+  id :: Ob c a => c a a
+  (.) :: (Ob c a, Ob c b, Ob c c) => c b c -> c a b -> c a c
+</programlisting>
+              and the variable <literal>k</literal>, ranging over kinds, is in scope within the
+              class declaration.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              It is now possible to derive instances of
+              <literal>Generic1</literal> automatically. See <xref
+                linkend="generic-programming" /> for more information.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              There is a new FFI calling convention <literal>capi</literal>,
+              enabled by the <literal>CApiFFI</literal> extension. For example,
+              given the following declaration:
+<programlisting>
+foreign import capi "header.h f" f :: CInt -> IO CInt
+</programlisting>
+              GHC will generate code to call <literal>f</literal> using the C
+              API defined in the header <literal>header.h</literal>. Thus
+              <literal>f</literal> can be called even if it may be defined as a
+              CPP <literal>#define</literal>, rather than a proper function.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              There is a new pragma <literal>CTYPE</literal>, which can be used
+              to specify the C type that a Haskell type corresponds to, when it
+              is used with the <literal>capi</literal> calling convention.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              Generic default methods are now allowed for multi-parameter type classes.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              A constructor of a GADT is now considered infix (by a derived
+              <literal>Show</literal> instance) if it is a two-argument
+              operator with a fixity declaration (<ulink
+                url="http://hackage.haskell.org/trac/ghc/ticket/5712">#5712</ulink>).
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              There is a new extension <literal>InstanceSigs</literal>, which
+              allows type signatures to be specified in instance declarations.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              GHC now supports numeric and string type literals (enabled by
+              <literal>DataKinds</literal>), of kind <literal>Nat</literal> and
+              <literal>Symbol</literal> respectively (see <xref
+                  linkend="promoted-literals" />).
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              The type <literal>Any</literal> can now be used as an argument
+              for <literal>foreign prim</literal> functions.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              The <literal>mdo</literal> keyword has been reintroduced. This
+              keyword can be used to create <literal>do</literal> expressions
+              with recursive bindings. The behavior of the
+              <literal>rec</literal> keyword has been changed, so that it does
+              not perform automatic segmentation in a <literal>do</literal>
+              expression anymore.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              There is a new syntactic construct (enabled by the <literal>LambdaCase</literal> extension)
+              for creating an anonymous function out of a <literal>case</literal> expression. For example,
+              the following expression:
+<programlisting>
+\case
+    Nothing -> 0
+    Just n  -> n
+</programlisting>
+              is equivalent to:
+<programlisting>
+\x -> case x of
+    Nothing -> 0
+    Just n  -> n
+</programlisting>
+              See <xref linkend="lambda-case" /> for more details.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              There is a new syntactic construct (enabled by the
+              <literal>MultiWayIf</literal> extension) to create conditional
+              expressions with multiple branches. For example, you can now
+              write:
+<programlisting>
+if | x == 0    -> [...]
+   | x &gt; 1     -> [...]
+   | x &lt; 0     -> [...]
+   | otherwise -> [...]
+</programlisting>
+              See <xref linkend="multi-way-if" /> for more information.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              Some limitations on the usage of unboxed tuples have been lifted.
+              For example, when the <literal>UnboxedTuples</literal> extension
+              is on, an unboxed tuple can now be used as the type of a
+              constructor, function argument, or variable:
+<programlisting>
+data Foo = Foo (# Int, Int #)
 
-            <listitem>
-                <para>
-                    TODO
-                    CAPI now supported (it was in 7.4, but not
-                    documented or officially supported).
-                </para>
-            </listitem>
+f :: (# Int, Int #) -&gt; (# Int, Int #)
+f x = x
+
+g :: (# Int, Int #) -&gt; Int
+g (# a,b #) = a
+
+h x = let y = (# x,x #) in ...
+</programlisting>
+            </para>
+            <para>
+              Unboxed tuple can now also be nested:
+<programlisting>
+f :: (# Int, (# Int, Int #), Bool #)
+</programlisting>
+            </para>
+          </listitem>
         </itemizedlist>
     </sect3>
 
     <sect3>
         <title>Compiler</title>
         <itemizedlist>
-            <listitem>
-                <para>
-                    TODO
-                </para>
-            </listitem>
+          <listitem>
+             <para>
+               The <literal>-package</literal> flag now correctly loads only
+               the most recent version of a package (<ulink
+                 url="http://hackage.haskell.org/trac/ghc/ticket/7030">#7030</ulink>).
+             </para>
+           </listitem>
+          <listitem>
+             <para>
+               In <literal>--make</literal> mode, GHC now gives an indication
+               of why a module is being recompiled.
+             </para>
+          </listitem>
+          <listitem>
+            <para>
+              There is a new flag <literal>-freg-liveness</literal> flag to control if
+                STG liveness information is used for optimisation. The flag is
+                enabled by default.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              Package database flags have been renamed from
+              <literal>-package-conf*</literal> to
+              <literal>-package-db*</literal>.
+            </para>
+          </listitem>
+          <listitem>
+            <para>
+              It is now possible to hide the global package db, and specify the
+              order of the user and global package databases in the stack (see
+              <xref linkend="package-databases" />).
+            </para>
+          </listitem>
         </itemizedlist>
     </sect3>
 
     <sect3>
         <title>GHCi</title>
         <itemizedlist>
-            <listitem>
-                <para>
-                    TODO
-                </para>
-            </listitem>
+           <listitem>
+              <para>
+                Commands defined later have now precedence in the resolution of
+                abbreviated commands (<ulink
+                  url="http://hackage.haskell.org/trac/ghc/ticket/3858">#3858</ulink>).
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                It is now possible to specify a custom pretty-printing function
+                for expressions evaluated at the prompt using the
+                <literal>-interactive-print</literal> flag.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                GHCi now supports loading additional <literal>.ghci</literal>
+                files via the <literal>-ghci-script</literal> flag (<ulink
+                  url="http://hackage.haskell.org/trac/ghc/ticket/5265">#5265</ulink>).
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                A new <literal>:seti</literal> command has been introduced,
+                which sets an option that applies only at the prompt.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                Files are now reloaded after having been edited with the <literal>:edit</literal> command.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                <literal>default</literal> declarations can now be entered at the GHCi prompt.
+              </para>
+           </listitem>
         </itemizedlist>
     </sect3>
 
     <sect3>
         <title>Template Haskell</title>
         <itemizedlist>
-            <listitem>
-                <para>
-                    TODO
-                </para>
-            </listitem>
+           <listitem>
+              <para>
+                Promoted kinds and kind polymorphism are now supported in
+                Template Haskell.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                It is now possible to create fixity declarations in Template
+                Haskell (<ulink
+                  url="http://hackage.haskell.org/trac/ghc/ticket/1541">#1541</ulink>).
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                Primitive byte-array literals can now be created with Template
+                Haskell (<ulink
+                  url="http://hackage.haskell.org/trac/ghc/ticket/5877">#5877</ulink>).
+              </para>
+           </listitem>
         </itemizedlist>
     </sect3>
 
     <sect3>
-        <title>Profiling</title>
+        <title>Runtime system</title>
         <itemizedlist>
             <listitem>
-                <para>
-                    TODO
-                </para>
+              <para>
+                The presentation of parallel GC work balance in <literal>+RTS
+                  -s</literal> is now expressed as a percentage value (with
+                100% being "perfect") instead of a number from 1 to N, with N
+                being the number of capabilities.
+              </para>
             </listitem>
-        </itemizedlist>
-    </sect3>
-
-    <sect3>
-        <title>Event logging</title>
-        <itemizedlist>
-
             <listitem>
-                <para>
-                    TODO
-                </para>
+              <para>
+                The RTS now supports changing the number of capabilities at runtime
+                with <literal>Control.Concurrent.setNumCapabilities</literal>: <xref
+                  linkend="parallel-options" />.
+              </para>
             </listitem>
-        </itemizedlist>
-    </sect3>
-
-    <sect3>
-        <title>Runtime system</title>
-        <itemizedlist>
             <listitem>
-                <para>
-                    TODO
-                </para>
+              <para>
+                The internal timer is now based on a monotonic clock in both
+                the threaded and non-threaded RTS, on all tier-1 platforms.
+              </para>
             </listitem>
         </itemizedlist>
     </sect3>
@@ -115,11 +355,16 @@
     <sect3>
         <title>Build system</title>
         <itemizedlist>
-            <listitem>
-                <para>
-                    TODO
-                </para>
-            </listitem>
+           <listitem>
+              <para>
+                GHC >= 7.0 is now required for bootstrapping.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                Windows 64bit is now a supported platform.
+              </para>
+           </listitem>
         </itemizedlist>
     </sect3>
   </sect2>
@@ -128,7 +373,6 @@
     <title>Libraries</title>
 
     <para>
-        TODO
         There have been some changes that have effected multiple
         libraries:
     </para>
@@ -136,17 +380,41 @@
     <itemizedlist>
         <listitem>
             <para>
-                TODO
+                The deprecated function <literal>catch</literal> has been
+                removed from <literal>Prelude</literal>.
             </para>
         </listitem>
     </itemizedlist>
 
+    <para>
+        The following libraries have been removed from the GHC tree:
+    </para>
+
+    <itemizedlist>
+        <listitem>
+            <para>extensible-exceptions</para>
+        </listitem>
+        <listitem>
+            <para>mtl</para>
+        </listitem>
+    </itemizedlist>
+
+    <para>
+        The following libraries have been added to the GHC tree:
+    </para>
+
+    <itemizedlist>
+        <listitem>
+            <para>tranformers (version 0.3.0.0)</para>
+        </listitem>
+    </itemizedlist>
+
     <sect3>
         <title>array</title>
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 0.4.0.1 (was 0.4.0.0)
                 </para>
             </listitem>
         </itemizedlist>
@@ -155,11 +423,143 @@
     <sect3>
         <title>base</title>
         <itemizedlist>
-            <listitem>
-                <para>
-                    Version number TODO (was TODO)
-                </para>
-            </listitem>
+           <listitem>
+              <para>
+                Version number 4.6.0.0 (was 4.5.1.0)
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                The <literal>Text.Read</literal> module now exports functions
+<programlisting>
+readEither :: Read a => String -> Either String a
+readMaybe :: Read a => String -> Maybe a
+</programlisting>
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                An infix alias for <literal>mappend</literal> in <literal>Data.Monoid</literal> has been introduced:
+<programlisting>
+(&lt;&gt;) :: Monoid m => m -> m -> m
+</programlisting>
+
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                The <literal>Bits</literal> class does not have a <literal>Num</literal> superclass anymore.
+              </para>
+              <para>
+                You can make code that works with both
+                Haskell98/Haskell2010 and GHC by:
+                <itemizedlist>
+                  <listitem>
+                    <para>
+                      Whenever you make a <literal>Bits</literal> instance
+                      of a type, also make <literal>Num</literal> instance, and
+                    </para>
+                  </listitem>
+                  <listitem>
+                    <para>
+                      Whenever you give a function, instance or class a
+                      <literal>Bits t</literal> constraint, also give it
+                      a <literal>Num t</literal> constraint.
+                    </para>
+                  </listitem>
+                </itemizedlist>
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                <literal>Applicative</literal> and
+                <literal>Alternative</literal> instances for the
+                <literal>ReadP</literal> and <literal>ReadPrec</literal> monads
+                have been added.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                <literal>foldl'</literal> and <literal>foldr'</literal> in
+                <literal>Data.Foldable</literal> are now methods of the
+                <literal>Foldable</literal> class.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                The deprecated <literal>Control.OldException</literal> module has now been removed.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                Strict versions of <literal>modifyIORef</literal> and <literal>atomicModifyIORef</literal> have been added to the <literal>Data.IORef</literal> module:
+<programlisting>
+modifyIORef' :: IORef a -> (a -> a) -> IO ()
+atomicModifyIORef' :: IORef a -> (a -> (a,b)) -> IO b
+</programlisting>
+              </para>
+              <para>
+                Similarly, a strict version of <literal>modifySTRef</literal>
+                has been added to <literal>Data.STRef</literal>.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                A bug in the fingerprint calculation for
+                <literal>TypeRep</literal> (<ulink
+                  url="http://hackage.haskell.org/trac/ghc/ticket/5962">#5962</ulink>)
+                has been fixed.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                A new function <literal>lookupEnv</literal> has been added to
+                <literal>System.Environment</literal>, which behaves like
+                <literal>getEnv</literal>, but returns
+                <literal>Nothing</literal> when the environment variable is
+                not defined, instead of throwing an exception.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                There is a new function <literal>getGCStatsEnabled</literal> in
+                <literal>GHC.Stats</literal>, which checks whether GC stats
+                have been enabled (for example, via the <literal>-T</literal>
+                RTS flag).
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                <literal>QSem</literal> in
+                <literal>Control.Concurrent</literal> is now deprecated, and
+                will be removed in GHC 7.8. Please use an alternative, e.g. the
+                SafeSemaphore package, instead.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                A new function <literal>getExecutablePath</literal> has been
+                added to <literal>System.Environment</literal>. This function
+                returns the full path of the current executable, as opposed to
+                <literal>getProgName</literal>, which only returns the base
+                name.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                The <literal>Data.HashTable</literal> module is now deprecated,
+                and will be removed in GHC 7.8. Please use an alternative, e.g.
+                the hashtables package, instead.
+              </para>
+           </listitem>
+           <listitem>
+              <para>
+                The <literal>Data.Ord</literal> module now exports the
+                <literal>Down</literal> <literal>newtype</literal>, which
+                reverses the sort order of its argument.
+              </para>
+           </listitem>
+
         </itemizedlist>
     </sect3>
 
@@ -179,7 +579,7 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 0.5.1.1 (was 0.5.1.0)
                 </para>
             </listitem>
         </itemizedlist>
@@ -190,7 +590,20 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 0.10.0.0 (was 0.9.2.1)
+                </para>
+            </listitem>
+            <listitem>
+                <para>
+                    A new module
+                    <literal>Data.ByteString.Lazy.Builder</literal> has been
+                    added.
+                </para>
+                <para>
+                    The new module defines a <literal>Builder</literal> monoid,
+                    which allows to efficiently construct bytestrings by
+                    concatenation. Possible applications include binary
+                    serialization, targets for efficient pretty-printers, etc.
                 </para>
             </listitem>
         </itemizedlist>
@@ -201,14 +614,14 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 1.16.0 (was 1.14.0)
                 </para>
             </listitem>
 
             <listitem>
                 <para>
                     For details of the changes to the Cabal library,
-                    plese see the Cabal changelog.
+                    please see the Cabal changelog.
                 </para>
             </listitem>
         </itemizedlist>
@@ -219,7 +632,16 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 0.5.0.0 (was 0.4.2.1)
+                </para>
+            </listitem>
+
+            <listitem>
+                <para>
+                    See <ulink
+                        url="http://www.haskell.org/pipermail/haskell-cafe/2012-May/101082.html">the
+                        announcement</ulink> for details of the changes to the
+                    containers library.
                 </para>
             </listitem>
         </itemizedlist>
@@ -230,7 +652,7 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 1.3.0.1 (was 1.3.0.0)
                 </para>
             </listitem>
         </itemizedlist>
@@ -241,18 +663,12 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 1.2.0.0 (was 1.1.0.2)
                 </para>
             </listitem>
-        </itemizedlist>
-    </sect3>
-
-    <sect3>
-        <title>extensible-exceptions</title>
-        <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    The dependency on the old-time package has been changed to time.
                 </para>
             </listitem>
         </itemizedlist>
@@ -263,7 +679,7 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 1.3.0.1 (was 1.3.0.0)
                 </para>
             </listitem>
         </itemizedlist>
@@ -285,7 +701,7 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 2.0.0.2 (was 2.0.0.1)
                 </para>
             </listitem>
         </itemizedlist>
@@ -296,7 +712,7 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 1.1.1.0 (was 1.1.0.1)
                 </para>
             </listitem>
         </itemizedlist>
@@ -307,9 +723,34 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 3.9.0.0 (was 3.8.7.3)
                 </para>
             </listitem>
+            <listitem>
+                <para>
+                    <literal>Compiler.Hoopl.Block</literal> now contains the
+                    Block datatype and all the operations on blocks.
+                </para>
+            </listitem>
+            <listitem>
+                <para>
+                    <literal>Compiler.Hoopl.Graph</literal> now has the
+                    operations on Graphs.
+                </para>
+            </listitem>
+            <listitem>
+                <para>
+                    <literal>Compiler.Hoopl.Util</literal> and
+                    <literal>Compiler.Hoopl.GraphUtil</literal> have been
+                    removed; their contents have been moved to other modules.
+                </para>
+            </listitem>
+            <listitem>
+                <para>The Dataflow algorithms have been optimized.</para>
+            </listitem>
+            <listitem>
+                <para>Numerous other API changes.</para>
+            </listitem>
         </itemizedlist>
     </sect3>
 
@@ -318,7 +759,12 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 0.6.0.0 (was 0.5.1.1)
+                </para>
+            </listitem>
+            <listitem>
+                <para>
+                    The dependency on the old-time package has been changed to time.
                 </para>
             </listitem>
         </itemizedlist>
@@ -329,7 +775,7 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 0.5.0.0 (was 0.4.0.0)
                 </para>
             </listitem>
         </itemizedlist>
@@ -340,7 +786,7 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 1.0.0.5 (was 1.0.0.4)
                 </para>
             </listitem>
         </itemizedlist>
@@ -351,29 +797,25 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 1.1.0.1 (was 1.1.0.0)
                 </para>
             </listitem>
         </itemizedlist>
     </sect3>
 
     <sect3>
-        <title>pretty</title>
+        <title>process</title>
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 1.1.0.2 (was 1.1.0.1)
                 </para>
             </listitem>
-        </itemizedlist>
-    </sect3>
-
-    <sect3>
-        <title>process</title>
-        <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Asynchronous exception bugs in
+                    <literal>readProcess</literal> and
+                    <literal>readProcessWithExitCode</literal> have been fixed.
                 </para>
             </listitem>
         </itemizedlist>
@@ -384,7 +826,24 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 2.8.0.0 (was 2.7.0.0)
+                </para>
+            </listitem>
+            <listitem>
+                <para>
+                    Promoted kinds and kind polymorphism are now supported in Template Haskell.
+                </para>
+            </listitem>
+            <listitem>
+                <para>
+                    Fixity declarations have been added to Template Haskell.
+                </para>
+            </listitem>
+            <listitem>
+                <para>
+                    The <literal>StringPrimL</literal> constructor for
+                    <literal>Lit</literal> now takes a <literal>Word8</literal>
+                    array, instead of a <literal>String</literal>.
                 </para>
             </listitem>
         </itemizedlist>
@@ -395,7 +854,7 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 1.4.1 (was 1.4)
                 </para>
             </listitem>
         </itemizedlist>
@@ -406,7 +865,22 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 2.6.0.0 (was 2.5.1.1)
+                </para>
+            </listitem>
+            <listitem>
+                <para>
+                    Bindings for <literal>mkdtemp</literal> and <literal>mkstemps</literal> have been added.
+                </para>
+            </listitem>
+            <listitem>
+                <para>
+                    New functions <literal>setEnvironment</literal> and <literal>cleanEnv</literal> have been added.
+                </para>
+            </listitem>
+            <listitem>
+                <para>
+                    Bindings for functions to access high resolution timestamps have been added.
                 </para>
             </listitem>
         </itemizedlist>
@@ -417,7 +891,7 @@
         <itemizedlist>
             <listitem>
                 <para>
-                    Version number TODO (was TODO)
+                    Version number 2.3.0.0 (was 2.2.2.0)
                 </para>
             </listitem>
         </itemizedlist>

docs/users_guide/ffi-chap.xml

@@ -164,7 +164,7 @@ foreign import ccall interruptible
       <sect2 id="ffi-capi">
         <title>The CAPI calling convention</title>
         <para>
-          The <literal>CAPI</literal> extension allows a calling
+          The <literal>CApiFFI</literal> extension allows a calling
           convention of <literal>capi</literal> to be used in foreign
           declarations, e.g.
 

docs/users_guide/glasgow_exts.xml

@@ -71,17 +71,18 @@ documentation</ulink> describes all the libraries that come with GHC.
 <para>GHC is built on a raft of primitive data types and operations;
 "primitive" in the sense that they cannot be defined in Haskell itself.
 While you really can use this stuff to write fast code,
-  we generally find it a lot less painful, and more satisfying in the
-  long run, to use higher-level language features and libraries.  With
-  any luck, the code you write will be optimised to the efficient
-  unboxed version in any case.  And if it isn't, we'd like to know
-  about it.</para>
+we generally find it a lot less painful, and more satisfying in the
+long run, to use higher-level language features and libraries.  With
+any luck, the code you write will be optimised to the efficient
+unboxed version in any case.  And if it isn't, we'd like to know
+about it.</para>
 
 <para>All these primitive data types and operations are exported by the
 library <literal>GHC.Prim</literal>, for which there is
 <ulink url="&libraryGhcPrimLocation;/GHC-Prim.html">detailed online documentation</ulink>.
 (This documentation is generated from the file <filename>compiler/prelude/primops.txt.pp</filename>.)
 </para>
+
 <para>
 If you want to mention any of the primitive data types or operations in your
 program, you must first import <literal>GHC.Prim</literal> to bring them
@@ -94,8 +95,7 @@ and <link linkend="unboxed-tuples">unboxed tuples</link>, which
 we briefly summarise here. </para>
 
 <sect2 id="glasgow-unboxed">
-<title>Unboxed types
-</title>
+<title>Unboxed types</title>
 
 <para>
 <indexterm><primary>Unboxed types (Glasgow extension)</primary></indexterm>
@@ -202,8 +202,7 @@ since <literal>b</literal> has type <literal>Int#</literal>.
 </sect2>
 
 <sect2 id="unboxed-tuples">
-<title>Unboxed Tuples
-</title>
+<title>Unboxed tuples</title>
 
 <para>
 Unboxed tuples aren't really exported by <literal>GHC.Exts</literal>;
@@ -238,46 +237,19 @@ tuples to avoid unnecessary allocation during sequences of operations.
 </para>
 
 <para>
-There are some pretty stringent restrictions on the use of unboxed tuples:
+There are some restrictions on the use of unboxed tuples:
 <itemizedlist>
-<listitem>
 
+<listitem>
 <para>
 Values of unboxed tuple types are subject to the same restrictions as
 other unboxed types; i.e. they may not be stored in polymorphic data
 structures or passed to polymorphic functions.
-
 </para>
 </listitem>
-<listitem>
 
-<para>
-No variable can have an unboxed tuple type, nor may a constructor or function
-argument have an unboxed tuple type.  The following are all illegal:
-<programlisting>
-  data Foo = Foo (# Int, Int #)
-
-  f :: (# Int, Int #) -&#62; (# Int, Int #)
-  f x = x
-
-  g :: (# Int, Int #) -&#62; Int
-  g (# a,b #) = a
-
-  h x = let y = (# x,x #) in ...
-</programlisting>
-</para>
-</listitem>
 <listitem>
 <para>
-Unboxed tuples may not be nested. So this is illegal:
-<programlisting>
-f :: (# Int, (# Int, Int #), Bool #)
-</programlisting>
-</para>
-</listitem>
-</itemizedlist>
-</para>
-<para>
 The typical use of unboxed tuples is simply to return multiple values,
 binding those multiple results with a <literal>case</literal> expression, thus:
 <programlisting>
@@ -298,6 +270,10 @@ above example desugars like this:
         in ..body..
 </programlisting>
 Indeed, the bindings can even be recursive.
+</para>
+</listitem>
+</itemizedlist>
+
 </para>
 
 </sect2>
@@ -656,7 +632,7 @@ type Typ
 data TypView = Unit
              | Arrow Typ Typ
 
-view :: Type -> TypeView
+view :: Typ -> TypView
 
 -- additional operations for constructing Typ's ...
 </programlisting>
@@ -3750,7 +3726,7 @@ We reuse the keyword <literal>default</literal> to signal that a signature
 applies to the default method only; when defining instances of the
 <literal>Enum</literal> class, the original type <literal>[a]</literal> of
 <literal>enum</literal> still applies. When giving an empty instance, however,
-the default implementation <literal>map to0 genum</literal> is filled-in,
+the default implementation <literal>map to genum</literal> is filled-in,
 and type-checked with the type
 <literal>(Generic a, GEnum (Rep a)) => [a]</literal>.
 </para>
@@ -7065,6 +7041,94 @@ If you supply a type signature, then the flag has no effect.
 </sect1>
 <!-- ==================== End of type system extensions =================  -->
 
+<sect1 id="defer-type-errors">
+<title>Deferring type errors to runtime</title>
+  <para>
+    While developing, sometimes it is desirable to allow compilation to succeed
+    even if there are type errors in the code. Consider the following case:
+<programlisting>
+module Main where
+
+a :: Int
+a = 'a'
+
+main = print "b"
+</programlisting>
+    Even though <literal>a</literal> is ill-typed, it is not used in the end, so if
+    all that we're interested in is <literal>main</literal> it can be useful to be
+    able to ignore the problems in <literal>a</literal>.
+  </para>
+  <para>
+    For more motivation and details please refer to the <ulink
+      url="http://hackage.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime">HaskellWiki</ulink>
+    page or the <ulink
+      url="http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/">original
+      paper</ulink>.
+  </para>
+
+<sect2><title>Enabling deferring of type errors</title>
+  <para>
+    The flag <literal>-fdefer-type-errors</literal> controls whether type
+    errors are deferred to runtime. Type errors will still be emitted as
+    warnings, but will not prevent compilation.
+  </para>
+  <para>
+    At runtime, whenever a term containing a type error would need to be
+    evaluated, the error is converted into a runtime exception.
+    Note that type errors are deferred as much as possible during runtime, but
+    invalid coercions are never performed, even when they would ultimately
+    result in a value of the correct type. For example, given the following
+    code:
+<programlisting>
+x :: Int
+x = 0
+
+y :: Char
+y = x
+
+z :: Int
+z = y
+</programlisting>
+    evaluating <literal>z</literal> will result in a runtime type error.
+  </para>
+</sect2>
+<sect2><title>Deferred type errors in GHCi</title>
+  <para>
+    The flag <literal>-fdefer-type-errors</literal> works in GHCi as well, with
+    one exception: for "naked" expressions typed at the prompt, type
+    errors don't get delayed, so for example:
+<programlisting>
+Prelude> fst (True, 1 == 'a')
+
+&lt;interactive&gt;:2:12:
+    No instance for (Num Char) arising from the literal `1'
+    Possible fix: add an instance declaration for (Num Char)
+    In the first argument of `(==)', namely `1'
+    In the expression: 1 == 'a'
+    In the first argument of `fst', namely `(True, 1 == 'a')'
+</programlisting>
+Otherwise, in the common case of a simple type error such as 
+typing <literal>reverse True</literal> at the prompt, you would get a warning and then
+an immediately-following type error when the expression is evaluated.
+  </para>
+  <para>
+    This exception doesn't apply to statements, as the following example demonstrates:
+<programlisting>
+Prelude> let x = (True, 1 == 'a')
+
+&lt;interactive&gt;:3:16: Warning:
+    No instance for (Num Char) arising from the literal `1'
+    Possible fix: add an instance declaration for (Num Char)
+    In the first argument of `(==)', namely `1'
+    In the expression: 1 == 'a'
+    In the expression: (True, 1 == 'a')
+Prelude> fst x
+True
+</programlisting>
+  </para>
+</sect2>
+</sect1>
+
 <!-- ====================== TEMPLATE HASKELL =======================  -->
 
 <sect1 id="template-haskell">
@@ -9447,7 +9511,7 @@ Sometimes, however, this approach is over-cautious, and we <emphasis>do</emphasi
 rule to fire, even though doing so would duplicate redex.  There is no way that GHC can work out
 when this is a good idea, so we provide the CONLIKE pragma to declare it, thus:
 <programlisting>
-{-# INLINE[1] CONLIKE f #-}
+{-# INLINE CONLIKE [1] f #-}
 f x = <replaceable>blah</replaceable>
 </programlisting>
 CONLIKE is a modifier to an INLINE or NOINLINE pragma.  It specifies that an application

docs/users_guide/intro.xml

@@ -278,8 +278,11 @@
 	<term>Stable snapshots</term>
 	<listitem>
 	  <para>
-      We may make snapshot releases of the current
-      stable branch <ulink url="http://www.haskell.org/ghc/dist/stable/dist/">available for download</ulink>, and the latest sources are available from <ulink url="http://hackage.haskell.org/trac/ghc/wiki/DarcsRepositories">the darcs repositories</ulink>.
+            We may make snapshot releases of the current stable branch <ulink
+            url="http://www.haskell.org/ghc/dist/stable/dist/">available for
+            download</ulink>, and the latest sources are available from <ulink
+            url="http://hackage.haskell.org/trac/ghc/wiki/Repositories">the git
+            repositories</ulink>.
 	  </para>
 
 	  <para>Stable snapshot releases are named
@@ -310,8 +313,11 @@
 	<term>Unstable snapshots</term>
 	<listitem>
 	  <para>
-      We may make snapshot releases of the
-      HEAD <ulink url="http://www.haskell.org/ghc/dist/current/dist/">available for download</ulink>, and the latest sources are available from <ulink url="http://hackage.haskell.org/trac/ghc/wiki/DarcsRepositories">the darcs repositories</ulink>.
+            We may make snapshot releases of the HEAD <ulink
+            url="http://www.haskell.org/ghc/dist/current/dist/">available for
+            download</ulink>, and the latest sources are available from <ulink
+            url="http://hackage.haskell.org/trac/ghc/wiki/Repositories">the git
+            repositories</ulink>.
 	  </para>
 
 	  <para>Unstable snapshot releases are named