Merge commit with origin/master
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 21 Oct 2014 14:11:29 +0000 (15:11 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 21 Oct 2014 14:11:29 +0000 (15:11 +0100)
168 files changed:
compiler/basicTypes/SrcLoc.lhs
compiler/basicTypes/Var.lhs
compiler/coreSyn/CorePrep.lhs
compiler/deSugar/Desugar.lhs
compiler/deSugar/DsBinds.lhs
compiler/ghci/Debugger.hs
compiler/ghci/RtClosureInspect.hs
compiler/main/DynFlags.hs
compiler/main/ErrUtils.lhs
compiler/main/PprTyThing.hs
compiler/main/TidyPgm.lhs
compiler/nativeGen/AsmCodeGen.lhs
compiler/simplCore/CoreMonad.lhs
compiler/simplCore/SimplCore.lhs
compiler/simplCore/SimplMonad.lhs
compiler/simplCore/Simplify.lhs
compiler/typecheck/FamInst.lhs
compiler/typecheck/Flattening-notes [new file with mode: 0644]
compiler/typecheck/FunDeps.lhs
compiler/typecheck/Inst.lhs
compiler/typecheck/TcBinds.lhs
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcDeriv.lhs
compiler/typecheck/TcEnv.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcEvidence.lhs
compiler/typecheck/TcExpr.lhs
compiler/typecheck/TcGenDeriv.lhs
compiler/typecheck/TcGenGenerics.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcPat.lhs
compiler/typecheck/TcPatSyn.lhs
compiler/typecheck/TcRnDriver.lhs
compiler/typecheck/TcRnMonad.lhs
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcRules.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs
compiler/types/FamInstEnv.lhs
compiler/types/InstEnv.lhs
compiler/utils/Outputable.lhs
libraries/time
rts/Linker.c
rts/RtsStartup.c
testsuite/tests/deSugar/should_compile/T2431.stderr
testsuite/tests/deriving/should_fail/T9071.stderr
testsuite/tests/deriving/should_fail/T9071_2.stderr
testsuite/tests/gadt/T3169.stderr
testsuite/tests/gadt/T7293.stderr
testsuite/tests/gadt/T7294.stderr
testsuite/tests/gadt/gadt21.stderr
testsuite/tests/ghc-api/apirecomp001/apirecomp001.stderr
testsuite/tests/ghci.debugger/scripts/break026.stdout
testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs
testsuite/tests/indexed-types/should_compile/Simple13.hs
testsuite/tests/indexed-types/should_compile/Simple8.hs
testsuite/tests/indexed-types/should_compile/T3017.stderr
testsuite/tests/indexed-types/should_compile/T3208b.stderr
testsuite/tests/indexed-types/should_compile/T3826.hs
testsuite/tests/indexed-types/should_compile/T4494.hs
testsuite/tests/indexed-types/should_compile/T7804.hs
testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.hs
testsuite/tests/indexed-types/should_fail/GADTwrong1.hs
testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr
testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
testsuite/tests/indexed-types/should_fail/Overlap9.stderr
testsuite/tests/indexed-types/should_fail/T1897b.stderr
testsuite/tests/indexed-types/should_fail/T1900.stderr
testsuite/tests/indexed-types/should_fail/T2544.hs
testsuite/tests/indexed-types/should_fail/T2544.stderr
testsuite/tests/indexed-types/should_fail/T2627b.hs
testsuite/tests/indexed-types/should_fail/T2664.hs
testsuite/tests/indexed-types/should_fail/T2664.stderr
testsuite/tests/indexed-types/should_fail/T2693.stderr
testsuite/tests/indexed-types/should_fail/T4093a.hs
testsuite/tests/indexed-types/should_fail/T4174.stderr
testsuite/tests/indexed-types/should_fail/T4179.stderr
testsuite/tests/indexed-types/should_fail/T4272.stderr
testsuite/tests/indexed-types/should_fail/T5439.stderr
testsuite/tests/indexed-types/should_fail/T5934.stderr
testsuite/tests/indexed-types/should_fail/T7010.stderr
testsuite/tests/indexed-types/should_fail/T7729.stderr
testsuite/tests/indexed-types/should_fail/T7729a.hs
testsuite/tests/indexed-types/should_fail/T7729a.stderr
testsuite/tests/indexed-types/should_fail/T7786.hs
testsuite/tests/indexed-types/should_fail/T8129.stdout
testsuite/tests/indexed-types/should_fail/T8227.hs
testsuite/tests/indexed-types/should_fail/T8227.stderr
testsuite/tests/indexed-types/should_fail/T8518.stderr
testsuite/tests/indexed-types/should_fail/T9036.stderr
testsuite/tests/numeric/should_compile/T7116.stdout
testsuite/tests/parser/should_compile/T2245.stderr
testsuite/tests/perf/compiler/T5837.hs
testsuite/tests/perf/compiler/T5837.stderr
testsuite/tests/polykinds/T7438.stderr
testsuite/tests/rebindable/rebindable6.stderr
testsuite/tests/roles/should_compile/Roles13.stderr
testsuite/tests/roles/should_compile/T8958.stderr
testsuite/tests/simplCore/should_compile/EvalTest.stdout
testsuite/tests/simplCore/should_compile/T3717.stderr
testsuite/tests/simplCore/should_compile/T3772.stdout
testsuite/tests/simplCore/should_compile/T4201.stdout
testsuite/tests/simplCore/should_compile/T4306.stdout
testsuite/tests/simplCore/should_compile/T4908.stderr
testsuite/tests/simplCore/should_compile/T4918.stdout
testsuite/tests/simplCore/should_compile/T4930.stderr
testsuite/tests/simplCore/should_compile/T5366.stdout
testsuite/tests/simplCore/should_compile/T6056.stderr
testsuite/tests/simplCore/should_compile/T7360.stderr
testsuite/tests/simplCore/should_compile/T7865.stdout
testsuite/tests/simplCore/should_compile/T8832.stdout
testsuite/tests/simplCore/should_compile/T8832.stdout-ws-32
testsuite/tests/simplCore/should_compile/T9400.stderr
testsuite/tests/simplCore/should_compile/rule2.stderr
testsuite/tests/simplCore/should_compile/spec-inline.stderr
testsuite/tests/th/T3319.stderr
testsuite/tests/th/T3600.stderr
testsuite/tests/th/T5217.stderr
testsuite/tests/th/all.T
testsuite/tests/typecheck/should_compile/FD1.stderr
testsuite/tests/typecheck/should_compile/FD2.stderr
testsuite/tests/typecheck/should_compile/T3346.hs
testsuite/tests/typecheck/should_compile/T8474.hs
testsuite/tests/typecheck/should_compile/T9708.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/T9708.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs
testsuite/tests/typecheck/should_compile/all.T
testsuite/tests/typecheck/should_compile/tc231.hs
testsuite/tests/typecheck/should_compile/tc231.stderr
testsuite/tests/typecheck/should_fail/ContextStack2.hs
testsuite/tests/typecheck/should_fail/ContextStack2.stderr
testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr
testsuite/tests/typecheck/should_fail/T1899.stderr
testsuite/tests/typecheck/should_fail/T2688.stderr
testsuite/tests/typecheck/should_fail/T5236.stderr
testsuite/tests/typecheck/should_fail/T5300.stderr
testsuite/tests/typecheck/should_fail/T5684.stderr
testsuite/tests/typecheck/should_fail/T5853.stderr
testsuite/tests/typecheck/should_fail/T7453.stderr
testsuite/tests/typecheck/should_fail/T7748a.stderr
testsuite/tests/typecheck/should_fail/T8142.stderr
testsuite/tests/typecheck/should_fail/T8450.hs
testsuite/tests/typecheck/should_fail/T8450.stderr
testsuite/tests/typecheck/should_fail/T8883.stderr
testsuite/tests/typecheck/should_fail/T9305.stderr
testsuite/tests/typecheck/should_fail/mc21.stderr
testsuite/tests/typecheck/should_fail/mc22.stderr
testsuite/tests/typecheck/should_fail/mc25.stderr
testsuite/tests/typecheck/should_fail/tcfail019.stderr
testsuite/tests/typecheck/should_fail/tcfail067.stderr
testsuite/tests/typecheck/should_fail/tcfail068.hs
testsuite/tests/typecheck/should_fail/tcfail068.stderr
testsuite/tests/typecheck/should_fail/tcfail072.stderr
testsuite/tests/typecheck/should_fail/tcfail131.stderr
testsuite/tests/typecheck/should_fail/tcfail143.stderr
testsuite/tests/typecheck/should_fail/tcfail171.stderr
testsuite/tests/typecheck/should_fail/tcfail186.stderr
testsuite/tests/typecheck/should_fail/tcfail201.stderr
testsuite/tests/typecheck/should_fail/tcfail204.stderr
testsuite/tests/typecheck/should_run/T5751.hs
testsuite/tests/typecheck/should_run/tcrun036.hs

index ab58a4f..6b46454 100644 (file)
@@ -83,7 +83,6 @@ import Data.Bits
 import Data.Data
 import Data.List
 import Data.Ord
-import System.FilePath
 \end{code}
 
 %************************************************************************
@@ -191,15 +190,19 @@ cmpRealSrcLoc (SrcLoc s1 l1 c1) (SrcLoc s2 l2 c2)
 
 instance Outputable RealSrcLoc where
     ppr (SrcLoc src_path src_line src_col)
-      = getPprStyle $ \ sty ->
-        if userStyle sty || debugStyle sty then
-            hcat [ pprFastFilePath src_path, char ':',
-                   int src_line,
-                   char ':', int src_col
-                 ]
-        else
-            hcat [text "{-# LINE ", int src_line, space,
-                  char '\"', pprFastFilePath src_path, text " #-}"]
+      = hcat [ pprFastFilePath src_path <> colon
+             , int src_line <> colon
+             , int src_col ]
+
+-- I don't know why there is this style-based difference
+--        if userStyle sty || debugStyle sty then
+--            hcat [ pprFastFilePath src_path, char ':',
+--                   int src_line,
+--                   char ':', int src_col
+--                 ]
+--        else
+--            hcat [text "{-# LINE ", int src_line, space,
+--                  char '\"', pprFastFilePath src_path, text " #-}"]
 
 instance Outputable SrcLoc where
     ppr (RealSrcLoc l) = ppr l
@@ -432,50 +435,56 @@ instance Ord SrcSpan where
 
 
 instance Outputable RealSrcSpan where
-    ppr span
-      = getPprStyle $ \ sty ->
-        if userStyle sty || debugStyle sty then
-           text (showUserRealSpan True span)
-        else
-           hcat [text "{-# LINE ", int (srcSpanStartLine span), space,
-                 char '\"', pprFastFilePath $ srcSpanFile span, text " #-}"]
+    ppr span = pprUserRealSpan True span
+
+-- I don't know why there is this style-based difference
+--      = getPprStyle $ \ sty ->
+--        if userStyle sty || debugStyle sty then
+--           text (showUserRealSpan True span)
+--        else
+--           hcat [text "{-# LINE ", int (srcSpanStartLine span), space,
+--                 char '\"', pprFastFilePath $ srcSpanFile span, text " #-}"]
 
 instance Outputable SrcSpan where
-    ppr span
-      = getPprStyle $ \ sty ->
-        if userStyle sty || debugStyle sty then
-           pprUserSpan True span
-        else
-           case span of
-           UnhelpfulSpan _ -> panic "Outputable UnhelpfulSpan"
-           RealSrcSpan s -> ppr s
+    ppr span = pprUserSpan True span
 
-pprUserSpan :: Bool -> SrcSpan -> SDoc
-pprUserSpan _         (UnhelpfulSpan s) = ftext s
-pprUserSpan show_path (RealSrcSpan s)   = text (showUserRealSpan show_path s)
+-- I don't know why there is this style-based difference
+--      = getPprStyle $ \ sty ->
+--        if userStyle sty || debugStyle sty then
+--           pprUserSpan True span
+--        else
+--           case span of
+--           UnhelpfulSpan _ -> panic "Outputable UnhelpfulSpan"
+--           RealSrcSpan s -> ppr s
 
 showUserSpan :: Bool -> SrcSpan -> String
-showUserSpan _         (UnhelpfulSpan s) = unpackFS s
-showUserSpan show_path (RealSrcSpan s)   = showUserRealSpan show_path s
-
-showUserRealSpan :: Bool -> RealSrcSpan -> String
-showUserRealSpan show_path (SrcSpanOneLine src_path line start_col end_col)
-  = (if show_path then normalise (unpackFS src_path) ++ ":" else "")
- ++ show line ++ ":" ++ show start_col
- ++ (if end_col - start_col <= 1 then "" else '-' : show (end_col - 1))
+showUserSpan show_path span = showSDocSimple (pprUserSpan show_path span)
+
+pprUserSpan :: Bool -> SrcSpan -> SDoc
+pprUserSpan _         (UnhelpfulSpan s) = ftext s
+pprUserSpan show_path (RealSrcSpan s)   = pprUserRealSpan show_path s
+
+pprUserRealSpan :: Bool -> RealSrcSpan -> SDoc
+pprUserRealSpan show_path (SrcSpanOneLine src_path line start_col end_col)
+  = hcat [ ppWhen show_path (pprFastFilePath src_path <> colon)
+         , int line <> colon
+         , int start_col
+         , ppUnless (end_col - start_col <= 1) (char '-' <> int (end_col - 1)) ]
             -- For single-character or point spans, we just
             -- output the starting column number
 
-showUserRealSpan show_path (SrcSpanMultiLine src_path sline scol eline ecol)
-  = (if show_path then normalise (unpackFS src_path) ++ ":" else "")
- ++ "(" ++ show sline ++ "," ++ show scol ++ ")"
- ++ "-"
- ++ "(" ++ show eline ++ "," ++ show ecol' ++ ")"
-    where ecol' = if ecol == 0 then ecol else ecol - 1
-
-showUserRealSpan show_path (SrcSpanPoint src_path line col)
-  = (if show_path then normalise (unpackFS src_path) ++ ":" else "")
- ++ show line ++ ":" ++ show col
+pprUserRealSpan show_path (SrcSpanMultiLine src_path sline scol eline ecol)
+  = hcat [ ppWhen show_path (pprFastFilePath src_path <> colon)
+         , parens (int sline <> comma <> int scol)
+         , char '-'
+         , parens (int eline <> comma <> int ecol') ]
+ where
+   ecol' = if ecol == 0 then ecol else ecol - 1
+
+pprUserRealSpan show_path (SrcSpanPoint src_path line col)
+  = hcat [ ppWhen show_path (pprFastFilePath src_path <> colon)
+         , int line <> colon
+         , int col ]
 \end{code}
 
 %************************************************************************
index f7e5f67..62253c8 100644 (file)
@@ -206,16 +206,16 @@ After CoreTidy, top-level LocalIds are turned into GlobalIds
 
 \begin{code}
 instance Outputable Var where
-  ppr var = ppr (varName var) <+> ifPprDebug (brackets (ppr_debug var))
--- Printing the type on every occurrence is too much!
---            <+> if (not (gopt Opt_SuppressVarKinds dflags))
---                then ifPprDebug (text "::" <+> ppr (tyVarKind var) <+> text ")")
---                else empty
-
-ppr_debug :: Var -> SDoc
-ppr_debug (TyVar {})                           = ptext (sLit "tv")
-ppr_debug (TcTyVar {tc_tv_details = d})        = pprTcTyVarDetails d
-ppr_debug (Id { idScope = s, id_details = d }) = ppr_id_scope s <> pprIdDetails d
+  ppr var = ppr (varName var) <> getPprStyle (ppr_debug var)
+
+ppr_debug :: Var -> PprStyle -> SDoc
+ppr_debug (TyVar {}) sty 
+  | debugStyle sty = brackets (ptext (sLit "tv"))
+ppr_debug (TcTyVar {tc_tv_details = d}) sty
+  | dumpStyle sty || debugStyle sty = brackets (pprTcTyVarDetails d)
+ppr_debug (Id { idScope = s, id_details = d }) sty
+  | debugStyle sty = brackets (ppr_id_scope s <> pprIdDetails d)
+ppr_debug _ _ = empty
 
 ppr_id_scope :: IdScope -> SDoc
 ppr_id_scope GlobalId              = ptext (sLit "gid")
index bbf104b..6d79462 100644 (file)
@@ -21,7 +21,7 @@ import PrelNames
 import CoreUtils
 import CoreArity
 import CoreFVs
-import CoreMonad        ( endPass, CoreToDo(..) )
+import CoreMonad        ( endPassIO, CoreToDo(..) )
 import CoreSyn
 import CoreSubst
 import MkCore hiding( FloatBind(..) )   -- We use our own FloatBind here
@@ -172,7 +172,7 @@ corePrepPgm dflags hsc_env binds data_tycons = do
                       floats2 <- corePrepTopBinds initialCorePrepEnv implicit_binds
                       return (deFloatTop (floats1 `appendFloats` floats2))
 
-    endPass hsc_env CorePrep binds_out []
+    endPassIO hsc_env alwaysQualify CorePrep binds_out []
     return binds_out
 
 corePrepExpr :: DynFlags -> HscEnv -> CoreExpr -> IO CoreExpr
index 3160b35..0b4ac3c 100644 (file)
@@ -39,7 +39,7 @@ import Rules
 import TysPrim (eqReprPrimTyCon)
 import TysWiredIn (coercibleTyCon )
 import BasicTypes       ( Activation(.. ) )
-import CoreMonad        ( endPass, CoreToDo(..) )
+import CoreMonad        ( endPassIO, CoreToDo(..) )
 import MkCore
 import FastString
 import ErrUtils
@@ -94,6 +94,7 @@ deSugar hsc_env
                             tcg_hpc          = other_hpc_info })
 
   = do { let dflags = hsc_dflags hsc_env
+             print_unqual = mkPrintUnqualified dflags rdr_env
         ; showPass dflags "Desugar"
 
         -- Desugar the program
@@ -147,14 +148,14 @@ deSugar hsc_env
 
 #ifdef DEBUG
           -- Debug only as pre-simple-optimisation program may be really big
-        ; endPass hsc_env CoreDesugar final_pgm rules_for_imps
+        ; endPassIO hsc_env print_unqual CoreDesugar final_pgm rules_for_imps
 #endif
         ; (ds_binds, ds_rules_for_imps, ds_vects)
             <- simpleOptPgm dflags mod final_pgm rules_for_imps vects0
                          -- The simpleOptPgm gets rid of type
                          -- bindings plus any stupid dead code
 
-        ; endPass hsc_env CoreDesugarOpt ds_binds ds_rules_for_imps
+        ; endPassIO hsc_env print_unqual CoreDesugarOpt ds_binds ds_rules_for_imps
 
         ; let used_names = mkUsedNames tcg_env
         ; deps <- mkDependencies tcg_env
index 8c2541c..a3aac1b 100644 (file)
@@ -51,6 +51,7 @@ import Class
 import DataCon  ( dataConWorkId )
 import Name
 import MkId     ( seqId )
+import IdInfo   ( IdDetails(..) )
 import Var
 import VarSet
 import Rules
@@ -214,6 +215,9 @@ makeCorePair dflags gbl_id is_default_method dict_arity rhs
   | is_default_method                 -- Default methods are *always* inlined
   = (gbl_id `setIdUnfolding` mkCompulsoryUnfolding rhs, rhs)
 
+  | DFunId _ is_newtype <- idDetails gbl_id
+  = (mk_dfun_w_stuff is_newtype, rhs)
+
   | otherwise
   = case inlinePragmaSpec inline_prag of
           EmptyInlineSpec -> (gbl_id, rhs)
@@ -237,6 +241,22 @@ makeCorePair dflags gbl_id is_default_method dict_arity rhs
        = pprTrace "makeCorePair: arity missing" (ppr gbl_id) $
          (gbl_id `setIdUnfolding` mkInlineUnfolding Nothing rhs, rhs)
 
+                -- See Note [ClassOp/DFun selection] in TcInstDcls
+                -- See Note [Single-method classes]  in TcInstDcls
+    mk_dfun_w_stuff is_newtype
+       | is_newtype 
+       = gbl_id `setIdUnfolding`  mkInlineUnfolding (Just 0) rhs
+                `setInlinePragma` alwaysInlinePragma { inl_sat = Just 0 }
+       | otherwise
+       = gbl_id `setIdUnfolding`  mkDFunUnfolding dfun_bndrs dfun_constr dfun_args
+                `setInlinePragma` dfunInlinePragma
+    (dfun_bndrs, dfun_body) = collectBinders (simpleOptExpr rhs)
+    (dfun_con, dfun_args)   = collectArgs dfun_body
+    dfun_constr | Var id <- dfun_con
+                , DataConWorkId con <- idDetails id
+                = con
+                | otherwise = pprPanic "makeCorePair: dfun" (ppr rhs)
+
 
 dictArity :: [Var] -> Arity
 -- Don't count coercion variables in arity
index bd15329..26aad6f 100644 (file)
@@ -29,6 +29,7 @@ import Kind
 import GHC
 import Outputable
 import PprTyThing
+import ErrUtils
 import MonadUtils
 import DynFlags
 import Exception
index 0b69492..1f751d1 100644 (file)
@@ -596,7 +596,7 @@ liftTcM = id
 newVar :: Kind -> TR TcType
 newVar = liftTcM . newFlexiTyVarTy
 
-instTyVars :: [TyVar] -> TR ([TcTyVar], [TcType], TvSubst)
+instTyVars :: [TyVar] -> TR (TvSubst, [TcTyVar])
 -- Instantiate fresh mutable type variables from some TyVars
 -- This function preserves the print-name, which helps error messages
 instTyVars = liftTcM . tcInstTyVars
@@ -613,7 +613,7 @@ type RttiInstantiation = [(TcTyVar, TyVar)]
 --   mapping from new (instantiated) -to- old (skolem) type variables
 instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation)
 instScheme (tvs, ty)
-  = liftTcM $ do { (tvs', _, subst) <- tcInstTyVars tvs
+  = liftTcM $ do { (subst, tvs') <- tcInstTyVars tvs
                  ; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs]
                  ; return (substTy subst ty, rtti_inst) }
 
@@ -950,7 +950,7 @@ getDataConArgTys dc con_app_ty
   = do { let UnaryRep rep_con_app_ty = repType con_app_ty
        ; traceTR (text "getDataConArgTys 1" <+> (ppr con_app_ty $$ ppr rep_con_app_ty
                    $$ ppr (tcSplitTyConApp_maybe rep_con_app_ty)))
-       ; (_, _, subst) <- instTyVars (univ_tvs ++ ex_tvs)
+       ; (subst, _) <- instTyVars (univ_tvs ++ ex_tvs)
        ; addConstraint rep_con_app_ty (substTy subst (dataConOrigResTy dc))
               -- See Note [Constructor arg types]
        ; let con_arg_tys = substTys subst (dataConRepArgTys dc)
@@ -1183,8 +1183,8 @@ congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
             | otherwise = do
                traceTR (text "(Upgrade) upgraded " <> ppr ty <>
                         text " in presence of newtype evidence " <> ppr new_tycon)
-               (_, vars, _) <- instTyVars (tyConTyVars new_tycon)
-               let ty' = mkTyConApp new_tycon vars
+               (_, vars) <- instTyVars (tyConTyVars new_tycon)
+               let ty' = mkTyConApp new_tycon (mkTyVarTys vars)
                    UnaryRep rep_ty = repType ty'
                _ <- liftTcM (unifyType ty rep_ty)
         -- assumes that reptype doesn't ^^^^ touch tyconApp args
index 7ae04ee..8f63cef 100644 (file)
@@ -51,8 +51,6 @@ module DynFlags (
         dynFlagDependencies,
         tablesNextToCode, mkTablesNextToCode,
 
-        printOutputForUser, printInfoForUser,
-
         Way(..), mkBuildTag, wayRTSOnly, addWay', updateWays,
         wayGeneralFlags, wayUnsetGeneralFlags,
 
@@ -1542,16 +1540,6 @@ newtype FlushErr = FlushErr (IO ())
 defaultFlushErr :: FlushErr
 defaultFlushErr = FlushErr $ hFlush stderr
 
-printOutputForUser :: DynFlags -> PrintUnqualified -> SDoc -> IO ()
-printOutputForUser = printSevForUser SevOutput
-
-printInfoForUser :: DynFlags -> PrintUnqualified -> SDoc -> IO ()
-printInfoForUser = printSevForUser SevInfo
-
-printSevForUser :: Severity -> DynFlags -> PrintUnqualified -> SDoc -> IO ()
-printSevForUser sev dflags unqual doc
-    = log_action dflags dflags sev noSrcSpan (mkUserStyle unqual AllTheWay) doc
-
 {-
 Note [Verbosity levels]
 ~~~~~~~~~~~~~~~~~~~~~~~
index c43064e..8a47639 100644 (file)
@@ -27,7 +27,8 @@ module ErrUtils (
         mkDumpDoc, dumpSDoc,
 
         --  * Messages during compilation
-        putMsg, putMsgWith,
+        putMsg, printInfoForUser, printOutputForUser,
+        logInfo, logOutput,
         errorMsg,
         fatalErrorMsg, fatalErrorMsg', fatalErrorMsg'',
         compilationProgressMsg,
@@ -237,7 +238,7 @@ dumpIfSet dflags flag hdr doc
 dumpIfSet_dyn :: DynFlags -> DumpFlag -> String -> SDoc -> IO ()
 dumpIfSet_dyn dflags flag hdr doc
   | dopt flag dflags
-  = dumpSDoc dflags flag hdr doc
+  = dumpSDoc dflags alwaysQualify flag hdr doc
   | otherwise
   = return ()
 
@@ -254,12 +255,13 @@ mkDumpDoc hdr doc
 -- | Write out a dump.
 --      If --dump-to-file is set then this goes to a file.
 --      otherwise emit to stdout.
--- 
+--
 -- When hdr is empty, we print in a more compact format (no separators and
 -- blank lines)
-dumpSDoc :: DynFlags -> DumpFlag -> String -> SDoc -> IO ()
-dumpSDoc dflags flag hdr doc
+dumpSDoc :: DynFlags -> PrintUnqualified -> DumpFlag -> String -> SDoc -> IO ()
+dumpSDoc dflags print_unqual flag hdr doc
  = do let mFile = chooseDumpFile dflags flag
+          dump_style = mkDumpStyle print_unqual
       case mFile of
             Just fileName
                  -> do
@@ -278,7 +280,7 @@ dumpSDoc dflags flag hdr doc
                                              $$ blankLine
                                              $$ doc
                                         return $ mkDumpDoc hdr d
-                        defaultLogActionHPrintDoc dflags handle doc' defaultDumpStyle
+                        defaultLogActionHPrintDoc dflags handle doc' dump_style
                         hClose handle
 
             -- write the dump to stdout
@@ -286,7 +288,7 @@ dumpSDoc dflags flag hdr doc
               let (doc', severity)
                     | null hdr  = (doc, SevOutput)
                     | otherwise = (mkDumpDoc hdr doc, SevDump)
-              log_action dflags dflags severity noSrcSpan defaultDumpStyle doc'
+              log_action dflags dflags severity noSrcSpan dump_style doc'
 
 
 -- | Choose where to put a dump file based on DynFlags
@@ -340,18 +342,9 @@ ifVerbose dflags val act
   | verbosity dflags >= val = act
   | otherwise               = return ()
 
-putMsg :: DynFlags -> MsgDoc -> IO ()
-putMsg dflags msg = log_action dflags dflags SevInfo noSrcSpan defaultUserStyle msg
-
-putMsgWith :: DynFlags -> PrintUnqualified -> MsgDoc -> IO ()
-putMsgWith dflags print_unqual msg
-  = log_action dflags dflags SevInfo noSrcSpan sty msg
-  where
-    sty = mkUserStyle print_unqual AllTheWay
-
 errorMsg :: DynFlags -> MsgDoc -> IO ()
-errorMsg dflags msg =
-    log_action dflags dflags SevError noSrcSpan (defaultErrStyle dflags) msg
+errorMsg dflags msg
+   = log_action dflags dflags SevError noSrcSpan (defaultErrStyle dflags) msg
 
 fatalErrorMsg :: DynFlags -> MsgDoc -> IO ()
 fatalErrorMsg dflags msg = fatalErrorMsg' (log_action dflags) dflags msg
@@ -365,25 +358,45 @@ fatalErrorMsg'' fm msg = fm msg
 
 compilationProgressMsg :: DynFlags -> String -> IO ()
 compilationProgressMsg dflags msg
-  = ifVerbose dflags 1 (log_action dflags dflags SevOutput noSrcSpan defaultUserStyle (text msg))
+  = ifVerbose dflags 1 $
+    logOutput dflags defaultUserStyle (text msg)
 
 showPass :: DynFlags -> String -> IO ()
 showPass dflags what
-  = ifVerbose dflags 2 (log_action dflags dflags SevInfo noSrcSpan defaultUserStyle (text "***" <+> text what <> colon))
+  = ifVerbose dflags 2 $
+    logInfo dflags defaultUserStyle (text "***" <+> text what <> colon)
 
 debugTraceMsg :: DynFlags -> Int -> MsgDoc -> IO ()
-debugTraceMsg dflags val msg
-  = ifVerbose dflags val (log_action dflags dflags SevInfo noSrcSpan defaultDumpStyle msg)
+debugTraceMsg dflags val msg = ifVerbose dflags val $
+                               logInfo dflags defaultDumpStyle msg
+
+putMsg :: DynFlags -> MsgDoc -> IO ()
+putMsg dflags msg = logInfo dflags defaultUserStyle msg
+
+printInfoForUser :: DynFlags -> PrintUnqualified -> MsgDoc -> IO ()
+printInfoForUser dflags print_unqual msg
+  = logInfo dflags (mkUserStyle print_unqual AllTheWay) msg
+
+printOutputForUser :: DynFlags -> PrintUnqualified -> MsgDoc -> IO ()
+printOutputForUser dflags print_unqual msg
+  = logOutput dflags (mkUserStyle print_unqual AllTheWay) msg
+
+logInfo :: DynFlags -> PprStyle -> MsgDoc -> IO ()
+logInfo dflags sty msg = log_action dflags dflags SevInfo noSrcSpan sty msg
+
+logOutput :: DynFlags -> PprStyle -> MsgDoc -> IO ()
+-- Like logInfo but with SevOutput rather then SevInfo
+logOutput dflags sty msg = log_action dflags dflags SevOutput noSrcSpan sty msg
 
 prettyPrintGhcErrors :: ExceptionMonad m => DynFlags -> m a -> m a
 prettyPrintGhcErrors dflags
     = ghandle $ \e -> case e of
                       PprPanic str doc ->
-                          pprDebugAndThen dflags panic str doc
+                          pprDebugAndThen dflags panic (text str) doc
                       PprSorry str doc ->
-                          pprDebugAndThen dflags sorry str doc
+                          pprDebugAndThen dflags sorry (text str) doc
                       PprProgramError str doc ->
-                          pprDebugAndThen dflags pgmError str doc
+                          pprDebugAndThen dflags pgmError (text str) doc
                       _ ->
                           liftIO $ throwIO e
 \end{code}
index eed4671..240e63b 100644 (file)
@@ -128,7 +128,7 @@ pprTyThingInContextLoc tyThing
 ------------------------
 ppr_ty_thing :: Bool -> [OccName] -> TyThing -> SDoc
 -- We pretty-print 'TyThing' via 'IfaceDecl'
--- See Note [Pretty-pringint TyThings]
+-- See Note [Pretty-printing TyThings]
 ppr_ty_thing hdr_only path ty_thing
   = pprIfaceDecl ss (tyThingToIfaceDecl ty_thing)
   where
index 55efca1..abe167d 100644 (file)
@@ -138,7 +138,7 @@ mkBootModDetailsTc hsc_env
                   tcg_fam_insts = fam_insts
                 }
   = do  { let dflags = hsc_dflags hsc_env
-        ; showPass dflags CoreTidy
+        ; showPassIO dflags CoreTidy
 
         ; let { insts'      = map (tidyClsInstDFun globaliseAndTidyId) insts
               ; type_env1  = mkBootTypeEnv (availsToNameSet exports)
@@ -299,6 +299,7 @@ RHSs, so that they print nicely in interfaces.
 tidyProgram :: HscEnv -> ModGuts -> IO (CgGuts, ModDetails)
 tidyProgram hsc_env  (ModGuts { mg_module    = mod
                               , mg_exports   = exports
+                              , mg_rdr_env   = rdr_env
                               , mg_tcs       = tcs
                               , mg_insts     = insts
                               , mg_fam_insts = fam_insts
@@ -316,8 +317,9 @@ tidyProgram hsc_env  (ModGuts { mg_module    = mod
   = do  { let { dflags     = hsc_dflags hsc_env
               ; omit_prags = gopt Opt_OmitInterfacePragmas dflags
               ; expose_all = gopt Opt_ExposeAllUnfoldings  dflags
+              ; print_unqual = mkPrintUnqualified dflags rdr_env
               }
-        ; showPass dflags CoreTidy
+        ; showPassIO dflags CoreTidy
 
         ; let { type_env = typeEnvFromEntities [] tcs fam_insts
 
@@ -375,7 +377,7 @@ tidyProgram hsc_env  (ModGuts { mg_module    = mod
               ; alg_tycons = filter isAlgTyCon (typeEnvTyCons type_env)
               }
 
-        ; endPass hsc_env CoreTidy all_tidy_binds tidy_rules
+        ; endPassIO hsc_env print_unqual CoreTidy all_tidy_binds tidy_rules
 
           -- If the endPass didn't print the rules, but ddump-rules is
           -- on, print now
index 5b4a517..56c18ea 100644 (file)
@@ -316,8 +316,7 @@ finishNativeGen dflags ncgImpl bufh@(BufHandle _ _ h) (imports, prof)
                         $ [ Color.raGraph stat
                                 | stat@Color.RegAllocStatsStart{} <- stats]
 
-                dumpSDoc dflags Opt_D_dump_asm_stats "NCG stats"
-                        $ Color.pprStats stats graphGlobal
+                dump_stats (Color.pprStats stats graphGlobal)
 
                 dumpIfSet_dyn dflags
                         Opt_D_dump_asm_conflicts "Register conflict graph"
@@ -332,13 +331,14 @@ finishNativeGen dflags ncgImpl bufh@(BufHandle _ _ h) (imports, prof)
         -- dump global NCG stats for linear allocator
         (case concat $ catMaybes linearStats of
                 []      -> return ()
-                stats   -> dumpSDoc dflags Opt_D_dump_asm_stats "NCG stats"
-                                $ Linear.pprStats (concat native) stats)
+                stats   -> dump_stats (Linear.pprStats (concat native) stats))
 
         -- write out the imports
         Pretty.printDoc Pretty.LeftMode (pprCols dflags) h
                 $ withPprStyleDoc dflags (mkCodeStyle AsmStyle)
                 $ makeImportsDoc dflags (concat imports)
+  where
+    dump_stats = dumpSDoc dflags alwaysQualify Opt_D_dump_asm_stats "NCG stats"
 
 cmmNativeGenStream :: (Outputable statics, Outputable instr, Instruction instr)
               => DynFlags
index 8d2d3bf..3405f52 100644 (file)
@@ -28,6 +28,7 @@ module CoreMonad (
     -- ** Reading from the monad
     getHscEnv, getRuleBase, getModule,
     getDynFlags, getOrigNameCache, getPackageFamInstEnv,
+    getPrintUnqualified,
 
     -- ** Writing to the monad
     addSimplCount,
@@ -43,7 +44,7 @@ module CoreMonad (
     getAnnotations, getFirstAnnotations,
 
     -- ** Debug output
-    showPass, endPass, dumpPassResult, lintPassResult,
+    showPass, showPassIO, endPass, endPassIO, dumpPassResult, lintPassResult,
     lintInteractiveExpr, dumpIfSet,
 
     -- ** Screen output
@@ -132,15 +133,28 @@ be, and it makes a conveneint place.  place for them.  They print out
 stuff before and after core passes, and do Core Lint when necessary.
 
 \begin{code}
-showPass :: DynFlags -> CoreToDo -> IO ()
-showPass dflags pass = Err.showPass dflags (showPpr dflags pass)
-
-endPass :: HscEnv -> CoreToDo -> CoreProgram -> [CoreRule] -> IO ()
-endPass hsc_env pass binds rules
-  = do { dumpPassResult dflags mb_flag (ppr pass) (pprPassDetails pass) binds rules
+showPass :: CoreToDo -> CoreM ()
+showPass pass = do { dflags <- getDynFlags
+                   ; liftIO $ showPassIO dflags pass }
+
+showPassIO :: DynFlags -> CoreToDo -> IO ()
+showPassIO dflags pass = Err.showPass dflags (showPpr dflags pass)
+
+endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> CoreM ()
+endPass pass binds rules
+  = do { hsc_env <- getHscEnv
+       ; print_unqual <- getPrintUnqualified
+       ; liftIO $ endPassIO hsc_env print_unqual pass binds rules }
+
+endPassIO :: HscEnv -> PrintUnqualified
+          -> CoreToDo -> CoreProgram -> [CoreRule] -> IO ()
+-- Used by the IO-is CorePrep too
+endPassIO hsc_env print_unqual pass binds rules
+  = do { dumpPassResult dflags print_unqual mb_flag
+                        (ppr pass) (pprPassDetails pass) binds rules
        ; lintPassResult hsc_env pass binds }
   where
-    dflags = hsc_dflags hsc_env
+    dflags  = hsc_dflags hsc_env
     mb_flag = case coreDumpFlag pass of
                 Just flag | dopt flag dflags                    -> Just flag
                           | dopt Opt_D_verbose_core2core dflags -> Just flag
@@ -151,15 +165,16 @@ dumpIfSet dflags dump_me pass extra_info doc
   = Err.dumpIfSet dflags dump_me (showSDoc dflags (ppr pass <+> extra_info)) doc
 
 dumpPassResult :: DynFlags
-               -> Maybe DumpFlag                -- Just df => show details in a file whose
+               -> PrintUnqualified
+               -> Maybe DumpFlag        -- Just df => show details in a file whose
                                         --            name is specified by df
                -> SDoc                  -- Header
                -> SDoc                  -- Extra info to appear after header
                -> CoreProgram -> [CoreRule]
                -> IO ()
-dumpPassResult dflags mb_flag hdr extra_info binds rules
+dumpPassResult dflags unqual mb_flag hdr extra_info binds rules
   | Just flag <- mb_flag
-  = Err.dumpSDoc dflags flag (showSDoc dflags hdr) dump_doc
+  = Err.dumpSDoc dflags unqual flag (showSDoc dflags hdr) dump_doc
 
   | otherwise
   = Err.debugTraceMsg dflags 2 size_doc
@@ -781,6 +796,7 @@ data CoreReader = CoreReader {
         cr_hsc_env :: HscEnv,
         cr_rule_base :: RuleBase,
         cr_module :: Module,
+        cr_print_unqual :: PrintUnqualified,
 #ifdef GHCI
         cr_globals :: (MVar PersistentLinkerState, Bool)
 #else
@@ -854,9 +870,10 @@ runCoreM :: HscEnv
          -> RuleBase
          -> UniqSupply
          -> Module
+         -> PrintUnqualified
          -> CoreM a
          -> IO (a, SimplCount)
-runCoreM hsc_env rule_base us mod m = do
+runCoreM hsc_env rule_base us mod print_unqual m = do
         glbls <- saveLinkerGlobals
         liftM extract $ runIOEnv (reader glbls) $ unCoreM m state
   where
@@ -864,7 +881,8 @@ runCoreM hsc_env rule_base us mod m = do
             cr_hsc_env = hsc_env,
             cr_rule_base = rule_base,
             cr_module = mod,
-            cr_globals = glbls
+            cr_globals = glbls,
+            cr_print_unqual = print_unqual
         }
     state = CoreState {
             cs_uniq_supply = us
@@ -934,6 +952,9 @@ getHscEnv = read cr_hsc_env
 getRuleBase :: CoreM RuleBase
 getRuleBase = read cr_rule_base
 
+getPrintUnqualified :: CoreM PrintUnqualified
+getPrintUnqualified = read cr_print_unqual
+
 addSimplCount :: SimplCount -> CoreM ()
 addSimplCount count = write (CoreWriter { cw_simpl_count = count })
 
index 2a70dcf..8908cb3 100644 (file)
@@ -76,9 +76,9 @@ core2core hsc_env guts
 
        ; let builtin_passes = getCoreToDo dflags
        ;
-       ; (guts2, stats) <- runCoreM hsc_env hpt_rule_base us mod $
-                        do { all_passes <- addPluginPasses dflags builtin_passes
-                           ; runCorePasses all_passes guts }
+       ; (guts2, stats) <- runCoreM hsc_env hpt_rule_base us mod print_unqual $
+                           do { all_passes <- addPluginPasses dflags builtin_passes
+                              ; runCorePasses all_passes guts }
 
 {--
        ; Err.dumpIfSet_dyn dflags Opt_D_dump_core_pipeline
@@ -99,6 +99,7 @@ core2core hsc_env guts
     -- consume the ModGuts to find the module) but somewhat ugly because mg_module may
     -- _theoretically_ be changed during the Core pipeline (it's part of ModGuts), which
     -- would mean our cached value would go out of date.
+    print_unqual = mkPrintUnqualified dflags (mg_rdr_env guts)
 \end{code}
 
 
@@ -384,11 +385,9 @@ runCorePasses passes guts
     do_pass guts CoreDoNothing = return guts
     do_pass guts (CoreDoPasses ps) = runCorePasses ps guts
     do_pass guts pass
-       = do { hsc_env <- getHscEnv
-            ; let dflags = hsc_dflags hsc_env
-            ; liftIO $ showPass dflags pass
+       = do { showPass pass
             ; guts' <- doCorePass pass guts
-            ; liftIO $ endPass hsc_env pass (mg_binds guts') (mg_rules guts')
+            ; endPass pass (mg_binds guts') (mg_rules guts')
             ; return guts' }
 
 doCorePass :: CoreToDo -> ModGuts -> CoreM ModGuts
@@ -596,6 +595,7 @@ simplifyPgmIO :: CoreToDo
 simplifyPgmIO pass@(CoreDoSimplify max_iterations mode)
               hsc_env us hpt_rule_base
               guts@(ModGuts { mg_module = this_mod
+                            , mg_rdr_env = rdr_env
                             , mg_binds = binds, mg_rules = rules
                             , mg_fam_inst_env = fam_inst_env })
   = do { (termination_msg, it_count, counts_out, guts')
@@ -610,10 +610,11 @@ simplifyPgmIO pass@(CoreDoSimplify max_iterations mode)
         ; return (counts_out, guts')
     }
   where
-    dflags      = hsc_dflags hsc_env
-    dump_phase  = dumpSimplPhase dflags mode
-    simpl_env   = mkSimplEnv mode
-    active_rule = activeRule simpl_env
+    dflags       = hsc_dflags hsc_env
+    print_unqual = mkPrintUnqualified dflags rdr_env
+    dump_phase   = dumpSimplPhase dflags mode
+    simpl_env    = mkSimplEnv mode
+    active_rule  = activeRule simpl_env
 
     do_iteration :: UniqSupply
                  -> Int          -- Counts iterations
@@ -709,7 +710,7 @@ simplifyPgmIO pass@(CoreDoSimplify max_iterations mode)
            let { binds2 = {-# SCC "ZapInd" #-} shortOutIndirections binds1 } ;
 
                 -- Dump the result of this iteration
-           dump_end_iteration dflags iteration_no counts1 binds2 rules1 ;
+           dump_end_iteration dflags print_unqual iteration_no counts1 binds2 rules1 ;
            lintPassResult hsc_env pass binds2 ;
 
                 -- Loop
@@ -727,10 +728,10 @@ simplifyPgmIO pass@(CoreDoSimplify max_iterations mode)
 simplifyPgmIO _ _ _ _ _ = panic "simplifyPgmIO"
 
 -------------------
-dump_end_iteration :: DynFlags -> Int
-             -> SimplCount -> CoreProgram -> [CoreRule] -> IO ()
-dump_end_iteration dflags iteration_no counts binds rules
-  = dumpPassResult dflags mb_flag hdr pp_counts binds rules
+dump_end_iteration :: DynFlags -> PrintUnqualified -> Int
+                   -> SimplCount -> CoreProgram -> [CoreRule] -> IO ()
+dump_end_iteration dflags print_unqual iteration_no counts binds rules
+  = dumpPassResult dflags print_unqual mb_flag hdr pp_counts binds rules
   where
     mb_flag | dopt Opt_D_dump_simpl_iterations dflags = Just Opt_D_dump_simpl_phases
             | otherwise                               = Nothing
index 6a90883..e5561b2 100644 (file)
@@ -29,6 +29,7 @@ import CoreMonad
 import Outputable
 import FastString
 import MonadUtils
+import ErrUtils
 import Control.Monad       ( when, liftM, ap )
 \end{code}
 
index f044be5..cc55529 100644 (file)
@@ -1615,8 +1615,9 @@ tryRules env rules fn args call_cont
       | otherwise
       = return ()
 
-    log_rule dflags flag hdr details = liftIO . dumpSDoc dflags flag "" $
-      sep [text hdr, nest 4 details]
+    log_rule dflags flag hdr details
+      = liftIO . dumpSDoc dflags alwaysQualify flag "" $
+                   sep [text hdr, nest 4 details]
 \end{code}
 
 Note [Optimising tagToEnum#]
index 016dc08..08b7e9d 100644 (file)
@@ -56,21 +56,17 @@ newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst
 -- Called from the vectoriser monad too, hence the rather general type
 newFamInst flavor axiom@(CoAxiom { co_ax_branches = FirstBranch branch
                                  , co_ax_tc = fam_tc })
-  = do { (subst, tvs') <- tcInstSigTyVarsLoc loc tvs
-       ; return (FamInst { fi_fam      = fam_tc_name
+  | CoAxBranch { cab_tvs = tvs
+               , cab_lhs = lhs
+               , cab_rhs = rhs } <- branch
+  = do { (subst, tvs') <- freshenTyVarBndrs tvs
+       ; return (FamInst { fi_fam      = tyConName fam_tc
                          , fi_flavor   = flavor
                          , fi_tcs      = roughMatchTcs lhs
                          , fi_tvs      = tvs'
                          , fi_tys      = substTys subst lhs
                          , fi_rhs      = substTy  subst rhs
                          , fi_axiom    = axiom }) }
-  where
-    fam_tc_name = tyConName fam_tc
-    CoAxBranch { cab_loc = loc
-               , cab_tvs = tvs
-               , cab_lhs = lhs
-               , cab_rhs = rhs } = branch
-
 \end{code}
 
 
diff --git a/compiler/typecheck/Flattening-notes b/compiler/typecheck/Flattening-notes
new file mode 100644 (file)
index 0000000..bc56d28
--- /dev/null
@@ -0,0 +1,635 @@
+ToDo:
+
+* get rid of getEvTerm?
+
+* ctev_loc should have a decent name ctEvLoc
+
+* Float only CTyEqCans.   kind-incompatible things should be CNonCanonical,
+  so they won't float and generate a duplicate kind-unify message
+
+  Then we can stop disabling floating when there are insolubles,
+  and that will improve mc21 etc
+
+* Note [Do not add duplicate derived isols]
+  This mostly doesn't apply now, except for the fundeps
+
+* No need to zonk now we are unflattening
+
+* TcInteract, Note [Efficient orientation]?
+
+* inert_funeqs, inert_eqs: keep only the CtEvidence.
+   They are all CFunEqCans, CTyEqCans
+
+* Update Note [Preparing inert set for implications]
+* remove/rewrite TcMType Note [Unflattening while zonking]
+
+* Consider individual data tpyes for CFunEqCan etc
+
+Remaining errors
+============================
+Unexpected failures:
+   generics                      GenDerivOutput1_1 [stderr mismatch] (normal)
+
+ghcirun002: internal error: ASSERTION FAILED: file rts/Interpreter.c, line 773
+   ghci/should_run               ghcirun002 [bad exit code] (ghci)
+
+-package dependencies: array-0.5.0.1@array_GX4NwjS8xZkC2ZPtjgwhnz
++package dependencies: array-0.5.0.1 base-4.8.0.0
+   safeHaskell/check/pkg01       safePkg01 [bad stdout] (normal)
+
+
+Wierd looking pattern synonym thing
+   ghci/scripts                       T8776 [bad stdout] (ghci)
+   patsyn/should_fail                 mono [stderr mismatch] (normal)
+
+Derived equalities   fmv1 ~ Maybe a, fmv2 ~ Maybe b
+   indexed-types/should_fail     T4093a [stderr mismatch] (normal)
+
+Not sure
+   indexed-types/should_fail     ExtraTcsUntch [stderr mismatch] (normal)
+
+Order of finding iprovements
+   typecheck/should_compile      TcTypeNatSimple [exit code non-0] (normal)
+
+
+
+-----------------
+Unflattening
+~~~~~~~~~~~~
+
+    [W] G a ~ Int
+    [W] F (G a) ~ G a
+
+do not want to end up with 
+    [W} F Int ~ Int
+because that might actually hold!  Better to end up with the two above
+unsolved constraints.  The flat form will be
+
+    G a ~ fuv1     (CFunEqCan)
+    F fuv1 ~ fuv2  (CFunEqCan)
+    fuv1 ~ Int     (CTyEqCan)
+    fuv1 ~ fuv2    (CTyEqCan)
+
+Flatten using the fun-eqs first.
+
+
+Another example:
+    [W] F a ~ alpha
+flattens to
+    [W] F a ~ fuv   (CFunEqCan)
+    [W] fuv ~ alpha (CTyEqCan)    
+We must solve both!
+
+----------------------
+Outer given is rewritten by an inner given, then there must have been an inner given equality, hence the “given-eq” flag will be true anyway.
+
+Inner given rewritten by outer, retains its level (ie. The inner one)
+
+--------------------
+Try: rewrite wanted with wanted only for fuvs (not all meta-tyvars)
+
+But:   fuv ~ alpha[0]
+       alpha[0] ~ fuv’
+Now we don’t see that fuv ~ fuv’, which is a problem for injectivity detection.
+
+Conclusion: rewrite watneds with wanted for all untouchables.
+
+skol ~ untch, must re-orieint to untch ~ skol, so that we can use it to rewrite.
+
+
+--------------
+f :: [a] -> [b] -> blah
+f (e1 :: F Int) (e2 :: F Int)
+
+we get
+   F Int ~ fuv
+   fuv ~ [alpha]
+   fuv ~ [beta]
+
+We want: alpha := beta (which might unlock something else).  So rewriting wanted with wanted helps here.
+
+
+-----------------------------------
+indexed-types/should_fail/T4093a
+
+Is this type ambiguous:  (Foo e ~ Maybe e) => Foo e
+
+ [G] Foo e ~ Maybe e
+ [W] Foo e ~ Foo ee
+ [W] Foo ee ~ Maybe ee)
+---
+ [G] Foo e ~ fsk
+ [G] fsk ~ Maybe e
+
+ [W] Foo e ~ fmv1
+ [W] Foo ee ~ fmv2
+ [W] fmv1 ~ fmv2
+ [W] fmv2 ~ Maybe ee
+
+--->   fmv1 := fsk
+ [W] Foo ee ~ fmv2
+ [W] fsk ~ fmv2
+ [W] fmv2 ~ Maybe ee
+
+--->
+ [W] Foo ee ~ fmv2
+ [W] fmv2 ~ Maybe e
+ [W] fmv2 ~ Maybe ee
+
+Now maybe we shuld get [D] e ~ ee, and then we'd solve it entirely.
+But if in a smilar situation we got [D] Int ~ Bool we'd be back
+to complaining about wanted/wanted interactions.  This must arise
+also for fundeps.
+
+----------------------------------------
+indexed-types/should_compile/T44984
+
+  [W] H (F Bool) ~ H alpha
+  [W] alpha ~ F Bool
+-->
+  F Bool  ~ fuv0
+  H fuv0  ~ fuv1
+  H alpha ~ fuv2
+
+  fuv1 ~ fuv2
+  fuv0 ~ alpha
+
+flatten
+~~~~~~~
+  fuv0  := F Bool
+  fuv1  := H (F Bool)
+  fuv2  := H alpha
+  alpha := F Bool
+plus
+  fuv1 ~ fuv2
+
+But these two are equal under the above assumptions.
+Solve by Refl.
+
+
+--- under plan B, namely solve fuv1:=fuv2 eagerly ---
+  [W] H (F Bool) ~ H alpha
+  [W] alpha ~ F Bool
+-->
+  F Bool  ~ fuv0
+  H fuv0  ~ fuv1
+  H alpha ~ fuv2
+
+  fuv1 ~ fuv2
+  fuv0 ~ alpha
+-->
+  F Bool  ~ fuv0   
+  H fuv0  ~ fuv1
+  H alpha ~ fuv2    fuv2 := fuv1
+
+  fuv0 ~ alpha
+
+flatten
+  fuv0 := F Bool
+  fuv1 := H fuv0 = H (F Bool)
+  retain   H alpha ~ fuv2
+    because fuv2 has been filled
+  alpha := F Bool
+
+
+----------------------------
+indexed-types/should_failt/T4179
+
+after solving
+  [W] fuv_1 ~ fuv_2
+  [W] A3 (FCon x)           ~ fuv_1    (CFunEqCan)
+  [W] A3 (x (aoa -> fuv_2)) ~ fuv_2    (CFunEqCan)
+
+----------------------------------------
+indexed-types/should_fail/T7729a
+
+a)  [W]   BasePrimMonad (Rand m) ~ m1
+b)  [W]   tt m1 ~ BasePrimMonad (Rand m)
+
+--->  process (b) first
+    BasePrimMonad (Ramd m) ~ fuv_atH
+    fuv_atH ~ tt m1
+  
+--->  now process (a)
+    m1 ~ s_atH ~ tt m1    -- An obscure occurs check
+
+
+----------------------------------------
+typecheck/TcTypeNatSimple
+
+Original constraint
+  [W] x + y ~ x + alpha  (non-canonical)
+==>
+  [W] x + y     ~ fuv1   (CFunEqCan)
+  [W] x + alpha ~ fuv2   (CFuneqCan)
+  [W] fuv1 ~ fuv2        (CTyEqCan)
+
+(sigh)
+
+----------------------------------------
+indexed-types/should_fail/GADTwrong1
+
+  [G] Const a ~ ()
+==> flatten
+  [G] fsk ~ ()
+  work item: Const a ~ fsk
+==> fire top rule
+  [G] fsk ~ ()
+  work item fsk ~ ()
+
+Surely the work item should rewrite to () ~ ()?  Well, maybe not;
+it'a very special case.  More generally, our givens look like 
+F a ~ Int, where (F a) is not reducible.
+
+----------------------------------------
+indexed_types/should_fail/T7786
+
+  BuriedUnder sub k Empty ~ fsk _ajP
+  Intersect fsk_ajP inv ~ s_aJM
+  xxx[1] ~ s_aJM
+  forall . (xxx ~ Empty 
+         => Intersect (BuriedUnder sub k Empty) inv ~ Empty
+
+Conclusion: unflatten before solving nested implications
+
+----------------------------------------
+indexed_types/should_fail/T8227:
+
+Why using a different can-rewrite rule in CFunEqCan heads
+does not work.
+
+Assuming NOT rewriting wanteds with wanteds
+
+   Inert: [W] fsk_aBh ~ fuv_aBk -> fuv_aBk
+          [W] fuv_aBk ~ fsk_aBh
+
+          [G] Scalar fsk_aBg ~ fsk_aBh
+          [G] V a ~ f_aBg
+
+   Worklist includes  [W] Scalar fuv_aBi ~ fuv_aBk
+   fuv_aBi, fuv_aBk are flatten unificaiton variables
+
+   Work item: [W] V fsk_aBh ~ fuv_aBi
+
+Note that the inert wanteds are cyclic, because we do not rewrite
+wanteds with wanteds.
+
+
+Then we go into a loop when normalise the work-item, because we
+use rewriteOrSame on the argument of V.
+
+Conclusion: Don't make canRewrite context specific; instead use 
+[W] a ~ ty to rewrite a wanted iff 'a' is a unification variable.
+
+
+----------------------------------------
+IndTypesPerfMerge is interesting
+
+From the ambiguity check for 
+  f :: (F a ~ a) => a
+we get:
+      [G] F a ~ a
+      [W] F alpha ~ alpha, alpha ~ a
+
+    From Givens we get
+      [G] F a ~ fsk, fsk ~ a
+
+    Now if we flatten we get
+      [W] alpha ~ fuv, F alpha ~ fuv, alpha ~ a
+
+    Now, processing the first one first, choosing alpha := fuv
+      [W] F fuv ~ fuv, fuv ~ a
+
+    And now we are stuck.  We must either *unify* fuv := a, or
+    use the fuv ~ a to rewrite F fuv ~ fuv, so we can make it
+    meet up with the given F a ~ blah.
+
+Here is a somewhat similar case:
+
+   type family G a :: *
+
+   blah :: (G a ~ Bool, Eq (G a)) => a -> a
+   blah = error "urk"
+
+   foo x = blah x
+
+For foo we get
+   [W] Eq (G a), G a ~ Bool
+Flattening
+   [W] G a ~ fuv, Eq fuv, fuv ~ Bool
+We can't simplify away the Eq Bool unless we substitute for 
+Maybe that doesn't matter: we would still be left with unsolved
+G a ~ Bool.
+
+--------------------------
+Trac #9318 has a very simple program leading to
+
+  [W] F Int ~ Int
+  [W] F Int ~ Bool
+
+We don't want to get "Error Int~Bool".  But if fuv's can rewrite
+wanteds, we will
+
+  [W] fuv ~ Int
+  [W] fuv ~ Bool
+--->
+  [W] Int ~ Bool
+
+
+The new flattening story
+~~~~~~~~~~~~~~~~~~~~~~~~
+* A "flatten-skolem", fsk, is a *unification* variable
+  (ie with an IORef inside it)
+
+* A CFunEqCan is either of form
+     [G] <F xis> : F xis ~ fsk   -- fsk is a FlatSkol
+     [W]       x : F xis ~ usk   -- usk is a unification variable,
+                                 -- but untouchable
+  where
+     x is the witness variable
+     fsk is a flatten skolem
+     xis are function-free
+  CFunEqCans are always [Wanted], or [Given]
+
+  usk untouchable just means that in a CTyVarEq, say,
+       usk ~ Int
+  we do NOT unify usk.
+
+* KEY INSIGHTS:
+
+   - A given flatten-skolem, fsk, is known a-priori to be equal to
+     F xis (the LHS), with <F xis> evidence
+
+   - A unification flatten-skolem, usk, stands for the as-yet-unknown 
+     type to which (F xis) will eventually reduce
+
+
+* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
+                       then xis1 /= xis2 
+  i.e. at most one CFunEqCan with a particular LHS
+
+* Each canonical CFunEqCan x : F xis ~ fsk/usk has its own
+  distinct evidence variable x and flatten-skolem fsk/usk.
+  Why? We make a fresh fsk/usk when the constraint is born;
+  and we never rewrite the RHS of a CFunEqCan.
+
+* CFunEqCans are the *only* way that function applications appear in
+  canonical constraints.  Function applications in any other
+  constraint must be gotten rid of by flattening, thereby generating
+  fresh CFunEqCans.
+
+* Flattening a type (F xis):
+    - If any member of fvs(xis) is a touchable unification variable
+                                or a unification flatten-skolem usk
+      then create new [W] x : F xis ~ usk
+      else create new [G] x : F xis ~ fsk
+      with fresh evidence variable x and flatten-skolem fsk/usk
+
+      NB: givens never contain touchable unification variables
+
+    - Add it to the work list
+
+    - Replace (F xis) with fsk/usk in the type you are flattening
+
+    - You can also add the CFunEqCan to the "flat cache", which
+      simply keeps track of all the function applications you
+      have flattened. 
+
+    - If (F xis) is in the cache already, just
+      use its fsk/usk and evidence x, and emit nothing.
+
+    - No need to substitute in the flat-cache. It's not the end
+      of the world if we start with, say (F alpha ~ usk1) and
+      (F Int ~ usk2) and then find alpha := Int.  Athat will
+      simply give rise to usk1 := usk2 via [Interacting rule] below
+
+* Canonicalising a CFunEqan [G/W] x : F xis ~ fks/usk
+    - Flatten xis (to substitute any tyvars; there are already no functions)
+                  cos :: xis ~ flat_xis
+    - New wanted  x2 :: F flat_xis ~ fsk/usk
+    - Add new wanted to flat cache
+    - Discharge x = F cos ; x2
+
+* Unification flatten-skolems, usk, ONLY get unified when either
+    a) The CFunEqCan takes a step, using an axiom
+    b) During un-flattening at the very, very end
+  They are never unified in any other form of equality.
+  For example [W] fsk ~ Int  is stuck; it does not unify with fsk.
+
+* We *never* substitute in the RHS (i.e. the fsk) of a CFunEqCan.
+  That would destroy the invariant about the shape of a CFunEqCan,
+  and it would risk wanted/wanted interactions. The only way we
+  learn information about fsk is when the CFunEqCan takes a step.
+
+  However we *do* substitute in the LHS of a CFunEqCan (else it
+  would never get to fire!)
+
+* [Interacting rule]
+    (inert)     [W] x1 : F tys ~ usk1
+    (work item) [W] x2 : F tys ~ usk2
+  Just solve one from the other:
+    x2 := x1
+    usk2 := usk1
+  This just unites the two fsks into one.
+  Always solve given from wanted if poss.
+
+* [Firing rule: wanteds]
+    (work item) [W] x : F tys ~ fuv
+    instantiate axiom: ax_co : F tys ~ rhs
+
+   Dischard fuv:
+      fuv := alpha
+      x := ax_co ; sym x2
+      [W] x2 : alpha ~ rhs  (Non-canonical)
+   discharging the work item. This is the way that usk's get
+   unified; even though they are "untouchable".
+
+   NB: this deals with the case where fuv appears in xi, which can
+   happen; it just happens through the non-canonical stuff
+
+   Possible short cut if rhs = G rhs_tys, 
+   where G is a type function.  Then
+      - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
+      - Add G rhs_xis ~ fuv to flat cache
+      - New wanted [W] x2 : G rhs_xis ~ fuv
+      - Discharge x := co ; G cos ; x2
+
+* [Firing rule: givens]
+    (work item) [G] g : F tys ~ fsk
+    instantiate axiom: co : F tys ~ rhs
+
+   Now add non-canonical (since rhs is not flat)
+      [G] (sym g ; co) : fsk ~ rhs
+
+   Short cut for when rhs = G rhs_tys and G is a type function
+      [G] (co ; g) : G tys ~ fsk
+   But need to flatten tys:  flat_cos : tys ~ flat_tys
+      [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk
+
+Floating
+~~~~~~~~
+Principle 1: do floating as if you un-flattened first
+
+For example:
+   [2] forall s.  () => (F alpha[1] s ~ fuv, alpha[1] ~ Maybe fuv)
+   and axiom F (Maybe _) x = x
+
+Here we obviously cannot float (F alpha s ~ fuv) since it mentions s,
+*and hence* cannot float alpha ~ Maybe fuv
+
+BUT consider this:
+   [2] forall s.  () => (F alpha[1] t ~ fuv, alpha[1] ~ Maybe fuv)
+   and axiom F (Maybe _) x = x
+
+Here we really *should* float both constraints, since they are
+equivalent to this (un-flattened) constraint
+   [2] forall s.  alpha[1] ~ Maybe (F alpha[1] t)
+which is clearly floatable.
+
+Principle 2: start the quest for floating with (a[n] ~ xi), where
+a is an untouchable unification variable.  Reason: the whole point
+of floating is to make thse
+
+Algorithm.  Start with ([W] a[n] ~ xi)
+            Look at free vars of xi
+               - unification variable: promote if necessary
+               - fuv: float if its CFunEqCan is floatable
+               - skolem bound at this level: do not float
+               - fsk: look at the free vars of its value
+                      (in that case maybe promote a ~ F Int,
+                      rather than a ~ fsk, perhaps)
+            (see Principle 1)
+
+---------------
+----------------
+Preparing the inert set for implications
+
+   type instance F True a b = a
+   type instance F False a b = b
+
+   [W] x : F c a b ~ fsk
+   [G] gamma ~ fsk
+   (c ~ True)  => a ~ gamma
+   (c ~ False) => b ~ gamma
+--> (c ~ True branch)  Push in as given non-canonical
+   [G] g : (c ~ True)
+   [G] x : F c a b ~ fsk  (nc)
+   [W] a ~ fsk,
+--> flatten
+   [G] g : (c ~ True)
+   [G] sym x1 ; x : fsk1 ~ fsk
+   [W] x1 : F c a b ~ fsk1 (canon)
+  [W] a ~ fsk,
+---> subst c
+   [G] g : (c ~ True)
+   [G] sym x1 ; x : fsk1 ~ fsk
+   [W] x2 : F True a b ~ fsk1 (canon)
+   x1 = F g a b ; x2
+   [W] a ~ fsk,
+---> step  ax : F True a b ~ a
+   [G] g : (c ~ True)
+   [G] sym x1 ; x : fsk1 ~ fsk
+   [W] x2 : F True a b ~ fsk1 (canon)
+   [G] <a> : fsk1 := a
+   x2 = ax
+
+   [W] a ~ fsk,
+
+--------------------------
+Simple20
+~~~~~~~~
+axiom F [a] = [F a]
+
+ [G] F [a] ~ a
+-->
+ [G] fsk ~ a
+ [G] [F a] ~ fsk  (nc)
+-->
+ [G] F a ~ fsk2
+ [G] fsk ~ [fsk2] 
+ [G] fsk ~ a
+-->
+ [G] F a ~ fsk2
+ [G] a ~ [fsk2]
+ [G] fsk ~ a
+
+
+-------------------------------------------
+Simple13  with unification-fsks only
+~~~~~~~~  (This is why unif-fsks-only doesn't work)
+
+  [G] g : a ~ [F a]
+
+---> Flatten given
+  g' = g;[x]
+  [G] g'  : a ~ [usk]
+  [W] x : F a ~ usk
+
+--> subst a in x
+       x = F g' ; x2
+   [W] x2 : F [usk] ~ usk
+
+And now we have an evidence cycle between g' and x.
+
+If we used a given instead (ie current story)
+
+  [G] g : a ~ [F a]
+
+---> Flatten given
+  g' = g;[x]
+  [G] g'  : a ~ [fsk]
+  [G] <F a> : F a ~ fsk
+
+---> Substitute for a
+  [G] g'  : a ~ [fsk]
+  [G] F (sym g'); <F a> : F [fsk] ~ fsk
+
+
+
+-------------------------------------------
+Why given-fsks, alone, doesn't work
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+  [W] w : alpha ~ [F alpha Int]
+
+---> flatten
+  w = ...w'...
+  [W] w' : alpha ~ [fsk]
+  [G] <F alpha Int> : F alpha Int ~ fsk
+
+--> unify (no occurs check)
+  alpha := [fsk]
+
+But since fsk = F alpha Int, this is really an occurs check error.  If
+that is all we know about alpha, we will succeed in constraint
+solving, producing a program with an infinite type.
+
+Even if we did finally get (g : fsk ~ Boo)l by solving (F alpha Int ~ fsk)
+using axiom, zonking would not see it, so (x::alpha) sitting in the
+tree will get zonked to an infinite type.  (Zonking always only does
+refl stuff.)
+
+
+
+
+-------------------------------
+Why is it right to treat fuv's differently to ordinary univ vars?
+
+  f :: forall a. a -> a -> Bool
+  g :: F Int -> F Int -> Bool
+
+Consider
+  f (x:Int) (y:Bool)
+This gives alpha~Int, alpha~Bool.  There is an inconsistency,
+but really only one error.  SherLoc may tell you which location
+is most likely, based on other occurrences of alpha.
+
+Consider
+  g (x:Int) (y:Bool)
+Here we get (F Int ~ Int, F Int ~ Bool), which flattens to
+  (fuv ~ Int, fuv ~ Bool)
+But there are really TWO separate errors.  We must not complain
+about Int~Bool.  Moreover these two errors could arise in entirely
+unrelated parts of the code.  (In the alpha case, there must be
+*some* connection (eg v:alpha in common envt).)
+
index 283886e..36dc641 100644 (file)
@@ -15,7 +15,7 @@ module FunDeps (
         Equation(..), pprEquation,
         improveFromInstEnv, improveFromAnother,
         checkInstCoverage, checkFunDeps,
-        growThetaTyVars, pprFundeps
+        pprFundeps
     ) where
 
 #include "HsVersions.h"
@@ -41,46 +41,6 @@ import Data.Maybe       ( isJust )
 
 %************************************************************************
 %*                                                                      *
-\subsection{Close type variables}
-%*                                                                      *
-%************************************************************************
-
-Note [Growing the tau-tvs using constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-(growThetaTyVars insts tvs) is the result of extending the set
-    of tyvars tvs using all conceivable links from pred
-
-E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
-Then growThetaTyVars preds tvs = {a,b,c}
-
-Notice that
-   growThetaTyVars is conservative       if v might be fixed by vs
-                                         => v `elem` grow(vs,C)
-
-\begin{code}
-growThetaTyVars :: ThetaType -> TyVarSet -> TyVarSet
--- See Note [Growing the tau-tvs using constraints]
-growThetaTyVars theta tvs
-  | null theta = tvs
-  | otherwise  = fixVarSet mk_next tvs
-  where
-    mk_next tvs = foldr grow_one tvs theta
-    grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
-
-growPredTyVars :: PredType
-               -> 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
-    pred_tvs = tyVarsOfType pred
-\end{code}
-
-
-%************************************************************************
-%*                                                                      *
 \subsection{Generate equations from functional dependencies}
 %*                                                                      *
 %************************************************************************
index 9998a1e..154df92 100644 (file)
@@ -15,6 +15,7 @@ module Inst (
 
        newOverloadedLit, mkOverLit,
 
+       newClsInst,
        tcGetInsts, tcGetInstEnvs, getOverlapFlag,
        tcExtendLocalInstEnv, instCallConstraints, newMethodFromName,
        tcSyntaxName,
@@ -44,6 +45,8 @@ import Type
 import Coercion ( Role(..) )
 import TcType
 import HscTypes
+import Class( Class )
+import MkId( mkDictFunId )
 import Id
 import Name
 import Var      ( EvVar, varType, setVarType )
@@ -167,9 +170,14 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
 
 deeplyInstantiate orig ty
   | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
-  = do { (_, tys, subst) <- tcInstTyVars tvs
+  = do { (subst, tvs') <- tcInstTyVars tvs
        ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
-       ; wrap1 <- instCall orig tys (substTheta subst theta)
+       ; let theta' = substTheta subst theta
+       ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
+       ; traceTc "Instantiating (deply)" (vcat [ ppr ty
+                                               , text "with" <+> ppr tvs'
+                                               , text "args:" <+> ppr ids1
+                                               , text "theta:" <+>  ppr theta' ])
        ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
        ; return (mkWpLams ids1
                     <.> wrap2
@@ -377,18 +385,19 @@ syntaxNameCtxt name orig ty tidy_env
 %************************************************************************
 
 \begin{code}
-getOverlapFlag :: TcM OverlapFlag
-getOverlapFlag
+getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
+getOverlapFlag overlap_mode
   = do  { dflags <- getDynFlags
         ; let overlap_ok    = xopt Opt_OverlappingInstances dflags
               incoherent_ok = xopt Opt_IncoherentInstances  dflags
               use x = OverlapFlag { isSafeOverlap = safeLanguageOn dflags
                                   , overlapMode   = x }
-              overlap_flag | incoherent_ok = use Incoherent
-                           | overlap_ok    = use Overlaps
-                           | otherwise     = use NoOverlap
+              default_oflag | incoherent_ok = use Incoherent
+                            | overlap_ok    = use Overlaps
+                            | otherwise     = use NoOverlap
 
-        ; return overlap_flag }
+              final_oflag = setOverlapModeMaybe default_oflag overlap_mode
+        ; return final_oflag }
 
 tcGetInstEnvs :: TcM (InstEnv, InstEnv)
 -- Gets both the external-package inst-env
@@ -400,6 +409,22 @@ tcGetInsts :: TcM [ClsInst]
 -- Gets the local class instances.
 tcGetInsts = fmap tcg_insts getGblEnv
 
+newClsInst :: Maybe OverlapMode -> Name -> [TyVar] -> ThetaType
+           -> Class -> [Type] -> TcM ClsInst
+newClsInst overlap_mode dfun_name tvs theta clas tys
+  = do { (subst, tvs') <- freshenTyVarBndrs tvs
+             -- Be sure to freshen those type variables,
+             -- so they are sure not to appear in any lookup
+       ; let tys'   = substTys subst tys
+             theta' = substTheta subst theta
+             dfun   = mkDictFunId dfun_name tvs' theta' clas tys'
+             -- Substituting in the DFun type just makes sure that
+             -- we are using TyVars rather than TcTyVars
+             -- Not sure if this is really the right place to do so,
+             -- but it'll do fine
+       ; oflag <- getOverlapFlag overlap_mode
+       ; return (mkLocalInstance dfun oflag tvs' clas tys') }
+
 tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
   -- Add new locally-defined instances
 tcExtendLocalInstEnv dfuns thing_inside
@@ -463,7 +488,11 @@ addLocalInst (home_ie, my_insts) ispec
            dupInstErr ispec (head dups)
 
          ; return (extendInstEnv home_ie' ispec, ispec:my_insts') }
+\end{code}
 
+Errors and tracing
+
+\begin{code}
 traceDFuns :: [ClsInst] -> TcRn ()
 traceDFuns ispecs
   = traceTc "Adding instances:" (vcat (map pp ispecs))
@@ -502,13 +531,12 @@ addClsInstsErr herald ispecs
 \begin{code}
 ---------------- Getting free tyvars -------------------------
 tyVarsOfCt :: Ct -> TcTyVarSet
--- NB: the
-tyVarsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
-tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
-tyVarsOfCt (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
-tyVarsOfCt (CIrredEvCan { cc_ev = ev })                 = tyVarsOfType (ctEvPred ev)
-tyVarsOfCt (CHoleCan { cc_ev = ev })                    = tyVarsOfType (ctEvPred ev)
-tyVarsOfCt (CNonCanonical { cc_ev = ev })               = tyVarsOfType (ctEvPred ev)
+tyVarsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })     = extendVarSet (tyVarsOfType xi) tv
+tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_fsk = fsk }) = extendVarSet (tyVarsOfTypes tys) fsk
+tyVarsOfCt (CDictCan { cc_tyargs = tys })                = tyVarsOfTypes tys
+tyVarsOfCt (CIrredEvCan { cc_ev = ev })                  = tyVarsOfType (ctEvPred ev)
+tyVarsOfCt (CHoleCan { cc_ev = ev })                     = tyVarsOfType (ctEvPred ev)
+tyVarsOfCt (CNonCanonical { cc_ev = ev })                = tyVarsOfType (ctEvPred ev)
 
 tyVarsOfCts :: Cts -> TcTyVarSet
 tyVarsOfCts = foldrBag (unionVarSet . tyVarsOfCt) emptyVarSet
@@ -522,10 +550,10 @@ tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
 
 tyVarsOfImplic :: Implication -> TyVarSet
 -- Only called on *zonked* things, hence no need to worry about flatten-skolems
-tyVarsOfImplic (Implic { ic_skols = skols, ic_fsks = fsks
-                             , ic_given = givens, ic_wanted = wanted })
+tyVarsOfImplic (Implic { ic_skols = skols
+                       , ic_given = givens, ic_wanted = wanted })
   = (tyVarsOfWC wanted `unionVarSet` tyVarsOfTypes (map evVarPred givens))
-    `delVarSetList` skols `delVarSetList` fsks
+    `delVarSetList` skols
 
 tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet
 tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
index c286d3b..d0e875c 100644 (file)
@@ -31,8 +31,9 @@ import TcPat
 import TcMType
 import PatSyn
 import ConLike
+import FamInstEnv( normaliseType )
+import FamInst( tcGetFamInstEnvs )
 import Type( tidyOpenType )
-import FunDeps( growThetaTyVars )
 import TyCon
 import TcType
 import TysPrim
@@ -591,14 +592,15 @@ tcPolyInfer
   -> [LHsBind Name]
   -> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
 tcPolyInfer rec_tc prag_fn tc_sig_fn mono closed bind_list
-  = do { ((binds', mono_infos), wanted)
-             <- captureConstraints $
+  = do { (((binds', mono_infos), untch), wanted)
+             <- captureConstraints  $
+                captureUntouchables $
                 tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
 
        ; let name_taus = [(name, idType mono_id) | (name, _, mono_id) <- mono_infos]
        ; traceTc "simplifyInfer call" (ppr name_taus $$ ppr wanted)
        ; (qtvs, givens, mr_bites, ev_binds)
-                 <- simplifyInfer closed mono name_taus wanted
+                 <- simplifyInfer untch mono name_taus wanted
 
        ; theta   <- zonkTcThetaType (map evVarPred givens)
        ; exports <- checkNoErrs $ mapM (mkExport prag_fn qtvs theta) mono_infos
@@ -677,15 +679,20 @@ mkInferredPolyId :: Name -> [TyVar] -> TcThetaType -> TcType -> TcM Id
 -- the right type variables and theta to quantify over
 -- See Note [Validity of inferred types]
 mkInferredPolyId poly_name qtvs theta mono_ty
-  = addErrCtxtM (mk_bind_msg True False poly_name inferred_poly_ty) $
-    do { checkValidType (InfSigCtxt poly_name) inferred_poly_ty
-       ; return (mkLocalId poly_name inferred_poly_ty) }
-  where
-    my_tvs2 = closeOverKinds (growThetaTyVars theta (tyVarsOfType mono_ty))
+  = do { fam_envs <- tcGetFamInstEnvs
+
+       ; let (_co, norm_mono_ty) = normaliseType fam_envs Nominal mono_ty
+               -- Unification may not have normalised the type, so do it
+               -- here to make it as uncomplicated as possible.
+             my_tvs2 = closeOverKinds (growThetaTyVars theta (tyVarsOfType norm_mono_ty))
                   -- Include kind variables!  Trac #7916
-    my_tvs   = filter (`elemVarSet` my_tvs2) qtvs   -- Maintain original order
-    my_theta = filter (quantifyPred my_tvs2) theta
-    inferred_poly_ty = mkSigmaTy my_tvs my_theta mono_ty
+             my_tvs   = filter (`elemVarSet` my_tvs2) qtvs   -- Maintain original order
+             my_theta = filter (quantifyPred my_tvs2) theta
+             inferred_poly_ty = mkSigmaTy my_tvs my_theta norm_mono_ty
+
+       ; addErrCtxtM (mk_bind_msg True False poly_name inferred_poly_ty) $
+         checkValidType (InfSigCtxt poly_name) inferred_poly_ty
+       ; return (mkLocalId poly_name inferred_poly_ty) }
 
 mk_bind_msg :: Bool -> Bool -> Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
 mk_bind_msg inferred want_ambig poly_name poly_ty tidy_env
index d58d5db..d243667 100644 (file)
@@ -2,8 +2,8 @@
 {-# LANGUAGE CPP #-}
 
 module TcCanonical(
-    canonicalize, emitWorkNC,
-    StopOrContinue (..)
+    canonicalize, 
+    flattenMany, FlattenEnv(..), FlattenMode(..)
  ) where
 
 #include "HsVersions.h"
@@ -18,17 +18,16 @@ import TyCon
 import TypeRep
 import Var
 import VarEnv
+import Name( isSystemName )
 import OccName( OccName )
 import Outputable
 import Control.Monad    ( when )
 import DynFlags( DynFlags )
 import VarSet
 import TcSMonad
-import FastString
 
 import Util
 import BasicTypes
-import Maybes( catMaybes )
 \end{code}
 
 
@@ -71,35 +70,6 @@ phase cannot be rewritten any further from the inerts (but maybe /it/ can
 rewrite an inert or still interact with an inert in a further phase in the
 simplifier.
 
-\begin{code}
-
--- Informative results of canonicalization
-data StopOrContinue
-  = ContinueWith Ct   -- Either no canonicalization happened, or if some did
-                      -- happen, it is still safe to just keep going with this
-                      -- work item.
-  | Stop              -- Some canonicalization happened, extra work is now in
-                      -- the TcS WorkList.
-
-instance Outputable StopOrContinue where
-  ppr Stop             = ptext (sLit "Stop")
-  ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
-
-
-continueWith :: Ct -> TcS StopOrContinue
-continueWith = return . ContinueWith
-
-andWhenContinue :: TcS StopOrContinue
-                -> (Ct -> TcS StopOrContinue)
-                -> TcS StopOrContinue
-andWhenContinue tcs1 tcs2
-  = do { r <- tcs1
-       ; case r of
-           Stop            -> return Stop
-           ContinueWith ct -> tcs2 ct }
-
-\end{code}
-
 Note [Caching for canonicals]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Our plan with pre-canonicalization is to be able to solve a constraint
@@ -158,7 +128,7 @@ EvBinds, so we are again good.
 -- Top-level canonicalization
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-canonicalize :: Ct -> TcS StopOrContinue
+canonicalize :: Ct -> TcS (StopOrContinue Ct)
 canonicalize ct@(CNonCanonical { cc_ev = ev })
   = do { traceTcS "canonicalize (non-canonical)" (ppr ct)
        ; {-# SCC "canEvVar" #-}
@@ -178,16 +148,16 @@ canonicalize (CTyEqCan { cc_ev = ev
 canonicalize (CFunEqCan { cc_ev = ev
                         , cc_fun    = fn
                         , cc_tyargs = xis1
-                        , cc_rhs    = xi2 })
+                        , cc_fsk    = fsk })
   = {-# SCC "canEqLeafFunEq" #-}
-    canEqLeafFun ev NotSwapped fn xis1 xi2 xi2
+    canCFunEqCan ev fn xis1 fsk
 
 canonicalize (CIrredEvCan { cc_ev = ev })
   = canIrred ev
 canonicalize (CHoleCan { cc_ev = ev, cc_occ = occ })
   = canHole ev occ
 
-canEvNC :: CtEvidence -> TcS StopOrContinue
+canEvNC :: CtEvidence -> TcS (StopOrContinue Ct)
 -- Called only for non-canonical EvVars
 canEvNC ev
   = case classifyPredType (ctEvPred ev) of
@@ -205,13 +175,13 @@ canEvNC ev
 %************************************************************************
 
 \begin{code}
-canTuple :: CtEvidence -> [PredType] -> TcS StopOrContinue
+canTuple :: CtEvidence -> [PredType] -> TcS (StopOrContinue Ct)
 canTuple ev tys
   = do { traceTcS "can_pred" (text "TuplePred!")
        ; let xcomp = EvTupleMk
              xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]
-       ; ctevs <- xCtEvidence ev (XEvTerm tys xcomp xdecomp)
-       ; canEvVarsCreated ctevs }
+       ; xCtEvidence ev (XEvTerm tys xcomp xdecomp)
+       ; stopWith ev "Decomposed tuple constraint" }
 \end{code}
 
 %************************************************************************
@@ -223,7 +193,7 @@ canTuple ev tys
 \begin{code}
 canClass, canClassNC
    :: CtEvidence
-   -> Class -> [Type] -> TcS StopOrContinue
+   -> Class -> [Type] -> TcS (StopOrContinue Ct)
 -- Precondition: EvVar is class evidence
 
 -- The canClassNC version is used on non-canonical constraints
@@ -236,19 +206,18 @@ canClassNC ev cls tys
     `andWhenContinue` emitSuperclasses
 
 canClass ev cls tys
-  = do { (xis, cos) <- flattenMany FMFullFlatten ev tys
+  = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
+       ; (xis, cos) <- flattenMany fmode tys
        ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
              xi = mkClassPred cls xis
+             mk_ct new_ev = CDictCan { cc_ev = new_ev
+                                     , cc_tyargs = xis, cc_class = cls }
        ; mb <- rewriteEvidence ev xi co
        ; traceTcS "canClass" (vcat [ ppr ev <+> ppr cls <+> ppr tys
                                    , ppr xi, ppr mb ])
-       ; case mb of
-           Nothing -> return Stop
-           Just new_ev -> continueWith $
-                          CDictCan { cc_ev = new_ev
-                                   , cc_tyargs = xis, cc_class = cls } }
+       ; return (fmap mk_ct mb) }
 
-emitSuperclasses :: Ct -> TcS StopOrContinue
+emitSuperclasses :: Ct -> TcS (StopOrContinue Ct)
 emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls })
             -- Add superclasses of this one here, See Note [Adding superclasses].
             -- But only if we are not simplifying the LHS of a rule.
@@ -337,8 +306,7 @@ newSCWorkFromFlavored flavor cls xis
              xev = XEvTerm { ev_preds  =  sc_theta
                            , ev_comp   = panic "Can't compose for given!"
                            , ev_decomp = xev_decomp }
-       ; ctevs <- xCtEvidence flavor xev
-       ; emitWorkNC ctevs }
+       ; xCtEvidence flavor xev }
 
   | isEmptyVarSet (tyVarsOfTypes xis)
   = return () -- Wanteds with no variables yield no deriveds.
@@ -347,20 +315,19 @@ newSCWorkFromFlavored flavor cls xis
   | otherwise -- Wanted case, just add those SC that can lead to improvement.
   = do { let sc_rec_theta = transSuperClasses cls xis
              impr_theta   = filter is_improvement_pty sc_rec_theta
-             loc          = ctev_loc flavor
+             loc          = ctEvLoc flavor
        ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
-       ; mb_der_evs <- mapM (newDerived loc) impr_theta
-       ; emitWorkNC (catMaybes mb_der_evs) }
+       ; mapM_ (emitNewDerived loc) impr_theta }
 
 is_improvement_pty :: PredType -> Bool
 -- Either it's an equality, or has some functional dependency
 is_improvement_pty ty = go (classifyPredType ty)
   where
-    go (EqPred {})         = True
+    go (EqPred t1 t2)       = not (t1 `tcEqType` t2)
     go (ClassPred cls _tys) = not $ null fundeps
-      where (_,fundeps) = classTvsFds cls
-    go (TuplePred ts)      = any is_improvement_pty ts
-    go (IrredPred {})      = True -- Might have equalities after reduction?
+                            where (_,fundeps) = classTvsFds cls
+    go (TuplePred ts)       = any is_improvement_pty ts
+    go (IrredPred {})       = True -- Might have equalities after reduction?
 \end{code}
 
 
@@ -372,16 +339,18 @@ is_improvement_pty ty = go (classifyPredType ty)
 
 
 \begin{code}
-canIrred :: CtEvidence -> TcS StopOrContinue
+canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
 -- Precondition: ty not a tuple and no other evidence form
 canIrred old_ev
   = do { let old_ty = ctEvPred old_ev
+             fmode  = FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }
+                      -- Flatten (F [a]), say, so that it can reduce to Eq a
        ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty)
-       ; (xi,co) <- flatten FMFullFlatten old_ev old_ty -- co :: xi ~ old_ty
+       ; (xi,co) <- flatten fmode old_ty -- co :: xi ~ old_ty
        ; mb <- rewriteEvidence old_ev xi co
        ; case mb of {
-             Nothing     -> return Stop ;
-             Just new_ev ->
+             Stop ev s           -> return (Stop ev s) ;
+             ContinueWith new_ev ->
 
     do { -- Re-classify, in case flattening has improved its shape
        ; case classifyPredType (ctEvPred new_ev) of
@@ -391,15 +360,16 @@ canIrred old_ev
            _                 -> continueWith $
                                 CIrredEvCan { cc_ev = new_ev } } } }
 
-canHole :: CtEvidence -> OccName -> TcS StopOrContinue
+canHole :: CtEvidence -> OccName -> TcS (StopOrContinue Ct)
 canHole ev occ
-  = do { let ty = ctEvPred ev
-       ; (xi,co) <- flatten FMFullFlatten ev ty -- co :: xi ~ ty
+  = do { let ty    = ctEvPred ev
+             fmode = FE { fe_ev = ev, fe_mode = FM_SubstOnly }
+       ; (xi,co) <- flatten fmode ty -- co :: xi ~ ty
        ; mb <- rewriteEvidence ev xi co
        ; case mb of
-             Just new_ev -> emitInsoluble (CHoleCan { cc_ev = new_ev, cc_occ = occ })
-             Nothing     -> return ()   -- Found a cached copy; won't happen
-       ; return Stop }
+           ContinueWith new_ev -> do { emitInsoluble (CHoleCan { cc_ev = new_ev, cc_occ = occ })
+                                     ; stopWith new_ev "Emit insoluble hole" }
+           Stop ev s -> return (Stop ev s) } -- Found a cached copy; won't happen
 \end{code}
 
 %************************************************************************
@@ -449,97 +419,101 @@ it expands the synonym and proceeds; if not, it simply returns the
 unexpanded synonym.
 
 \begin{code}
-data FlattenMode = FMSubstOnly | FMFullFlatten
-                   -- See Note [Flattening under a forall]
+data FlattenEnv
+  = FE { fe_mode :: FlattenMode
+       , fe_ev   :: CtEvidence }
+
+data FlattenMode  -- Postcondition for all three: inert wrt the type substitution
+  = FM_FlattenAll          -- Postcondition: function-free
+
+  | FM_Avoid TcTyVar Bool  -- Postcondition:
+                           --  * tyvar is only mentioned in result under a rigid path
+                           --    e.g.   [a] is ok, but F a won't happen
+                           --  * If flat_top is True, top level is not a function application
+                           --   (but under type constructors is ok e.g. [F a])
+
+  | FM_SubstOnly           -- See Note [Flattening under a forall]
 
 -- Flatten a bunch of types all at once.
-flattenMany ::  FlattenMode
-            -> CtEvidence
-            -> [Type] -> TcS ([Xi], [TcCoercion])
+flattenMany :: FlattenEnv -> [Type] -> TcS ([Xi], [TcCoercion])
 -- Coercions :: Xi ~ Type
 -- Returns True iff (no flattening happened)
--- NB: The EvVar inside the 'ctxt :: CtEvidence' is unused,
+-- NB: The EvVar inside the 'fe_ev :: CtEvidence' is unused,
 --     we merely want (a) Given/Solved/Derived/Wanted info
 --                    (b) the GivenLoc/WantedLoc for when we create new evidence
-flattenMany f ctxt tys
+flattenMany fmode tys
   = -- pprTrace "flattenMany" empty $
     go tys
   where go []       = return ([],[])
-        go (ty:tys) = do { (xi,co)    <- flatten f ctxt ty
+        go (ty:tys) = do { (xi,co)    <- flatten fmode ty
                          ; (xis,cos)  <- go tys
                          ; return (xi:xis,co:cos) }
 
-flatten :: FlattenMode
-        -> CtEvidence -> TcType -> TcS (Xi, TcCoercion)
+flatten :: FlattenEnv -> TcType -> TcS (Xi, TcCoercion)
 -- Flatten a type to get rid of type function applications, returning
 -- the new type-function-free type, and a collection of new equality
 -- constraints.  See Note [Flattening] for more detail.
 --
 -- Postcondition: Coercion :: Xi ~ TcType
 
-flatten _ xi@(LitTy {}) = return (xi, mkTcNomReflCo xi)
+flatten _ xi@(LitTy {}) = return (xi, mkTcNomReflCo xi)
 
-flatten f ctxt (TyVarTy tv)
-  = flattenTyVar f ctxt tv
+flatten fmode (TyVarTy tv)
+  = flattenTyVar fmode tv
 
-flatten f ctxt (AppTy ty1 ty2)
-  = do { (xi1,co1) <- flatten f ctxt ty1
-       ; (xi2,co2) <- flatten f ctxt ty2
+flatten fmode (AppTy ty1 ty2)
+  = do { (xi1,co1) <- flatten fmode ty1
+       ; (xi2,co2) <- flatten fmode ty2
        ; traceTcS "flatten/appty" (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$ ppr co1 $$ ppr xi2 $$ ppr co2)
        ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) }
 
-flatten f ctxt (FunTy ty1 ty2)
-  = do { (xi1,co1) <- flatten f ctxt ty1
-       ; (xi2,co2) <- flatten f ctxt ty2
+flatten fmode (FunTy ty1 ty2)
+  = do { (xi1,co1) <- flatten fmode ty1
+       ; (xi2,co2) <- flatten fmode ty2
        ; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) }
 
-flatten f ctxt (TyConApp tc tys)
+flatten fmode (TyConApp tc tys)
 
   -- Expand type synonyms that mention type families 
   -- on the RHS; see Note [Flattening synonyms]
   | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
-  , any isSynFamilyTyCon (tyConsOfType rhs)
-  = flatten f ctxt (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
-
-  -- For * a normal data type application
-  --     * data family application
-  --     * type synonym application whose RHS does not mention type families
-  --             See Note [Flattening synonyms]
-  -- we just recursively flatten the arguments.
-  | not (isSynFamilyTyCon tc)
-  = do { (xis,cos) <- flattenMany f ctxt tys
-       ; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
+  , let expanded_ty = mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys'
+  = case fe_mode fmode of
+      FM_FlattenAll | any isSynFamilyTyCon (tyConsOfType rhs)
+                   -> flatten fmode expanded_ty
+                    | otherwise
+                   -> flattenTyConApp fmode tc tys
+      _ -> flattenTyConApp fmode tc tys
 
   -- Otherwise, it's a type function application, and we have to
   -- flatten it away as well, and generate a new given equality constraint
   -- between the application and a newly generated flattening skolem variable.
-  | otherwise
-  = ASSERT( tyConArity tc <= length tys )       -- Type functions are saturated
-      do { (xis, cos) <- flattenMany f ctxt tys
-         ; let (xi_args,  xi_rest)  = splitAt (tyConArity tc) xis
-               (cos_args, cos_rest) = splitAt (tyConArity tc) cos
-                 -- The type function might be *over* saturated
-                 -- in which case the remaining arguments should
-                 -- be dealt with by AppTys
-
-         ; (rhs_xi, ret_co) <- flattenNestedFamApp f ctxt tc xi_args
+  | isSynFamilyTyCon tc
+  = flattenFamApp fmode tc tys
 
-                  -- Emit the flat constraints
-         ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
-                                            --    cf Trac #5655
-                  , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo Nominal tc cos_args) $
-                    cos_rest
-                  )
-         }
-
-flatten _f ctxt ty@(ForAllTy {})
+  -- For * a normal data type application
+  --     * data family application
+  -- we just recursively flatten the arguments.
+  | otherwise  -- Switch off the flat_top bit in FM_Avoid
+  , let fmode' = case fmode of
+                   FE { fe_mode = FM_Avoid tv _ }
+                     -> fmode { fe_mode = FM_Avoid tv False }
+                   _ -> fmode
+  = flattenTyConApp fmode' tc tys
+
+flatten fmode ty@(ForAllTy {})
 -- We allow for-alls when, but only when, no type function
 -- applications inside the forall involve the bound type variables.
   = do { let (tvs, rho) = splitForAllTys ty
-       ; (rho', co) <- flatten FMSubstOnly ctxt rho
+       ; (rho', co) <- flatten (fmode { fe_mode = FM_SubstOnly }) rho
                          -- Substitute only under a forall
                          -- See Note [Flattening under a forall]
        ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
+
+flattenTyConApp :: FlattenEnv -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
+flattenTyConApp fmode tc tys
+  = do { (xis, cos) <- flattenMany fmode tys
+       ; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
 \end{code}
 
 Note [Flattening synonyms]
@@ -578,59 +552,84 @@ because now the 'b' has escaped its scope.  We'd have to flatten to
 and we have not begun to think about how to make that work!
 
 \begin{code}
-flattenNestedFamApp :: FlattenMode -> CtEvidence
-                    -> TyCon -> [TcType]   -- Exactly-saturated type function application
-                    -> TcS (Xi, TcCoercion)
-flattenNestedFamApp FMSubstOnly _ tc xi_args
-  = do { let fam_ty = mkTyConApp tc xi_args
-       ; return (fam_ty, mkTcNomReflCo fam_ty) }
-
-flattenNestedFamApp FMFullFlatten ctxt tc xi_args  -- Eactly saturated
-  = do { let fam_ty = mkTyConApp tc xi_args
-       ; mb_ct <- lookupFlatEqn tc xi_args
+flattenFamApp, flattenExactFamApp, flattenExactFamApp_fully
+  :: FlattenEnv -> TyCon -> [TcType] -> TcS (Xi, TcCoercion)
+  -- flattenFamApp      can be over-saturated
+  -- flattenExactFamApp is exactly saturated
+  -- Postcondition: Coercion :: Xi ~ F tys
+flattenFamApp fmode tc tys  -- Can be over-saturated
+    = ASSERT( tyConArity tc <= length tys )  -- Type functions are saturated
+                 -- The type function might be *over* saturated
+                 -- in which case the remaining arguments should
+                 -- be dealt with by AppTys
+      do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys
+         ; (xi1, co1) <- flattenExactFamApp fmode tc tys1
+               -- co1 :: xi1 ~ F tys1
+         ; (xis_rest, cos_rest) <- flattenMany fmode tys_rest
+               -- cos_res :: xis_rest ~ tys_rest
+         ; return ( mkAppTys xi1 xis_rest   -- NB mkAppTys: rhs_xi might not be a type variable
+                                            --    cf Trac #5655
+                  , mkTcAppCos co1 cos_rest -- (rhs_xi :: F xis) ; (F cos :: F xis ~ F tys)
+                  ) }
+
+flattenExactFamApp fmode tc tys
+  = case fe_mode fmode of
+       FM_SubstOnly -> do { (xis, cos) <- flattenMany fmode tys
+                          ; return ( mkTyConApp tc xis
+                                   , mkTcTyConAppCo Nominal tc cos ) }
+
+       FM_Avoid tv flat_top -> do { (xis, cos) <- flattenMany fmode tys
+                                  ; if flat_top || tv `elemVarSet` tyVarsOfTypes xis
+                                    then flattenExactFamApp_fully fmode tc tys
+                                    else return ( mkTyConApp tc xis
+                                                , mkTcTyConAppCo Nominal tc cos ) }
+       FM_FlattenAll -> flattenExactFamApp_fully fmode tc tys
+
+flattenExactFamApp_fully fmode tc tys
+  = do { (xis, cos) <- flattenMany (fmode { fe_mode = FM_FlattenAll })tys
+       ; let ret_co = mkTcTyConAppCo Nominal tc cos
+              -- ret_co :: F xis ~ F tys
+             ctxt_ev = fe_ev fmode
+
+       ; mb_ct <- lookupFlatCache tc xis
        ; case mb_ct of
-           Just (ctev, rhs_ty)
-             | ctev `canRewriteOrSame `ctxt    -- Must allow [W]/[W]
-             -> -- You may think that we can just return (cc_rhs ct) but not so.
-                --            return (mkTcCoVarCo (ctId ct), cc_rhs ct, [])
-                -- The cached constraint resides in the cache so we have to flatten
-                -- the rhs to make sure we have applied any inert substitution to it.
-                -- Alternatively we could be applying the inert substitution to the
-                -- cache as well when we interact an equality with the inert.
-                -- The design choice is: do we keep the flat cache rewritten or not?
-                -- For now I say we don't keep it fully rewritten.
-               do { (rhs_xi,co) <- flatten FMFullFlatten ctev rhs_ty
-                  ; let final_co = evTermCoercion (ctEvTerm ctev)
-                                   `mkTcTransCo` mkTcSymCo co
-                  ; traceTcS "flatten/flat-cache hit" $ (ppr ctev $$ ppr rhs_xi $$ ppr final_co)
-                  ; return (rhs_xi, final_co) }
-
-           _ -> do { (ctev, rhs_xi) <- newFlattenSkolem ctxt fam_ty
-                   ; extendFlatCache tc xi_args ctev rhs_xi
-
-                   -- The new constraint (F xi_args ~ rhs_xi) is not necessarily inert
+           Just (co, fsk)  -- co :: F xis ~ fsk
+             | isFskTyVar fsk || not (isGiven ctxt_ev)
+             ->  -- Usable hit in the flat-cache
+                 -- isFskTyVar checks for a "given" in the cache
+                do { traceTcS "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr fsk $$ ppr co)
+                   ; (fsk_xi, fsk_co) <- flattenTyVar fmode fsk
+                          -- The fsk may already have been unified, so flatten it
+                          -- fsk_co :: fsk_xi ~ fsk
+                   ; return (fsk_xi, fsk_co `mkTcTransCo` mkTcSymCo co `mkTcTransCo` ret_co) }
+                                    -- :: fsk_xi ~ F xis
+
+           _ -> do { let fam_ty = mkTyConApp tc xis
+                   ; (ev, fsk) <- newFlattenSkolem ctxt_ev fam_ty
+                   ; extendFlatCache tc xis (ctEvCoercion ev, fsk)
+
+                   -- The new constraint (F xis ~ fsk) is not necessarily inert
                    -- (e.g. the LHS may be a redex) so we must put it in the work list
-                   ; let ct = CFunEqCan { cc_ev     = ctev
+                   ; let ct = CFunEqCan { cc_ev     = ev
                                         , cc_fun    = tc
-                                        , cc_tyargs = xi_args
-                                        , cc_rhs    = rhs_xi }
-                   ; updWorkListTcS $ extendWorkListFunEq ct
+                                        , cc_tyargs = xis
+                                        , cc_fsk    = fsk }
+                   ; updWorkListTcS (extendWorkListFunEq ct)
 
-                   ; traceTcS "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr rhs_xi $$ ppr ctev)
-                   ; return (rhs_xi, evTermCoercion (ctEvTerm ctev)) }
-       }
+                   ; traceTcS "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr fsk $$ ppr ev)
+                   ; return (mkTyVarTy fsk, mkTcSymCo (ctEvCoercion ev) `mkTcTransCo` ret_co) } }
 \end{code}
 
 \begin{code}
-flattenTyVar :: FlattenMode -> CtEvidence -> TcTyVar -> TcS (Xi, TcCoercion)
+flattenTyVar :: FlattenEnv -> TcTyVar -> TcS (Xi, TcCoercion)
 -- "Flattening" a type variable means to apply the substitution to it
 -- The substitution is actually the union of the substitution in the TyBinds
 -- for the unification variables that have been unified already with the inert
 -- equalities, see Note [Spontaneously solved in TyBinds] in TcInteract.
 --
 -- Postcondition: co : xi ~ tv
-flattenTyVar f ctxt tv
-  = do { mb_yes <- flattenTyVarOuter f ctxt tv
+flattenTyVar fmode tv
+  = do { mb_yes <- flattenTyVarOuter (fe_ev fmode) tv
        ; case mb_yes of
            Left tv'         -> -- Done 
                                do { traceTcS "flattenTyVar1" (ppr tv $$ ppr (tyVarKind tv'))
@@ -639,15 +638,13 @@ flattenTyVar f ctxt tv
                                ty' = mkTyVarTy tv'
 
            Right (ty1, co1) -> -- Recurse
-                               do { (ty2, co2) <- flatten f ctxt ty1
+                               do { (ty2, co2) <- flatten fmode ty1
                                   ; traceTcS "flattenTyVar2" (ppr tv $$ ppr ty2)
                                   ; return (ty2, co2 `mkTcTransCo` co1) }
        }
 
 flattenTyVarOuter, flattenTyVarFinal 
-   :: FlattenMode -> CtEvidence
-   -> TcTyVar 
-   -> TcS (Either TyVar (TcType, TcCoercion))
+   :: CtEvidence -> TcTyVar -> TcS (Either TyVar (TcType, TcCoercion))
 -- Look up the tyvar in 
 --   a) the internal MetaTyVar box
 --   b) the tyvar binds 
@@ -656,9 +653,9 @@ flattenTyVarOuter, flattenTyVarFinal
 --        (Right (ty, co)) if found, with co :: ty ~ tv
 --                         NB: in the latter case ty is not necessarily flattened
 
-flattenTyVarOuter f ctxt tv
-  | not (isTcTyVar tv)            -- Happens when flatten under a (forall a. ty)
-  = flattenTyVarFinal f ctxt tv   -- So ty contains refernces to the non-TcTyVar a
+flattenTyVarOuter ctxt_ev tv
+  | not (isTcTyVar tv)             -- Happens when flatten under a (forall a. ty)
+  = flattenTyVarFinal ctxt_ev tv   -- So ty contains refernces to the non-TcTyVar a
   | otherwise
   = do { mb_ty <- isFilledMetaTyVar_maybe tv
        ; case mb_ty of {
@@ -666,39 +663,32 @@ flattenTyVarOuter f ctxt tv
                          ; return (Right (ty, mkTcNomReflCo ty)) } ;
            Nothing ->
 
-    -- Try in ty_binds
-    do { ty_binds <- getTcSTyBindsMap
-       ; case lookupVarEnv ty_binds tv of {
-           Just (_tv,ty) -> do { traceTcS "Following bound tyvar" (ppr tv <+> equals <+> ppr ty)
-                               ; return (Right (ty, mkTcNomReflCo ty)) } ;
-                                 -- NB: ty_binds coercions are all ReflCo,
-           Nothing ->
-
     -- Try in the inert equalities
     do { ieqs <- getInertEqs
        ; case lookupVarEnv ieqs tv of
-           Just (ct:_)                      -- If the first doesn't work,
-             | let ctev   = ctEvidence ct   -- the subsequent ones won't either
-                   rhs_ty = cc_rhs ct
-             , ctev `canRewrite` ctxt 
+           Just (ct:_)   -- If the first doesn't work,
+                         -- the subsequent ones won't either
+             | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
+             , eqCanRewrite tv ctev ctxt_ev
              ->  do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
-                    ; return (Right (rhs_ty, mkTcSymCo (evTermCoercion (ctEvTerm ctev)))) }
-                    -- NB: even if ct is Derived we are not going to
-                    -- touch the actual coercion so we are fine.
+                    ; return (Right (rhs_ty, mkTcSymCo (ctEvCoercion ctev))) }
+                    -- NB: ct is Derived then (fe_ev fmode) must be also, hence
+                    -- we are not going to touch the returned coercion
+                    -- so ctEvCoercion is fine.
 
-           _other -> flattenTyVarFinal f ctxt tv
-    } } } } }
+           _other -> flattenTyVarFinal ctxt_ev tv
+    } } }
 
-flattenTyVarFinal f ctxt tv
+flattenTyVarFinal ctxt_ev tv
   = -- Done, but make sure the kind is zonked
-    do { let knd = tyVarKind tv
-       ; (new_knd, _kind_co) <- flatten f ctxt knd
+    do { let kind       = tyVarKind tv
+             kind_fmode = FE { fe_ev = ctxt_ev, fe_mode = FM_SubstOnly }
+       ; (new_knd, _kind_co) <- flatten kind_fmode kind
        ; return (Left (setVarType tv new_knd)) }
 \end{code}
 
 Note [Non-idempotent inert substitution]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 The inert substitution is not idempotent in the broad sense. It is only idempotent in
 that it cannot rewrite the RHS of other inert equalities any further. An example of such
 an inert substitution is:
@@ -732,32 +722,14 @@ Insufficient (non-recursive) rewriting was the reason for #5668.
 %************************************************************************
 
 \begin{code}
-canEvVarsCreated :: [CtEvidence] -> TcS StopOrContinue
-canEvVarsCreated [] = return Stop
-    -- Add all but one to the work list
-    -- and return the first (if any) for futher processing
-canEvVarsCreated (ev : evs)
-  = do { emitWorkNC evs; canEvNC ev }
-          -- Note the "NC": these are fresh goals, not necessarily canonical
-
-emitWorkNC :: [CtEvidence] -> TcS ()
-emitWorkNC evs
-  | null evs  = return ()
-  | otherwise = do { traceTcS "Emitting fresh work" (vcat (map ppr evs))
-                   ; updWorkListTcS (extendWorkListCts (map mk_nc evs)) }
-  where
-    mk_nc ev = mkNonCanonical ev
-
--------------------------
-canEqNC :: CtEvidence -> Type -> Type -> TcS StopOrContinue
+canEqNC :: CtEvidence -> Type -> Type -> TcS (StopOrContinue Ct)
 canEqNC ev ty1 ty2 = can_eq_nc ev ty1 ty1 ty2 ty2
 
-
 can_eq_nc, can_eq_nc' 
    :: CtEvidence 
    -> Type -> Type    -- LHS, after and before type-synonym expansion, resp 
    -> Type -> Type    -- RHS, after and before type-synonym expansion, resp 
-   -> TcS StopOrContinue
+   -> TcS (StopOrContinue Ct)
 
 can_eq_nc ev ty1 ps_ty1 ty2 ps_ty2
   = do { traceTcS "can_eq_nc" $ 
@@ -769,13 +741,13 @@ can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2
   | Just ty1' <- tcView ty1 = can_eq_nc ev ty1' ps_ty1 ty2  ps_ty2
   | Just ty2' <- tcView ty2 = can_eq_nc ev ty1  ps_ty1 ty2' ps_ty2
 
--- Type family on LHS or RHS take priority
-can_eq_nc' ev (TyConApp fn tys) _ ty2 ps_ty2
-  | isSynFamilyTyCon fn
-  = canEqLeafFun ev NotSwapped fn tys ty2 ps_ty2
-can_eq_nc' ev ty1 ps_ty1 (TyConApp fn tys) _
-  | isSynFamilyTyCon fn
-  = canEqLeafFun ev IsSwapped fn tys ty1 ps_ty1
+-- Type family on LHS or RHS take priority over tyvars,
+-- so that  tv ~ F ty gets flattened
+-- Otherwise  F a ~ F a  might not get solved!
+can_eq_nc' ev (TyConApp fn1 tys1) _ ty2 ps_ty2
+  | isSynFamilyTyCon fn1 = can_eq_fam_nc ev NotSwapped fn1 tys1 ty2 ps_ty2
+can_eq_nc' ev ty1 ps_ty1 (TyConApp fn2 tys2) _
+  | isSynFamilyTyCon fn2 = can_eq_fam_nc ev IsSwapped fn2 tys2 ty1 ps_ty1
 
 -- Type variable on LHS or RHS are next
 can_eq_nc' ev (TyVarTy tv1) _ ty2 ps_ty2
@@ -792,7 +764,7 @@ can_eq_nc' ev ty1@(LitTy l1) _ (LitTy l2) _
  | l1 == l2
   = do { when (isWanted ev) $
          setEvBind (ctev_evar ev) (EvCoercion (mkTcNomReflCo ty1))
-       ; return Stop }
+       ; stopWith ev "Equal LitTy" }
 
 -- Decomposable type constructor applications 
 -- Synonyms and type functions (which are not decomposable)
@@ -826,11 +798,11 @@ can_eq_nc' ev s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
           do { traceTcS "Creating implication for polytype equality" $ ppr ev
              ; ev_term <- deferTcSForAllEq Nominal loc (tvs1,body1) (tvs2,body2)
              ; setEvBind orig_ev ev_term
-             ; return Stop } }
+             ; stopWith ev "Deferred polytype equality" } }
  | otherwise
  = do { traceTcS "Ommitting decomposition of given polytype equality" $
         pprEq s1 s2    -- See Note [Do not decompose given polytype equalities]
-      ; return Stop }
+      ; stopWith ev "Discard given polytype equality" }
 
 can_eq_nc' ev (AppTy s1 t1) ps_ty1 ty2 ps_ty2
   = can_eq_app ev NotSwapped s1 t1 ps_ty1 ty2 ps_ty2
@@ -842,21 +814,38 @@ can_eq_nc' ev _ ps_ty1 _ ps_ty2
   = canEqFailure ev ps_ty1 ps_ty2
 
 ------------
+can_eq_fam_nc :: CtEvidence -> SwapFlag
+              -> TyCon -> [TcType]
+              -> TcType -> TcType
+              -> TcS (StopOrContinue Ct)
+-- Canonicalise a non-canonical equality of form (F tys ~ ty)
+--   or the swapped version thereof
+-- Flatten both sides and go round again
+can_eq_fam_nc ev swapped fn tys rhs ps_rhs
+  = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
+       ; (xi_lhs, co_lhs) <- flattenFamApp fmode fn tys
+       ; mb_ct <- rewriteEqEvidence ev swapped xi_lhs rhs co_lhs (mkTcNomReflCo rhs)
+       ; case mb_ct of
+           Stop ev s           -> return (Stop ev s)
+           ContinueWith new_ev -> can_eq_nc new_ev xi_lhs xi_lhs rhs ps_rhs }
+
+------------
 can_eq_app, can_eq_flat_app
     :: CtEvidence -> SwapFlag
-    -> Type -> Type -> Type  -- LHS (s1 t2), after and before type-synonym expansion, resp 
-    -> Type -> Type          -- RHS (ty2),   after and before type-synonym expansion, resp 
-    -> TcS StopOrContinue
+    -> Type -> Type -> Type  -- LHS (s1 t2), after and before type-synonym expansion, resp
+    -> Type -> Type          -- RHS (ty2),   after and before type-synonym expansion, resp
+    -> TcS (StopOrContinue Ct)
 -- See Note [Canonicalising type applications]
 can_eq_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
   =  do { traceTcS "can_eq_app 1" $
           vcat [ ppr ev, ppr swapped, ppr s1, ppr t1, ppr ty2 ]
-        ; (xi_s1, co_s1) <- flatten FMSubstOnly ev s1
+        ; let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
+        ; (xi_s1, co_s1) <- flatten fmode s1
         ; traceTcS "can_eq_app 2" $ vcat [ ppr ev, ppr xi_s1 ]
         ; if s1 `tcEqType` xi_s1
           then can_eq_flat_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
           else
-     do { (xi_t1, co_t1) <- flatten FMSubstOnly ev t1
+     do { (xi_t1, co_t1) <- flatten fmode t1
              -- We flatten t1 as well so that (xi_s1 xi_t1) is well-kinded
              -- If we form (xi_s1 t1) that might (appear) ill-kinded, 
              -- and then crash in a call to typeKind
@@ -867,8 +856,8 @@ can_eq_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
                                      co1 (mkTcNomReflCo ps_ty2)
         ; traceTcS "can_eq_app 4" $ vcat [ ppr ev, ppr xi1, ppr co1 ]
         ; case mb_ct of
-           Nothing     -> return Stop
-           Just new_ev -> can_eq_nc new_ev xi1 xi1 ty2 ps_ty2 }}
+            Stop ev s           -> return (Stop ev s)
+            ContinueWith new_ev -> can_eq_nc new_ev xi1 xi1 ty2 ps_ty2 }}
 
 -- Preconditions: s1  is already flattened
 --                ty2 is not a type variable, so flattening
@@ -887,15 +876,15 @@ can_eq_flat_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
                  xevdecomp x = let xco = evTermCoercion x
                                in [ EvCoercion (mkTcLRCo CLeft xco)
                                   , EvCoercion (mkTcLRCo CRight xco)]
-           ; ctevs <- xCtEvidence ev (XEvTerm [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xevcomp xevdecomp)
-           ; canEvVarsCreated ctevs }
+           ; xCtEvidence ev (XEvTerm [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xevcomp xevdecomp)
+           ; stopWith ev "Decomposed AppTy" }
 
 
 ------------------------
 canDecomposableTyConApp :: CtEvidence
                         -> TyCon -> [TcType]
                         -> TyCon -> [TcType]
-                        -> TcS StopOrContinue
+                        -> TcS (StopOrContinue Ct)
 canDecomposableTyConApp ev tc1 tys1 tc2 tys2
   | tc1 /= tc2 || length tys1 /= length tys2
     -- Fail straight away for better error messages
@@ -906,25 +895,26 @@ canDecomposableTyConApp ev tc1 tys1 tc2 tys2
 
 canDecomposableTyConAppOK :: CtEvidence
                           -> TyCon -> [TcType] -> [TcType]
-                          -> TcS StopOrContinue
+                          -> TcS (StopOrContinue Ct)
 
 canDecomposableTyConAppOK ev tc1 tys1 tys2
   = do { let xcomp xs  = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs))
              xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
              xev = XEvTerm (zipWith mkTcEqPred tys1 tys2) xcomp xdecomp
-       ; ctevs <- xCtEvidence ev xev
-       ; canEvVarsCreated ctevs }
+       ; xCtEvidence ev xev
+       ; stopWith ev "Decomposed TyConApp" }
 
-canEqFailure :: CtEvidence -> TcType -> TcType -> TcS StopOrContinue
+canEqFailure :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct)
 -- See Note [Make sure that insolubles are fully rewritten]
 canEqFailure ev ty1 ty2
-  = do { (s1, co1) <- flatten FMSubstOnly ev ty1
-       ; (s2, co2) <- flatten FMSubstOnly ev ty2
+  = do { let fmode = FE { fe_ev = ev, fe_mode = FM_SubstOnly }
+       ; (s1, co1) <- flatten fmode ty1
+       ; (s2, co2) <- flatten fmode ty2
        ; mb_ct <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
        ; case mb_ct of
-           Just new_ev -> emitInsoluble (mkNonCanonical new_ev)
-           Nothing -> pprPanic "canEqFailure" (ppr ev $$ ppr ty1 $$ ppr ty2)
-       ; return Stop }
+           ContinueWith new_ev -> do { emitInsoluble (mkNonCanonical new_ev)
+                                     ; stopWith new_ev "Definitely not equal" }
+           Stop ev s -> pprPanic "canEqFailure" (s $$ ppr ev $$ ppr ty1 $$ ppr ty2) }
 \end{code}
 
 Note [Canonicalising type applications]
@@ -1044,7 +1034,6 @@ given constraints with wanted constraints.
 
 Suppose we have an inert constraint set
 
-
   tg_1 ~ xig_1         -- givens
   tg_2 ~ xig_2
   ...
@@ -1078,60 +1067,41 @@ inert set is an idempotent subustitution...
     introduce any new ones.
 
 \begin{code}
-canEqLeafFun :: CtEvidence 
-             -> SwapFlag
+canCFunEqCan :: CtEvidence 
              -> TyCon -> [TcType]   -- LHS
-             -> TcType -> TcType    -- RHS
-             -> TcS StopOrContinue
-canEqLeafFun ev swapped fn tys1 ty2 ps_ty2
-  | length tys1 > tyConArity fn
-  = -- Over-saturated type function on LHS: 
-    -- flatten LHS, leaving an AppTy, and go around again
-    do { (xi1, co1) <- flatten FMFullFlatten ev (mkTyConApp fn tys1)
-       ; mb <- rewriteEqEvidence ev swapped xi1 ps_ty2 
-                                 co1 (mkTcNomReflCo ps_ty2)
-       ; case mb of
-            Nothing     -> return Stop
-            Just new_ev -> can_eq_nc new_ev xi1 xi1 ty2 ps_ty2 }
-
-  | otherwise
-  = -- ev :: F tys1 ~ ty2,   if not swapped
-    -- ev :: ty2 ~ F tys1,   if swapped                                    
-    ASSERT( length tys1 == tyConArity fn )  
-        -- Type functions are never under-saturated
-        -- Previous equation checks for over-saturation
-    do { traceTcS "canEqLeafFun" $ pprEq (mkTyConApp fn tys1) ps_ty2
-
-            -- Flatten type function arguments
-            -- cos1 :: xis1 ~ tys1
-            -- co2  :: xi2 ~ ty2
-      ; (xis1,cos1) <- flattenMany FMFullFlatten ev tys1
-      ; (xi2, co2)  <- flatten     FMFullFlatten ev ps_ty2
-
-       ; let fam_head = mkTyConApp fn xis1
-             co1      = mkTcTyConAppCo Nominal fn cos1
-       ; mb <- rewriteEqEvidence ev swapped fam_head xi2 co1 co2
-
-       ; let k1 = typeKind fam_head
-             k2 = typeKind xi2
-       ; case mb of
-            Nothing     -> return Stop
-            Just new_ev | k1 `isSubKind` k2
-                        -- Establish CFunEqCan kind invariant
-                        -> continueWith (CFunEqCan { cc_ev = new_ev, cc_fun = fn
-                                                   , cc_tyargs = xis1, cc_rhs = xi2 })
-                        | otherwise
-                        -> checkKind new_ev fam_head k1 xi2 k2 }
+             -> TcTyVar             -- RHS
+             -> TcS (StopOrContinue Ct)
+-- ^ Canonicalise a CFunEqCan.  We know that 
+--     the arg types are already flat, 
+-- and the RHS is a fsk, which we must *not* substitute.
+-- So just substitute in the LHS
+canCFunEqCan ev fn tys fsk
+  = do { let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
+       ; (tys', cos) <- flattenMany fmode tys
+                        -- cos :: tys' ~ tys
+       ; let lhs_co  = mkTcTyConAppCo Nominal fn cos
+                        -- :: F tys' ~ F tys
+             new_lhs = mkTyConApp fn tys'
+             fsk_ty  = mkTyVarTy fsk
+       ; mb_ev <- rewriteEqEvidence ev NotSwapped new_lhs fsk_ty 
+                                    lhs_co (mkTcNomReflCo fsk_ty)
+       ; case mb_ev of {
+           Stop ev s        -> return (Stop ev s) ;
+           ContinueWith ev' -> 
+
+    do { extendFlatCache fn tys' (ctEvCoercion ev', fsk)
+       ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn
+                                 , cc_tyargs = tys', cc_fsk = fsk }) } } }
 
 ---------------------
 canEqTyVar :: CtEvidence -> SwapFlag
            -> TcTyVar 
            -> TcType -> TcType
-           -> TcS StopOrContinue
+           -> TcS (StopOrContinue Ct)
 -- A TyVar on LHS, but so far un-zonked
 canEqTyVar ev swapped tv1 ty2 ps_ty2              -- ev :: tv ~ s2
   = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped)
-       ; mb_yes <- flattenTyVarOuter FMFullFlatten ev tv1 
+       ; mb_yes <- flattenTyVarOuter ev tv1
        ; case mb_yes of
            Right (ty1, co1) -> -- co1 :: ty1 ~ tv1
                                do { mb <- rewriteEqEvidence ev swapped  ty1 ps_ty2
@@ -1139,10 +1109,12 @@ canEqTyVar ev swapped tv1 ty2 ps_ty2              -- ev :: tv ~ s2
                                   ; traceTcS "canEqTyVar2" (vcat [ppr tv1, ppr ty2, ppr swapped, ppr ty1,
                                                                   ppUnless (isDerived ev) (ppr co1)])
                                   ; case mb of
-                                      Nothing     -> return Stop
-                                      Just new_ev -> can_eq_nc new_ev ty1 ty1 ty2 ps_ty2 }
+                                      Stop ev s           -> return (Stop ev s)
+                                      ContinueWith new_ev -> can_eq_nc new_ev ty1 ty1 ty2 ps_ty2 }
 
-           Left tv1' -> do { (xi2, co2) <- flatten FMFullFlatten ev ps_ty2 -- co2 :: xi2 ~ ps_ty2
+           Left tv1' -> do { let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
+                                 -- Flatten the RHS less vigorously, to avoid gratuitous flattening
+                           ; (xi2, co2) <- flatten fmode ps_ty2 -- co2 :: xi2 ~ ps_ty2
                                            -- Use ps_ty2 to preserve type synonyms if poss
                            ; dflags <- getDynFlags
                            ; canEqTyVar2 dflags ev swapped tv1' xi2 co2 } }
@@ -1153,7 +1125,7 @@ canEqTyVar2 :: DynFlags
             -> TcTyVar      -- olhs
             -> TcType       -- nrhs
             -> TcCoercion   -- nrhs ~ orhs
-            -> TcS StopOrContinue
+            -> TcS (StopOrContinue Ct)
 -- LHS is an inert type variable, 
 -- and RHS is fully rewritten, but with type synonyms
 -- preserved as much as possible
@@ -1171,87 +1143,127 @@ canEqTyVar2 dflags ev swapped tv1 xi2 co2
        ; let k1 = tyVarKind tv1
              k2 = typeKind xi2'
        ; case mb of
-            Nothing     -> return Stop
-            Just new_ev | k2 `isSubKind` k1
-                        -- Establish CTyEqCan kind invariant
-                        -- Reorientation has done its best, but the kinds might
-                        -- simply be incompatible
-                        -> continueWith (CTyEqCan { cc_ev = new_ev
-                                                  , cc_tyvar  = tv1, cc_rhs = xi2' })
-                        | otherwise
-                        -> checkKind new_ev xi1 k1 xi2' k2 }
+            Stop ev s -> return (Stop ev s)
+            ContinueWith new_ev 
+                | k2 `isSubKind` k1
+                -- Establish CTyEqCan kind invariant
+                -- Reorientation has done its best, but the kinds might
+                -- simply be incompatible
+                -> continueWith (CTyEqCan { cc_ev = new_ev
+                                          , cc_tyvar  = tv1, cc_rhs = xi2' })
+                | otherwise
+                -> incompatibleKind new_ev xi1 k1 xi2' k2 }
 
   | otherwise  -- Occurs check error
   = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2
        ; case mb of
-           Nothing     -> return ()
-           Just new_ev -> emitInsoluble (mkNonCanonical new_ev)
-                          -- If we have a ~ [a], it is not canonical, and in particular
-                          -- we don't want to rewrite existing inerts with it, otherwise
-                          -- we'd risk divergence in the constraint solver
-       ; return Stop }
+           Stop ev s           -> return (Stop ev s)
+           ContinueWith new_ev -> do { emitInsoluble (mkNonCanonical new_ev)
+              -- If we have a ~ [a], it is not canonical, and in particular
+              -- we don't want to rewrite existing inerts with it, otherwise
+              -- we'd risk divergence in the constraint solver
+                                     ; stopWith new_ev "Occurs check" } }
   where
     xi1 = mkTyVarTy tv1
     co1 = mkTcNomReflCo xi1
 
 
-canEqTyVarTyVar :: CtEvidence       -- tv1 ~ orhs (or orhs ~ tv1, if swapped)
+
+canEqTyVarTyVar :: CtEvidence           -- tv1 ~ orhs (or orhs ~ tv1, if swapped)
                 -> SwapFlag
-                -> TyVar -> TyVar   -- tv2, tv2
-                -> TcCoercion       -- tv2 ~ orhs
-                -> TcS StopOrContinue
+                -> TcTyVar -> TcTyVar   -- tv2, tv2
+                -> TcCoercion           -- tv2 ~ orhs
+                -> TcS (StopOrContinue Ct)
 -- Both LHS and RHS rewrote to a type variable,
+-- If swapped = NotSwapped, then
+--     rw_orhs = tv1, rw_olhs = orhs
+--     rw_nlhs = tv2, rw_nrhs = xi1
+-- See note [Canonical ordering for equality constraints].
 canEqTyVarTyVar ev swapped tv1 tv2 co2
   | tv1 == tv2
   = do { when (isWanted ev) $
          ASSERT( tcCoercionRole co2 == Nominal )
          setEvBind (ctev_evar ev) (EvCoercion (maybeSym swapped co2))
-       ; return Stop }  
-
-  | reorient_me  -- See note [Canonical ordering for equality constraints].
-                 -- True => the kinds are compatible, 
-                 --         so no need for further sub-kind check
-                 -- If swapped = NotSwapped, then
-                 --     rw_orhs = tv1, rw_olhs = orhs
-                 --     rw_nlhs = tv2, rw_nrhs = xi1
-  = do { mb <- rewriteEqEvidence ev (flipSwap swapped)  xi2 xi1
-                                 co2 (mkTcNomReflCo xi1)
-       ; case mb of
-           Nothing     -> return Stop
-           Just new_ev -> continueWith (CTyEqCan { cc_ev = new_ev
-                                                 , cc_tyvar  = tv2, cc_rhs = xi1 }) }
-
-  | otherwise
-  = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 
-                                 (mkTcNomReflCo xi1) co2
-       ; case mb of
-           Nothing     -> return Stop
-           Just new_ev | k2 `isSubKind` k1
-                       -> continueWith (CTyEqCan { cc_ev = new_ev
-                                                 , cc_tyvar = tv1, cc_rhs = xi2 })
-                       | otherwise
-                       -> checkKind new_ev xi1 k1 xi2 k2 } 
+       ; stopWith ev "Equal tyvars" }
+
+  | incompat_kind   = incompat
+  | isFmvTyVar tv1  = do_fmv swapped            tv1 xi1 xi2 co1 co2
+  | isFmvTyVar tv2  = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
+  | same_kind       = if swap_over then do_swap else no_swap
+  | k1_sub_k2       = do_swap   -- Note [Kind orientation for CTyEqCan]
+  | otherwise       = no_swap   -- k2_sub_k1
   where
-    reorient_me 
-      | k1 `tcEqKind` k2    = tv2 `better_than` tv1
-      | k1 `isSubKind` k2   = True  -- Note [Kind orientation for CTyEqCan]
-      | otherwise           = False -- in TcRnTypes
-
     xi1 = mkTyVarTy tv1
     xi2 = mkTyVarTy tv2
     k1  = tyVarKind tv1
     k2  = tyVarKind tv2
-
-    tv2 `better_than` tv1
-      | isMetaTyVar tv1     = False   -- Never swap a meta-tyvar
-      | isFlatSkolTyVar tv1 = isMetaTyVar tv2
-      | otherwise           = isMetaTyVar tv2 || isFlatSkolTyVar tv2
-                            -- Note [Eliminate flat-skols]
-
-checkKind :: CtEvidence         -- t1~t2
-          -> TcType -> TcKind
-          -> TcType -> TcKind   -- s1~s2, flattened and zonked
-          -> TcS StopOrContinue
+    co1 = mkTcNomReflCo xi1
+    k1_sub_k2     = k1 `isSubKind` k2
+    k2_sub_k1     = k2 `isSubKind` k1
+    same_kind     = k1_sub_k2 && k2_sub_k1
+    incompat_kind = not (k1_sub_k2 || k2_sub_k1)
+
+    no_swap = canon_eq swapped            tv1 xi1 xi2 co1 co2
+    do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
+
+    canon_eq swapped tv1 xi1 xi2 co1 co2
+        -- ev  : tv1 ~ orhs  (not swapped) or   orhs ~ tv1   (swapped)
+        -- co1 : xi1 ~ tv1
+        -- co2 : xi2 ~ tv2
+      = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2
+           ; let mk_ct ev' = CTyEqCan { cc_ev = ev', cc_tyvar = tv1, cc_rhs = xi2 }
+           ; return (fmap mk_ct mb) }
+
+    do_fmv swapped tv1 xi1 xi2 co1 co2
+      | same_kind 
+      = canon_eq swapped tv1 xi1 xi2 co1 co2
+      | otherwise  -- Presumably tv1 `subKind` tv2, which is the wrong way round
+      = ASSERT2( k1_sub_k2, ppr tv1 $$ ppr tv2 )
+        ASSERT2( isWanted ev, ppr ev )  -- Only wanteds have flatten meta-vars
+        do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
+           ; new_ev <- newWantedEvVarNC (ctEvLoc ev) (mkTcEqPred tv_ty xi2)
+           ; emitWorkNC [new_ev]
+           ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev `mkTcTransCo` co2) }
+
+    incompat
+      = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 (mkTcNomReflCo xi1) co2
+           ; case mb of
+               Stop ev s        -> return (Stop ev s)
+               ContinueWith ev' -> incompatibleKind ev' xi1 k1 xi2 k2 }
+
+    swap_over
+      -- If tv1 is touchable, swap only if tv2 is also
+      -- touchable and it's strictly better to update the latter
+      -- But see Note [Avoid unnecessary swaps]
+      | Just lvl1 <- metaTyVarUntouchables_maybe tv1
+      = case metaTyVarUntouchables_maybe tv2 of
+          Nothing   -> False
+          Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
+                    | lvl1 `strictlyDeeperThan` lvl2 -> False
+                    | otherwise                      -> nicer_to_update_tv2
+
+      -- So tv1 is not a meta tyvar
+      -- If only one is a meta tyvar, put it on the left
+      -- This is not because it'll be solved; but becuase
+      -- the floating step looks for meta tyvars on the left
+      | isMetaTyVar tv2 = True
+
+      -- So neither is a meta tyvar
+
+      -- If only one is a flatten tyvar, put it on the left
+      -- See Note [Eliminate flat-skols]
+      | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
+
+      | otherwise = False
+
+    nicer_to_update_tv2
+      =  (isSigTyVar tv1                 && not (isSigTyVar tv2))
+      || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
+
+incompatibleKind :: CtEvidence         -- t1~t2
+                 -> TcType -> TcKind
+                 -> TcType -> TcKind   -- s1~s2, flattened and zonked
+                 -> TcS (StopOrContinue Ct)
 -- LHS and RHS have incompatible kinds, so emit an "irreducible" constraint
 --       CIrredEvCan (NOT CTyEqCan or CFunEqCan)
 -- for the type equality; and continue with the kind equality constraint.
@@ -1260,23 +1272,33 @@ checkKind :: CtEvidence         -- t1~t2
 --
 -- See Note [Equalities with incompatible kinds]
 
-checkKind new_ev s1 k1 s2 k2   -- See Note [Equalities with incompatible kinds]
+incompatibleKind new_ev s1 k1 s2 k2   -- See Note [Equalities with incompatible kinds]
   = ASSERT( isKind k1 && isKind k2 )
     do { traceTcS "canEqLeaf: incompatible kinds" (vcat [ppr k1, ppr k2])
 
          -- Create a derived kind-equality, and solve it
-       ; mw <- newDerived kind_co_loc (mkTcEqPred k1 k2)
-       ; case mw of
-           Nothing  -> return ()
-           Just kev -> emitWorkNC [kev]
+       ; emitNewDerived kind_co_loc (mkTcEqPred k1 k2)
 
          -- Put the not-currently-soluble thing into the inert set
        ; continueWith (CIrredEvCan { cc_ev = new_ev }) }
   where
-    loc = ctev_loc new_ev
+    loc = ctEvLoc new_ev
     kind_co_loc = setCtLocOrigin loc (KindEqOrigin s1 s2 (ctLocOrigin loc))
 \end{code}
 
+Note [Avoid unnecessary swaps]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we swap without actually improving matters, we can get an infnite loop.
+Consider
+    work item:  a ~ b
+   inert item:  b ~ c
+We canonicalise the work-time to (a ~ c).  If we then swap it before
+aeding to the inert set, we'll add (c ~ a), and therefore kick out the
+inert guy, so we get
+   new work item:  b ~ c
+   inert item:     c ~ a
+And now the cycle just repeats
+
 Note [Eliminate flat-skols]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have  [G] Num (F [a])
index a086ec1..dd3c7b4 100644 (file)
@@ -39,12 +39,10 @@ import HscTypes
 import Avail
 
 import Unify( tcUnifyTy )
-import Id( idType )
 import Class
 import Type
 import Kind( isKind )
 import ErrUtils
-import MkId
 import DataCon
 import Maybes
 import RdrName
@@ -369,16 +367,15 @@ tcDeriving tycl_decls inst_decls deriv_decls
         -- Generic1 should use the same TcGenGenerics.MetaTyCons)
         ; (commonAuxs, auxDerivStuff) <- commonAuxiliaries $ map forgetTheta early_specs
 
-        ; overlap_flag <- getOverlapFlag
         ; let (infer_specs, given_specs) = splitEarlyDerivSpec early_specs
-        ; insts1 <- mapM (genInst True overlap_flag commonAuxs) given_specs
+        ; insts1 <- mapM (genInst True commonAuxs) given_specs
 
         -- the stand-alone derived instances (@insts1@) are used when inferring
         -- the contexts for "deriving" clauses' instances (@infer_specs@)
         ; final_specs <- extendLocalInstEnv (map (iSpec . fstOf3) insts1) $
-                         inferInstanceContexts overlap_flag infer_specs
+                         inferInstanceContexts infer_specs
 
-        ; insts2 <- mapM (genInst False overlap_flag commonAuxs) final_specs
+        ; insts2 <- mapM (genInst False commonAuxs) final_specs
 
         ; let (inst_infos, deriv_stuff, maybe_fvs) = unzip3 (insts1 ++ insts2)
         ; loc <- getSrcSpanM
@@ -390,8 +387,8 @@ tcDeriving tycl_decls inst_decls deriv_decls
 
         ; dflags <- getDynFlags
         ; unless (isEmptyBag inst_info) $
-            liftIO (dumpIfSet_dyn dflags Opt_D_dump_deriv "Derived instances"
-                   (ddump_deriving inst_info rn_binds newTyCons famInsts))
+             liftIO (dumpIfSet_dyn dflags Opt_D_dump_deriv "Derived instances"
+                        (ddump_deriving inst_info rn_binds newTyCons famInsts))
 
         ; let all_tycons = map ATyCon (bagToList newTyCons)
         ; gbl_env <- tcExtendGlobalEnv all_tycons $
@@ -402,8 +399,8 @@ tcDeriving tycl_decls inst_decls deriv_decls
         ; return (addTcgDUs gbl_env all_dus, inst_info, rn_binds) }
   where
     ddump_deriving :: Bag (InstInfo Name) -> HsValBinds Name
-                   -> Bag TyCon                 -- ^ Empty data constructors
-                   -> Bag (FamInst)             -- ^ Rep type family instances
+                   -> Bag TyCon               -- ^ Empty data constructors
+                   -> Bag FamInst             -- ^ Rep type family instances
                    -> SDoc
     ddump_deriving inst_infos extra_binds repMetaTys repFamInsts
       =    hang (ptext (sLit "Derived instances:"))
@@ -478,21 +475,19 @@ renameDeriv is_boot inst_infos bagBinds
       inst_info@(InstInfo { iSpec = inst
                           , iBinds = InstBindings
                             { ib_binds = binds
+                            , ib_tyvars = tyvars
                             , ib_pragmas = sigs
-                            , ib_extensions = exts -- only for type-checking
+                            , ib_extensions = exts -- Only for type-checking
                             , ib_derived = sa } })
-        =       -- Bring the right type variables into
-                -- scope (yuk), and rename the method binds
-           ASSERT( null sigs )
-           bindLocalNamesFV (map Var.varName tyvars) $
+        =  ASSERT( null sigs )
+           bindLocalNamesFV tyvars $
            do { (rn_binds, fvs) <- rnMethodBinds (is_cls_nm inst) (\_ -> []) binds
               ; let binds' = InstBindings { ib_binds = rn_binds
-                                           , ib_pragmas = []
-                                           , ib_extensions = exts
-                                           , ib_derived = sa }
+                                          , ib_tyvars = tyvars
+                                          , ib_pragmas = []
+                                          , ib_extensions = exts
+                                          , ib_derived = sa }
               ; return (inst_info { iBinds = binds' }, fvs) }
-        where
-          (tyvars, _) = tcSplitForAllTys (idType (instanceDFunId inst))
 \end{code}
 
 Note [Newtype deriving and unused constructors]
@@ -1704,11 +1699,11 @@ ordered by sorting on type varible, tv, (major key) and then class, k,
 \end{itemize}
 
 \begin{code}
-inferInstanceContexts :: OverlapFlag -> [DerivSpec ThetaOrigin] -> TcM [DerivSpec ThetaType]
+inferInstanceContexts :: [DerivSpec ThetaOrigin] -> TcM [DerivSpec ThetaType]
 
-inferInstanceContexts [] = return []
+inferInstanceContexts [] = return []
 
-inferInstanceContexts oflag infer_specs
+inferInstanceContexts infer_specs
   = do  { traceTc "inferInstanceContexts" $ vcat (map pprDerivSpec infer_specs)
         ; iterate_deriv 1 initial_solutions }
   where
@@ -1734,7 +1729,7 @@ inferInstanceContexts oflag infer_specs
       | otherwise
       = do {      -- Extend the inst info from the explicit instance decls
                   -- with the current set of solutions, and simplify each RHS
-             inst_specs <- zipWithM (mkInstance oflag) current_solns infer_specs
+             inst_specs <- zipWithM newDerivClsInst current_solns infer_specs
            ; new_solns <- checkNoErrs $
                           extendLocalInstEnv inst_specs $
                           mapM gen_soln infer_specs
@@ -1767,15 +1762,10 @@ inferInstanceContexts oflag infer_specs
         the_pred = mkClassPred clas inst_tys
 
 ------------------------------------------------------------------
-mkInstance :: OverlapFlag -> ThetaType -> DerivSpec theta -> TcM ClsInst
-mkInstance overlap_flag theta
-           (DS { ds_name = dfun_name
-               , ds_tvs = tvs, ds_cls = clas, ds_tys = tys })
-  = do { (subst, tvs') <- tcInstSkolTyVars tvs
-       ; return (mkLocalInstance dfun overlap_flag tvs' clas (substTys subst tys)) }
-  where
-    dfun = mkDictFunId dfun_name tvs theta clas tys
-
+newDerivClsInst :: ThetaType -> DerivSpec theta -> TcM ClsInst
+newDerivClsInst theta (DS { ds_name = dfun_name, ds_overlap = overlap_mode
+                          , ds_tvs = tvs, ds_cls = clas, ds_tys = tys })
+  = newClsInst overlap_mode dfun_name tvs theta clas tys
 
 extendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
 -- Add new locally-defined instances; don't bother to check
@@ -1990,22 +1980,21 @@ the renamer.  What a great hack!
 -- case of instances for indexed families.
 --
 genInst :: Bool             -- True <=> standalone deriving
-        -> OverlapFlag
         -> CommonAuxiliaries
-        -> DerivSpec ThetaType 
+        -> DerivSpec ThetaType
         -> TcM (InstInfo RdrName, BagDerivStuff, Maybe Name)
-genInst _standalone_deriv default_oflag comauxs
+genInst _standalone_deriv comauxs
         spec@(DS { ds_tvs = tvs, ds_tc = rep_tycon, ds_tc_args = rep_tc_args
                  , ds_theta = theta, ds_newtype = is_newtype, ds_tys = tys
-                 , ds_overlap = overlap_mode
                  , ds_name = dfun_name, ds_cls = clas, ds_loc = loc })
   | is_newtype   -- See Note [Bindings for Generalised Newtype Deriving]
-  = do { inst_spec <- mkInstance oflag theta spec
+  = do { inst_spec <- newDerivClsInst theta spec
        ; traceTc "genInst/is_newtype" (vcat [ppr loc, ppr clas, ppr tvs, ppr tys, ppr rhs_ty])
        ; return ( InstInfo
                     { iSpec   = inst_spec
                     , iBinds  = InstBindings
                         { ib_binds = gen_Newtype_binds loc clas tvs tys rhs_ty
+                        , ib_tyvars = map Var.varName tvs   -- Scope over bindings
                         , ib_pragmas = []
                         , ib_extensions = [ Opt_ImpredicativeTypes
                                           , Opt_RankNTypes ]
@@ -2015,19 +2004,20 @@ genInst _standalone_deriv default_oflag comauxs
               -- See Note [Newtype deriving and unused constructors]
 
   | otherwise
-  = do { (meth_binds, deriv_stuff) <- genDerivStuff loc clas 
+  = do { (meth_binds, deriv_stuff) <- genDerivStuff loc clas
                                         dfun_name rep_tycon
                                         (lookup rep_tycon comauxs)
-       ; inst_spec <- mkInstance oflag theta spec
+       ; inst_spec <- newDerivClsInst theta spec
+       ; traceTc "newder" (ppr inst_spec)
        ; let inst_info = InstInfo { iSpec   = inst_spec
                                   , iBinds  = InstBindings
                                                 { ib_binds = meth_binds
+                                                , ib_tyvars = map Var.varName tvs
                                                 , ib_pragmas = []
                                                 , ib_extensions = []
                                                 , ib_derived = True } }
        ; return ( inst_info, deriv_stuff, Nothing ) }
   where
-    oflag  = setOverlapModeMaybe default_oflag overlap_mode
     rhs_ty = newTyConInstRhs rep_tycon rep_tc_args
 
 genDerivStuff :: SrcSpan -> Class -> Name -> TyCon
@@ -2036,12 +2026,12 @@ genDerivStuff :: SrcSpan -> Class -> Name -> TyCon
 genDerivStuff loc clas dfun_name tycon comaux_maybe
   | let ck = classKey clas
   , ck `elem` [genClassKey, gen1ClassKey]   -- Special case because monadic
-  = let gk = if ck == genClassKey then Gen0 else Gen1 
+  = let gk = if ck == genClassKey then Gen0 else Gen1
         -- TODO NSF: correctly identify when we're building Both instead of One
         Just metaTyCons = comaux_maybe -- well-guarded by commonAuxiliaries and genInst
     in do
       (binds, faminst) <- gen_Generic_binds gk tycon metaTyCons (nameModule dfun_name)
-      return (binds, DerivFamInst faminst `consBag` emptyBag)
+      return (binds, unitBag (DerivFamInst faminst))
 
   | otherwise                      -- Non-monadic generators
   = do dflags <- getDynFlags
index e9e4c18..9eeaaa2 100644 (file)
@@ -723,10 +723,15 @@ iDFunId info = instanceDFunId (iSpec info)
 
 data InstBindings a
   = InstBindings
-      { ib_binds :: (LHsBinds a)  -- Bindings for the instance methods
-      , ib_pragmas :: [LSig a]    -- User pragmas recorded for generating
-                                  -- specialised instances
-      , ib_extensions :: [ExtensionFlag] -- any extra extensions that should
+      { ib_tyvars  :: [Name]        -- Names of the tyvars from the instance head
+                                    -- that are lexically in scope in the bindings
+
+      , ib_binds   :: (LHsBinds a)  -- Bindings for the instance methods
+
+      , ib_pragmas :: [LSig a]      -- User pragmas recorded for generating
+                                    -- specialised instances
+
+      , ib_extensions :: [ExtensionFlag] -- Any extra extensions that should
                                          -- be enabled when type-checking this
                                          -- instance; needed for
                                          -- GeneralizedNewtypeDeriving
index 210bd79..9e9e551 100644 (file)
@@ -40,6 +40,7 @@ import FastString
 import Outputable
 import SrcLoc
 import DynFlags
+import StaticFlags      ( opt_PprStyle_Debug )
 import ListSetOps       ( equivClasses )
 
 import Data.Maybe
@@ -424,14 +425,15 @@ mkErrorMsg ctxt ct msg
        ; err_info <- mkErrInfo (cec_tidy ctxt) (tcl_ctxt tcl_env)
        ; mkLongErrAt (tcl_loc tcl_env) msg err_info }
 
-type UserGiven = ([EvVar], SkolemInfo, SrcSpan)
+type UserGiven = ([EvVar], SkolemInfo, Bool, SrcSpan)
 
 getUserGivens :: ReportErrCtxt -> [UserGiven]
 -- One item for each enclosing implication
 getUserGivens (CEC {cec_encl = ctxt})
   = reverse $
-    [ (givens, info, tcl_loc env)
-    | Implic {ic_given = givens, ic_env = env, ic_info = info } <- ctxt
+    [ (givens, info, no_eqs, tcl_loc env)
+    | Implic { ic_given = givens, ic_env = env
+             , ic_no_eqs = no_eqs, ic_info = info } <- ctxt
     , not (null givens) ]
 \end{code}
 
@@ -606,12 +608,13 @@ mkEqErr1 ctxt ct
        ; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc)
        ; let (is_oriented, wanted_msg) = mk_wanted_extra tidy_orig
        ; dflags <- getDynFlags
+       ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctLocOrigin loc) $$ pprCtOrigin tidy_orig) 
        ; mkEqErr_help dflags (ctxt {cec_tidy = env1})
                       (wanted_msg $$ binds_msg)
                       ct is_oriented ty1 ty2 }
   where
     ev         = ctEvidence ct
-    loc        = ctev_loc ev
+    loc        = ctEvLoc ev
     (ty1, ty2) = getEqPredTys (ctEvPred ev)
 
     mk_given :: [Implication] -> (CtLoc, SDoc)
@@ -794,7 +797,8 @@ misMatchOrCND ctxt ct oriented ty1 ty2
   | otherwise
   = couldNotDeduce givens ([mkTcEqPred ty1 ty2], orig)
   where
-    givens = getUserGivens ctxt
+    givens = [ given | given@(_, _, no_eqs, _) <- getUserGivens ctxt, not no_eqs]
+             -- Keep only UserGivens that have some equalities
     orig   = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }
 
 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
@@ -809,7 +813,7 @@ pp_givens givens
          (g:gs) ->      ppr_given (ptext (sLit "from the context")) g
                  : map (ppr_given (ptext (sLit "or from"))) gs
     where
-       ppr_given herald (gs, skol_info, loc)
+       ppr_given herald (gs, skol_info, _, loc)
            = hang (herald <+> pprEvVarTheta gs)
                 2 (sep [ ptext (sLit "bound by") <+> ppr skol_info
                        , ptext (sLit "at") <+> ppr loc])
@@ -985,7 +989,9 @@ mkDictErr ctxt cts
   = ASSERT( not (null cts) )
     do { inst_envs <- tcGetInstEnvs
        ; fam_envs  <- tcGetFamInstEnvs
-       ; lookups   <- mapM (lookup_cls_inst inst_envs) cts
+       ; let (ct1:_) = cts  -- ct1 just for its location
+             min_cts = elim_superclasses cts
+       ; lookups   <- mapM (lookup_cls_inst inst_envs) min_cts
        ; let (no_inst_cts, overlap_cts) = partition is_no_inst lookups
 
        -- Report definite no-instance errors,
@@ -996,8 +1002,6 @@ mkDictErr ctxt cts
        ; (ctxt, err) <- mk_dict_err fam_envs ctxt (head (no_inst_cts ++ overlap_cts))
        ; mkErrorMsg ctxt ct1 err }
   where
-    ct1:_ = elim_superclasses cts
-
     no_givens = null (getUserGivens ctxt)
 
     is_no_inst (ct, (matches, unifiers, _))
@@ -1067,7 +1071,7 @@ mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell))
 
     add_to_ctxt_fixes has_ambig_tvs
       | not has_ambig_tvs && all_tyvars
-      , (orig:origs) <- mapMaybe get_good_orig (cec_encl ctxt)
+      , (orig:origs) <- usefulContext ctxt pred 
       = [sep [ ptext (sLit "add") <+> pprParendType pred
                <+> ptext (sLit "to the context of")
              , nest 2 $ ppr_skol orig $$
@@ -1078,11 +1082,6 @@ mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell))
     ppr_skol (PatSkol dc _) = ptext (sLit "the data constructor") <+> quotes (ppr dc)
     ppr_skol skol_info      = ppr skol_info
 
-        -- Do not suggest adding constraints to an *inferred* type signature!
-    get_good_orig ic = case ic_info ic of
-                         SigSkol (InfSigCtxt {}) _ -> Nothing
-                         origin                    -> Just origin
-
     no_inst_msg
       | clas == coercibleClass
       = let (ty1, ty2) = getEqPredTys pred
@@ -1139,7 +1138,7 @@ mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell))
             givens = getUserGivens ctxt
             matching_givens = mapMaybe matchable givens
 
-            matchable (evvars,skol_info,loc)
+            matchable (evvars,skol_info,_,loc)
               = case ev_vars_matching of
                      [] -> Nothing
                      _  -> Just $ hang (pprTheta ev_vars_matching)
@@ -1217,6 +1216,22 @@ mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell))
                            , ptext (sLit "is not in scope") ])
         | otherwise = Nothing
 
+usefulContext :: ReportErrCtxt -> TcPredType -> [SkolemInfo]
+usefulContext ctxt pred
+  = go (cec_encl ctxt)
+  where
+    pred_tvs = tyVarsOfType pred
+    go [] = []
+    go (ic : ics)
+       = case ic_info ic of
+               -- Do not suggest adding constraints to an *inferred* type signature!
+           SigSkol (InfSigCtxt {}) _ -> rest
+           info                      -> info : rest
+       where
+          -- Stop when the context binds a variable free in the predicate
+          rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
+               | otherwise                                 = go ics
+
 show_fixes :: [SDoc] -> SDoc
 show_fixes []     = empty
 show_fixes (f:fs) = sep [ ptext (sLit "Possible fix:")
@@ -1408,7 +1423,8 @@ relevantBindings want_filtering ctxt ct
                                  <+> ppr (getSrcLoc id)))]
                   new_seen = tvs_seen `unionVarSet` id_tvs
 
-            ; if (want_filtering && id_tvs `disjointVarSet` ct_tvs)
+            ; if (want_filtering && not opt_PprStyle_Debug 
+                                 && id_tvs `disjointVarSet` ct_tvs)
                        -- We want to filter out this binding anyway
                        -- so discard it silently
               then go tidy_env n_left tvs_seen docs discards tc_bndrs
@@ -1464,7 +1480,7 @@ solverDepthErrorTcS cnt ev
              tidy_pred = tidyType tidy_env pred
        ; failWithTcM (tidy_env, hang (msg cnt) 2 (ppr tidy_pred)) }
   where
-    loc   = ctev_loc ev
+    loc   = ctEvLoc ev
     depth = ctLocDepth loc
     value = subGoalCounterValue cnt depth
     msg CountConstraints =
index 3b2a3d6..d0481c8 100644 (file)
@@ -28,6 +28,7 @@ module TcEvidence (
   mkTcAxiomRuleCo,
   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo,
   isTcReflCo, getTcCoVar_maybe,
+  tcLiftCoSubst, 
   tcCoercionRole, eqVarRole
   ) where
 #include "HsVersions.h"
@@ -339,6 +340,28 @@ coVarsOfTcCo tc_co
 
     get_bndrs :: Bag EvBind -> VarSet
     get_bndrs = foldrBag (\ (EvBind b _) bs -> extendVarSet bs b) emptyVarSet
+
+tcLiftCoSubst :: TcTyVar -> TcCoercion -> TcType -> TcCoercion
+-- Substitute the_tv -> the_co in the given type, at Nominal role
+-- Like Coercion.liftCoSubst, but for TcCoercion, and 
+-- specialised for Nominal role
+tcLiftCoSubst the_tv the_co ty
+ = ASSERT( tcCoercionRole the_co == Nominal )
+   go ty
+ where
+   go ty@(TyVarTy tv)
+     | tv == the_tv = the_co
+     | otherwise    = TcRefl Nominal ty
+   go ty@(LitTy {}) = TcRefl Nominal ty
+
+   go (AppTy ty1 ty2)   = mkTcAppCo         (go ty1) (go ty2)
+   go (FunTy ty1 ty2)   = mkTcFunCo Nominal (go ty1) (go ty2)
+   go (TyConApp tc tys) = mkTcTyConAppCo Nominal tc (map go tys)
+                          -- We are building a Nominal coercion, so the TyCon's
+                          -- args must all be Nominal coercions too, regardless
+                          -- of the TyCon's arg rules (c.f. Coercion.tyConRolesX)
+   go ty@(ForAllTy _ _) = pprPanic "tcLiftCoSubst" (ppr ty)
+     -- Substituting under a for-all is awkward
 \end{code}
 
 Pretty printing
index 29020b4..487ee4f 100644 (file)
@@ -698,7 +698,7 @@ tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
 
               mk_inst_ty :: TvSubst -> (TKVar, TcType) -> TcM (TvSubst, TcType)
               -- Deals with instantiation of kind variables
-              --   c.f. TcMType.tcInstTyVarsX
+              --   c.f. TcMType.tcInstTyVars
               mk_inst_ty subst (tv, result_inst_ty)
                 | is_fixed_tv tv   -- Same as result type
                 = return (extendTvSubst subst tv result_inst_ty, result_inst_ty)
@@ -706,7 +706,8 @@ tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
                 = do { new_ty <- newFlexiTyVarTy (TcType.substTy subst (tyVarKind tv))
                      ; return (extendTvSubst subst tv new_ty, new_ty) }
 
-        ; (_, result_inst_tys, result_subst) <- tcInstTyVars con1_tvs
+        ; (result_subst, con1_tvs') <- tcInstTyVars con1_tvs
+        ; let result_inst_tys = mkTyVarTys con1_tvs'
 
         ; (scrut_subst, scrut_inst_tys) <- mapAccumLM mk_inst_ty emptyTvSubst
                                                       (con1_tvs `zip` result_inst_tys)
@@ -734,7 +735,7 @@ tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
         -- Phew!
         ; return $ mkHsWrapCo co_res $
           RecordUpd (mkLHsWrap scrut_co record_expr') rbinds'
-                                   relevant_cons scrut_inst_tys result_inst_tys  }
+                    relevant_cons scrut_inst_tys result_inst_tys  }
   where
     upd_fld_names = hsRecFields rbinds
 
@@ -1111,11 +1112,12 @@ instantiateOuter orig id
   = return (HsVar id, tau)
 
   | otherwise
-  = do { (_, tys, subst) <- tcInstTyVars tvs
-       ; doStupidChecks id tys
-       ; let theta' = substTheta subst theta
-       ; traceTc "Instantiating" (ppr id <+> text "with" <+> (ppr tys $$ ppr theta'))
-       ; wrap <- instCall orig tys theta'
+  = do { (subst, tvs') <- tcInstTyVars tvs
+       ; let tys'   = mkTyVarTys tvs'
+             theta' = substTheta subst theta
+       ; doStupidChecks id tys'
+       ; traceTc "Instantiating" (ppr id <+> text "with" <+> (ppr tys' $$ ppr theta'))
+       ; wrap <- instCall orig tys' theta'
        ; return (mkHsWrap wrap (HsVar id), TcType.substTy subst tau) }
   where
     (tvs, theta, tau) = tcSplitSigmaTy (idType id)
index e416aaf..31e31ed 100644 (file)
@@ -85,7 +85,7 @@ data DerivStuff     -- Please add this auxiliary stuff
 
   -- Generics
   | DerivTyCon TyCon                   -- New data types
-  | DerivFamInst (FamInst)             -- New type family instances
+  | DerivFamInst FamInst               -- New type family instances
 
   -- New top-level auxiliary bindings
   | DerivHsBind (LHsBind RdrName, LSig RdrName) -- Also used for SYB
index c3efb32..fed7583 100644 (file)
@@ -135,6 +135,7 @@ metaTyConsToDerivStuff tc metaDts =
         d_metaTycon = metaD metaDts
         d_inst   = mk_inst dClas d_metaTycon d_dfun_name
         d_binds  = InstBindings { ib_binds = dBinds
+                                , ib_tyvars = []
                                 , ib_pragmas = []
                                 , ib_extensions = []
                                 , ib_derived = True }
@@ -145,6 +146,7 @@ metaTyConsToDerivStuff tc metaDts =
         c_insts = [ mk_inst cClas c ds
                   | (c, ds) <- myZip1 c_metaTycons c_dfun_names ]
         c_binds = [ InstBindings { ib_binds = c
+                                 , ib_tyvars = []
                                  , ib_pragmas = []
                                  , ib_extensions = []
                                  , ib_derived = True }
@@ -157,6 +159,7 @@ metaTyConsToDerivStuff tc metaDts =
         s_insts = map (map (\(s,ds) -> mk_inst sClas s ds))
                       (myZip2 s_metaTycons s_dfun_names)
         s_binds = [ [ InstBindings { ib_binds = s
+                                   , ib_tyvars = []
                                    , ib_pragmas = []
                                    , ib_extensions = []
                                    , ib_derived = True }
@@ -504,6 +507,7 @@ tc_mkRepFamInsts gk tycon metaDts mod =
                         (nameSrcSpan (tyConName tycon))
 
      ; let axiom = mkSingleCoAxiom rep_name tyvars fam_tc appT repTy
+     ; traceTc "tc_mkrep" (ppr fam_tc $$ ppr tyvars)
      ; newFamInst SynFamilyInst axiom  }
 
 --------------------------------------------------------------------------------
index c9f0e2f..d6f237f 100644 (file)
@@ -425,9 +425,11 @@ tc_hs_type hs_ty@(HsPArrTy elt_ty) exp_kind
 tc_hs_type hs_ty@(HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind@(EK exp_k _ctxt)
      -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
   | Just tup_sort <- tupKindSort_maybe exp_k
-  = tc_tuple hs_ty tup_sort hs_tys exp_kind
+  = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
+    tc_tuple hs_ty tup_sort hs_tys exp_kind
   | otherwise
-  = do { (tys, kinds) <- mapAndUnzipM tc_infer_lhs_type hs_tys
+  = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys) 
+       ; (tys, kinds) <- mapAndUnzipM tc_infer_lhs_type hs_tys
        ; kinds <- mapM zonkTcKind kinds
            -- Infer each arg type separately, because errors can be
            -- confusing if we give them a shared kind.  Eg Trac #7410
@@ -554,7 +556,8 @@ tc_tuple hs_ty tup_sort tys exp_kind
 
 finish_tuple :: HsType Name -> TupleSort -> [TcType] -> ExpKind -> TcM TcType
 finish_tuple hs_ty tup_sort tau_tys exp_kind
-  = do { checkExpectedKind hs_ty res_kind exp_kind
+  = do { traceTc "finish_tuple" (ppr res_kind $$ ppr exp_kind $$ ppr exp_kind)
+       ; checkExpectedKind hs_ty res_kind exp_kind
        ; checkWiredInTyCon tycon
        ; return (mkTyConApp tycon tau_tys) }
   where
index 3dc295a..7e73c85 100644 (file)
@@ -540,17 +540,11 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
         ; dfun_name <- newDFunName clas inst_tys (getLoc poly_ty)
                 -- Dfun location is that of instance *header*
 
-        ; overlap_flag <-
-            do defaultOverlapFlag <- getOverlapFlag
-               return $ setOverlapModeMaybe defaultOverlapFlag overlap_mode
-        ; (subst, tyvars') <- tcInstSkolTyVars tyvars
-        ; let dfun      = mkDictFunId dfun_name tyvars theta clas inst_tys
-              ispec     = mkLocalInstance dfun overlap_flag tyvars' clas (substTys subst inst_tys)
-                            -- Be sure to freshen those type variables,
-                            -- so they are sure not to appear in any lookup
-              inst_info = InstInfo { iSpec  = ispec
+        ; ispec <- newClsInst overlap_mode dfun_name tyvars theta clas inst_tys
+        ; let inst_info = InstInfo { iSpec  = ispec
                                    , iBinds = InstBindings
                                      { ib_binds = binds
+                                     , ib_tyvars = map Var.varName tyvars -- Scope over bindings
                                      , ib_pragmas = uprags
                                      , ib_extensions = []
                                      , ib_derived = False } }
@@ -821,7 +815,6 @@ So right here in tcInstDecls2 we must re-extend the type envt with
 the default method Ids replete with their INLINE pragmas.  Urk.
 
 \begin{code}
-
 tcInstDecl2 :: InstInfo Name -> TcM (LHsBinds Id)
             -- Returns a binding for the dfun
 tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
@@ -839,7 +832,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
 
        ; dfun_ev_vars <- newEvVars dfun_theta
 
-       ; (sc_binds, sc_ev_vars) <- tcSuperClasses dfun_id inst_tyvars dfun_ev_vars sc_theta'
+       ; sc_ev_vars <- tcSuperClasses dfun_id inst_tyvars dfun_ev_vars sc_theta'
 
        -- Deal with 'SPECIALISE instance' pragmas
        -- See Note [SPECIALISE instance pragmas]
@@ -847,11 +840,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
 
         -- Typecheck the methods
        ; (meth_ids, meth_binds)
-           <- tcExtendTyVarEnv inst_tyvars $
-                -- The inst_tyvars scope over the 'where' part
-                -- Those tyvars are inside the dfun_id's type, which is a bit
-                -- bizarre, but OK so long as you realise it!
-              tcInstanceMethods dfun_id clas inst_tyvars dfun_ev_vars
+           <- tcInstanceMethods dfun_id clas inst_tyvars dfun_ev_vars
                                 inst_tys spec_inst_info
                                 op_items ibinds
 
@@ -882,9 +871,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
              arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
 
                 -- Do not inline the dfun; instead give it a magic DFunFunfolding
-                -- See Note [ClassOp/DFun selection]
-                -- See also note [Single-method classes]
-             (dfun_id_w_fun, dfun_spec_prags)
+             (_dfun_id_w_fun, dfun_spec_prags)
                 | isNewTyCon class_tc
                 = ( dfun_id `setInlinePragma` alwaysInlinePragma { inl_sat = Just 0 }
                   , SpecPrags [] )   -- Newtype dfuns just inline unconditionally,
@@ -901,13 +888,13 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                          map mk_meth_app meth_ids
              mk_meth_app meth_id = Var meth_id `mkTyApps` inst_tv_tys `mkVarApps` dfun_ev_vars
 
-             export = ABE { abe_wrap = idHsWrapper, abe_poly = dfun_id_w_fun
+             export = ABE { abe_wrap = idHsWrapper, abe_poly = dfun_id
                           , abe_mono = self_dict, abe_prags = dfun_spec_prags }
                           -- NB: see Note [SPECIALISE instance pragmas]
              main_bind = AbsBinds { abs_tvs = inst_tyvars
                                   , abs_ev_vars = dfun_ev_vars
                                   , abs_exports = [export]
-                                  , abs_ev_binds = sc_binds
+                                  , abs_ev_binds = emptyTcEvBinds
                                   , abs_binds = unitBag dict_bind }
 
        ; return (unitBag (L loc main_bind) `unionBags`
@@ -919,22 +906,23 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
 
 ------------------------------
 tcSuperClasses :: DFunId -> [TcTyVar] -> [EvVar] -> TcThetaType
-               -> TcM (TcEvBinds, [EvVar])
+               -> TcM [EvVar]
 -- See Note [Silent superclass arguments]
 tcSuperClasses dfun_id inst_tyvars dfun_ev_vars sc_theta
+  | null inst_tyvars && null dfun_ev_vars
+  = emitWanteds ScOrigin sc_theta
+
+  | otherwise
   = do {   -- Check that all superclasses can be deduced from
            -- the originally-specified dfun arguments
-       ; (sc_binds, sc_evs) <- checkConstraints InstSkol inst_tyvars orig_ev_vars $
-                               emitWanteds ScOrigin sc_theta
+       ; _ <- checkConstraints InstSkol inst_tyvars orig_ev_vars $
+              emitWanteds ScOrigin sc_theta
 
-       ; if null inst_tyvars && null dfun_ev_vars
-         then return (sc_binds,       sc_evs)
-         else return (emptyTcEvBinds, sc_lam_args) }
+       ; return (map (find dfun_ev_vars) sc_theta) }
   where
     n_silent     = dfunNSilent dfun_id
     orig_ev_vars = drop n_silent dfun_ev_vars
 
-    sc_lam_args = map (find dfun_ev_vars) sc_theta
     find [] pred
       = pprPanic "tcInstDecl2" (ppr dfun_id $$ ppr (idType dfun_id) $$ ppr pred)
     find (ev:evs) pred
@@ -1195,10 +1183,13 @@ tcInstanceMethods :: DFunId -> Class -> [TcTyVar]
 tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                   (spec_inst_prags, prag_fn)
                   op_items (InstBindings { ib_binds = binds
+                                         , ib_tyvars = lexical_tvs
                                          , ib_pragmas = sigs
                                          , ib_extensions = exts
                                          , ib_derived    = is_derived })
-  = do { traceTc "tcInstMeth" (ppr sigs $$ ppr binds)
+  = tcExtendTyVarEnv2 (lexical_tvs `zip` tyvars) $
+       -- The lexical_tvs scope over the 'where' part
+    do { traceTc "tcInstMeth" (ppr sigs $$ ppr binds)
        ; let hs_sig_fn = mkHsSigFun sigs
        ; checkMinimalDefinition
        ; set_exts exts $ mapAndUnzipM (tc_item hs_sig_fn) op_items }
index 747eb91..e0b2d9f 100644 (file)
@@ -2,8 +2,8 @@
 {-# LANGUAGE CPP #-}
 
 module TcInteract (
-     solveInteractGiven,  -- Solves [EvVar],GivenLoc
-     solveInteract,       -- Solves Cts
+     solveFlatGivens,    -- Solves [EvVar],GivenLoc
+     solveFlatWanteds    -- Solves Cts
   ) where
 
 #include "HsVersions.h"
@@ -38,8 +38,6 @@ import TcErrors
 import TcSMonad
 import Bag
 
-import Control.Monad ( foldM )
-import Data.Maybe ( catMaybes )
 import Data.List( partition )
 
 import VarEnv
@@ -82,46 +80,34 @@ If in Step 1 no such element exists, we have exceeded our context-stack
 depth and will simply fail.
 
 \begin{code}
-solveInteractGiven :: CtLoc -> [TcTyVar] -> [EvVar] -> TcS (Bool, [TcTyVar])
-solveInteractGiven loc old_fsks givens
+solveFlatGivens :: CtLoc -> [EvVar] -> TcS ()
+solveFlatGivens loc givens
   | null givens  -- Shortcut for common case
-  = return (True, old_fsks)
+  = return ()
   | otherwise
-  = do { implics1 <- solveInteract fsk_bag
-
-       ; (no_eqs, more_fsks, implics2) <- getGivenInfo (solveInteract given_bag)
-       ; MASSERT( isEmptyBag implics1 && isEmptyBag implics2 )
-           -- empty implics because we discard Given equalities between
-           -- foralls (see Note [Do not decompose given polytype equalities]
-           -- in TcCanonical), and those are the ones that can give
-           -- rise to new implications
-
-       ; return (no_eqs, more_fsks ++ old_fsks) }
+  = solveFlats given_bag
   where
     given_bag = listToBag [ mkNonCanonical $ CtGiven { ctev_evtm = EvId ev_id
                                                      , ctev_pred = evVarPred ev_id
                                                      , ctev_loc = loc }
                           | ev_id <- givens ]
 
-    -- See Note [Given flatten-skolems] in TcSMonad
-    fsk_bag = listToBag [ mkNonCanonical $ CtGiven { ctev_evtm = EvCoercion (mkTcNomReflCo tv_ty)
-                                                   , ctev_pred = pred
-                                                   , ctev_loc = loc }
-                        | tv <- old_fsks
-                        , let FlatSkol fam_ty = tcTyVarDetails tv
-                              tv_ty = mkTyVarTy tv
-                              pred  = mkTcEqPred fam_ty tv_ty
-                        ]
+solveFlatWanteds :: Cts -> TcS WantedConstraints
+solveFlatWanteds wanteds
+  = do { solveFlats wanteds
+       ; getInertUnsolved }
 
 -- The main solver loop implements Note [Basic Simplifier Plan]
 ---------------------------------------------------------------
-solveInteract :: Cts -> TcS (Bag Implication)
+solveFlats :: Cts -> TcS ()
 -- Returns the final InertSet in TcS
 -- Has no effect on work-list or residual-iplications
-solveInteract cts
-  = {-# SCC "solveInteract" #-}
-    withWorkList cts $
+-- The constraints are initially examined in left-to-right order
+
+solveFlats cts
+  = {-# SCC "solveFlats" #-}
     do { dyn_flags <- getDynFlags
+       ; updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
        ; solve_loop (maxSubGoalDepth dyn_flags) }
   where
     solve_loop max_depth
@@ -136,7 +122,7 @@ solveInteract cts
                 -> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
 
 type WorkItem = Ct
-type SimplifierStage = WorkItem -> TcS StopOrContinue
+type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
 
 data SelectWorkItem
        = NoWorkRemaining      -- No more work left (effectively we're done!)
@@ -177,26 +163,27 @@ runSolverPipeline pipeline workItem
 
        ; final_is <- getTcSInerts
        ; case final_res of
-           Stop            -> do { traceTcS "End solver pipeline (discharged) }"
-                                       (ptext (sLit "inerts    = ") <+> ppr final_is)
+           Stop ev s       -> do { traceFireTcS ev s
+                                 ; traceTcS "End solver pipeline (discharged) }"
+                                       (ptext (sLit "inerts =") <+> ppr final_is)
                                  ; return () }
-           ContinueWith ct -> do { traceFireTcS ct (ptext (sLit "Kept as inert"))
+           ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (ptext (sLit "Kept as inert"))
                                  ; traceTcS "End solver pipeline (not discharged) }" $
-                                       vcat [ ptext (sLit "final_item = ") <+> ppr ct
+                                       vcat [ ptext (sLit "final_item =") <+> ppr ct
                                             , pprTvBndrs (varSetElems $ tyVarsOfCt ct)
-                                            , ptext (sLit "inerts     = ") <+> ppr final_is]
+                                            , ptext (sLit "inerts     =") <+> ppr final_is]
                                  ; insertInertItemTcS ct }
        }
-  where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue -> TcS StopOrContinue
-        run_pipeline [] res = return res
-        run_pipeline _ Stop = return Stop
+  where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct 
+                     -> TcS (StopOrContinue Ct)
+        run_pipeline [] res        = return res
+        run_pipeline _ (Stop ev s) = return (Stop ev s)
         run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
           = do { traceTcS ("runStage " ++ stg_name ++ " {")
                           (text "workitem   = " <+> ppr ct)
                ; res <- stg ct
                ; traceTcS ("end stage " ++ stg_name ++ " }") empty
-               ; run_pipeline stgs res
-               }
+               ; run_pipeline stgs res }
 \end{code}
 
 Example 1:
@@ -266,27 +253,21 @@ or, equivalently,
 
 type StopNowFlag = Bool    -- True <=> stop after this interaction
 
-interactWithInertsStage :: WorkItem -> TcS StopOrContinue
+interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
 -- Precondition: if the workitem is a CTyEqCan then it will not be able to
 -- react with anything at this stage.
 
 interactWithInertsStage wi
   = do { inerts <- getTcSInerts
        ; let ics = inert_cans inerts
-       ; (mb_ics', stop) <- case wi of
+       ; case wi of
              CTyEqCan    {} -> interactTyVarEq ics wi
              CFunEqCan   {} -> interactFunEq   ics wi
              CIrredEvCan {} -> interactIrred   ics wi
              CDictCan    {} -> interactDict    ics wi
-             _ -> pprPanic "interactWithInerts" (ppr wi)
+             _ -> pprPanic "interactWithInerts" (ppr wi) }
                 -- CHoleCan are put straight into inert_frozen, so never get here
                 -- CNonCanonical have been canonicalised
-       ; case mb_ics' of
-           Just ics' -> setTcSInerts (inerts { inert_cans = ics' })
-           Nothing   -> return ()
-       ; case stop of
-            True  -> return Stop
-            False -> return (ContinueWith wi) }
 \end{code}
 
 \begin{code}
@@ -336,7 +317,7 @@ solveOneFromTheOther ev_i ev_w
 -- we can rewrite them. We can never improve using this:
 -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
 -- mean that (ty1 ~ ty2)
-interactIrred :: InertCans -> Ct -> TcS (Maybe InertCans, StopNowFlag)
+interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 
 interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
   | let pred = ctEvPred ev_w
@@ -346,16 +327,19 @@ interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
   , let ctev_i = ctEvidence ct_i
   = ASSERT( null rest )
     do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
-       ; let inerts' = case inert_effect of
-                          IRKeep    -> Nothing
-                          IRDelete  -> Just (inerts { inert_irreds = others })
-                          IRReplace -> Just (inerts { inert_irreds = extendCts others workItem })
-       ; when stop_now $ traceFireTcS workItem $
-         ptext (sLit "Irred equal") <+> parens (ppr inert_effect)
-       ; return (inerts', stop_now) }
+       ; case inert_effect of
+            IRKeep    -> return ()
+            IRDelete  -> updInertIrreds (\_ -> others)
+            IRReplace -> updInertIrreds (\_ -> others `snocCts` workItem)
+                         -- These const upd's assume that solveOneFromTheOther
+                         -- has no side effects on InertCans
+       ; if stop_now then
+            return (Stop ev_w (ptext (sLit "Irred equal") <+> parens (ppr inert_effect)))
+       ; else
+            continueWith workItem }
 
   | otherwise
-  = return (Nothing, False)
+  = continueWith workItem
 
 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
 \end{code}
@@ -367,19 +351,19 @@ interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
 *********************************************************************************
 
 \begin{code}
-interactDict :: InertCans -> Ct -> TcS (Maybe InertCans, StopNowFlag)
+interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
-  | let dicts = inert_dicts inerts
-  , Just ct_i <- findDict (inert_dicts inerts) cls tys
+  | Just ct_i <- findDict (inert_dicts inerts) cls tys
   , let ctev_i = ctEvidence ct_i
   = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
-       ; let inerts' = case inert_effect of
-                          IRKeep    -> Nothing
-                          IRDelete  -> Just (inerts { inert_dicts = delDict dicts cls tys })
-                          IRReplace -> Just (inerts { inert_dicts = addDict dicts cls tys workItem })
-       ; when stop_now $ traceFireTcS workItem $
-         ptext (sLit "Dict equal") <+> parens (ppr inert_effect)
-       ; return (inerts', stop_now) }
+       ; case inert_effect of
+           IRKeep    -> return ()
+           IRDelete  -> updInertDicts $ \ ds -> delDict ds cls tys
+           IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
+       ; if stop_now then
+            return (Stop ev_w (ptext (sLit "Dict equal") <+> parens (ppr inert_effect)))
+         else 
+            continueWith workItem }
 
   | cls `hasKey` ipClassNameKey
   , isGiven ev_w
@@ -389,16 +373,17 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
   = do { mapBagM_ (addFunDepWork workItem) (findDictsByClass (inert_dicts inerts) cls)
                -- Standard thing: create derived fds and keep on going. Importantly we don't
                -- throw workitem back in the worklist because this can cause loops (see #5236)
-       ; return (Nothing, False) }
+       ; continueWith workItem  }
 
 interactDict _ wi = pprPanic "interactDict" (ppr wi)
 
-interactGivenIP :: InertCans -> Ct -> TcS (Maybe InertCans, StopNowFlag)
+interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
 -- Work item is Given (?x:ty)
 -- See Note [Shadowing of Implicit Parameters]
-interactGivenIP inerts workItem@(CDictCan { cc_class = cls, cc_tyargs = tys@(ip_str:_) })
-  = do { traceFireTcS workItem $ ptext (sLit "Given IP")
-       ; return (Just (inerts { inert_dicts = addDict filtered_dicts cls tys workItem }), True) }
+interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
+                                          , cc_tyargs = tys@(ip_str:_) })
+  = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
+       ; stopWith ev "Given IP" }
   where
     dicts           = inert_dicts inerts
     ip_dicts        = findDictsByClass dicts cls
@@ -417,21 +402,13 @@ addFunDepWork work_ct inert_ct
   = do {  let fd_eqns :: [Equation CtLoc]
               fd_eqns = [ eqn { fd_loc = derived_loc }
                         | eqn <- improveFromAnother inert_pred work_pred ]
-       ; fd_work <- rewriteWithFunDeps fd_eqns
+       ; rewriteWithFunDeps fd_eqns
                 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
                 -- NB: We do create FDs for given to report insoluble equations that arise
                 -- from pairs of Givens, and also because of floating when we approximate
                 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
                 -- Also see Note [When improvement happens]
-
-       ; traceTcS "addFuNDepWork"
-                  (vcat [ text "inertItem =" <+> ppr inert_ct
-                        , text "workItem  =" <+> ppr work_ct
-                        , text "fundeps =" <+> ppr fd_work ])
-
-       ; case fd_work of
-           [] -> return ()
-           _  -> updWorkListTcS (extendWorkListEqs fd_work)    }
+    }
   where
     work_pred  = ctPred work_ct
     inert_pred = ctPred inert_ct
@@ -499,93 +476,72 @@ I can think of two ways to fix this:
 *********************************************************************************
 
 \begin{code}
-interactFunEq :: InertCans -> Ct -> TcS (Maybe InertCans, StopNowFlag)
+interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
+-- Try interacting the work item with the inert set
 interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
-                                         , cc_tyargs = args, cc_rhs = rhs })
-  | (CFunEqCan { cc_ev = ev_i, cc_rhs = rhs_i } : _) <- matching_inerts
-  , ev_i `canRewrite` ev
-  = do { traceTcS "interact with inerts: FunEq/FunEq" $
-         vcat [ text "workItem =" <+> ppr workItem
-              , text "inertItem=" <+> ppr ev_i ]
-       ; solveFunEq ev_i rhs_i ev rhs
-       ; return (Nothing, True) }
-
-  | (ev_i : _) <- [ ev_i | CFunEqCan { cc_ev = ev_i, cc_rhs = rhs_i } <- matching_inerts
-                         , rhs_i `tcEqType` rhs    -- Duplicates
-                         , ev_i `canRewriteOrSame` ev ]
-  = do { when (isWanted ev) (setEvBind (ctev_evar ev) (ctEvTerm ev_i))
-       ; return (Nothing, True) }
-
-  | eq_is@(eq_i : _) <- matching_inerts
-  , ev `canRewrite` ctEvidence eq_i   -- This is unusual
-  = do { let solve (CFunEqCan { cc_ev = ev_i, cc_rhs = rhs_i })
-                      = solveFunEq ev rhs ev_i rhs_i
-             solve ct = pprPanic "interactFunEq" (ppr ct)
-       ; mapM_ solve eq_is
-       ; return (Just (inerts { inert_funeqs = replaceFunEqs funeqs tc args workItem }), True) }
-
-  | (CFunEqCan { cc_rhs = rhs_i } : _) <- matching_inerts
-  = -- We have  F ty ~ r1, F ty ~ r2, but neither can rewrite the other;
-    -- for example, they might both be Derived, or both Wanted
-    -- So we generate a new derived equality r1~r2
-    do { mb <- newDerived loc (mkTcEqPred rhs_i rhs)
-       ; case mb of
-           Just x  -> updWorkListTcS (extendWorkListEq (mkNonCanonical x))
-           Nothing -> return ()
-       ; return (Nothing, False) }
-
-   | Just ops <- isBuiltInSynFamTyCon_maybe tc
-   = do { let is = findFunEqsByTyCon funeqs tc
-        ; traceTcS "builtInCandidates: " $ ppr is
-        ; let interact = sfInteractInert ops args rhs
-        ; impMbs <- sequence
-                 [ do mb <- newDerived (ctev_loc iev) (mkTcEqPred lhs_ty rhs_ty)
-                      case mb of
-                        Just x -> return $ Just $ mkNonCanonical x
-                        Nothing -> return Nothing
-                 | CFunEqCan { cc_tyargs = iargs
-                             , cc_rhs = ixi
-                             , cc_ev = iev } <- is
-                 , Pair lhs_ty rhs_ty <- interact iargs ixi
-                 ]
-        ; let imps = catMaybes impMbs
-        ; unless (null imps) $ updWorkListTcS (extendWorkListEqs imps)
-        ; return (Nothing, False) }
+                                         , cc_tyargs = args, cc_fsk = fsk })
+  | Just (CFunEqCan { cc_ev = ev_i, cc_fsk = fsk_i }) <- matching_inerts
+  = if ev_i `canRewriteOrSame` ev
+    then  -- Rewrite work-item using inert
+      do { traceTcS "reactFunEq (discharge work item):" $
+           vcat [ text "workItem =" <+> ppr workItem
+                , text "inertItem=" <+> ppr ev_i ]
+         ; reactFunEq ev_i fsk_i ev fsk
+         ; stopWith ev "Inert rewrites work item" }
+    else  -- Rewrite intert using work-item
+      do { traceTcS "reactFunEq (rewrite inert item):" $
+           vcat [ text "workItem =" <+> ppr workItem
+                , text "inertItem=" <+> ppr ev_i ]
+         ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
+               -- Do the updInertFunEqs before the reactFunEq, so that
+               -- we don't kick out the inertItem as well as consuming it!
+         ; reactFunEq ev fsk ev_i fsk_i
+         ; stopWith ev "Work item rewrites inert" }
+
+  | Just ops <- isBuiltInSynFamTyCon_maybe tc
+  = do { let matching_funeqs = findFunEqsByTyCon funeqs tc
+       ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk)
+             do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev })
+                = mapM_ (emitNewDerivedEq (ctEvLoc iev)) 
+                        (interact iargs (lookupFlattenTyVar eqs ifsk))
+             do_one ct = pprPanic "interactFunEq" (ppr ct)
+       ; mapM_ do_one matching_funeqs
+       ; traceTcS "builtInCandidates 1: " $ vcat [ ptext (sLit "Candidates:") <+> ppr matching_funeqs
+                                                 , ptext (sLit "TvEqs:") <+> ppr eqs ]
+       ; return (ContinueWith workItem) }
 
   | otherwise
-  = return (Nothing, False)
+  = return (ContinueWith workItem)
   where
+    eqs    = inert_eqs inerts
     funeqs = inert_funeqs inerts
     matching_inerts = findFunEqs funeqs tc args
-    loc = ctev_loc ev
 
 interactFunEq _ wi = pprPanic "interactFunEq" (ppr wi)
 
+lookupFlattenTyVar :: TyVarEnv EqualCtList -> TcTyVar -> TcType
+-- ^ Look up a flatten-tyvar in the inert TyVarEqs
+lookupFlattenTyVar inert_eqs ftv 
+  = case lookupVarEnv inert_eqs ftv of
+      Just (CTyEqCan { cc_rhs = rhs } : _) -> rhs
+      _                                    -> mkTyVarTy ftv
 
-solveFunEq :: CtEvidence    -- From this  :: F tys ~ xi1
-           -> Type
-           -> CtEvidence    -- Solve this :: F tys ~ xi2
-           -> Type
+reactFunEq :: CtEvidence -> TcTyVar    -- From this  :: F tys ~ fsk1
+           -> CtEvidence -> TcTyVar    -- Solve this :: F tys ~ fsk2
            -> TcS ()
-solveFunEq from_this xi1 solve_this xi2
-  = do { ctevs <- xCtEvidence solve_this xev
-             -- No caching!  See Note [Cache-caused loops]
-             -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
-
-       ; emitWorkNC ctevs }
-  where
-    from_this_co = evTermCoercion $ ctEvTerm from_this
-
-    xev = XEvTerm [mkTcEqPred xi2 xi1] xcomp xdecomp
-
-    -- xcomp : [(xi2 ~ xi1)] -> (F tys ~ xi2)
-    xcomp [x] = EvCoercion (from_this_co `mkTcTransCo` mk_sym_co x)
-    xcomp _   = panic "No more goals!"
-
-    -- xdecomp : (F tys ~ xi2) -> [(xi2 ~ xi1)]
-    xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` from_this_co)]
-
-    mk_sym_co x = mkTcSymCo (evTermCoercion x)
+reactFunEq from_this fsk1 (CtGiven { ctev_evtm = tm, ctev_loc = loc }) fsk2
+  = do { let fsk_eq_co = mkTcSymCo (evTermCoercion tm)
+                         `mkTcTransCo` ctEvCoercion from_this
+                         -- :: fsk2 ~ fsk1
+             fsk_eq_pred = mkTcEqPred (mkTyVarTy fsk2) (mkTyVarTy fsk1)
+       ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
+       ; emitWorkNC [new_ev] }
+
+reactFunEq from_this fuv1 (CtWanted { ctev_evar = evar }) fuv2
+  = dischargeFmv evar fuv2 (ctEvCoercion from_this) (mkTyVarTy fuv1)
+
+reactFunEq _ _ solve_this@(CtDerived {}) _
+  = pprPanic "reactFunEq" (ppr solve_this)
 \end{code}
 
 Note [Cache-caused loops]
@@ -677,8 +633,8 @@ test when solving pairwise CFunEqCan.
 *********************************************************************************
 
 \begin{code}
-interactTyVarEq :: InertCans -> Ct -> TcS (Maybe InertCans, StopNowFlag)
--- CTyEqCans are always consumed, returning Stop
+interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
+-- CTyEqCans are always consumed, so always returns Stop
 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs , cc_ev = ev })
   | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
                              <- findTyEqs (inert_eqs inerts) tv
@@ -686,9 +642,9 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs , cc_ev
                          , rhs_i `tcEqType` rhs ]
   =  -- Inert:     a ~ b
      -- Work item: a ~ b
-    do { when (isWanted ev) (setEvBind (ctev_evar ev) (ctEvTerm ev_i))
-       ; traceFireTcS workItem (ptext (sLit "Solved from inert"))
-       ; return (Nothing, True) }
+    do { when (isWanted ev) $
+         setEvBind (ctev_evar ev) (ctEvTerm ev_i)
+       ; stopWith ev "Solved from inert" }
 
   | Just tv_rhs <- getTyVar_maybe rhs
   , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
@@ -697,41 +653,97 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs , cc_ev
                          , rhs_i `tcEqType` mkTyVarTy tv ]
   =  -- Inert:     a ~ b
      -- Work item: b ~ a
-    do { when (isWanted ev) (setEvBind (ctev_evar ev)
-                                (EvCoercion (mkTcSymCo (evTermCoercion (ctEvTerm ev_i)))))
-       ; traceFireTcS workItem (ptext (sLit "Solved from inert (r)"))
-       ; return (Nothing, True) }
+    do { when (isWanted ev) $
+         setEvBind (ctev_evar ev)
+                   (EvCoercion (mkTcSymCo (ctEvCoercion ev_i)))
+       ; stopWith ev "Solved from inert (r)" }
 
   | otherwise
-  = do { mb_solved <- trySpontaneousSolve ev tv rhs
-       ; case mb_solved of
-           SPCantSolve   -- Includes givens
-              -> do { untch <- getUntouchables
-                    ; traceTcS "Can't solve tyvar equality"
-                          (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
-                                , ppWhen (isMetaTyVar tv) $
-                                  nest 4 (text "Untouchable level of" <+> ppr tv
-                                          <+> text "is" <+> ppr (metaTyVarUntouchables tv))
-                                , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
-                                , text "Untouchables =" <+> ppr untch ])
-                    ; (n_kicked, inerts') <- kickOutRewritable ev tv inerts
-                    ; traceFireTcS workItem $
-                      ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked
-                    ; return (Just (addInertCan inerts' workItem), True) }
-
-
-           SPSolved new_tv
-              -- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
-              -- see Note [Spontaneously solved in TyBinds]
-              -> do { (n_kicked, inerts') <- kickOutRewritable givenFlavour new_tv inerts
-                    ; traceFireTcS workItem $
-                      ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked
-                    ; return (Just inerts', True) } }
+  = do { untch <- getUntouchables
+       ; if canSolveByUnification untch ev tv rhs
+         then do { solveByUnification ev tv rhs
+                 ; n_kicked <- kickOutRewritable givenFlavour tv
+                               -- givenFlavour because the tv := xi is given
+                 ; return (Stop ev (ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked)) }
+
+         else do { traceTcS "Can't solve tyvar equality"
+                       (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
+                             , ppWhen (isMetaTyVar tv) $
+                               nest 4 (text "Untouchable level of" <+> ppr tv
+                                       <+> text "is" <+> ppr (metaTyVarUntouchables tv))
+                             , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
+                             , text "Untouchables =" <+> ppr untch ])
+                 ; n_kicked <- kickOutRewritable ev tv
+                 ; updInertCans (\ ics -> addInertCan ics workItem)
+                 ; return (Stop ev (ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked)) } }
 
 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
 
+-- @trySpontaneousSolve wi@ solves equalities where one side is a
+-- touchable unification variable.
+-- Returns True <=> spontaneous solve happened
+canSolveByUnification :: Untouchables -> CtEvidence -> TcTyVar -> Xi -> Bool
+canSolveByUnification untch gw tv xi
+  | isGiven gw   -- See Note [Touchables and givens]
+  = False
+
+  | isTouchableMetaTyVar untch tv
+  = case metaTyVarInfo tv of
+      SigTv -> is_tyvar xi
+      _     -> True
+
+  | otherwise    -- Untouchable
+  = False
+  where
+    is_tyvar xi
+      = case tcGetTyVar_maybe xi of
+          Nothing -> False
+          Just tv -> case tcTyVarDetails tv of
+                       MetaTv { mtv_info = info }
+                                   -> case info of
+                                        SigTv -> True
+                                        _     -> False
+                       SkolemTv {} -> True
+                       FlatSkol {} -> False
+                       RuntimeUnk  -> True
+
+solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
+-- Solve with the identity coercion
+-- Precondition: kind(xi) is a sub-kind of kind(tv)
+-- Precondition: CtEvidence is Wanted or Derived
+-- See [New Wanted Superclass Work] to see why solveByUnification
+--     must work for Derived as well as Wanted
+-- Returns: workItem where
+--        workItem = the new Given constraint
+--
+-- NB: No need for an occurs check here, because solveByUnification always
+--     arises from a CTyEqCan, a *canonical* constraint.  Its invariants
+--     say that in (a ~ xi), the type variable a does not appear in xi.
+--     See TcRnTypes.Ct invariants.
+--
+-- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
+-- see Note [Spontaneously solved in TyBinds]
+solveByUnification wd tv xi
+  = do { let tv_ty = mkTyVarTy tv
+       ; traceTcS "Sneaky unification:" $
+                       vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
+                             text "Coercion:" <+> pprEq tv_ty xi,
+                             text "Left Kind is:" <+> ppr (typeKind tv_ty),
+                             text "Right Kind is:" <+> ppr (typeKind xi) ]
+
+       ; let xi' = defaultKind xi
+               -- We only instantiate kind unification variables
+               -- with simple kinds like *, not OpenKind or ArgKind
+               -- cf TcUnify.uUnboundKVar
+
+       ; setWantedTyBind tv xi'
+       ; when (isWanted wd) $
+         setEvBind (ctEvId wd) (EvCoercion (mkTcNomReflCo xi')) }
+
+
 givenFlavour :: CtEvidence
 -- Used just to pass to kickOutRewritable
+-- and to guide 'flatten' for givens
 givenFlavour = CtGiven { ctev_pred = panic "givenFlavour:ev"
                        , ctev_evtm = panic "givenFlavour:tm"
                        , ctev_loc  = panic "givenFlavour:loc" }
@@ -760,24 +772,32 @@ these binds /and/ the inerts for potentially unsolved or other given equalities.
 kickOutRewritable :: CtEvidence   -- Flavour of the equality that is
                                   -- being added to the inert set
                   -> TcTyVar      -- The new equality is tv ~ ty
-                  -> InertCans
-                  -> TcS (Int, InertCans)
+                  -> TcS Int
 kickOutRewritable new_ev new_tv
-                  inert_cans@(IC { inert_eqs = tv_eqs
-                                 , inert_dicts  = dictmap
-                                 , inert_funeqs = funeqmap
-                                 , inert_irreds = irreds
-                                 , inert_insols = insols
-                                 , inert_no_eqs = no_eqs })
-  | new_tv `elemVarEnv` tv_eqs   -- Fast path: there is at least one equality for tv
-                                 -- so kick-out will do nothing
-  = return (0, inert_cans)
-  | otherwise
-  = do { traceTcS "kickOutRewritable" $
-            vcat [ text "tv = " <+> ppr new_tv
-                 , ptext (sLit "Kicked out =") <+> ppr kicked_out]
+  = do { ics <- getInertCans
+       ; if isWanted new_ev && 
+            new_tv `elemVarEnv` inert_eqs ics  
+         then          -- Fast path: there is at least one equality
+            return 0   --  for tv, so kick-out will do nothing
+          
+         else
+    do { let (kicked_out, ics') = kick_out new_ev new_tv ics
+       ; setInertCans ics'
        ; updWorkListTcS (appendWorkList kicked_out)
-       ; return (workListSize kicked_out, inert_cans_in) }
+
+       ; unless (isEmptyWorkList kicked_out) $ 
+         csTraceTcS $ 
+         hang (ptext (sLit "Kick out, tv =") <+> ppr new_tv)
+            2 (ppr kicked_out)
+       ; return (workListSize kicked_out) } }
+
+kick_out :: CtEvidence -> TcTyVar -> InertCans -> (WorkList, InertCans)
+kick_out new_ev new_tv (IC { inert_eqs = tv_eqs
+                           , inert_dicts  = dictmap
+                           , inert_funeqs = funeqmap
+                           , inert_irreds = irreds
+                           , inert_insols = insols })
+  = (kicked_out, inert_cans_in)
   where
                 -- NB: Notice that don't rewrite
                 -- inert_solved_dicts, and inert_solved_funeqs
@@ -787,28 +807,28 @@ kickOutRewritable new_ev new_tv
                        , inert_dicts = dicts_in
                        , inert_funeqs = feqs_in
                        , inert_irreds = irs_in
-                       , inert_insols = insols_in
-                       , inert_no_eqs = no_eqs }
+                       , inert_insols = insols_in }
 
-    kicked_out = WorkList { wl_eqs    = tv_eqs_out
-                          , wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
-                          , wl_rest   = bagToList (dicts_out `andCts` irs_out
-                                                   `andCts` insols_out) }
+    kicked_out = WL { wl_eqs    = tv_eqs_out
+                    , wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
+                    , wl_rest   = bagToList (dicts_out `andCts` irs_out
+                                             `andCts` insols_out)
+                    , wl_implics = emptyBag }
 
     (tv_eqs_out,  tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
-    (feqs_out,   feqs_in)    = partitionFunEqs  kick_out_ct    funeqmap
-    (dicts_out,  dicts_in)   = partitionDicts   kick_out_ct    dictmap
+    (feqs_out,   feqs_in)    = partitionFunEqs  kick_out_ct funeqmap
+    (dicts_out,  dicts_in)   = partitionDicts   kick_out_ct dictmap
     (irs_out,    irs_in)     = partitionBag     kick_out_irred irreds
     (insols_out, insols_in)  = partitionBag     kick_out_ct    insols
       -- Kick out even insolubles; see Note [Kick out insolubles]
 
     kick_out_ct :: Ct -> Bool
-    kick_out_ct ct =  new_ev `canRewrite` ctEvidence ct
+    kick_out_ct ct =  eqCanRewrite new_tv new_ev (ctEvidence ct)
                    && new_tv `elemVarSet` tyVarsOfCt ct
          -- See Note [Kicking out inert constraints]
 
     kick_out_irred :: Ct -> Bool
-    kick_out_irred ct =  new_ev `canRewrite` ctEvidence ct
+    kick_out_irred ct =  eqCanRewrite new_tv new_ev (ctEvidence ct)
                       && new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct)
           -- See Note [Kicking out Irreds]
 
@@ -824,9 +844,10 @@ kickOutRewritable new_ev new_tv
 
     kick_out_eq :: Ct -> Bool
     kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = ev })
-      =  (new_ev `canRewrite` ev)  -- See Note [Delicate equality kick-out]
-      && (new_tv `elemVarSet` kind_vars ||    -- (1)
-          (not (ev `canRewrite` new_ev) &&    -- (2)
+      =  (eqCanRewrite new_tv new_ev ev)  -- See Note [Delicate equality kick-out]
+      && (new_tv == tv ||                    
+          new_tv `elemVarSet` kind_vars ||       -- (1)
+          (not (eqCanRewrite tv ev new_ev) &&    -- (2)
            new_tv `elemVarSet` (extendVarSet (tyVarsOfType rhs) tv)))
       where
         kind_vars = tyVarsOfType (tyVarKind tv) `unionVarSet`
@@ -865,7 +886,6 @@ closeOverKinds to make sure we see k2.
 This is not pretty. Maybe (~) should have kind 
    (~) :: forall k1 k1. k1 -> k2 -> Constraint
 
-
 Note [Kick out insolubles]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
@@ -880,6 +900,11 @@ Note [Delicate equality kick-out]
 When adding an equality (a ~ xi), we kick out an inert type-variable
 equality (b ~ phi) in two cases
 
+(0) If the new tyvar is the same as the old one
+      Work item: [G] a ~ blah
+      Inert:     [W} a ~ foo
+    A particular case is when flatten-skolems get their value we must propagate
+
 (1) If the new tyvar appears in the kind vars of the LHS or RHS of
     the inert.  Example:
     Work item: [G] k ~ *
@@ -889,7 +914,10 @@ equality (b ~ phi) in two cases
     and can subsequently unify.
 
 (2) If the new tyvar appears in the RHS of the inert
-    AND the inert cannot rewrite the work item
+    AND the work item is strong enough to rewrite the inert
+
+    AND not (the inert can rewrite the work item)   <---------------------------------
+
           Work item:  [G] a ~ b
           Inert:      [W] b ~ [a]
     Now at this point the work item cannot be further rewritten by the
@@ -903,65 +931,13 @@ equality (b ~ phi) in two cases
          Work item: [W] a ~ Int
          Inert:     [W] b ~ [a]
     No need to kick out the inert, beause the inert substitution is not
-    necessarily idemopotent.  See Note [Non-idempotent inert substitution].
+    necessarily idemopotent.  See Note [Non-idempotent inert substitution]
+    in TcCanonical.
 
+          Work item:  [G] a ~ Int
+          Inert:      [G] b ~ [a]
 See also Note [Detailed InertCans Invariants]
 
-\begin{code}
-data SPSolveResult = SPCantSolve
-                   | SPSolved TcTyVar
-                     -- We solved this /unification/ variable to some type using reflexivity
-
--- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
--- SPSolved workItem' gives us a new *given* to go on
-
--- @trySpontaneousSolve wi@ solves equalities where one side is a
--- touchable unification variable.
-trySpontaneousSolve :: CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
-trySpontaneousSolve gw tv1 xi
-  | isGiven gw   -- See Note [Touchables and givens]
-  = return SPCantSolve
-
-  | Just tv2 <- tcGetTyVar_maybe xi
-  = do { tch1 <- isTouchableMetaTyVarTcS tv1
-       ; tch2 <- isTouchableMetaTyVarTcS tv2
-       ; case (tch1, tch2) of
-           (True,  True)  -> trySpontaneousEqTwoWay gw tv1 tv2
-           (True,  False) -> trySpontaneousEqOneWay gw tv1 xi
-           (False, True)  -> trySpontaneousEqOneWay gw tv2 (mkTyVarTy tv1)
-           _              -> return SPCantSolve }
-  | otherwise
-  = do { tch1 <- isTouchableMetaTyVarTcS tv1
-       ; if tch1 then trySpontaneousEqOneWay gw tv1 xi
-                 else return SPCantSolve }
-
-----------------
-trySpontaneousEqOneWay :: CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
--- tv is a MetaTyVar, not untouchable
-trySpontaneousEqOneWay gw tv xi
-  | not (isSigTyVar tv) || isTyVarTy xi
-  , typeKind xi `tcIsSubKind` tyVarKind tv
-  = solveWithIdentity gw tv xi
-  | otherwise -- Still can't solve, sig tyvar and non-variable rhs
-  = return SPCantSolve
-
-----------------
-trySpontaneousEqTwoWay :: CtEvidence -> TcTyVar -> TcTyVar -> TcS SPSolveResult
--- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
-
-trySpontaneousEqTwoWay gw tv1 tv2
-  | k1 `tcIsSubKind` k2 && nicer_to_update_tv2
-  = solveWithIdentity gw tv2 (mkTyVarTy tv1)
-  | k2 `tcIsSubKind` k1
-  = solveWithIdentity gw tv1 (mkTyVarTy tv2)
-  | otherwise
-  = return SPCantSolve
-  where
-    k1 = tyVarKind tv1
-    k2 = tyVarKind tv2
-    nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
-\end{code}
-
 Note [Avoid double unifications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The spontaneous solver has to return a given which mentions the unified unification
@@ -980,42 +956,6 @@ See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
 double unifications is the main reason we disallow touchable
 unification variables as RHS of type family equations: F xis ~ alpha.
 
-\begin{code}
-solveWithIdentity :: CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
--- Solve with the identity coercion
--- Precondition: kind(xi) is a sub-kind of kind(tv)
--- Precondition: CtEvidence is Wanted or Derived
--- See [New Wanted Superclass Work] to see why solveWithIdentity
---     must work for Derived as well as Wanted
--- Returns: workItem where
---        workItem = the new Given constraint
---
--- NB: No need for an occurs check here, because solveWithIdentity always
---     arises from a CTyEqCan, a *canonical* constraint.  Its invariants
---     say that in (a ~ xi), the type variable a does not appear in xi.
---     See TcRnTypes.Ct invariants.
-solveWithIdentity wd tv xi
-  = do { let tv_ty = mkTyVarTy tv
-       ; traceTcS "Sneaky unification:" $
-                       vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
-                             text "Coercion:" <+> pprEq tv_ty xi,
-                             text "Left Kind is:" <+> ppr (typeKind tv_ty),
-                             text "Right Kind is:" <+> ppr (typeKind xi) ]
-
-       ; let xi' = defaultKind xi
-               -- We only instantiate kind unification variables
-               -- with simple kinds like *, not OpenKind or ArgKind
-               -- cf TcUnify.uUnboundKVar
-
-       ; setWantedTyBind tv xi'
-       ; let refl_evtm = EvCoercion (mkTcNomReflCo xi')
-
-       ; when (isWanted wd) $
-              setEvBind (ctev_evar wd) refl_evtm
-
-       ; return (SPSolved tv) }
-\end{code}
-
 
 
 Note [Superclasses and recursive dictionaries]
@@ -1363,38 +1303,23 @@ To achieve this required some refactoring of FunDeps.lhs (nicer
 now!).
 
 \begin{code}
-rewriteWithFunDeps :: [Equation CtLoc] -> TcS [Ct]
+rewriteWithFunDeps :: [Equation CtLoc] -> TcS ()
 -- NB: The returned constraints are all Derived
 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
 rewriteWithFunDeps eqn_pred_locs
- = do { fd_cts <- mapM instFunDepEqn eqn_pred_locs
-      ; return (concat fd_cts) }
+ = mapM_ instFunDepEqn eqn_pred_locs
 
-instFunDepEqn :: Equation CtLoc -> TcS [Ct]
+instFunDepEqn :: Equation CtLoc -> TcS ()
 -- Post: Returns the position index as well as the corresponding FunDep equality
 instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
   = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
-       ; foldM (do_one subst) [] eqs }
+       ; mapM_ (do_one subst) eqs }
   where
-    do_one subst ievs (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
-       | tcEqType sty1 sty2
-       = return ievs -- Return no trivial equalities
-       | otherwise
-       = do { mb_eqv <- newDerived loc (mkTcEqPred sty1 sty2)
-            ; case mb_eqv of
-                 Just ev -> return (mkNonCanonical (ev {ctev_loc = loc}) : ievs)
-                 Nothing -> return ievs }
-                   -- We are eventually going to emit FD work back in the work list so
-                   -- it is important that we only return the /freshly created/ and not
-                   -- some existing equality!
-       where
-         sty1 = Type.substTy subst ty1
-         sty2 = Type.substTy subst ty2
+    do_one subst (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
+       = emitNewDerivedEq loc (Pair (Type.substTy subst ty1) (Type.substTy subst ty2))
 \end{code}
 
 
-
-
 *********************************************************************************
 *                                                                               *
                        The top-reaction Stage
@@ -1402,23 +1327,15 @@ instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
 *********************************************************************************
 
 \begin{code}
-topReactionsStage :: WorkItem -> TcS StopOrContinue
+topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
 topReactionsStage wi
  = do { inerts <- getTcSInerts
       ; tir <- doTopReact inerts wi
       ; case tir of
-          NoTopInt -> return (ContinueWith wi)
-          SomeTopInt rule what_next
-                   -> do { traceFireTcS wi $
-                           ptext (sLit "Top react:") <+> text rule
-                         ; return what_next } }
-
-data TopInteractResult
- = NoTopInt
- | SomeTopInt { tir_rule :: String, tir_new_item :: StopOrContinue }
+          ContinueWith wi -> return (ContinueWith wi)
+          Stop ev s       -> return (Stop ev (ptext (sLit "Top react:") <+> s)) }
 
-
-doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
+doTopReact :: InertSet -> WorkItem -> TcS (StopOrContinue Ct)
 -- The work item does not react with the inert set, so try interaction with top-level
 -- instances. Note:
 --
@@ -1429,30 +1346,26 @@ 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
-  = do { traceTcS "doTopReact" (ppr workItem)
-       ; case workItem of
-           CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis }
-              -> doTopReactDict inerts fl cls xis
-
-           CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args , cc_rhs = xi }
-              -> doTopReactFunEq workItem fl tc args xi
-
+doTopReact inerts work_item
+  = do { traceTcS "doTopReact" (ppr work_item)
+       ; case work_item of
+           CDictCan {}  -> doTopReactDict inerts work_item
+           CFunEqCan {} -> doTopReactFunEq work_item
            _  -> -- Any other work item does not react with any top-level equations
-                 return NoTopInt  }
+                 return (ContinueWith work_item)  }
 
 --------------------
-doTopReactDict :: InertSet -> CtEvidence -> Class -> [Xi] -> TcS TopInteractResult
+doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
 -- Try to use type-class instance declarations to simplify the constraint
-doTopReactDict inerts fl cls xis
+doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
+                                          , cc_tyargs = xis })
   | not (isWanted fl)   -- Never use instances for Given or Derived constraints
   = try_fundeps_and_return
 
   | Just ev <- lookupSolvedDict inerts cls xis   -- Cached
-  , ctEvCheckDepth (ctLocDepth (ctev_loc fl)) ev
+  , ctEvCheckDepth (ctLocDepth loc) ev
   = do { setEvBind dict_id (ctEvTerm ev);
-       ; return $ SomeTopInt { tir_rule = "Dict/Top (cached)"
-                             , tir_new_item = Stop } }
+       ; stopWith fl "Dict/Top (cached)" }
 
   | otherwise  -- Not cached
    = do { lkup_inst_res <- matchClassInst inerts cls xis loc
@@ -1461,20 +1374,18 @@ doTopReactDict inerts fl cls xis
                                           ; solve_from_instance wtvs ev_term }
                NoInstance -> try_fundeps_and_return }
    where
-     dict_id = ctEvId fl
+     dict_id = ASSERT( isWanted fl ) ctEvId fl
      pred = mkClassPred cls xis
-     loc = ctev_loc fl
+     loc = ctEvLoc fl
 
-     solve_from_instance :: [CtEvidence] -> EvTerm -> TcS TopInteractResult
+     solve_from_instance :: [CtEvidence] -> EvTerm -> TcS (StopOrContinue Ct)
       -- Precondition: evidence term matches the predicate workItem
      solve_from_instance evs ev_term
         | null evs
         = do { traceTcS "doTopReact/found nullary instance for" $
                ppr dict_id
              ; setEvBind dict_id ev_term
-             ; return $
-               SomeTopInt { tir_rule = "Dict/Top (solved, no new work)"
-                          , tir_new_item = Stop } }
+             ; stopWith fl "Dict/Top (solved, no new work)" }
         | otherwise
         = do { traceTcS "doTopReact/found non-nullary instance for" $
                ppr dict_id
@@ -1482,9 +1393,7 @@ doTopReactDict inerts fl cls xis
              ; let mk_new_wanted ev
                        = mkNonCanonical (ev {ctev_loc = bumpCtLocDepth CountConstraints loc })
              ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
-             ; return $
-               SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
-                          , tir_new_item = Stop } }
+             ; stopWith fl "Dict/Top (solved, more work)" }
 
      -- We didn't solve it; so try functional dependencies with
      -- the instance environment, and return
@@ -1497,66 +1406,135 @@ doTopReactDict inerts fl cls xis
                   fd_eqns = [ fd { fd_loc = loc { ctl_origin = FunDepOrigin2 pred (ctl_origin loc)
                                                                              inst_pred inst_loc } }
                             | fd@(FDEqn { fd_loc = inst_loc, fd_pred1 = inst_pred })
-                                 <- improveFromInstEnv instEnvs pred ]
-            ; fd_work <- rewriteWithFunDeps fd_eqns
-            ; unless (null fd_work) $
-              do { traceTcS "Addig FD work" (ppr pred $$ vcat (map pprEquation fd_eqns) $$ ppr fd_work)
-                 ; updWorkListTcS (extendWorkListEqs fd_work) }
-            ; return NoTopInt }
+                            <- improveFromInstEnv instEnvs pred ]
+            ; rewriteWithFunDeps fd_eqns
+            ; continueWith work_item }
 
---------------------
-doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi -> TcS TopInteractResult
-doTopReactFunEq _ct fl fun_tc args xi
-  = ASSERT(isSynFamilyTyCon fun_tc) -- No associated data families have
-                                     -- reached this far
-    -- Look in the cache of solved funeqs
-    do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
-       ; case findFunEq fun_eq_cache fun_tc args of {
-           Just (ctev, rhs_ty)
-             | ctev `canRewriteOrSame` fl  -- See Note [Cached solved FunEqs]
-             -> ASSERT( not (isDerived ctev) )
-                succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
-           _other ->
+doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
 
+--------------------
+doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
+doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
+                                     , cc_tyargs = args , cc_fsk = fsk })
+  = ASSERT(isSynFamilyTyCon fam_tc) -- No associated data families
+                                    -- have reached this far
+    ASSERT( not (isDerived old_ev) )   -- CFunEqCan is never Derived
     -- Look up in top-level instances, or built-in axiom
-    do { match_res <- matchFam fun_tc args   -- See Note [MATCHING-SYNONYMS]
+    do { match_res <- matchFam fam_tc args   -- See Note [MATCHING-SYNONYMS]
        ; case match_res of {
-           Nothing -> do { try_improvement; return NoTopInt } ;
-           Just (co, ty) ->
+           Nothing -> do { try_improvement; continueWith work_item } ;
+           Just (ax_co, rhs_ty)
 
     -- Found a top-level instance
-    do {    -- Add it to the solved goals
-         unless (isDerived fl) (addSolvedFunEq fun_tc args fl xi)
 
-       ; succeed_with "Fun/Top" co ty } } } } }
+    | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
+    , isSynFamilyTyCon tc
+    , tc_args `lengthIs` tyConArity tc    -- Short-cut
+    -> shortCutReduction old_ev fsk ax_co tc tc_args
+         -- Try shortcut; see Note [Short cut for top-level reaction]
+
+    | isGiven old_ev  -- Not shortcut
+    -> do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
+                -- final_co :: fsk ~ rhs_ty
+          ; new_ev <- newGivenEvVar deeper_loc (mkTcEqPred (mkTyVarTy fsk) rhs_ty,
+                                                EvCoercion final_co)
+          ; emitWorkNC [new_ev]   -- Non-cannonical; that will mean we flatten rhs_ty
+          ; stopWith old_ev "Fun/Top (given)" }
+
+    | not (fsk `elemVarSet` tyVarsOfType rhs_ty)
+    -> do { dischargeFmv (ctEvId old_ev) fsk ax_co rhs_ty
+          ; traceTcS "doTopReactFunEq" $
+            vcat [ text "old_ev:" <+> ppr old_ev
+                 , nest 2 (text ":=") <+> ppr ax_co ]
+          ; stopWith old_ev "Fun/Top (wanted)" }
+
+    | otherwise -- We must not assign ufsk := ...ufsk...!
+    -> do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
+          ; new_ev <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
+          ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
+              --    ax_co :: fam_tc args ~ rhs_ty
+              --       ev :: alpha ~ rhs_ty
+              --     ufsk := alpha
+              -- final_co :: fam_tc args ~ alpha
+          ; dischargeFmv (ctEvId old_ev) fsk final_co alpha_ty
+          ; traceTcS "doTopReactFunEq (occurs)" $
+            vcat [ text "old_ev:" <+> ppr old_ev
+                 , nest 2 (text ":=") <+> ppr final_co
+                 , text "new_ev:" <+> ppr new_ev ]
+          ; emitWorkNC [new_ev]
+              -- By emitting this as non-canonical, we deal with all
+              -- flattening, occurs-check, and ufsk := ufsk issues
+          ; stopWith old_ev "Fun/Top (wanted)" } } }
   where
-    loc = ctev_loc fl
+    loc = ctEvLoc old_ev
+    deeper_loc = bumpCtLocDepth CountTyFunApps loc
 
     try_improvement
-      | Just ops <- isBuiltInSynFamTyCon_maybe fun_tc
-      = do { let eqns = sfInteractTop ops args xi
-           ; impsMb <- mapM (\(Pair x y) -> newDerived loc (mkTcEqPred x y)) eqns
-           ; let work = map mkNonCanonical (catMaybes impsMb)
-           ; unless (null work) (updWorkListTcS (extendWorkListEqs work)) }
+      | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
+      = do { inert_eqs <- getInertEqs
+           ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk)
+           ; mapM_ (emitNewDerivedEq loc) eqns }
       | otherwise
       = return ()
 
-    succeed_with :: String -> TcCoercion -> TcType -> TcS TopInteractResult
-    succeed_with str co rhs_ty    -- co :: fun_tc args ~ rhs_ty
-      = do { ctevs <- xCtEvidence fl xev
-           ; traceTcS ("doTopReactFunEq " ++ str) (ppr ctevs)
-           ; case ctevs of
-               [ctev] -> updWorkListTcS $ extendWorkListEq $
-                         mkNonCanonical (ctev { ctev_loc = bumpCtLocDepth CountTyFunApps loc })
-               ctevs -> -- No subgoal (because it's cached)
-                        ASSERT( null ctevs) return ()
-           ; return $ SomeTopInt { tir_rule = str
-                                 , tir_new_item = Stop } }
-      where
-        xdecomp x = [EvCoercion (mkTcSymCo co `mkTcTransCo` evTermCoercion x)]
-        xcomp [x] = EvCoercion (co `mkTcTransCo` evTermCoercion x)
-        xcomp _   = panic "No more goals!"
-        xev = XEvTerm [mkTcEqPred rhs_ty xi] xcomp xdecomp
+doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
+
+shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
+                  -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
+shortCutReduction old_ev fsk ax_co fam_tc tc_args
+  | isGiven old_ev
+  = do { (xis, cos) <- flattenMany (FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }) tc_args
+               -- ax_co :: F args ~ G tc_args
+               -- cos   :: xis ~ tc_args
+               -- old_ev :: F args ~ fsk
+               -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
+
+       ; new_ev <- newGivenEvVar deeper_loc
+                         ( mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
+                         , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
+                                        `mkTcTransCo` mkTcSymCo ax_co
+                                        `mkTcTransCo` ctEvCoercion old_ev) )
+
+       ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
+       ; updWorkListTcS (extendWorkListFunEq new_ct)
+       ; stopWith old_ev "Fun/Top (given, shortcut)" }
+
+  | otherwise
+  = ASSERT( not (isDerived old_ev) )   -- Caller ensures this
+    do { (xis, cos) <- flattenMany (FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }) tc_args
+               -- ax_co :: F args ~ G tc_args
+               -- cos   :: xis ~ tc_args
+               -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
+               -- new_ev :: G xis ~ fsk
+               -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
+
+       ; new_ev <- newWantedEvVarNC loc (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
+       ; setEvBind (ctEvId old_ev)
+                   (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
+                                      `mkTcTransCo` ctEvCoercion new_ev))
+
+       ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
+       ; updWorkListTcS (extendWorkListFunEq new_ct)
+       ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
+  where
+    loc = ctEvLoc old_ev
+    deeper_loc = bumpCtLocDepth CountTyFunApps loc
+
+dischargeFmv :: EvVar -> TcTyVar -> TcCoercion -> TcType -> TcS ()
+-- (dischargeFmv x fmv co ty)
+--     [W] x :: F tys ~ fuv
+--        co :: F tys ~ ty
+-- Precondition: fuv is not filled, and fuv `notElem` ty
+--
+-- Then set fuv := ty,
+--      set x := co
+--      kick out any inert things that are now rewritable
+dischargeFmv evar fmv co xi
+  = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr evar $$ ppr fmv $$ ppr xi )
+    do { setWantedTyBind fmv xi
+       ; setEvBind evar (EvCoercion co)
+       ; n_kicked <- kickOutRewritable givenFlavour fmv
+       ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
 \end{code}
 
 Note [Cached solved FunEqs]
@@ -1836,13 +1814,15 @@ matchClassInst _ clas [ ty ] _
   -}
   makeDict evLit
     | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
+          -- co_dict :: KnownNat n ~ SNat n
     , [ meth ]   <- classMethods clas
     , Just tcRep <- tyConAppTyCon_maybe -- SNat
                       $ funResultTy         -- SNat n
                       $ dropForAlls         -- KnownNat n => SNat n
                       $ idType meth         -- forall n. KnownNat n => SNat n
     , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
-    = return (GenInst [] $ mkEvCast (EvLit evLit) (mkTcTransCo co_dict co_rep))
+          -- SNat n ~ Integer
+    = return (GenInst [] $ mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep)))
 
     | otherwise
     = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
index 301801a..91abcd3 100644 (file)
@@ -1,4 +1,4 @@
-o%
+%
 % (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
@@ -39,9 +39,11 @@ module TcMType (
   tcInstType,
   tcInstSkolTyVars, tcInstSuperSkolTyVars,tcInstSuperSkolTyVarsX,
   tcInstSigTyVarsLoc, tcInstSigTyVars,
-  tcInstSkolTyVar, tcInstSkolType,
+  tcInstSkolType,
   tcSkolDFunType, tcSuperSkolTyVars,
 
+  instSkolTyVars, freshenTyVarBndrs,
+
   --------------------------------
   -- Zonking
   zonkTcPredType,
@@ -51,7 +53,7 @@ module TcMType (
   zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType,
 
   zonkTcKind, defaultKindVarToStar,
-  zonkEvVar, zonkWC, zonkFlats, zonkId, zonkCt, zonkCts, zonkSkolemInfo,
+  zonkEvVar, zonkWC, zonkFlats, zonkId, zonkCt, zonkSkolemInfo,
 
   tcGetGlobalTyVars,
   ) where
@@ -61,10 +63,8 @@ module TcMType (
 -- friends:
 import TypeRep
 import TcType
-import TcEvidence
 import Type
 import Class
-import TyCon
 import Var
 
 -- others:
@@ -195,9 +195,8 @@ tcInstType inst_tyvars ty
                             ; return (tyvars', theta, tau) }
 
 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
--- Instantiate a type signature with skolem constants, but
--- do *not* give them fresh names, because we want the name to
--- be in the type environment: it is lexically scoped.
+-- Instantiate a type signature with skolem constants.
+-- We could give them fresh names, but no need to do so
 tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
 
 tcSuperSkolTyVars :: [TyVar] -> (TvSubst, [TcTyVar])
@@ -214,73 +213,73 @@ tcSuperSkolTyVar subst tv
     kind   = substTy subst (tyVarKind tv)
     new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
 
-tcInstSkolTyVar :: SrcSpan -> Bool -> TvSubst -> TyVar
-                -> TcRnIf gbl lcl (TvSubst, TcTyVar)
--- Instantiate the tyvar, using
---      * the occ-name and kind of the supplied tyvar,
---      * the unique from the monad,
---      * the location either from the tyvar (skol_info = SigSkol)
---                     or from the monad (otherwise)
-tcInstSkolTyVar loc overlappable subst tyvar
-  = do  { uniq <- newUnique
-        ; let new_name = mkInternalName uniq occ loc
-              new_tv   = mkTcTyVar new_name kind (SkolemTv overlappable)
-        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
-  where
-    old_name = tyVarName tyvar
-    occ      = nameOccName old_name
-    kind     = substTy subst (tyVarKind tyvar)
-
--- Wrappers
--- we need to be able to do this from outside the TcM monad:
 tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
-tcInstSkolTyVars = tcInstSkolTyVarsX (mkTopTvSubst [])
+tcInstSkolTyVars = tcInstSkolTyVars' False emptyTvSubst
 
 tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
-tcInstSuperSkolTyVars = fmap snd . tcInstSkolTyVars' True  (mkTopTvSubst [])
+tcInstSuperSkolTyVars = fmap snd . tcInstSuperSkolTyVarsX emptyTvSubst
 
-tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX
-  :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
-tcInstSkolTyVarsX      subst = tcInstSkolTyVars' False subst
-tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True  subst
+tcInstSuperSkolTyVarsX :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
+tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
 
 tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
 -- Precondition: tyvars should be ordered (kind vars first)
 -- see Note [Kind substitution when instantiating]
 -- Get the location from the monad; this is a complete freshening operation
-tcInstSkolTyVars' isSuperSkol subst tvs
+tcInstSkolTyVars' overlappable subst tvs
   = do { loc <- getSrcSpanM
-       ; mapAccumLM (tcInstSkolTyVar loc isSuperSkol) subst tvs }
+       ; instSkolTyVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
+
+mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
+mkTcSkolTyVar loc overlappable uniq old_name kind
+  = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
+              kind
+              (SkolemTv overlappable)
 
 tcInstSigTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
 -- We specify the location
-tcInstSigTyVarsLoc loc = mapAccumLM (tcInstSkolTyVar loc False) (mkTopTvSubst [])
+tcInstSigTyVarsLoc loc = instSkolTyVars (mkTcSkolTyVar loc False)
 
 tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
 -- Get the location from the TyVar itself, not the monad
-tcInstSigTyVars = mapAccumLM inst_tv (mkTopTvSubst [])
+tcInstSigTyVars
+  = instSkolTyVars mk_tv
   where
-    inst_tv subst tv = tcInstSkolTyVar (getSrcSpan tv) False subst tv
+    mk_tv uniq old_name kind
+       = mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
 
 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type with fresh skolem constants
 -- Binding location comes from the monad
 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
 
-newSigTyVar :: Name -> Kind -> TcM TcTyVar
-newSigTyVar name kind
-  = do { uniq <- newUnique
-       ; let name' = setNameUnique name uniq
-                      -- Use the same OccName so that the tidy-er
-                      -- doesn't gratuitously rename 'a' to 'a0' etc
-       ; details <- newMetaDetails SigTv
-       ; return (mkTcTyVar name' kind details) }
+------------------
+freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
+-- ^ Give fresh uniques to a bunch of TyVars, but they stay
+--   as TyVars, rather than becoming TcTyVars
+-- Used in FamInst.newFamInst, and Inst.newClsInst
+freshenTyVarBndrs = instSkolTyVars mk_tv
+  where
+    mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
 
-newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
-newMetaDetails info
-  = do { ref <- newMutVar Flexi
-       ; untch <- getUntouchables
-       ; return (MetaTv { mtv_info = info, mtv_ref = ref, mtv_untch = untch }) }
+------------------
+instSkolTyVars :: (Unique -> Name -> Kind -> TyVar)
+                -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
+instSkolTyVars mk_tv = instSkolTyVarsX mk_tv emptyTvSubst
+
+instSkolTyVarsX :: (Unique -> Name -> Kind -> TyVar)
+                -> TvSubst -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
+instSkolTyVarsX mk_tv = mapAccumLM (instSkolTyVarX mk_tv)
+
+instSkolTyVarX :: (Unique -> Name -> Kind -> TyVar)
+               -> TvSubst -> TyVar -> TcRnIf gbl lcl (TvSubst, TyVar)
+instSkolTyVarX mk_tv subst tyvar
+  = do  { uniq <- newUnique
+        ; let new_tv = mk_tv uniq old_name kind
+        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
+  where
+    old_name = tyVarName tyvar
+    kind     = substTy subst (tyVarKind tyvar)
 \end{code}
 
 Note [Kind substitution when instantiating]
@@ -312,12 +311,28 @@ newMetaTyVar meta_info kind
   = do  { uniq <- newUnique
         ; let name = mkTcTyVarName uniq s
               s = case meta_info of
-                        PolyTv -> fsLit "s"
-                        TauTv  -> fsLit "t"
-                        SigTv  -> fsLit "a"
+                        PolyTv     -> fsLit "s"
+                        TauTv      -> fsLit "t"
+                        FlatMetaTv -> fsLit "fmv"
+                        SigTv      -> fsLit "a"
         ; details <- newMetaDetails meta_info
         ; return (mkTcTyVar name kind details) }
 
+newSigTyVar :: Name -> Kind -> TcM TcTyVar
+newSigTyVar name kind
+  = do { uniq <- newUnique
+       ; let name' = setNameUnique name uniq
+                      -- Use the same OccName so that the tidy-er
+                      -- doesn't gratuitously rename 'a' to 'a0' etc
+       ; details <- newMetaDetails SigTv
+       ; return (mkTcTyVar name' kind details) }
+
+newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
+newMetaDetails info
+  = do { ref <- newMutVar Flexi
+       ; untch <- getUntouchables
+       ; return (MetaTv { mtv_info = info, mtv_ref = ref, mtv_untch = untch }) }
+
 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
 cloneMetaTyVar tv
   = ASSERT( isTcTyVar tv )
@@ -437,22 +452,16 @@ newPolyFlexiTyVarTy :: TcM TcType
 newPolyFlexiTyVarTy = do { tv <- newMetaTyVar PolyTv liftedTypeKind
                          ; return (TyVarTy tv) }
 
-tcInstTyVars :: [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
+tcInstTyVars :: [TKVar] -> TcM (TvSubst, [TcTyVar])
 -- Instantiate with META type variables
 -- Note that this works for a sequence of kind and type
 -- variables.  Eg    [ (k:BOX), (a:k->k) ]
 --             Gives [ (k7:BOX), (a8:k7->k7) ]
-tcInstTyVars tyvars = tcInstTyVarsX emptyTvSubst tyvars
+tcInstTyVars tyvars = mapAccumLM tcInstTyVarX emptyTvSubst tyvars
     -- emptyTvSubst has an empty in-scope set, but that's fine here
     -- Since the tyvars are freshly made, they cannot possibly be
     -- captured by any existing for-alls.
 
-tcInstTyVarsX :: TvSubst -> [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
--- The "X" part is because of extending the substitution
-tcInstTyVarsX subst tyvars =
-  do { (subst', tyvars') <- mapAccumLM tcInstTyVarX subst tyvars
-     ; return (tyvars', mkTyVarTys tyvars', subst') }
-
 tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar)
 -- Make a new unification variable tyvar whose Name and Kind come from
 -- an existing TyVar. We substitute kind variables in the kind.
@@ -585,6 +594,7 @@ skolemiseUnboundMetaTyVar tv details
               final_name = mkInternalName uniq (getOccName tv) span
               final_tv   = mkTcTyVar final_name final_kind details
 
+        ; traceTc "Skolemising" (ppr tv <+> ptext (sLit ":=") <+> ppr final_tv)
         ; writeMetaTyVar tv (mkTyVarTy final_tv)
         ; return final_tv }
 \end{code}
@@ -722,9 +732,7 @@ zonkTcPredType = zonkTcType
 
 \begin{code}
 zonkImplication :: Implication -> TcM (Bag Implication)
-zonkImplication implic@(Implic { ic_untch  = untch
-                               , ic_binds  = binds_var
-                               , ic_skols  = skols
+zonkImplication implic@(Implic { ic_skols  = skols
                                , ic_given  = given
                                , ic_wanted = wanted
                                , ic_info   = info })
@@ -732,12 +740,11 @@ zonkImplication implic@(Implic { ic_untch  = untch
                                                 -- as Trac #7230 showed
        ; given'  <- mapM zonkEvVar given
        ; info'   <- zonkSkolemInfo info
-       ; wanted' <- zonkWCRec binds_var untch wanted
+       ; wanted' <- zonkWCRec wanted
        ; if isEmptyWC wanted'
          then return emptyBag
          else return $ unitBag $
-              implic { ic_fsks   = []  -- Zonking removes all FlatSkol tyvars
-                     , ic_skols  = skols'
+              implic { ic_skols  = skols'
                      , ic_given  = given'
                      , ic_wanted = wanted'
                      , ic_info   = info' } }
@@ -747,56 +754,15 @@ zonkEvVar var = do { ty' <- zonkTcType (varType var)
                    ; return (setVarType var ty') }
 
 
-zonkWC :: EvBindsVar -- May add new bindings for wanted family equalities in here
-       -> WantedConstraints -> TcM WantedConstraints
-zonkWC binds_var wc
-  = do { untch <- getUntouchables
-       ; zonkWCRec binds_var untch wc }
+zonkWC :: WantedConstraints -> TcM WantedConstraints
+zonkWC wc = zonkWCRec wc
 
-zonkWCRec :: EvBindsVar
-          -> Untouchables
-          -> WantedConstraints -> TcM WantedConstraints
-zonkWCRec binds_var untch (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
-  = do { flat'   <- zonkFlats binds_var untch flat
+zonkWCRec :: WantedConstraints -> TcM WantedConstraints
+zonkWCRec (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
+  = do { flat'   <- zonkFlats flat
        ; implic' <- flatMapBagM zonkImplication implic
-       ; insol'  <- zonkCts insol -- No need to do the more elaborate zonkFlats thing
+       ; insol'  <- zonkFlats insol
        ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
-
-zonkFlats :: EvBindsVar -> Untouchables -> Cts -> TcM Cts
--- This zonks and unflattens a bunch of flat constraints
--- See Note [Unflattening while zonking]
-zonkFlats binds_var untch cts
-  = do { -- See Note [How to unflatten]
-         cts <- foldrBagM unflatten_one emptyCts cts
-       ; zonkCts cts }
-  where
-    unflatten_one orig_ct cts
-      = do { zct <- zonkCt orig_ct                -- First we need to fully zonk
-           ; mct <- try_zonk_fun_eq orig_ct zct   -- Then try to solve if family equation
-           ; return $ maybe cts (`consBag` cts) mct }
-
-    try_zonk_fun_eq orig_ct zct   -- See Note [How to unflatten]
-      | EqPred ty_lhs ty_rhs <- classifyPredType (ctPred zct)
-          -- NB: zonking de-classifies the constraint,
-          --     so we can't look for CFunEqCan
-      , Just tv <- getTyVar_maybe ty_rhs
-      , ASSERT2( not (isFloatedTouchableMetaTyVar untch tv), ppr tv )
-        isTouchableMetaTyVar untch tv
-      , not (isSigTyVar tv) || isTyVarTy ty_lhs     -- Never unify a SigTyVar with a non-tyvar
-      , typeKind ty_lhs `tcIsSubKind` tyVarKind tv  -- c.f. TcInteract.trySpontaneousEqOneWay
-      , not (tv `elemVarSet` tyVarsOfType ty_lhs)   -- Do not construct an infinite type
-      = ASSERT2( case tcSplitTyConApp_maybe ty_lhs of { Just (tc,_) -> isSynFamilyTyCon tc; _ -> False }, ppr orig_ct )
-        do { writeMetaTyVar tv ty_lhs
-           ; let evterm = EvCoercion (mkTcNomReflCo ty_lhs)
-                 evvar  = ctev_evar (cc_ev zct)
-           ; when (isWantedCt orig_ct) $         -- Can be derived (Trac #8129)
-             addTcEvBind binds_var evvar evterm
-           ; traceTc "zonkFlats/unflattening" $
-             vcat [ text "zct = " <+> ppr zct,
-                    text "binds_var = " <+> ppr binds_var ]
-           ; return Nothing }
-      | otherwise
-      = return (Just zct)
 \end{code}
 
 Note [Unflattening while zonking]
@@ -836,7 +802,7 @@ Consider them one by one.  For each such constraint C
          and discard C
 
 After processing all the flat constraints, zonk them again to propagate
-the inforamtion from later ones to earlier ones.  Eg
+the information from later ones to earlier ones.  Eg
   Start:  (F alpha ~ beta, G Int ~ alpha)
   Then we get beta := F alpha
               alpha := G Int
@@ -844,8 +810,13 @@ the inforamtion from later ones to earlier ones.  Eg
 
 
 \begin{code}
-zonkCts :: Cts -> TcM Cts
-zonkCts = mapBagM zonkCt
+zonkFlats :: Cts -> TcM Cts
+zonkFlats cts = do { cts' <- mapBagM zonkCt' cts
+                   ; traceTc "zonkFlats done:" (ppr cts')
+                   ; return cts' }
+
+zonkCt' :: Ct -> TcM Ct
+zonkCt' ct = zonkCt ct
 
 zonkCt :: Ct -> TcM Ct
 zonkCt ct@(CHoleCan { cc_ev = ev })
index 2f86f37..6fdbc52 100644 (file)
@@ -787,7 +787,7 @@ tcPatSynPat :: PatEnv -> Located Name -> PatSyn
 tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
   = do  { let (univ_tvs, ex_tvs, prov_theta, req_theta, arg_tys, ty) = patSynSig pat_syn
 
-        ; (univ_tvs', inst_tys, subst) <- tcInstTyVars univ_tvs
+        ; (subst, univ_tvs') <- tcInstTyVars univ_tvs
 
         ; checkExistentials ex_tvs penv
         ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
@@ -817,7 +817,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
                             LamPat mc -> PatSkol (PatSynCon pat_syn) mc
                             LetPat {} -> UnkSkol -- Doesn't matter
 
-        ; req_wrap <- instCall PatOrigin inst_tys req_theta'
+        ; req_wrap <- instCall PatOrigin (mkTyVarTys univ_tvs') req_theta'
         ; traceTc "instCall" (ppr req_wrap)
 
         ; traceTc "checkConstraints {" Outputable.empty
@@ -848,10 +848,10 @@ matchExpectedPatTy inner_match pat_ty
          -- that is the other way round to matchExpectedPatTy
 
   | otherwise
-  = do { (_, tys, subst) <- tcInstTyVars tvs
-       ; wrap1 <- instCall PatOrigin tys (substTheta subst theta)
+  = do { (subst, tvs') <- tcInstTyVars tvs
+       ; wrap1 <- instCall PatOrigin (mkTyVarTys tvs') (substTheta subst theta)
        ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (TcType.substTy subst tau)
-       ; return (wrap2 <.> wrap1 , arg_tys) }
+       ; return (wrap2 <.> wrap1, arg_tys) }
   where
     (tvs, theta, tau) = tcSplitSigmaTy pat_ty
 
@@ -868,7 +868,7 @@ matchExpectedConTy data_tc pat_ty
   | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc
          -- Comments refer to Note [Matching constructor patterns]
          -- co_tc :: forall a. T [a] ~ T7 a
-  = do { (_, tys, subst) <- tcInstTyVars (tyConTyVars data_tc)
+  = do { (subst, tvs') <- tcInstTyVars (tyConTyVars data_tc)
              -- tys = [ty1,ty2]
 
        ; traceTc "matchExpectedConTy" (vcat [ppr data_tc,
@@ -877,10 +877,11 @@ matchExpectedConTy data_tc pat_ty
        ; co1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty
              -- co1 : T (ty1,ty2) ~ pat_ty
 
-       ; let co2 = mkTcUnbranchedAxInstCo Nominal co_tc tys
+       ; let tys' = mkTyVarTys tvs'
+             co2 = mkTcUnbranchedAxInstCo Nominal co_tc tys'
              -- co2 : T (ty1,ty2) ~ T7 ty1 ty2
 
-       ; return (mkTcSymCo co2 `mkTcTransCo` co1, tys) }
+       ; return (mkTcSymCo co2 `mkTcTransCo` co1, tys') }
 
   | otherwise
   = matchExpectedTyConApp data_tc pat_ty
index 9b2b511..d27ab4f 100644 (file)
@@ -48,18 +48,23 @@ tcPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
                   psb_def = lpat, psb_dir = dir }
   = do { traceTc "tcPatSynDecl {" $ ppr name $$ ppr lpat
        ; tcCheckPatSynPat lpat
-       ; pat_ty <- newFlexiTyVarTy openTypeKind
+       ; 
 
        ; let (arg_names, is_infix) = case details of
                  PrefixPatSyn names      -> (map unLoc names, False)
                  InfixPatSyn name1 name2 -> (map unLoc [name1, name2], True)
-       ; ((lpat', args), wanted) <- captureConstraints       $
-                                    tcPat PatSyn lpat pat_ty $
-                                    mapM tcLookupId arg_names
-       ; let named_taus = (name, pat_ty):map (\arg -> (getName arg, varType arg)) args
+       ; (((lpat', (args, pat_ty)), untch), wanted) 
+            <- captureConstraints       $
+               captureUntouchables      $
+               do { pat_ty <- newFlexiTyVarTy openTypeKind
+                  ; tcPat PatSyn lpat pat_ty $
+               do { args <- mapM tcLookupId arg_names
+                  ; return (args, pat_ty) } }
+
+       ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
 
        ; traceTc "tcPatSynDecl::wanted" (ppr named_taus $$ ppr wanted)
-       ; (qtvs, req_dicts, _mr_bites, ev_binds) <- simplifyInfer True False named_taus wanted
+       ; (qtvs, req_dicts, _mr_bites, ev_binds) <- simplifyInfer untch False named_taus wanted
 
        ; (ex_vars, prov_dicts) <- tcCollectEx lpat'
        ; let univ_tvs   = filter (not . (`elemVarSet` ex_vars)) qtvs
index 9898b46..2bb8d2d 100644 (file)
@@ -1490,11 +1490,12 @@ tcRnExpr hsc_env rdr_expr
         -- it might have a rank-2 type (e.g. :t runST)
     uniq <- newUnique ;
     let { fresh_it  = itName uniq (getLoc rdr_expr) } ;
-    ((_tc_expr, res_ty), lie) <- captureConstraints $ 
-                                 tcInferRho rn_expr ;
+    (((_tc_expr, res_ty), untch), lie) <- captureConstraints  $
+                                          captureUntouchables $
+                                          tcInferRho rn_expr ;
     ((qtvs, dicts, _, _), lie_top) <- captureConstraints $
                                       {-# SCC "simplifyInfer" #-}
-                                      simplifyInfer True {- Free vars are closed -}
+                                      simplifyInfer untch
                                                     False {- No MR for now -}
                                                     [(fresh_it, res_ty)]
                                                     lie ;
@@ -1764,7 +1765,7 @@ tcDump env
 
         -- Dump short output if -ddump-types or -ddump-tc
         when (dopt Opt_D_dump_types dflags || dopt Opt_D_dump_tc dflags)
-             (dumpTcRn short_dump) ;
+             (printForUserTcRn short_dump) ;
 
         -- Dump bindings if -ddump-tc
         dumpOptTcRn Opt_D_dump_tc (mkDumpDoc "Typechecker" full_dump)
index c3215b3..3df8a2c 100644 (file)
@@ -188,8 +188,7 @@ initTc hsc_env hsc_src keep_rn_syntax mod do_this
         lie <- readIORef lie_var ;
         if isEmptyWC lie
            then return ()
-           else pprPanic "initTc: unsolved constraints"
-                         (pprWantedsWithLocs lie) ;
+           else pprPanic "initTc: unsolved constraints" (ppr lie) ;
 
         -- Collect any error messages
         msgs <- readIORef errs_var ;
@@ -484,25 +483,35 @@ traceIf      = traceOptIf Opt_D_dump_if_trace
 traceHiDiffs = traceOptIf Opt_D_dump_hi_diffs
 
 
-traceOptIf :: DumpFlag -> SDoc -> TcRnIf m n ()  -- No RdrEnv available, so qualify everything
-traceOptIf flag doc = whenDOptM flag $
-                          do dflags <- getDynFlags
-                             liftIO (printInfoForUser dflags alwaysQualify doc)
+traceOptIf :: DumpFlag -> SDoc -> TcRnIf m n ()
+traceOptIf flag doc 
+  = whenDOptM flag $    -- No RdrEnv available, so qualify everything
+    do { dflags <- getDynFlags
+       ; liftIO (putMsg dflags doc) }
 
 traceOptTcRn :: DumpFlag -> SDoc -> TcRn ()
 -- Output the message, with current location if opt_PprStyle_Debug
-traceOptTcRn flag doc = whenDOptM flag $ do
-                        { loc  <- getSrcSpanM
-                        ; let real_doc
-                                | opt_PprStyle_Debug = mkLocMessage SevInfo loc doc
-                                | otherwise = doc   -- The full location is
-                                                    -- usually way too much
-                        ; dumpTcRn real_doc }
+traceOptTcRn flag doc 
+  = whenDOptM flag $
+    do { loc  <- getSrcSpanM
+       ; let real_doc
+               | opt_PprStyle_Debug = mkLocMessage SevInfo loc doc
+               | otherwise = doc   -- The full location is
+                                   -- usually way too much
+       ; dumpTcRn real_doc }
 
 dumpTcRn :: SDoc -> TcRn ()
-dumpTcRn doc = do { rdr_env <- getGlobalRdrEnv
-                  ; dflags <- getDynFlags
-                  ; liftIO (printInfoForUser dflags (mkPrintUnqualified dflags rdr_env) doc) }
+dumpTcRn doc
+  = do { dflags <- getDynFlags
+       ; rdr_env <- getGlobalRdrEnv
+       ; liftIO (logInfo dflags (mkDumpStyle (mkPrintUnqualified dflags rdr_env)) doc) }
+
+printForUserTcRn :: SDoc -> TcRn ()
+-- Like dumpTcRn, but for user consumption
+printForUserTcRn doc
+  = do { dflags <- getDynFlags
+       ; rdr_env <- getGlobalRdrEnv
+       ; liftIO (printInfoForUser dflags (mkPrintUnqualified dflags rdr_env) doc) }
 
 debugDumpTcRn :: SDoc -> TcRn ()
 debugDumpTcRn doc | opt_NoDebugOutput = return ()
@@ -695,14 +704,6 @@ reportWarning warn
          errs_var <- getErrsVar ;
          (warns, errs) <- readTcRef errs_var ;
          writeTcRef errs_var (warns `snocBag` warn, errs) }
-
-dumpDerivingInfo :: SDoc -> TcM ()
-dumpDerivingInfo doc
-  = do { dflags <- getDynFlags
-       ; when (dopt Opt_D_dump_deriv dflags) $ do
-       { rdr_env <- getGlobalRdrEnv
-       ; let unqual = mkPrintUnqualified dflags rdr_env
-       ; liftIO (putMsgWith dflags unqual doc) } }
 \end{code}
 
 
@@ -1049,12 +1050,14 @@ newTcEvBinds = do { ref <- newTcRef emptyEvBindMap
 
 addTcEvBind :: EvBindsVar -> EvVar -> EvTerm -> TcM ()
 -- Add a binding to the TcEvBinds by side effect
-addTcEvBind (EvBindsVar ev_ref _) var t
-  = do { bnds <- readTcRef ev_ref
-       ; writeTcRef ev_ref (extendEvBinds bnds var t) }
+addTcEvBind (EvBindsVar ev_ref _) ev_id ev_tm
+  = do { traceTc "addTcEvBind" $ vcat [ text "ev_id =" <+> ppr ev_id
+                                      , text "ev_tm =" <+> ppr ev_tm ]
+       ; bnds <- readTcRef ev_ref
+       ; writeTcRef ev_ref (extendEvBinds bnds ev_id ev_tm) }
 
 getTcEvBinds :: EvBindsVar -> TcM (Bag EvBind)
-getTcEvBinds (EvBindsVar ev_ref _) 
+getTcEvBinds (EvBindsVar ev_ref _)
   = do { bnds <- readTcRef ev_ref
        ; return (evBindMapBinds bnds) }
 
index 22765a7..4d0b2e1 100644 (file)
@@ -45,14 +45,14 @@ module TcRnTypes(
 
         -- Canonical constraints
         Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, dropDerivedWC,
-        singleCt, listToCts, ctsElts, extendCts, extendCtsList,
+        singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
         isEmptyCts, isCTyEqCan, isCFunEqCan,
         isCDictCan_Maybe, isCFunEqCan_maybe,
         isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
         isGivenCt, isHoleCt,
         ctEvidence, ctLoc, ctPred,
         mkNonCanonical, mkNonCanonicalCt,
-        ctEvPred, ctEvTerm, ctEvId, ctEvCheckDepth,
+        ctEvPred, ctEvLoc, ctEvTerm, ctEvCoercion, ctEvId, ctEvCheckDepth,
 
         WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
         andWC, unionsWC, addFlats, addImplics, mkFlatWC, addInsols,
@@ -72,10 +72,10 @@ module TcRnTypes(
         CtEvidence(..),
         mkGivenLoc,
         isWanted, isGiven, isDerived,
-        canRewrite, canRewriteOrSame,
+        eqCanRewrite, canRewriteOrSame,
 
         -- Pretty printing
-        pprEvVarTheta, pprWantedsWithLocs,
+        pprEvVarTheta, 
         pprEvVars, pprEvVarWithType,
         pprArising, pprArisingAt,
 
@@ -932,9 +932,9 @@ type Cts = Bag Ct
 data Ct
   -- Atomic canonical constraints
   = CDictCan {  -- e.g.  Num xi
-      cc_ev :: CtEvidence,   -- See Note [Ct/evidence invariant]
+      cc_ev     :: CtEvidence, -- See Note [Ct/evidence invariant]
       cc_class  :: Class,
-      cc_tyargs :: [Xi]
+      cc_tyargs :: [Xi]        -- cc_tyargs are function-free, hence Xi
     }
 
   | CIrredEvCan {  -- These stand for yet-unusable predicates
@@ -946,26 +946,40 @@ data Ct
         -- See Note [CIrredEvCan constraints]
     }
 
-  | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
-       -- Invariant:
+  | CTyEqCan {  -- tv ~ rhs
+       -- Invariants:
        --   * tv not in tvs(xi)   (occurs check)
-       --   * typeKind xi `subKind` typeKind tv
+       --   * If tv is a TauTv, then rhs has no foralls
+       --       (this avoids substituting a forall for the tyvar in other types)
+       --   * typeKind ty `subKind` typeKind tv
        --       See Note [Kind orientation for CTyEqCan]
-       --   * We prefer unification variables on the left *JUST* for efficiency
-      cc_ev :: CtEvidence,    -- See Note [Ct/evidence invariant]
+       --   * rhs is not necessarily function-free,
+       --       but it has no top-level function.
+       --     E.g. a ~ [F b]  is fine
+       --     but  a ~ F b    is not
+       --   * If rhs is also a tv, then it is oriented to give best chance of
+       --     unification happening; eg if rhs is touchable then lhs is too
+      cc_ev     :: CtEvidence, -- See Note [Ct/evidence invariant]
       cc_tyvar  :: TcTyVar,
-      cc_rhs    :: Xi
+      cc_rhs    :: TcType      -- Not necessarily function-free (hence not Xi)
+                               -- See invariants above
     }
 
-  | CFunEqCan {  -- F xis ~ xi
-       -- Invariant: * isSynFamilyTyCon cc_fun
-       --            * typeKind (F xis) `subKind` typeKind xi
-       --       See Note [Kind orientation for CFunEqCan]
+  | CFunEqCan {  -- F xis ~ fsk
+       -- Invariants:
+       --   * isSynFamilyTyCon cc_fun
+       --   * typeKind (F xis) = tyVarKind fsk
+       --   * always Nominal role
+       --   * always Given or Wanted, never Derived
       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
-                                --    we should have decomposed)
+
+      cc_tyargs :: [Xi],        -- cc_tyargs are function-free (hence Xi)
+        -- Either under-saturated or exactly saturated
+        --    *never* over-saturated (because if so
+        --    we should have decomposed)
+
+      cc_fsk    :: TcTyVar
     }
 
   | CNonCanonical {        -- See Note [NonCanonical Semantics]
@@ -981,11 +995,13 @@ data Ct
 
 Note [Kind orientation for CTyEqCan]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Given an equality  (t:* ~ s:Open), we absolutely want to re-orient it.
-We can't solve it by updating t:=s, ragardless of how touchable 't' is,
-because the kinds don't work.  Indeed we don't want to leave it with
-the orientation (t ~ s), because if that gets into the inert set we'll
-start replacing t's by s's, and that too is the wrong way round.
+Given an equality (t:* ~ s:Open), we can't solve it by updating t:=s,
+ragardless of how touchable 't' is, because the kinds don't work.
+
+Instead we absolutely must re-orient it. Reason: if that gets into the
+inert set we'll start replacing t's by s's, and that might make a
+kind-correct type into a kind error.  After re-orienting,
+we may be able to solve by updating s:=t.
 
 Hence in a CTyEqCan, (t:k1 ~ xi:k2) we require that k2 is a subkind of k1.
 
@@ -1062,7 +1078,7 @@ ctEvidence :: Ct -> CtEvidence
 ctEvidence = cc_ev
 
 ctLoc :: Ct -> CtLoc
-ctLoc = ctev_loc . cc_ev
+ctLoc = ctEvLoc . ctEvidence
 
 ctPred :: Ct -> PredType
 -- See Note [Ct/evidence invariant]
@@ -1092,7 +1108,7 @@ comprehensible error.  Particularly:
 
  * Insoluble derived wanted equalities (e.g. [D] Int ~ Bool) may
    arise from functional dependency interactions.  We are careful
-   to keep a good CtOrigin on such constriants (FunDepOrigin1, FunDepOrigin2)
+   to keep a good CtOrigin on such constraints (FunDepOrigin1, FunDepOrigin2)
    so that we can produce a good error message (Trac #9612)
 
 Since we leave these Derived constraints in the residual WantedConstraints,
@@ -1173,8 +1189,11 @@ listToCts = listToBag
 ctsElts :: Cts -> [Ct]
 ctsElts = bagToList
 
-extendCts :: Cts -> Ct -> Cts
-extendCts = snocBag
+consCts :: Ct -> Cts -> Cts
+consCts = consBag
+
+snocCts :: Cts -> Ct -> Cts
+snocCts = snocBag
 
 extendCtsList :: Cts -> [Ct] -> Cts
 extendCtsList cts xs | null xs   = cts
@@ -1251,15 +1270,15 @@ addInsols wc cts
 instance Outputable WantedConstraints where
   ppr (WC {wc_flat = f, wc_impl = i, wc_insol = n})
    = ptext (sLit "WC") <+> braces (vcat
-        [ if isEmptyBag f then empty else
-          ptext (sLit "wc_flat =")  <+> pprBag ppr f
-        , if isEmptyBag i then empty else
-          ptext (sLit "wc_impl =")  <+> pprBag ppr i
-        , if isEmptyBag n then empty else
-          ptext (sLit "wc_insol =") <+> pprBag ppr n ])
-
-pprBag :: (a -> SDoc) -> Bag a -> SDoc
-pprBag pp b = foldrBag (($$) . pp) empty b
+        [ ppr_bag (ptext (sLit "wc_flat")) f
+        , ppr_bag (ptext (sLit "wc_insol")) n
+        , ppr_bag (ptext (sLit "wc_impl")) i ])
+
+ppr_bag :: Outputable a => SDoc -> Bag a -> SDoc
+ppr_bag doc bag
+ | isEmptyBag bag = empty
+ | otherwise      = hang (doc <+> equals) 
+                       2 (foldrBag (($$) . ppr) empty bag)
 \end{code}
 
 
@@ -1283,10 +1302,6 @@ data Implication
                                  --   (order does not matter)
                                  -- See Invariant (GivenInv) in TcType
 
-      ic_fsks  :: [TcTyVar],     -- Extra flatten-skolems introduced by
-                                 -- by flattening the givens
-                                 -- See Note [Given flatten-skolems]
-
       ic_no_eqs :: Bool,         -- True  <=> ic_givens have no equalities, for sure
                                  -- False <=> ic_givens might have equalities
 
@@ -1302,19 +1317,19 @@ data Implication
     }
 
 instance Outputable Implication where
-  ppr (Implic { ic_untch = untch, ic_skols = skols, ic_fsks = fsks
+  ppr (Implic { ic_untch = untch, ic_skols = skols
               , ic_given = given, ic_no_eqs = no_eqs
-              , ic_wanted = wanted
+              , ic_wanted = wanted, ic_insol = insol
               , ic_binds = binds, ic_info = info })
-   = ptext (sLit "Implic") <+> braces
-     (sep [ ptext (sLit "Untouchables =") <+> ppr untch
-          , ptext (sLit "Skolems =") <+> pprTvBndrs skols
-          , ptext (sLit "Flatten-skolems =") <+> pprTvBndrs fsks
-          , ptext (sLit "No-eqs =") <+> ppr no_eqs
-          , ptext (sLit "Given =") <+> pprEvVars given
-          , ptext (sLit "Wanted =") <+> ppr wanted
-          , ptext (sLit "Binds =") <+> ppr binds
-          , pprSkolInfo info ])
+   = hang (ptext (sLit "Implic") <+> lbrace)
+        2 (sep [ ptext (sLit "Untouchables =") <+> ppr untch
+               , ptext (sLit "Skolems =") <+> pprTvBndrs skols
+               , ptext (sLit "No-eqs =") <+> ppr no_eqs
+               , ptext (sLit "Insol =") <+> ppr insol
+               , hang (ptext (sLit "Given ="))  2 (pprEvVars given)
+               , hang (ptext (sLit "Wanted =")) 2 (ppr wanted)
+               , ptext (sLit "Binds =") <+> ppr binds
+               , pprSkolInfo info ] <+> rbrace)
 \end{code}
 
 Note [Shadowing in a constraint]
@@ -1385,12 +1400,6 @@ pprEvVarTheta ev_vars = pprTheta (map evVarPred ev_vars)
 
 pprEvVarWithType :: EvVar -> SDoc
 pprEvVarWithType v = ppr v <+> dcolon <+> pprType (evVarPred v)
-
-pprWantedsWithLocs :: WantedConstraints -> SDoc
-pprWantedsWithLocs wcs
-  =  vcat [ pprBag ppr (wc_flat wcs)
-          , pprBag ppr (wc_impl wcs)
-          , pprBag ppr (wc_insol wcs) ]
 \end{code}
 
 %************************************************************************
@@ -1428,16 +1437,26 @@ ctEvPred :: CtEvidence -> TcPredType
 -- The predicate of a flavor
 ctEvPred = ctev_pred
 
+ctEvLoc :: CtEvidence -> CtLoc
+ctEvLoc = ctev_loc
+
 ctEvTerm :: CtEvidence -> EvTerm
 ctEvTerm (CtGiven   { ctev_evtm = tm }) = tm
 ctEvTerm (CtWanted  { ctev_evar = ev }) = EvId ev
 ctEvTerm ctev@(CtDerived {}) = pprPanic "ctEvTerm: derived constraint cannot have id"
                                       (ppr ctev)
 
+ctEvCoercion :: CtEvidence -> TcCoercion
+-- ctEvCoercion ev = evTermCoercion (ctEvTerm ev)
+ctEvCoercion (CtGiven   { ctev_evtm = tm }) = evTermCoercion tm
+ctEvCoercion (CtWanted  { ctev_evar = v })  = mkTcCoVarCo v
+ctEvCoercion ctev@(CtDerived {}) = pprPanic "ctEvCoercion: derived constraint cannot have id"
+                                      (ppr ctev)
+
 -- | Checks whether the evidence can be used to solve a goal with the given minimum depth
 ctEvCheckDepth :: SubGoalDepth -> CtEvidence -> Bool
 ctEvCheckDepth _      (CtGiven {})   = True -- Given evidence has infinite depth
-ctEvCheckDepth min ev@(CtWanted {})  = min <= ctLocDepth (ctev_loc ev)
+ctEvCheckDepth min ev@(CtWanted {})  = min <= ctLocDepth (ctEvLoc ev)
 ctEvCheckDepth _   ev@(CtDerived {}) = pprPanic "ctEvCheckDepth: cannot consider derived evidence" (ppr ev)
 
 ctEvId :: CtEvidence -> TcId
@@ -1464,13 +1483,14 @@ isDerived (CtDerived {}) = True
 isDerived _              = False
 
 -----------------------------------------
-canRewrite :: CtEvidence -> CtEvidence -> Bool
+eqCanRewrite :: TcTyVar -> CtEvidence -> CtEvidence -> Bool
 -- Very important function!
 -- See Note [canRewrite and canRewriteOrSame]
-canRewrite (CtGiven {})   _              = True
-canRewrite (CtWanted {})  (CtDerived {}) = True
-canRewrite (CtDerived {}) (CtDerived {}) = True  -- Derived can't solve wanted/given
-canRewrite _ _ = False             -- No evidence for a derived, anyway
+eqCanRewrite _  (CtGiven {})   _              = True
+eqCanRewrite _  (CtWanted {})  (CtDerived {}) = True
+eqCanRewrite tv (CtWanted {})  (CtWanted {})  = not (isFmvTyVar tv) && isMetaTyVar tv
+eqCanRewrite _  (CtDerived {}) (CtDerived {}) = True  -- Derived can't solve wanted/given
+eqCanRewrite _ _ _ = False             -- No evidence for a derived, anyway
 
 canRewriteOrSame :: CtEvidence -> CtEvidence -> Bool
 canRewriteOrSame (CtGiven {})   _              = True
@@ -1628,11 +1648,13 @@ data CtLoc = CtLoc { ctl_origin :: CtOrigin
   --    source location:  tcl_loc   :: SrcSpan
   --    context:          tcl_ctxt  :: [ErrCtxt]
   --    binder stack:     tcl_bndrs :: [TcIdBinders]
+  --    level:            tcl_untch :: Untouchables
 
-mkGivenLoc :: SkolemInfo -> TcLclEnv -> CtLoc
-mkGivenLoc skol_info env = CtLoc { ctl_origin = GivenOrigin skol_info
-                                 , ctl_env = env
-                                 , ctl_depth = initialSubGoalDepth }
+mkGivenLoc :: Untouchables -> SkolemInfo -> TcLclEnv -> CtLoc
+mkGivenLoc untch skol_info env 
+  = CtLoc { ctl_origin = GivenOrigin skol_info
+          , ctl_env    = env { tcl_untch = untch }
+          , ctl_depth  = initialSubGoalDepth }
 
 ctLocEnv :: CtLoc -> TcLclEnv
 ctLocEnv = ctl_env
@@ -1775,9 +1797,6 @@ pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) ptext (sLit "Unk
 \begin{code}
 data CtOrigin
   = GivenOrigin SkolemInfo
-  | FlatSkolOrigin              -- Flatten-skolems created for Givens
-                                -- Note [When does an implication have given equalities?]
-                                -- in TcSimplify
 
   -- All the others are for *wanted* constraints
   | OccurrenceOf Name           -- Occurrence of an overloaded identifier
@@ -1836,7 +1855,6 @@ data CtOrigin
   | UnboundOccurrenceOf RdrName
   | ListOrigin          -- An overloaded list
 
-
 ctoHerald :: SDoc
 ctoHerald = ptext (sLit "arising from")
 
@@ -1887,7 +1905,6 @@ pprCtOrigin simple_origin
 
 ----------------
 pprCtO :: CtOrigin -> SDoc  -- Ones that are short one-liners
-pprCtO FlatSkolOrigin        = ptext (sLit "a given flatten-skolem")
 pprCtO (OccurrenceOf name)   = hsep [ptext (sLit "a use of"), quotes (ppr name)]
 pprCtO AppOrigin             = ptext (sLit "an application")
 pprCtO (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
index 3b405b3..f1d528f 100644 (file)
@@ -168,7 +168,6 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
        ; rhs_binds_var <- newTcEvBinds
        ; emitImplication $ Implic { ic_untch  = noUntouchables
                                   , ic_skols  = qtkvs
-                                  , ic_fsks   = []
                                   , ic_no_eqs = False
                                   , ic_given  = lhs_evs
                                   , ic_wanted = rhs_wanted
@@ -183,7 +182,6 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
        ; lhs_binds_var <- newTcEvBinds
        ; emitImplication $ Implic { ic_untch  = noUntouchables
                                   , ic_skols  = qtkvs
-                                  , ic_fsks   = []
                                   , ic_no_eqs = False
                                   , ic_given  = lhs_evs
                                   , ic_wanted = other_lhs_wanted
index 034c7a8..f29c78b 100644 (file)
@@ -7,32 +7,30 @@ module TcSMonad (
        -- Canonical constraints, definition is now in TcRnTypes
 
     WorkList(..), isEmptyWorkList, emptyWorkList,
-    workListFromEq, workListFromNonEq, workListFromCt,
-    extendWorkListEq, extendWorkListFunEq,
+    extendWorkListFunEq,
     extendWorkListNonEq, extendWorkListCt,
-    extendWorkListCts, extendWorkListEqs, appendWorkList, selectWorkItem,
-    withWorkList, workListSize,
+    extendWorkListCts, appendWorkList, selectWorkItem,
+    workListSize,
 
     updWorkListTcS, updWorkListTcS_return,
 
-    updTcSImplics,
+    updInertCans, updInertDicts, updInertIrreds, updInertFunEqs,
 
     Ct(..), Xi, tyVarsOfCt, tyVarsOfCts,
-    emitInsoluble,
+    emitInsoluble, emitWorkNC,
 
     isWanted, isDerived,
     isGivenCt, isWantedCt, isDerivedCt,
 
-    canRewrite,
     mkGivenLoc,
 
     TcS, runTcS, runTcSWithEvBinds, failTcS, panicTcS, traceTcS, -- Basic functionality
-    traceFireTcS, bumpStepCountTcS,
+    traceFireTcS, bumpStepCountTcS, csTraceTcS,
     tryTcS, nestTcS, nestImplicTcS, recoverTcS,
     wrapErrTcS, wrapWarnTcS,
 
     -- Getting and setting the flattening cache
-    addSolvedDict, addSolvedFunEq, getGivenInfo,
+    addSolvedDict, 
 
     -- Marking stuff as used
     addUsedRdrNamesTcS,
@@ -41,14 +39,18 @@ module TcSMonad (
 
     setEvBind,
     XEvTerm(..),
-    MaybeNew (..), isFresh, freshGoal, freshGoals, getEvTerm, getEvTerms,
+    MaybeNew (..), isFresh, freshGoals, getEvTerm, getEvTerms,
+
+    StopOrContinue(..), continueWith, stopWith, andWhenContinue,
 
     xCtEvidence,        -- Transform a CtEvidence during a step
     rewriteEvidence,    -- Specialized version of xCtEvidence for coercions
     rewriteEqEvidence,  -- Yet more specialised, for equality coercions
     maybeSym,
 
-    newWantedEvVar, newWantedEvVarNC, newWantedEvVarNonrec, newDerived,
+    newTcEvBinds, newWantedEvVar, newWantedEvVarNC, newWantedEvVarNonrec, 
+    newEvVar, newGivenEvVar, newDerived, 
+    emitNewDerived, emitNewDerivedEq,
     instDFunConstraints,
 
        -- Creation of evidence variables
@@ -56,26 +58,29 @@ module TcSMonad (
 
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
-    getTcEvBindsMap, getTcSTyBindsMap,
+    getTcEvBindsMap, 
 
-    lookupFlatEqn, newFlattenSkolem,            -- Flatten skolems
+    lookupFlatCache, newFlattenSkolem,            -- Flatten skolems
 
         -- Deque
     Deque(..), insertDeque, emptyDeque,
 
         -- Inerts
     InertSet(..), InertCans(..),
-    getInertEqs,
-    emptyInert, getTcSInerts, setTcSInerts,
+    getInertCans, setInertCans, getInertEqs,
+    emptyInert, getTcSInerts, setTcSInerts, setInertFunEqs,
     getInertUnsolved, checkAllSolved,
+    getInertGivens,
     prepareInertsForImplications,
-    addInertCan, insertInertItemTcS,
+    addInertCan, insertInertItemTcS, insertFunEq,
     EqualCtList,
     lookupSolvedDict, extendFlatCache,
 
-    findFunEq, findTyEqs,
     findDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
-    findFunEqsByTyCon, findFunEqs, addFunEq, replaceFunEqs, partitionFunEqs,
+
+    findFunEq, findTyEqs, 
+    findFunEqsByTyCon, findFunEqs, partitionFunEqs,
+    sizeFunEqMap,
 
     instDFunType,                              -- Instantiation
     newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
@@ -122,11 +127,10 @@ import Name
 import RdrName (RdrName, GlobalRdrEnv)
 import RnEnv (addUsedRdrNames)
 import Var
-import VarSet
 import VarEnv
+import VarSet
 import Outputable
 import Bag
-import MonadUtils
 import UniqSupply
 
 import FastString
@@ -137,13 +141,13 @@ import TcRnTypes
 import BasicTypes
 import Unique
 import UniqFM
-import Maybes ( orElse, catMaybes, firstJusts )
-import Pair ( pSnd )
+import Maybes ( orElse, firstJusts )
 
 import TrieMap
-import Control.Monad( ap, when )
+import Control.Monad( ap, when, unless )
+import MonadUtils
 import Data.IORef
-import Data.List( partition )
+import Pair
 
 #ifdef DEBUG
 import Digraph
@@ -191,7 +195,10 @@ data Deque a = DQ [a] [a]   -- Insert in RH field, remove from LH field
                             -- First to remove is at head of LH field
 
 instance Outputable a => Outputable (Deque a) where
-  ppr (DQ as bs) = ppr (as ++ reverse bs)   -- Show first one to come out at the start
+  ppr q = ppr (dequeList q)
+
+dequeList :: Deque a -> [a]
+dequeList (DQ as bs) = as ++ reverse bs  -- First one to come out at the start
 
 emptyDeque :: Deque a
 emptyDeque = DQ [] []
@@ -216,75 +223,72 @@ extractDeque (DQ [] bs)     = case reverse bs of
                                 [] -> panic "extractDeque"
 
 -- See Note [WorkList priorities]
-data WorkList = WorkList { wl_eqs    :: [Ct]
-                         , wl_funeqs :: Deque Ct
-                         , wl_rest   :: [Ct]
-                         }
-
+data WorkList 
+  = WL { wl_eqs     :: [Ct]
+       , wl_funeqs  :: Deque Ct
+       , wl_rest    :: [Ct]
+       , wl_implics :: Bag Implication  -- See Note [Residual implications]
+    }
 
 appendWorkList :: WorkList -> WorkList -> WorkList
-appendWorkList new_wl orig_wl
-   = WorkList { wl_eqs    = wl_eqs new_wl    ++            wl_eqs orig_wl
-              , wl_funeqs = wl_funeqs new_wl `appendDeque` wl_funeqs orig_wl
-              , wl_rest   = wl_rest new_wl   ++            wl_rest orig_wl }
+appendWorkList 
+    (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1, wl_implics = implics1 })
+    (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2, wl_implics = implics2 })
+   = WL { wl_eqs     = eqs1     ++            eqs2
+        , wl_funeqs  = funeqs1  `appendDeque` funeqs2
+        , wl_rest    = rest1    ++            rest2
+        , wl_implics = implics1 `unionBags`   implics2 }
 
 
 workListSize :: WorkList -> Int
-workListSize (WorkList { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
+workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
   = length eqs + dequeSize funeqs + length rest
 
 extendWorkListEq :: Ct -> WorkList -> WorkList
--- Extension by equality
-extendWorkListEq ct wl
-  | Just {} <- isCFunEqCan_maybe ct
-  = extendWorkListFunEq ct wl
-  | otherwise
+extendWorkListEq ct wl 
   = wl { wl_eqs = ct : wl_eqs wl }
 
 extendWorkListFunEq :: Ct -> WorkList -> WorkList
 extendWorkListFunEq ct wl
   = wl { wl_funeqs = insertDeque ct (wl_funeqs wl) }
 
-extendWorkListEqs :: [Ct] -> WorkList -> WorkList
--- Append a list of equalities
-extendWorkListEqs cts wl = foldr extendWorkListEq wl cts
-
 extendWorkListNonEq :: Ct -> WorkList -> WorkList
 -- Extension by non equality
 extendWorkListNonEq ct wl
   = wl { wl_rest = ct : wl_rest wl }
 
+extendWorkListImplic :: Implication -> WorkList -> WorkList
+extendWorkListImplic implic wl
+  = wl { wl_implics = implic `consBag` wl_implics wl }
+
 extendWorkListCt :: Ct -> WorkList -> WorkList
 -- Agnostic
 extendWorkListCt ct wl
- | isEqPred (ctPred ct) = extendWorkListEq ct wl
- | otherwise = extendWorkListNonEq ct wl
+ = case classifyPredType (ctPred ct) of
+     EqPred ty1 _
+       | Just (tc,_) <- tcSplitTyConApp_maybe ty1
+       , isSynFamilyTyCon tc
+       -> extendWorkListFunEq ct wl
+       | otherwise
+       -> extendWorkListEq ct wl
+
+     _ -> extendWorkListNonEq ct wl
 
 extendWorkListCts :: [Ct] -> WorkList -> WorkList
 -- Agnostic
 extendWorkListCts cts wl = foldr extendWorkListCt wl cts
 
 isEmptyWorkList :: WorkList -> Bool
-isEmptyWorkList wl
-  = null (wl_eqs wl) &&  null (wl_rest wl) && isEmptyDeque (wl_funeqs wl)
+isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
+                    , wl_rest = rest, wl_implics = implics })
+  = null eqs && null rest && isEmptyDeque funeqs && isEmptyBag implics
 
 emptyWorkList :: WorkList
-emptyWorkList = WorkList { wl_eqs  = [], wl_rest = [], wl_funeqs = emptyDeque }
-
-workListFromEq :: Ct -> WorkList
-workListFromEq ct = extendWorkListEq ct emptyWorkList
-
-workListFromNonEq :: Ct -> WorkList
-workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList
-
-workListFromCt :: Ct -> WorkList
--- Agnostic
-workListFromCt ct | isEqPred (ctPred ct) = workListFromEq ct
-                  | otherwise            = workListFromNonEq ct
-
+emptyWorkList = WL { wl_eqs  = [], wl_rest = []
+                   , wl_funeqs = emptyDeque, wl_implics = emptyBag }
 
 selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
-selectWorkItem wl@(WorkList { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
+selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
   = case (eqs,feqs,rest) of
       (ct:cts,_,_)     -> (Just ct, wl { wl_eqs    = cts })
       (_,fun_eqs,_)    | Just (fun_eqs', ct) <- extractDeque fun_eqs
@@ -294,10 +298,18 @@ selectWorkItem wl@(WorkList { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
 
 -- Pretty printing
 instance Outputable WorkList where
-  ppr wl = vcat [ text "WorkList (eqs)   = " <+> ppr (wl_eqs wl)
-                , text "WorkList (funeqs)= " <+> ppr (wl_funeqs wl)
-                , text "WorkList (rest)  = " <+> ppr (wl_rest wl)
-                ]
+  ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
+          , wl_rest = rest, wl_implics = implics })
+   = text "WL" <+> (braces $
+     vcat [ ppUnless (null eqs) $ 
+            ptext (sLit "Eqs =") <+> vcat (map ppr eqs)
+          , ppUnless (isEmptyDeque feqs) $
+            ptext (sLit "Funeqs =") <+> vcat (map ppr (dequeList feqs))
+          , ppUnless (null rest) $
+            ptext (sLit "Eqs =") <+> vcat (map ppr rest)
+          , ppUnless (isEmptyBag implics) $
+            ptext (sLit "Implics =") <+> vcat (map ppr (bagToList implics))
+          ])
 \end{code}
 
 %************************************************************************
@@ -341,8 +353,8 @@ The InertCans represents a collection of constraints with the following properti
          idempotent as possible but this would only be true for
          constraints of the same flavor, so in total the inert
          substitution could not be idempotent, due to flavor-related
-         issued.  Note [Non-idempotent inert substitution] explains
-         what is going on.
+         issued.  Note [Non-idempotent inert substitution] in TcCanonical
+         explains what is going on.
 
        - Whenever a constraint ends up in the worklist we do
          recursively apply exhaustively the inert substitution to it
@@ -378,7 +390,7 @@ The reason for all this is simply to avoid re-solving goals we have solved alrea
 
 Note [Type family equations]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Type-family equations, of form (ev : F tys ~ ty), live in four places
+Type-family equations, of form (ev : F tys ~ ty), live in three places
 
   * The work-list, of course
 
@@ -393,11 +405,7 @@ Type-family equations, of form (ev : F tys ~ ty), live in four places
     a top-level goal.  Eg in the above example we don't want to solve w3
     using w3 itself!
 
-  * The inert_solved_funeqs.  These are all "solved" goals (see Note [Solved constraints]),
-    the result of using a top-level type-family instance.
-
-  * The inert_funeqs are un-solved but fully processed and in the InertCans.
-
+  * THe inert_funeqs are un-solved but fully processed and in the InertCans.
 
 \begin{code}
 -- All Given (fully known) or Wanted or Derived
@@ -408,7 +416,7 @@ data InertCans
               -- Some Refl equalities are also in tcs_ty_binds
               -- see Note [Spontaneously solved in TyBinds] in TcInteract
 
-       , inert_funeqs :: FunEqMap EqualCtList
+       , inert_funeqs :: FunEqMap Ct
               -- All CFunEqCans; index is the whole family head type.
 
        , inert_dicts :: DictMap Ct
@@ -421,13 +429,6 @@ data InertCans
 
        , inert_insols :: Cts
               -- Frozen errors (as non-canonicals)
-
-       , inert_no_eqs :: !Bool    
-              -- Set to False when adding a new equality
-              -- (eq/funeq) or potential equality (irred)
-              -- whose evidence is not a constant
-              -- See Note [When does an implication have given equalities?]
-              -- in TcSimplify
        }
 
 type EqualCtList = [Ct]
@@ -448,8 +449,10 @@ data InertSet
               -- Canonical Given, Wanted, Derived (no Solved)
               -- Sometimes called "the inert set"
 
-       , inert_flat_cache :: FunEqMap (CtEvidence, TcType)
+       , inert_flat_cache :: FunEqMap (TcCoercion, TcTyVar)
               -- See Note [Type family equations]
+              -- If    F tys :-> (co, fsk), 
+              -- then  co :: F tys ~ fsk
               -- Just a hash-cons cache for use when flattening only
               -- These include entirely un-processed goals, so don't use
               -- them to solve a top-level goal, else you may end up solving
@@ -457,17 +460,6 @@ data InertSet
               -- when allocating a new flatten-skolem.
               -- Not necessarily inert wrt top-level equations (or inert_cans)
 
-       , inert_fsks :: [TcTyVar]  -- Rigid flatten-skolems (arising from givens)
-                                  -- allocated in this local scope
-                                  -- See Note [Given flatten-skolems]
-
-       , inert_solved_funeqs :: FunEqMap (CtEvidence, TcType)
-              -- See Note [Type family equations]
-              -- Of form co :: F xis ~ xi
-              -- Always the result of using a top-level family axiom F xis ~ tau
-              -- No Deriveds
-              -- Not necessarily fully rewritten (by type substitutions)
-
        , inert_solved_dicts   :: DictMap CtEvidence
               -- Of form ev :: C t1 .. tn
               -- Always the result of using a top-level instance declaration
@@ -479,33 +471,12 @@ data InertSet
        }
 \end{code}
 
-Note [Given flatten-skolems]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we simplify the implication
-    forall b. C (F a) b => (C (F a) beta, blah)
-We'll flatten the givens, introducing a flatten-skolem, so the
-givens effectively look like
-    (C fsk b, F a ~ fsk)
-Then we simplify the wanteds, transforming (C (F a) beta) to (C fsk beta).
-Now, if we don't solve that wanted, we'll put it back into the residual
-implication.  But where is fsk bound?
-
-We solve this by recording the given flatten-skolems in the implication
-(the ic_fsks field), so it's as if we change the implication to
-    forall b, fsk. (C fsk b, F a ~ fsk) => (C fsk beta, blah)
-
-We don't need to explicitly record the (F a ~ fsk) constraint in the implication
-because we can recover it from inside the fsk TyVar itself.  But we do need
-to treat that (F a ~ fsk) as a new given.  See the fsk_bag stuff in
-TcInteract.solveInteractGiven.
-
 \begin{code}
 instance Outputable InertCans where
   ppr ics = vcat [ ptext (sLit "Equalities:")
                    <+> vcat (map ppr (varEnvElts (inert_eqs ics)))
                  , ptext (sLit "Type-function equalities:")
                    <+> vcat (map ppr (funEqsToList (inert_funeqs ics)))
-                 , ptext (sLit "No-eqs:") <+> ppr (inert_no_eqs ics)
                  , ptext (sLit "Dictionaries:")
                    <+> vcat (map ppr (Bag.bagToList $ dictsToBag (inert_dicts ics)))
                  , ptext (sLit "Irreds:")
@@ -516,8 +487,7 @@ instance Outputable InertCans where
 
 instance Outputable InertSet where
   ppr is = vcat [ ppr $ inert_cans is
-                , text "Solved dicts"  <+> int (sizeDictMap (inert_solved_dicts is))
-                , text "Solved funeqs" <+> int (sizeFunEqMap (inert_solved_funeqs is))]
+                , text "Solved dicts"  <+> int (sizeDictMap (inert_solved_dicts is)) ]
 
 emptyInert :: InertSet
 emptyInert
@@ -526,31 +496,23 @@ emptyInert
                          , inert_funeqs  = emptyFunEqs
                          , inert_irreds  = emptyCts
                          , inert_insols  = emptyCts
-                         , inert_no_eqs  = True  -- See Note [inert_fsks and inert_no_eqs]
                          }
-       , inert_fsks          = []  -- See Note [inert_fsks and inert_no_eqs]
        , inert_flat_cache    = emptyFunEqs
-       , inert_solved_funeqs = emptyFunEqs
        , inert_solved_dicts  = emptyDictMap }
 
 ---------------
 addInertCan :: InertCans -> Ct -> InertCans
 -- Precondition: item /is/ canonical
-addInertCan ics item@(CTyEqCan { cc_ev = ev })
+addInertCan ics item@(CTyEqCan {})
   = ics { inert_eqs = extendVarEnv_C (\eqs _ -> item : eqs)
                               (inert_eqs ics)
-                              (cc_tyvar item) [item]
-        , inert_no_eqs = isFlatSkolEv ev && inert_no_eqs ics }
-    -- See Note [When does an implication have given equalities?] in TcSimplify
+                              (cc_tyvar item) [item] }
 
-addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys, cc_ev = ev })
-  = ics { inert_funeqs = addFunEq (inert_funeqs ics) tc tys item
-        , inert_no_eqs = isFlatSkolEv ev && inert_no_eqs ics }
-    -- See Note [When does an implication have given equalities?] in TcSimplify
+addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
+  = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
 
 addInertCan ics item@(CIrredEvCan {})
-  = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item
-        , inert_no_eqs = False }
+  = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
        -- The 'False' is because the irreducible constraint might later instantiate
        -- to an equality.
        -- But since we try to simplify first, if there's a constraint function FC with
@@ -565,14 +527,6 @@ addInertCan _ item
     ppr item   -- Can't be CNonCanonical, CHoleCan,
                -- because they only land in inert_insols
 
-isFlatSkolEv :: CtEvidence -> Bool
--- True if (a) it's a Given and (b) it is evidence for
--- (or derived from) a flatten-skolem equality.
--- See Note [When does an implication have given equalities?] in TcSimplify
-isFlatSkolEv ev = case ctLocOrigin (ctev_loc ev) of
-                    FlatSkolOrigin -> True
-                    _              -> False
-
 --------------
 insertInertItemTcS :: Ct -> TcS ()
 -- Add a new item in the inerts of the monad
@@ -580,7 +534,7 @@ insertInertItemTcS item
   = do { traceTcS "insertInertItemTcS {" $
          text "Trying to insert new inert item:" <+> ppr item
 
-       ; updInertTcS (\ics -> ics { inert_cans = addInertCan (inert_cans ics) item })
+       ; updInertCans (\ics -> addInertCan ics item)
 
        ; traceTcS "insertInertItemTcS }" $ empty }
 
@@ -594,64 +548,72 @@ addSolvedDict item cls tys
        ; updInertTcS $ \ ics ->
              ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
 
-addSolvedFunEq :: TyCon -> [TcType] -> CtEvidence -> TcType -> TcS ()
-addSolvedFunEq fam_tc tys ev rhs_ty
-  = updInertTcS $ \ inert ->
-    inert { inert_solved_funeqs = insertFunEq (inert_solved_funeqs inert)
-                                              fam_tc tys (ev, rhs_ty) }