Equality constraint solver is now externally pure

[ghc-hetmet.git] / compiler / typecheck / TcTyFuns.lhs
diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs

index 0b026e1..c7fac2d 100644 (file)
--- a/compiler/typecheck/TcTyFuns.lhs
+++ b/compiler/typecheck/TcTyFuns.lhs
@@ -30,7 +30,6 @@ import Type
  import TypeRep         ( Type(..) )
  import TyCon
  import HsSyn
  import TypeRep         ( Type(..) )
  import TyCon
  import HsSyn
-import Id
  import VarEnv
  import VarSet
  import Var
  import VarEnv
  import VarSet
  import Var
@@ -39,6 +38,7 @@ import Bag
  import Outputable
  import SrcLoc  ( Located(..) )
  import Maybes
  import Outputable
  import SrcLoc  ( Located(..) )
  import Maybes
+import MonadUtils
  import FastString
  
  -- standard
  import FastString
  
  -- standard
@@ -70,21 +70,16 @@ tcUnfoldSynFamInst (TyConApp tycon tys)
    | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
    = return Nothing
    | otherwise
    | not (isOpenSynTyCon tycon)     -- unfold *only* _synonym_ family instances
    = return Nothing
    | otherwise
-  = do { -- we only use the indexing arguments for matching, 
-         -- not the additional ones
-       ; maybeFamInst <- tcLookupFamInst tycon idxTys
+  = do { -- The TyCon might be over-saturated, but that's ok for tcLookupFamInst
+       ; maybeFamInst <- tcLookupFamInst tycon tys
         ; case maybeFamInst of
             Nothing                -> return Nothing
         ; case maybeFamInst of
             Nothing                -> return Nothing
-           Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
-                                                   mkTyConApp coe_tc tys')
+           Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
+                                                   mkTyConApp coe_tc rep_tys)
               where
               where
-               tys'   = rep_tys ++ restTys
                 coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst" 
                                     (tyConFamilyCoercion_maybe rep_tc)
         }
                 coe_tc = expectJust "TcTyFuns.tcUnfoldSynFamInst" 
                                     (tyConFamilyCoercion_maybe rep_tc)
         }
-    where
-        n                = tyConArity tycon
-        (idxTys, restTys) = splitAt n tys
  tcUnfoldSynFamInst _other = return Nothing
  \end{code}
  
  tcUnfoldSynFamInst _other = return Nothing
  \end{code}
  
@@ -203,23 +198,67 @@ tcGenericNormaliseFamInstPred fun (EqPred ty1 ty2)
  %*                                                                     *
  %************************************************************************
  
  %*                                                                     *
  %************************************************************************
  
+Given a set of given, local constraints and a set of wanted constraints,
+simplify the wanted equalities as far as possible and normalise both local and
+wanted dictionaries with respect to the equalities.
+
+In addition to the normalised local dictionaries and simplified wanteds, the
+function yields bindings for instantiated meta variables (due to solving
+equality constraints) and dictionary bindings (due to simplifying class
+constraints).  The bag of type variable bindings only contains bindings for
+non-local variables - i.e., type variables other than those newly created by
+the present function.  Consequently, type improvement took place iff the bag
+of bindings contains any bindings for proper type variables (not just covars).
+The solver does not instantiate any non-local variables; i.e., the bindings
+must be executed by the caller.
+
+All incoming constraints are assumed to be zonked already.  All outgoing
+constraints will be zonked again.
+
+NB: The solver only has local effects that cannot be observed from outside.
+    In particular, it can be executed twice on the same constraint set with
+    the same result (modulo generated variables names).
+
  \begin{code}
  tcReduceEqs :: [Inst]             -- locals
              -> [Inst]             -- wanteds
              -> TcM ([Inst],       -- normalised locals (w/o equalities)
                      [Inst],       -- normalised wanteds (including equalities)
  \begin{code}
  tcReduceEqs :: [Inst]             -- locals
              -> [Inst]             -- wanteds
              -> TcM ([Inst],       -- normalised locals (w/o equalities)
                      [Inst],       -- normalised wanteds (including equalities)
-                    TcDictBinds,  -- bindings for all simplified dictionaries
-                    Bool)         -- whether any flexibles where instantiated
+                    TcTyVarBinds, -- bindings for meta type variables
+                    TcDictBinds)  -- bindings for all simplified dictionaries
  tcReduceEqs locals wanteds
  tcReduceEqs locals wanteds
-  = do { let (local_eqs  , local_dicts)   = partition isEqInst locals
-             (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
-       ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
-       ; eqCfg2 <- normaliseDicts False local_dicts
-       ; eqCfg3 <- normaliseDicts True  wanteds_dicts
-       ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig` eqCfg2 
-                                       `unionEqConfig` eqCfg3)
-       ; finaliseEqsAndDicts eqCfg
+  = do { ((locals, wanteds, dictBinds), tyBinds) <- getTcTyVarBinds $
+           do { let (local_eqs  , local_dicts)   = partition isEqInst locals
+                    (wanteds_eqs, wanteds_dicts) = partition isEqInst wanteds
+              ; eqCfg1 <- normaliseEqs (local_eqs ++ wanteds_eqs)
+              ; eqCfg2 <- normaliseDicts False local_dicts
+              ; eqCfg3 <- normaliseDicts True  wanteds_dicts
+              ; eqCfg <- propagateEqs (eqCfg1 `unionEqConfig` 
+                                       eqCfg2 `unionEqConfig`
+                                       eqCfg3) 
+              ; finaliseEqsAndDicts freeFlexibles eqCfg
+              }
+         -- execute type bindings of skolem flexibles...
+       ; tyBinds_pruned <- pruneTyBinds tyBinds freeFlexibles
+         -- ...and zonk the constraints to propagate the bindings
+       ; locals_z  <- zonkInsts locals
+       ; wanteds_z <- zonkInsts wanteds
+       ; return (locals_z, wanteds_z, tyBinds_pruned, dictBinds)
         }
         }
+   where
+     -- unification variables that appear in the environment and may not be
+     -- instantiated - this includes coercion variables
+     freeFlexibles = tcTyVarsOfInsts locals `unionVarSet` 
+                     tcTyVarsOfInsts wanteds
+
+     pruneTyBinds tybinds freeFlexibles
+       = do { let tybinds'                      = bagToList tybinds
+                  (skolem_tybinds, env_tybinds) = partition isSkolem tybinds'
+            ; execTcTyVarBinds (listToBag skolem_tybinds)
+            ; return $ listToBag env_tybinds
+            }
+       where
+         isSkolem (TcTyVarBind tv _ ) = not (tv `elemVarSet` freeFlexibles)
  \end{code}
  
  
  \end{code}
  
  
@@ -232,9 +271,6 @@ tcReduceEqs locals wanteds
  We maintain normalised equalities together with the skolems introduced as
  intermediates during flattening of equalities as well as 
  
  We maintain normalised equalities together with the skolems introduced as
  intermediates during flattening of equalities as well as 
  
-!!!TODO: We probably now can do without the skolem set.  It's not used during
-finalisation in the current code.
-
  \begin{code}
  -- |Configuration of normalised equalities used during solving.
  --
  \begin{code}
  -- |Configuration of normalised equalities used during solving.
  --
@@ -242,13 +278,8 @@ data EqConfig = EqConfig { eqs     :: [RewriteInst]     -- all equalities
                           , locals  :: [Inst]            -- given dicts
                           , wanteds :: [Inst]            -- wanted dicts
                           , binds   :: TcDictBinds       -- bindings
                           , locals  :: [Inst]            -- given dicts
                           , wanteds :: [Inst]            -- wanted dicts
                           , binds   :: TcDictBinds       -- bindings
-                         , skolems :: TyVarSet          -- flattening skolems
                           }
  
                           }
  
-addSkolems :: EqConfig -> TyVarSet -> EqConfig
-addSkolems eqCfg newSkolems 
-  = eqCfg {skolems = skolems eqCfg `unionVarSet` newSkolems}
-
  addEq :: EqConfig -> RewriteInst -> EqConfig
  addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
  
  addEq :: EqConfig -> RewriteInst -> EqConfig
  addEq eqCfg eq = eqCfg {eqs = eq : eqs eqCfg}
  
@@ -258,7 +289,6 @@ unionEqConfig eqc1 eqc2 = EqConfig
                            , locals  = locals eqc1 ++ locals eqc2
                            , wanteds = wanteds eqc1 ++ wanteds eqc2
                            , binds   = binds eqc1 `unionBags` binds eqc2
                            , locals  = locals eqc1 ++ locals eqc2
                            , wanteds = wanteds eqc1 ++ wanteds eqc2
                            , binds   = binds eqc1 `unionBags` binds eqc2
-                          , skolems = skolems eqc1 `unionVarSet` skolems eqc2
                            }
  
  emptyEqConfig :: EqConfig
                            }
  
  emptyEqConfig :: EqConfig
@@ -267,8 +297,11 @@ emptyEqConfig = EqConfig
                  , locals  = []
                  , wanteds = []
                  , binds   = emptyBag
                  , locals  = []
                  , wanteds = []
                  , binds   = emptyBag
-                , skolems = emptyVarSet
                  }
                  }
+
+instance Outputable EqConfig where
+  ppr (EqConfig {eqs = eqs, locals = locals, wanteds = wanteds, binds = binds})
+    = vcat [ppr eqs, ppr locals, ppr wanteds, ppr binds]
  \end{code}
  
  The set of operations on an equality configuration.  We obtain the initialise
  \end{code}
  
  The set of operations on an equality configuration.  We obtain the initialise
@@ -283,10 +316,11 @@ no further propoagation is possible.
  --
  normaliseEqs :: [Inst] -> TcM EqConfig
  normaliseEqs eqs 
  --
  normaliseEqs :: [Inst] -> TcM EqConfig
  normaliseEqs eqs 
-  = do { (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
-       ; return $ emptyEqConfig { eqs = concat eqss
-                                , skolems = unionVarSets skolemss 
-                                }
+  = do { ASSERTM2( allM wantedEqInstIsUnsolved eqs, ppr eqs )
+       ; traceTc $ ptext (sLit "Entering normaliseEqs")
+
+       ; eqss <- mapM normEqInst eqs
+       ; return $ emptyEqConfig { eqs = concat eqss }
         }
  
  -- |Flatten the type arguments of all dictionaries, returning the result as a 
         }
  
  -- |Flatten the type arguments of all dictionaries, returning the result as a 
@@ -297,13 +331,19 @@ normaliseEqs eqs
  --
  normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
  normaliseDicts isWanted insts
  --
  normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
  normaliseDicts isWanted insts
-  = do { (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted) 
-                                                           insts
+  = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
+                         ptext (if isWanted then sLit "[Wanted] for" 
+                                            else sLit "[Local] for"))
+                     4 (ppr insts)
+
+       ; (insts', eqss, bindss) <- mapAndUnzip3M (normDict isWanted) insts
+
+       ; traceTc $ hang (ptext (sLit "normaliseDicts returns"))
+                     4 (ppr insts' $$ ppr eqss)
         ; return $ emptyEqConfig { eqs     = concat eqss
                                  , locals  = if isWanted then [] else insts'
                                  , wanteds = if isWanted then insts' else []
                                  , binds   = unionManyBags bindss
         ; return $ emptyEqConfig { eqs     = concat eqss
                                  , locals  = if isWanted then [] else insts'
                                  , wanteds = if isWanted then insts' else []
                                  , binds   = unionManyBags bindss
-                                , skolems = unionVarSets skolemss
                                  }
         }
  
                                  }
         }
  
@@ -311,41 +351,41 @@ normaliseDicts isWanted insts
  --
  propagateEqs :: EqConfig -> TcM EqConfig
  propagateEqs eqCfg@(EqConfig {eqs = todoEqs}) 
  --
  propagateEqs :: EqConfig -> TcM EqConfig
  propagateEqs eqCfg@(EqConfig {eqs = todoEqs}) 
-  = propagate todoEqs (eqCfg {eqs = []})
+  = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
+                     4 (ppr eqCfg)
+
+       ; propagate todoEqs (eqCfg {eqs = []})
+       }
  
  -- |Finalise a set of equalities and associated dictionaries after
  
  -- |Finalise a set of equalities and associated dictionaries after
--- propagation.  The returned Boolean value is `True' iff any flexible
--- variables, except those introduced by flattening (i.e., those in the
--- `skolems' component of the argument) where instantiated. The first returned
--- set of instances are the locals (without equalities) and the second set are
--- all residual wanteds, including equalities. 
+-- propagation.  The first returned set of instances are the locals (without
+-- equalities) and the second set are all residual wanteds, including
+-- equalities.  In addition, we return all generated dictionary bindings.
  --
  --
--- Remove all identity dictinary bindings (i.e., those whose source and target
--- dictionary are the same).  This is important for termination, as
--- TcSimplify.reduceContext takes the presence of dictionary bindings as an
--- indicator that there was some improvement.
---
-finaliseEqsAndDicts :: EqConfig 
-                    -> TcM ([Inst], [Inst], TcDictBinds, Bool)
-finaliseEqsAndDicts (EqConfig { eqs     = eqs
-                              , locals  = locals
-                              , wanteds = wanteds
-                              , binds   = binds
-                              })
-  = do { (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds
-       ; (eqs'', improved) <- instantiateAndExtract eqs'
-       ; final_binds <- filterM nonTrivialDictBind $
-                          bagToList (subst_binds `unionBags` binds)
-       ; return (locals', eqs'' ++ wanteds', listToBag final_binds, improved)
+finaliseEqsAndDicts :: TcTyVarSet -> EqConfig 
+                    -> TcM ([Inst], [Inst], TcDictBinds)
+finaliseEqsAndDicts freeFlexibles (EqConfig { eqs     = eqs
+                                            , locals  = locals
+                                            , wanteds = wanteds
+                                            , binds   = binds
+                                            })
+  = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
+
+       ; (eqs', subst_binds, locals', wanteds') 
+           <- substitute eqs locals wanteds checkingMode freeFlexibles
+       ; eqs'' <- bindAndExtract eqs' checkingMode freeFlexibles
+       ; let final_binds = subst_binds `unionBags` binds
+
+         -- Assert that all cotvs of wanted equalities are still unfilled, and
+         -- zonk all final insts, to make any improvement visible
+       ; ASSERTM2( allM wantedEqInstIsUnsolved eqs'', ppr eqs'' )
+       ; zonked_locals  <- zonkInsts locals'
+       ; zonked_wanteds <- zonkInsts (eqs'' ++ wanteds')
+       ; return (zonked_locals, zonked_wanteds, final_binds)
         }
    where
         }
    where
-    nonTrivialDictBind (L _ (VarBind { var_id = ide1
-                                     , var_rhs = L _ (HsWrap _ (HsVar ide2))}))
-      = do { ty1 <- zonkTcType (idType ide1)
-           ; ty2 <- zonkTcType (idType ide2)
-           ; return $ not (ty1 `tcEqType` ty2)
-           }
-    nonTrivialDictBind _ = return True
+    checkingMode = length eqs > length wanteds || not (null locals)
+                     -- no local equalities or dicts => checking mode
  \end{code}
  
  
  \end{code}
  
  
@@ -357,7 +397,7 @@ finaliseEqsAndDicts (EqConfig { eqs     = eqs
  
  A normal equality is a properly oriented equality with associated coercion
  that contains at most one family equality (in its left-hand side) is oriented
  
  A normal equality is a properly oriented equality with associated coercion
  that contains at most one family equality (in its left-hand side) is oriented
-such that it may be used as a reqrite rule.  It has one of the following two 
+such that it may be used as a rewrite rule.  It has one of the following two 
  forms:
  
  (1) co :: F t1..tn ~ t  (family equalities)
  forms:
  
  (1) co :: F t1..tn ~ t  (family equalities)
@@ -370,50 +410,86 @@ Variable equalities fall again in two classes:
  
  The types t, t1, ..., tn may not contain any occurrences of synonym
  families.  Moreover, in Forms (2) & (3), the left-hand side may not occur in
  
  The types t, t1, ..., tn may not contain any occurrences of synonym
  families.  Moreover, in Forms (2) & (3), the left-hand side may not occur in
-the right-hand side, and the relation x > y is an arbitrary, but total order
-on type variables
-
-!!!TODO: We may need to keep track of swapping for error messages (and to
-re-orient on finilisation).
+the right-hand side, and the relation x > y is an (nearly) arbitrary, but
+total order on type variables.  The only restriction that we impose on that
+order is that for x > y, we are happy to instantiate x with y taking into
+account kinds, signature skolems etc (cf, TcUnify.uUnfilledVars).
  
  \begin{code}
  data RewriteInst
    = RewriteVar  -- Form (2) above
  
  \begin{code}
  data RewriteInst
    = RewriteVar  -- Form (2) above
-    { rwi_var   :: TyVar    -- may be rigid or flexible
-    , rwi_right :: TcType   -- contains no synonym family applications
-    , rwi_co    :: EqInstCo -- the wanted or given coercion
-    , rwi_loc   :: InstLoc
-    , rwi_name  :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
+    { rwi_var     :: TyVar    -- may be rigid or flexible
+    , rwi_right   :: TcType   -- contains no synonym family applications
+    , rwi_co      :: EqInstCo -- the wanted or given coercion
+    , rwi_loc     :: InstLoc
+    , rwi_name    :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
+    , rwi_swapped :: Bool     -- swapped orientation of original EqInst
      }
    | RewriteFam  -- Forms (1) above
      }
    | RewriteFam  -- Forms (1) above
-    { rwi_fam   :: TyCon    -- synonym family tycon
-    , rwi_args  :: [Type]   -- contain no synonym family applications
-    , rwi_right :: TcType   -- contains no synonym family applications
-    , rwi_co    :: EqInstCo -- the wanted or given coercion
-    , rwi_loc   :: InstLoc
-    , rwi_name  :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
+    { rwi_fam     :: TyCon    -- synonym family tycon
+    , rwi_args    :: [Type]   -- contain no synonym family applications
+    , rwi_right   :: TcType   -- contains no synonym family applications
+    , rwi_co      :: EqInstCo -- the wanted or given coercion
+    , rwi_loc     :: InstLoc
+    , rwi_name    :: Name     -- no semantic significance (cf. TcRnTypes.EqInst)
+    , rwi_swapped :: Bool     -- swapped orientation of original EqInst
      }
  
  isWantedRewriteInst :: RewriteInst -> Bool
  isWantedRewriteInst = isWantedCo . rwi_co
  
      }
  
  isWantedRewriteInst :: RewriteInst -> Bool
  isWantedRewriteInst = isWantedCo . rwi_co
  
-rewriteInstToInst :: RewriteInst -> Inst
+isRewriteVar :: RewriteInst -> Bool
+isRewriteVar (RewriteVar {}) = True
+isRewriteVar _               = False
+
+tyVarsOfRewriteInst :: RewriteInst -> TyVarSet
+tyVarsOfRewriteInst (RewriteVar {rwi_var = tv, rwi_right = ty})
+  = unitVarSet tv `unionVarSet` tyVarsOfType ty
+tyVarsOfRewriteInst (RewriteFam {rwi_args = args, rwi_right = ty})
+  = tyVarsOfTypes args `unionVarSet` tyVarsOfType ty
+
+rewriteInstToInst :: RewriteInst -> TcM Inst
  rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
  rewriteInstToInst eq@(RewriteVar {rwi_var = tv})
-  = EqInst
-    { tci_left  = mkTyVarTy tv
-    , tci_right = rwi_right eq
-    , tci_co    = rwi_co    eq
-    , tci_loc   = rwi_loc   eq
-    , tci_name  = rwi_name  eq
-    }
+  = deriveEqInst eq (mkTyVarTy tv) (rwi_right eq) (rwi_co eq)
  rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
  rewriteInstToInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
-  = EqInst
-    { tci_left  = mkTyConApp fam args
-    , tci_right = rwi_right eq
-    , tci_co    = rwi_co    eq
-    , tci_loc   = rwi_loc   eq
-    , tci_name  = rwi_name  eq
-    }
+  = deriveEqInst eq (mkTyConApp fam args) (rwi_right eq) (rwi_co eq)
+
+-- Derive an EqInst based from a RewriteInst, possibly swapping the types
+-- around. 
+--
+deriveEqInst :: RewriteInst -> TcType -> TcType -> EqInstCo -> TcM Inst
+deriveEqInst rewrite ty1 ty2 co
+  = do { co_adjusted <- if not swapped then return co 
+                                       else mkSymEqInstCo co (ty2, ty1)
+       ; return $ EqInst
+                  { tci_left  = left
+                  , tci_right = right
+                  , tci_co    = co_adjusted
+                  , tci_loc   = rwi_loc rewrite
+                  , tci_name  = rwi_name rewrite
+                  }
+       }
+  where
+    swapped       = rwi_swapped rewrite
+    (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
+
+instance Outputable RewriteInst where
+  ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
+    = hsep [ pprEqInstCo co <+> text "::" 
+           , ppr (mkTyConApp fam args)
+           , text "~>"
+           , ppr rhs
+           ]
+  ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
+    = hsep [ pprEqInstCo co <+> text "::" 
+           , ppr tv
+           , text "~>"
+           , ppr rhs
+           ]
+
+pprEqInstCo :: EqInstCo -> SDoc
+pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
+pprEqInstCo (Right co)  = ptext (sLit "Local") <+> ppr co
  \end{code}
  
  The following functions turn an arbitrary equality into a set of normal
  \end{code}
  
  The following functions turn an arbitrary equality into a set of normal
@@ -433,38 +509,46 @@ we drop that equality and raise an error if it is a wanted or a warning if it
  is a local.
  
  \begin{code}
  is a local.
  
  \begin{code}
-normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
+normEqInst :: Inst -> TcM [RewriteInst]
  -- Normalise one equality.
  normEqInst inst
    = ASSERT( isEqInst inst )
  -- Normalise one equality.
  normEqInst inst
    = ASSERT( isEqInst inst )
-    go ty1 ty2 (eqInstCoercion inst)
+    do { traceTc $ ptext (sLit "normEqInst of ") <+> 
+                   pprEqInstCo co <+> text "::" <+> 
+                   ppr ty1 <+> text "~" <+> ppr ty2
+       ; res <- go ty1 ty2 co
+
+       ; traceTc $ ptext (sLit "normEqInst returns") <+> ppr res
+       ; return res
+       }
    where
      (ty1, ty2) = eqInstTys inst
    where
      (ty1, ty2) = eqInstTys inst
+    co         = eqInstCoercion inst
  
        -- look through synonyms
      go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
      go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
  
        -- left-to-right rule with type family head
  
        -- look through synonyms
      go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
      go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
  
        -- left-to-right rule with type family head
-    go (TyConApp con args) ty2 co 
-      | isOpenSynTyCon con
-      = mkRewriteFam con args ty2 co
+    go ty1@(TyConApp con args) ty2 co 
+      | isOpenSynTyConApp ty1           -- only if not oversaturated
+      = mkRewriteFam False con args ty2 co
  
        -- right-to-left rule with type family head
      go ty1 ty2@(TyConApp con args) co 
  
        -- right-to-left rule with type family head
      go ty1 ty2@(TyConApp con args) co 
-      | isOpenSynTyCon con
+      | isOpenSynTyConApp ty2           -- only if not oversaturated
        = do { co' <- mkSymEqInstCo co (ty2, ty1)
        = do { co' <- mkSymEqInstCo co (ty2, ty1)
-           ; mkRewriteFam con args ty1 co'
+           ; mkRewriteFam True con args ty1 co'
             }
  
        -- no outermost family
      go ty1 ty2 co
             }
  
        -- no outermost family
      go ty1 ty2 co
-      = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
-           ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
+      = do { (ty1', co1, ty1_eqs) <- flattenType inst ty1
+           ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
             ; let ty12_eqs  = ty1_eqs ++ ty2_eqs
             ; let ty12_eqs  = ty1_eqs ++ ty2_eqs
-                 rewriteCo = co1 `mkTransCoercion` mkSymCoercion co2
+                 sym_co2   = mkSymCoercion co2
                   eqTys     = (ty1', ty2')
                   eqTys     = (ty1', ty2')
-           ; (co', ty12_eqs') <- adjustCoercions co rewriteCo eqTys ty12_eqs
+           ; (co', ty12_eqs') <- adjustCoercions co co1 sym_co2 eqTys ty12_eqs
             ; eqs <- checkOrientation ty1' ty2' co' inst
             ; if isLoopyEquality eqs ty12_eqs' 
               then do { if isWantedCo (tci_co inst)
             ; eqs <- checkOrientation ty1' ty2' co' inst
             ; if isLoopyEquality eqs ty12_eqs' 
               then do { if isWantedCo (tci_co inst)
@@ -473,64 +557,60 @@ normEqInst inst
                              eqInstMisMatch inst
                         else
                           warnDroppingLoopyEquality ty1 ty2
                              eqInstMisMatch inst
                         else
                           warnDroppingLoopyEquality ty1 ty2
-                     ; return ([], emptyVarSet)         -- drop the equality
+                     ; return ([])                 -- drop the equality
                       }
               else
                       }
               else
-               return (eqs ++ ty12_eqs',
-                      ty1_skolems `unionVarSet` ty2_skolems)
+               return (eqs ++ ty12_eqs')
             }
  
             }
  
-    mkRewriteFam con args ty2 co
-      = do { (args', cargs, args_eqss, args_skolemss) 
-               <- mapAndUnzip4M (flattenType inst) args
-           ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
-           ; let rewriteCo = mkTyConApp con cargs `mkTransCoercion` 
-                             mkSymCoercion co2
+    mkRewriteFam swapped con args ty2 co
+      = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
+           ; (ty2', co2, ty2_eqs) <- flattenType inst ty2
+           ; let co1       = mkTyConApp con cargs
+                 sym_co2   = mkSymCoercion co2
                   all_eqs   = concat args_eqss ++ ty2_eqs
                   eqTys     = (mkTyConApp con args', ty2')
                   all_eqs   = concat args_eqss ++ ty2_eqs
                   eqTys     = (mkTyConApp con args', ty2')
-           ; (co', all_eqs') <- adjustCoercions co rewriteCo eqTys all_eqs
+           ; (co', all_eqs') <- adjustCoercions co co1 sym_co2 eqTys all_eqs
             ; let thisRewriteFam = RewriteFam 
             ; let thisRewriteFam = RewriteFam 
-                                  { rwi_fam   = con
-                                  , rwi_args  = args'
-                                  , rwi_right = ty2'
-                                  , rwi_co    = co'
-                                  , rwi_loc   = tci_loc inst
-                                  , rwi_name  = tci_name inst
+                                  { rwi_fam     = con
+                                  , rwi_args    = args'
+                                  , rwi_right   = ty2'
+                                  , rwi_co      = co'
+                                  , rwi_loc     = tci_loc inst
+                                  , rwi_name    = tci_name inst
+                                  , rwi_swapped = swapped
                                    }
                                    }
-           ; return $ (thisRewriteFam : all_eqs',
-                       unionVarSets (ty2_skolems:args_skolemss))
+           ; return $ thisRewriteFam : all_eqs'
             }
  
      -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
      -- have a variable equality with 'a' on the lhs as the first equality.
      -- Then, check whether 'a' occurs in the lhs of any family equality
      -- generated by flattening.
             }
  
      -- If the original equality has the form a ~ T .. (F ...a...) ..., we will
      -- have a variable equality with 'a' on the lhs as the first equality.
      -- Then, check whether 'a' occurs in the lhs of any family equality
      -- generated by flattening.
-    isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs
-      = any inRewriteFam eqs
+    isLoopyEquality (RewriteVar {rwi_var = tv}:_) eqs = any inRewriteFam eqs
        where
          inRewriteFam (RewriteFam {rwi_args = args}) 
            = tv `elemVarSet` tyVarsOfTypes args
          inRewriteFam _ = False
      isLoopyEquality _ _ = False
  
        where
          inRewriteFam (RewriteFam {rwi_args = args}) 
            = tv `elemVarSet` tyVarsOfTypes args
          inRewriteFam _ = False
      isLoopyEquality _ _ = False
  
-normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds, TyVarSet)
+normDict :: Bool -> Inst -> TcM (Inst, [RewriteInst], TcDictBinds)
  -- Normalise one dictionary or IP constraint.
  normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
  -- Normalise one dictionary or IP constraint.
  normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
-  = do { (args', cargs, args_eqss, args_skolemss) 
-           <- mapAndUnzip4M (flattenType inst) args
+  = do { (args', cargs, args_eqss) <- mapAndUnzip3M (flattenType inst) args
         ; let rewriteCo = PredTy $ ClassP clas cargs
               eqs       = concat args_eqss
               pred'     = ClassP clas args'
         ; if null eqs
           then  -- don't generate a binding if there is nothing to flatten
         ; let rewriteCo = PredTy $ ClassP clas cargs
               eqs       = concat args_eqss
               pred'     = ClassP clas args'
         ; if null eqs
           then  -- don't generate a binding if there is nothing to flatten
-           return (inst, [], emptyBag, emptyVarSet)
+           return (inst, [], emptyBag)
           else do {
         ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
         ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
           else do {
         ; (inst', bind) <- mkDictBind inst isWanted rewriteCo pred'
         ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
-       ; return (inst', eqs', bind, unionVarSets args_skolemss)
+       ; return (inst', eqs', bind)
         }}
         }}
-normDict isWanted inst
-  = return (inst, [], emptyBag, emptyVarSet)
+normDict _isWanted inst
+  = return (inst, [], emptyBag)
  -- !!!TODO: Still need to normalise IP constraints.
  
  checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
  -- !!!TODO: Still need to normalise IP constraints.
  
  checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
@@ -552,15 +632,14 @@ checkOrientation ty1 ty2 co inst
             ; return []
             }
  
             ; return []
             }
  
-      -- two tvs, left greater => unchanged
+      -- two tvs (distinct tvs, due to previous equation)
      go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
      go ty1@(TyVarTy tv1) ty2@(TyVarTy tv2)
-      | tv1 > tv2
-      = mkRewriteVar tv1 ty2 co
-
-      -- two tvs, right greater => swap
-      | otherwise
-      = do { co' <- mkSymEqInstCo co (ty2, ty1)
-           ; mkRewriteVar tv2 ty1 co'
+      = do { isBigger <- tv1 `tvIsBigger` tv2
+           ; if isBigger                                      -- left greater
+               then mkRewriteVar False tv1 ty2 co             --   => unchanged
+               else do { co' <- mkSymEqInstCo co (ty2, ty1)   -- right greater
+                       ; mkRewriteVar True tv2 ty1 co'        --   => swap
+                       }
             }
  
        -- only lhs is a tv => unchanged
             }
  
        -- only lhs is a tv => unchanged
@@ -568,7 +647,7 @@ checkOrientation ty1 ty2 co inst
        | ty1 `tcPartOfType` ty2      -- occurs check!
        = occurCheckErr ty1 ty2
        | otherwise 
        | ty1 `tcPartOfType` ty2      -- occurs check!
        = occurCheckErr ty1 ty2
        | otherwise 
-      = mkRewriteVar tv1 ty2 co
+      = mkRewriteVar False tv1 ty2 co
  
        -- only rhs is a tv => swap
      go ty1 ty2@(TyVarTy tv2)
  
        -- only rhs is a tv => swap
      go ty1 ty2@(TyVarTy tv2)
@@ -576,7 +655,27 @@ checkOrientation ty1 ty2 co inst
        = occurCheckErr ty2 ty1
        | otherwise 
        = do { co' <- mkSymEqInstCo co (ty2, ty1)
        = occurCheckErr ty2 ty1
        | otherwise 
        = do { co' <- mkSymEqInstCo co (ty2, ty1)
-           ; mkRewriteVar tv2 ty1 co'
+           ; mkRewriteVar True tv2 ty1 co'
+           }
+
+      -- data type constructor application => decompose
+      -- NB: Special cased for efficiency - could be handled as type application
+    go (TyConApp con1 args1) (TyConApp con2 args2)
+      |  con1 == con2
+      && not (isOpenSynTyCon con1)   -- don't match family synonym apps
+      = do { co_args <- mkTyConEqInstCo co con1 (zip args1 args2)
+           ; eqss <- zipWith3M (\ty1 ty2 co -> checkOrientation ty1 ty2 co inst)
+                     args1 args2 co_args
+           ; return $ concat eqss
+           }
+
+      -- function type => decompose
+      -- NB: Special cased for efficiency - could be handled as type application
+    go (FunTy ty1_l ty1_r) (FunTy ty2_l ty2_r)
+      = do { (co_l, co_r) <- mkFunEqInstCo co (ty1_l, ty2_l) (ty1_r, ty2_r)
+           ; eqs_l <- checkOrientation ty1_l ty2_l co_l inst
+           ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
+           ; return $ eqs_l ++ eqs_r
             }
  
        -- type applications => decompose
             }
  
        -- type applications => decompose
@@ -588,96 +687,177 @@ checkOrientation ty1 ty2 co inst
             ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
             ; return $ eqs_l ++ eqs_r
             }
             ; eqs_r <- checkOrientation ty1_r ty2_r co_r inst
             ; return $ eqs_l ++ eqs_r
             }
--- !!!TODO: would be more efficient to handle the FunApp and the data
--- constructor application explicitly.
  
        -- inconsistency => type error
      go ty1 ty2
        = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
          eqInstMisMatch inst
  
  
        -- inconsistency => type error
      go ty1 ty2
        = ASSERT( (not . isForAllTy $ ty1) && (not . isForAllTy $ ty2) )
          eqInstMisMatch inst
  
-    mkRewriteVar tv ty co = return [RewriteVar 
-                                    { rwi_var   = tv
-                                    , rwi_right = ty
-                                    , rwi_co    = co
-                                    , rwi_loc   = tci_loc inst
-                                    , rwi_name  = tci_name inst
-                                    }]
+    mkRewriteVar swapped tv ty co = return [RewriteVar 
+                                            { rwi_var     = tv
+                                            , rwi_right   = ty
+                                            , rwi_co      = co
+                                            , rwi_loc     = tci_loc inst
+                                            , rwi_name    = tci_name inst
+                                            , rwi_swapped = swapped
+                                            }]
+
+    -- if tv1 `tvIsBigger` tv2, we make a rewrite rule tv1 ~> tv2
+    tvIsBigger :: TcTyVar -> TcTyVar -> TcM Bool
+    tvIsBigger tv1 tv2 
+      = isBigger tv1 (tcTyVarDetails tv1) tv2 (tcTyVarDetails tv2)
+      where
+        isBigger tv1 (SkolemTv _)     tv2 (SkolemTv _)
+          = return $ tv1 > tv2
+        isBigger _   (MetaTv _ _)     _   (SkolemTv _)
+          = return True
+        isBigger _   (SkolemTv _)     _   (MetaTv _ _)
+          = return False
+        isBigger tv1 (MetaTv info1 _) tv2 (MetaTv info2 _)
+          -- meta variable meets meta variable 
+          -- => be clever about which of the two to update 
+          --   (from TcUnify.uUnfilledVars minus boxy stuff)
+          = case (info1, info2) of
+              -- Avoid SigTvs if poss
+              (SigTv _, SigTv _)             -> return $ tv1 > tv2
+              (SigTv _, _      ) | k1_sub_k2 -> return False
+              (_,       SigTv _) | k2_sub_k1 -> return True
+
+              (_, _) 
+                | k1_sub_k2 &&
+                  k2_sub_k1    
+                  -> case (nicer_to_update tv1, nicer_to_update tv2) of
+                       (True, False) -> return True
+                       (False, True) -> return False
+                       _             -> return $ tv1 > tv2
+                | k1_sub_k2    -> return False
+                | k2_sub_k1    -> return True
+                | otherwise    -> kind_err >> return True
+              -- Update the variable with least kind info
+              -- See notes on type inference in Kind.lhs
+              -- The "nicer to" part only applies if the two kinds are the same,
+              -- so we can choose which to do.
+          where
+            kind_err = addErrCtxtM (unifyKindCtxt False tv1 (mkTyVarTy tv2)) $
+                       unifyKindMisMatch k1 k2
+
+            k1 = tyVarKind tv1
+            k2 = tyVarKind tv2
+            k1_sub_k2 = k1 `isSubKind` k2
+            k2_sub_k1 = k2 `isSubKind` k1
+
+            nicer_to_update tv = isSystemName (Var.varName tv)
+                -- Try to update sys-y type variables in preference to ones
+                -- gotten (say) by instantiating a polymorphic function with
+                -- a user-written type sig 
  
  flattenType :: Inst     -- context to get location  & name
              -> Type     -- the type to flatten
              -> TcM (Type,           -- the flattened type
                      Coercion,       -- coercion witness of flattening wanteds
  
  flattenType :: Inst     -- context to get location  & name
              -> Type     -- the type to flatten
              -> TcM (Type,           -- the flattened type
                      Coercion,       -- coercion witness of flattening wanteds
-                    [RewriteInst],  -- extra equalities
-                    TyVarSet)       -- new intermediate skolems
+                    [RewriteInst])  -- extra equalities
  -- Removes all family synonyms from a type by moving them into extra equalities
  -- Removes all family synonyms from a type by moving them into extra equalities
-flattenType inst ty
-  = go ty
+flattenType inst ty = go ty
    where
        -- look through synonyms
    where
        -- look through synonyms
-    go ty | Just ty' <- tcView ty = go ty'
+    go ty | Just ty' <- tcView ty 
+      = do { (ty_flat, co, eqs) <- go ty'
+           ; if null eqs
+             then     -- unchanged, keep the old type with folded synonyms
+               return (ty, ty, [])
+             else 
+               return (ty_flat, co, eqs)
+           }
+
+      -- type variable => nothing to do
+    go ty@(TyVarTy _)
+      = return (ty, ty, [])
  
  
-      -- type family application 
+      -- type family application & family arity matches number of args
        -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
      go ty@(TyConApp con args)
        -- => flatten to "gamma :: F t1'..tn' ~ alpha" (alpha & gamma fresh)
      go ty@(TyConApp con args)
-      | isOpenSynTyCon con
-      = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
+      | isOpenSynTyConApp ty   -- only if not oversaturated
+      = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
             ; alpha <- newFlexiTyVar (typeKind ty)
             ; let alphaTy = mkTyVarTy alpha
             ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
             ; let thisRewriteFam = RewriteFam 
             ; alpha <- newFlexiTyVar (typeKind ty)
             ; let alphaTy = mkTyVarTy alpha
             ; cotv <- newMetaCoVar (mkTyConApp con args') alphaTy
             ; let thisRewriteFam = RewriteFam 
-                                  { rwi_fam   = con
-                                  , rwi_args  = args'
-                                  , rwi_right = alphaTy
-                                  , rwi_co    = mkWantedCo cotv
-                                  , rwi_loc   = tci_loc inst
-                                  , rwi_name  = tci_name inst
+                                  { rwi_fam     = con
+                                  , rwi_args    = args'
+                                  , rwi_right   = alphaTy
+                                  , rwi_co      = mkWantedCo cotv
+                                  , rwi_loc     = tci_loc inst
+                                  , rwi_name    = tci_name inst
+                                  , rwi_swapped = True
                                    }
             ; return (alphaTy,
                       mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
                                    }
             ; return (alphaTy,
                       mkTyConApp con cargs `mkTransCoercion` mkTyVarTy cotv,
-                     thisRewriteFam : concat args_eqss,
-                     unionVarSets args_skolemss `extendVarSet` alpha)
-           }           -- adding new unflatten var inst
+                     thisRewriteFam : concat args_eqss)
+           }
  
        -- data constructor application => flatten subtypes
        -- NB: Special cased for efficiency - could be handled as type application
  
        -- data constructor application => flatten subtypes
        -- NB: Special cased for efficiency - could be handled as type application
-    go (TyConApp con args)
-      = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
-           ; return (mkTyConApp con args', 
-                     mkTyConApp con cargs,
-                     concat args_eqss,
-                     unionVarSets args_skolemss)
+    go ty@(TyConApp con args)
+      | not (isOpenSynTyCon con)   -- don't match oversaturated family apps
+      = do { (args', cargs, args_eqss) <- mapAndUnzip3M go args
+           ; if null args_eqss
+             then     -- unchanged, keep the old type with folded synonyms
+               return (ty, ty, [])
+             else 
+               return (mkTyConApp con args', 
+                       mkTyConApp con cargs,
+                       concat args_eqss)
             }
  
        -- function type => flatten subtypes
        -- NB: Special cased for efficiency - could be handled as type application
             }
  
        -- function type => flatten subtypes
        -- NB: Special cased for efficiency - could be handled as type application
-    go (FunTy ty_l ty_r)
-      = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
-           ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
-           ; return (mkFunTy ty_l' ty_r', 
-                     mkFunTy co_l co_r,
-                     eqs_l ++ eqs_r, 
-                     skolems_l `unionVarSet` skolems_r)
+    go ty@(FunTy ty_l ty_r)
+      = do { (ty_l', co_l, eqs_l) <- go ty_l
+           ; (ty_r', co_r, eqs_r) <- go ty_r
+           ; if null eqs_l && null eqs_r
+             then     -- unchanged, keep the old type with folded synonyms
+               return (ty, ty, [])
+             else 
+               return (mkFunTy ty_l' ty_r', 
+                       mkFunTy co_l co_r,
+                       eqs_l ++ eqs_r)
             }
  
        -- type application => flatten subtypes
             }
  
        -- type application => flatten subtypes
-    go (AppTy ty_l ty_r)
---      | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
-      = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
-           ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
-           ; return (mkAppTy ty_l' ty_r', 
-                     mkAppTy co_l co_r, 
-                     eqs_l ++ eqs_r, 
-                     skolems_l `unionVarSet` skolems_r)
+    go ty
+      | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
+                             -- need to use the smart split as ty may be an
+                             -- oversaturated family application
+      = do { (ty_l', co_l, eqs_l) <- go ty_l
+           ; (ty_r', co_r, eqs_r) <- go ty_r
+           ; if null eqs_l && null eqs_r
+             then     -- unchanged, keep the old type with folded synonyms
+               return (ty, ty, [])
+             else 
+               return (mkAppTy ty_l' ty_r', 
+                       mkAppTy co_l co_r, 
+                       eqs_l ++ eqs_r)
             }
  
             }
  
-      -- free of type families => leave as is
-    go ty
-      = ASSERT( not . isForAllTy $ ty )
-        return (ty, ty, [] , emptyVarSet)
+      -- forall type => panic if the body contains a type family
+      -- !!!TODO: As long as the family does not contain a quantified variable
+      --          we might pull it out, but what if it does contain a quantified
+      --          variable???
+    go ty@(ForAllTy _ body)
+      | null (tyFamInsts body)
+      = return (ty, ty, [])
+      | otherwise
+      = panic "TcTyFuns.flattenType: synonym family in a rank-n type"
+
+      -- we should never see a predicate type
+    go (PredTy _)
+      = panic "TcTyFuns.flattenType: unexpected PredType"
+
+    go _ = panic "TcTyFuns: suppress bogus warning"
  
  adjustCoercions :: EqInstCo            -- coercion of original equality
  
  adjustCoercions :: EqInstCo            -- coercion of original equality
-                -> Coercion            -- coercion witnessing the rewrite
+                -> Coercion            -- coercion witnessing the left rewrite
+                -> Coercion            -- coercion witnessing the right rewrite
                  -> (Type, Type)        -- types of flattened equality
                  -> [RewriteInst]       -- equalities from flattening
                  -> TcM (EqInstCo,      -- coercion for flattened equality
                  -> (Type, Type)        -- types of flattened equality
                  -> [RewriteInst]       -- equalities from flattening
                  -> TcM (EqInstCo,      -- coercion for flattened equality
@@ -685,17 +865,17 @@ adjustCoercions :: EqInstCo            -- coercion of original equality
  -- Depending on whether we flattened a local or wanted equality, that equality's
  -- coercion and that of the new equalities produced during flattening are
  -- adjusted .
  -- Depending on whether we flattened a local or wanted equality, that equality's
  -- coercion and that of the new equalities produced during flattening are
  -- adjusted .
-adjustCoercions co rewriteCo eqTys all_eqs
-
+adjustCoercions (Left cotv) co1 co2 (ty_l, ty_r) all_eqs
      -- wanted => generate a fresh coercion variable for the flattened equality
      -- wanted => generate a fresh coercion variable for the flattened equality
-  | isWantedCo co 
-  = do { co' <- mkRightTransEqInstCo co rewriteCo eqTys
-       ; return (co', all_eqs)
+  = do { cotv' <- newMetaCoVar ty_l ty_r
+       ; bindMetaTyVar cotv $ 
+           (co1 `mkTransCoercion` TyVarTy cotv' `mkTransCoercion` co2)
+       ; return (Left cotv', all_eqs)
         }
  
         }
  
+adjustCoercions co@(Right _) _co1 _co2 _eqTys all_eqs
      -- local => turn all new equalities into locals and update (but not zonk)
      --          the skolem
      -- local => turn all new equalities into locals and update (but not zonk)
      --          the skolem
-  | otherwise
    = do { all_eqs' <- mapM wantedToLocal all_eqs
         ; return (co, all_eqs')
         }
    = do { all_eqs' <- mapM wantedToLocal all_eqs
         ; return (co, all_eqs')
         }
@@ -728,17 +908,29 @@ mkDictBind dict isWanted rewriteCo pred
    where
      loc = tci_loc dict
  
    where
      loc = tci_loc dict
  
--- gamma :: Fam args ~ alpha
--- => alpha :: Fam args ~ alpha, with alpha := Fam args
+-- gamma ::^l Fam args ~ alpha
+-- => gamma ::^w Fam args ~ alpha, with alpha := Fam args & gamma := Fam args
  --    (the update of alpha will not be apparent during propagation, as we
  --    never follow the indirections of meta variables; it will be revealed
  --    when the equality is zonked)
  --    (the update of alpha will not be apparent during propagation, as we
  --    never follow the indirections of meta variables; it will be revealed
  --    when the equality is zonked)
+--
+--  NB: It's crucial to update *both* alpha and gamma, as gamma may already
+--      have escaped into some other coercions during normalisation.
+--
+--      We do actually update alpha and gamma by side effect (instead of
+--      only remembering the binding with `bindMetaTyVar', as we do for all
+--      other tyvars).  We can do this as the side effects are strictly
+--      *local*; we know that both alpha and gamma were just a moment ago
+--      introduced by normalisation. 
+--
  wantedToLocal :: RewriteInst -> TcM RewriteInst
  wantedToLocal eq@(RewriteFam {rwi_fam   = fam, 
                                rwi_args  = args, 
  wantedToLocal :: RewriteInst -> TcM RewriteInst
  wantedToLocal eq@(RewriteFam {rwi_fam   = fam, 
                                rwi_args  = args, 
-                              rwi_right = alphaTy@(TyVarTy alpha)})
+                              rwi_right = TyVarTy alpha,
+                              rwi_co    = Left gamma})
    = do { writeMetaTyVar alpha (mkTyConApp fam args)
    = do { writeMetaTyVar alpha (mkTyConApp fam args)
-       ; return $ eq {rwi_co = mkGivenCo alphaTy}
+       ; writeMetaTyVar gamma (mkTyConApp fam args)
+       ; return $ eq {rwi_co = mkGivenCo $ mkTyVarTy gamma}
         }
  wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
  \end{code}
         }
  wantedToLocal _ = panic "TcTyFuns.wantedToLocal"
  \end{code}
@@ -760,53 +952,53 @@ propagate (eq:eqs) eqCfg
         ; case optEqs of
  
                -- Top applied to 'eq' => retry with new equalities
         ; case optEqs of
  
                -- Top applied to 'eq' => retry with new equalities
-           Just (eqs2, skolems2) 
-             -> propagate (eqs2 ++ eqs) (eqCfg `addSkolems` skolems2)
+           Just eqs2 -> propagate (eqs2 ++ eqs) eqCfg
  
                -- Top doesn't apply => try subst rules with all other
                --   equalities, after that 'eq' can go into the residual list
  
                -- Top doesn't apply => try subst rules with all other
                --   equalities, after that 'eq' can go into the residual list
-           Nothing
-             -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
-                   ; propagate eqs' (eqCfg' `addEq` eq)
-                   }
-   }
+           Nothing   -> do { (eqs', eqCfg') <- applySubstRules eq eqs eqCfg
+                           ; propagate eqs' (eqCfg' `addEq` eq)
+                           }
+       }
  
  applySubstRules :: RewriteInst                    -- currently considered eq
                  -> [RewriteInst]                  -- todo eqs list
                  -> EqConfig                       -- residual
                  -> TcM ([RewriteInst], EqConfig)  -- new todo & residual
  applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
  
  applySubstRules :: RewriteInst                    -- currently considered eq
                  -> [RewriteInst]                  -- todo eqs list
                  -> EqConfig                       -- residual
                  -> TcM ([RewriteInst], EqConfig)  -- new todo & residual
  applySubstRules eq todoEqs (eqConfig@EqConfig {eqs = resEqs})
-  = do { (newEqs_t, unchangedEqs_t, skolems_t) <- mapSubstRules eq todoEqs
-       ; (newEqs_r, unchangedEqs_r, skolems_r) <- mapSubstRules eq resEqs
+  = do { (newEqs_t, unchangedEqs_t) <- mapSubstRules eq todoEqs
+       ; (newEqs_r, unchangedEqs_r) <- mapSubstRules eq resEqs
         ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
         ; return (newEqs_t ++ newEqs_r ++ unchangedEqs_t,
-                 eqConfig {eqs = unchangedEqs_r} 
-                   `addSkolems` (skolems_t `unionVarSet` skolems_r))
+                 eqConfig {eqs = unchangedEqs_r})
         }
  
  mapSubstRules :: RewriteInst     -- try substituting this equality
                -> [RewriteInst]   -- into these equalities
         }
  
  mapSubstRules :: RewriteInst     -- try substituting this equality
                -> [RewriteInst]   -- into these equalities
-              -> TcM ([RewriteInst], [RewriteInst], TyVarSet)
+              -> TcM ([RewriteInst], [RewriteInst])
  mapSubstRules eq eqs
  mapSubstRules eq eqs
-  = do { (newEqss, unchangedEqss, skolemss) <- mapAndUnzip3M (substRules eq) eqs
-       ; return (concat newEqss, concat unchangedEqss, unionVarSets skolemss)
+  = do { (newEqss, unchangedEqss) <- mapAndUnzipM (substRules eq) eqs
+       ; return (concat newEqss, concat unchangedEqss)
         }
    where
      substRules eq1 eq2
         }
    where
      substRules eq1 eq2
-      = do {   -- try the SubstFam rule
-             optEqs <- applySubstFam eq1 eq2
+      = do {traceTc $ hang (ptext (sLit "Trying subst rules with"))
+                        4 (ppr eq1 $$ ppr eq2)
+
+               -- try the SubstFam rule
+           ; optEqs <- applySubstFam eq1 eq2
             ; case optEqs of
             ; case optEqs of
-               Just (eqs, skolems) -> return (eqs, [], skolems)
-               Nothing             -> do 
+               Just eqs -> return (eqs, [])
+               Nothing  -> do 
             {   -- try the SubstVarVar rule
               optEqs <- applySubstVarVar eq1 eq2
             ; case optEqs of
             {   -- try the SubstVarVar rule
               optEqs <- applySubstVarVar eq1 eq2
             ; case optEqs of
-               Just (eqs, skolems) -> return (eqs, [], skolems)
-               Nothing             -> do 
+               Just eqs -> return (eqs, [])
+               Nothing  -> do 
             {   -- try the SubstVarFam rule
               optEqs <- applySubstVarFam eq1 eq2
             ; case optEqs of
             {   -- try the SubstVarFam rule
               optEqs <- applySubstVarFam eq1 eq2
             ; case optEqs of
-               Just eq -> return ([eq], [], emptyVarSet)
-               Nothing -> return ([], [eq2], emptyVarSet)
+               Just eq -> return ([eq], [])
+               Nothing -> return ([], [eq2])
                   -- if no rule matches, we return the equlity we tried to
                   -- substitute into unchanged
             }}}
                   -- if no rule matches, we return the equlity we tried to
                   -- substitute into unchanged
             }}}
@@ -824,7 +1016,7 @@ Returns Nothing if the rule could not be applied.  Otherwise, the resulting
  equality is normalised and a list of the normal equalities is returned.
  
  \begin{code}
  equality is normalised and a list of the normal equalities is returned.
  
  \begin{code}
-applyTop :: RewriteInst -> TcM (Maybe ([RewriteInst], TyVarSet))
+applyTop :: RewriteInst -> TcM (Maybe [RewriteInst])
  
  applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
    = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
  
  applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
    = do { optTyCo <- tcUnfoldSynFamInst (TyConApp fam args)
@@ -832,13 +1024,7 @@ applyTop eq@(RewriteFam {rwi_fam = fam, rwi_args = args})
             Nothing                -> return Nothing
             Just (lhs, rewrite_co) 
               -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
             Nothing                -> return Nothing
             Just (lhs, rewrite_co) 
               -> do { co' <- mkRightTransEqInstCo co rewrite_co (lhs, rhs)
-                   ; let eq' = EqInst 
-                               { tci_left  = lhs
-                               , tci_right = rhs
-                               , tci_co    = co'
-                               , tci_loc   = rwi_loc eq
-                               , tci_name  = rwi_name eq
-                               }
+                   ; eq' <- deriveEqInst eq lhs rhs co'
                     ; liftM Just $ normEqInst eq'
                     }
         }
                     ; liftM Just $ normEqInst eq'
                     }
         }
@@ -864,29 +1050,29 @@ equality co1 is not returned as it remain unaltered.)
  \begin{code}
  applySubstFam :: RewriteInst 
                -> RewriteInst 
  \begin{code}
  applySubstFam :: RewriteInst 
                -> RewriteInst 
-              -> TcM (Maybe ([RewriteInst], TyVarSet))
+              -> TcM (Maybe ([RewriteInst]))
  applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
                eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
  applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
                eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
+
+    -- rule matches => rewrite
    | fam1 == fam2 && tcEqTypes args1 args2 &&
      (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
    | fam1 == fam2 && tcEqTypes args1 args2 &&
      (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
--- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms
--- !!!Check whether anything breaks by making tcEqTypes look through synonyms.
--- !!!Should be ok and we don't want three type equalities.
    = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
    = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
-       ; let eq2' = EqInst 
-                    { tci_left  = lhs
-                    , tci_right = rhs
-                    , tci_co    = co2'
-                    , tci_loc   = rwi_loc eq2
-                    , tci_name  = rwi_name eq2
-                    }
+       ; eq2' <- deriveEqInst eq2 lhs rhs co2'
         ; liftM Just $ normEqInst eq2'
         }
         ; liftM Just $ normEqInst eq2'
         }
+
+    -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
+  | fam1 == fam2 && tcEqTypes args1 args2 &&
+    (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
+  = return $ Just [eq2]
+
    where
      lhs = rwi_right eq1
      rhs = rwi_right eq2
      co1 = eqInstCoType (rwi_co eq1)
      co2 = rwi_co eq2
    where
      lhs = rwi_right eq1
      rhs = rwi_right eq2
      co1 = eqInstCoType (rwi_co eq1)
      co2 = rwi_co eq2
+
  applySubstFam _ _ = return Nothing
  \end{code}
  
  applySubstFam _ _ = return Nothing
  \end{code}
  
@@ -903,28 +1089,29 @@ co2' is normalised and a list of the normal equalities is returned.  (The
  equality co1 is not returned as it remain unaltered.)
  
  \begin{code}
  equality co1 is not returned as it remain unaltered.)
  
  \begin{code}
-applySubstVarVar :: RewriteInst 
-                 -> RewriteInst 
-                 -> TcM (Maybe ([RewriteInst], TyVarSet))
+applySubstVarVar :: RewriteInst -> RewriteInst -> TcM (Maybe [RewriteInst])
  applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
                   eq2@(RewriteVar {rwi_var = tv2})
  applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
                   eq2@(RewriteVar {rwi_var = tv2})
+
+    -- rule matches => rewrite
    | tv1 == tv2 &&
      (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
    = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
    | tv1 == tv2 &&
      (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
    = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
-       ; let eq2' = EqInst 
-                    { tci_left  = lhs
-                    , tci_right = rhs
-                    , tci_co    = co2'
-                    , tci_loc   = rwi_loc eq2
-                    , tci_name  = rwi_name eq2
-                    }
+       ; eq2' <- deriveEqInst eq2 lhs rhs co2'
         ; liftM Just $ normEqInst eq2'
         }
         ; liftM Just $ normEqInst eq2'
         }
+
+    -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
+  | tv1 == tv2 &&
+    (isWantedRewriteInst eq1 || not (isWantedRewriteInst eq2))
+  = return $ Just [eq2]
+
    where
      lhs = rwi_right eq1
      rhs = rwi_right eq2
      co1 = eqInstCoType (rwi_co eq1)
      co2 = rwi_co eq2
    where
      lhs = rwi_right eq1
      rhs = rwi_right eq2
      co1 = eqInstCoType (rwi_co eq1)
      co2 = rwi_co eq2
+
  applySubstVarVar _ _ = return Nothing
  \end{code}
  
  applySubstVarVar _ _ = return Nothing
  \end{code}
  
@@ -942,6 +1129,8 @@ co2' is returned.  (The equality co1 is not returned as it remain unaltered.)
  
  \begin{code}
  applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
  
  \begin{code}
  applySubstVarFam :: RewriteInst -> RewriteInst -> TcM (Maybe RewriteInst)
+
+  -- rule matches => rewrite
  applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
                   eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
    | tv1 `elemVarSet` tyVarsOfTypes args2
  applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
                   eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
    | tv1 `elemVarSet` tyVarsOfTypes args2
@@ -956,6 +1145,13 @@ applySubstVarFam eq1@(RewriteVar {rwi_var = tv1})
      rhs2 = rwi_right eq2
      co1  = eqInstCoType (rwi_co eq1)
      co2  = rwi_co eq2
      rhs2 = rwi_right eq2
      co1  = eqInstCoType (rwi_co eq1)
      co2  = rwi_co eq2
+
+  -- rule would match with eq1 and eq2 swapped => put eq2 into todo list
+applySubstVarFam (RewriteFam {rwi_args = args1})
+                 eq2@(RewriteVar {rwi_var = tv2})
+  | tv2 `elemVarSet` tyVarsOfTypes args1
+  = return $ Just eq2
+
  applySubstVarFam _ _ = return Nothing
  \end{code}
  
  applySubstVarFam _ _ = return Nothing
  \end{code}
  
@@ -967,57 +1163,152 @@ applySubstVarFam _ _ = return Nothing
  %************************************************************************
  
  Exhaustive substitution of all variable equalities of the form co :: x ~ t
  %************************************************************************
  
  Exhaustive substitution of all variable equalities of the form co :: x ~ t
-(both local and wanted) into the left-hand sides of all other equalities.  This
-may lead to recursive equalities; i.e., (1) we need to apply the substitution
-implied by one variable equality exhaustively before turning to the next and
-(2) we need an occurs check.
+(both local and wanted) into the right-hand sides of all other equalities and
+of family equalities of the form co :: F t1..tn ~ alpha into both sides of all
+other *family* equalities.  This may lead to recursive equalities; i.e., (1)
+we need to apply the substitution implied by one equality exhaustively before
+turning to the next and (2) we need an occurs check.
  
  We also apply the same substitutions to the local and wanted class and IP
  
  We also apply the same substitutions to the local and wanted class and IP
-dictionaries.
+dictionaries.  
+
+We perform the substitutions in two steps:
+
+  Step A: Substitute variable equalities into the right-hand sides of all
+          other equalities (but wanted only into wanteds) and into class and IP 
+          constraints (again wanteds only into wanteds).
+
+  Step B: Substitute wanted family equalities `co :: F t1..tn ~ alpha', where
+          'alpha' is a skolem flexible (i.e., not free in the environment),
+          into the right-hand sides of all wanted variable equalities and into
+          both sides of all wanted family equalities.
+
+  Step C: Substitute the remaining wanted family equalities `co :: F t1..tn ~
+          alpha' into the right-hand sides of all wanted variable equalities
+          and into both sides of all wanted family equalities.
+
+In inference mode, we do not substitute into variable equalities in Steps B & C.
+
+The treatment of flexibles in wanteds is quite subtle.  We absolutely want to
+substitute variable equalities first; e.g., consider
+
+  F s ~ alpha, alpha ~ t
+
+If we don't substitute `alpha ~ t', we may instantiate `t' with `F s' instead.
+This would be bad as `F s' is less useful, eg, as an argument to a class
+constraint.  
+
+The restriction on substituting locals is necessary due to examples, such as
+
+  F delta ~ alpha, F alpha ~ delta,
+
+where `alpha' is a skolem flexible and `delta' a environment flexible. We need
+to produce `F (F delta) ~ delta' (and not `F (F alpha) ~ alpha'). Otherwise,
+we may wrongly claim to having performed an improvement, which can lead to
+non-termination of the combined class-family solver.
+
+We do also substitute flexibles, as in `alpha ~ t' into class constraints.
+When `alpha' is later instantiated, we'd get the same effect, but in the
+meantime the class constraint would miss some information, which would be a
+problem in an integrated equality-class solver.
  
  
-NB: Given that we apply the substitution corresponding to a single equality
-exhaustively, before turning to the next, and because we eliminate recursive
-equalities, all opportunities for subtitution will have been exhausted after
-we have considered each equality once.
+NB: 
+* Given that we apply the substitution corresponding to a single equality
+  exhaustively, before turning to the next, and because we eliminate recursive
+  equalities, all opportunities for subtitution will have been exhausted after
+  we have considered each equality once.
  
  \begin{code}
  substitute :: [RewriteInst]       -- equalities
             -> [Inst]              -- local class dictionaries
             -> [Inst]              -- wanted class dictionaries
  
  \begin{code}
  substitute :: [RewriteInst]       -- equalities
             -> [Inst]              -- local class dictionaries
             -> [Inst]              -- wanted class dictionaries
+           -> Bool                -- True ~ checking mode; False ~ inference
+           -> TyVarSet            -- flexibles free in the environment
             -> TcM ([RewriteInst], -- equalities after substitution
                     TcDictBinds,   -- all newly generated dictionary bindings
                     [Inst],        -- local dictionaries after substitution
                     [Inst])        -- wanted dictionaries after substitution
             -> TcM ([RewriteInst], -- equalities after substitution
                     TcDictBinds,   -- all newly generated dictionary bindings
                     [Inst],        -- local dictionaries after substitution
                     [Inst])        -- wanted dictionaries after substitution
-substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
+substitute eqs locals wanteds checkingMode freeFlexibles
+  = -- We achieve the sequencing of "Step A", "Step B", and "Step C" above by
+    -- sorting the equalities appropriately: first all variable, then all
+    -- family/skolem, and then the remaining family equalities. 
+    let (var_eqs, fam_eqs)             = partition isRewriteVar eqs
+        (fam_skolem_eqs, fam_eqs_rest) = partition isFamSkolemEq fam_eqs
+    in 
+    subst (var_eqs ++ fam_skolem_eqs ++ fam_eqs_rest) [] emptyBag locals wanteds
    where
    where
+    isFamSkolemEq (RewriteFam {rwi_right = ty})
+      | Just tv <- tcGetTyVar_maybe ty = not (tv `elemVarSet` freeFlexibles)
+    isFamSkolemEq _ = False
+
      subst [] res binds locals wanteds 
        = return (res, binds, locals, wanteds)
      subst [] res binds locals wanteds 
        = return (res, binds, locals, wanteds)
+
+    -- co :: x ~ t
      subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs) 
            res binds locals wanteds
      subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs) 
            res binds locals wanteds
-      = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr tv <+>
-                       ptext (sLit "->") <+> ppr ty
+      = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteVar]:") <+> 
+                       ppr eq
+
+             -- create the substitution
             ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
                   tySubst = zipOpenTvSubst [tv] [ty]
             ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
                   tySubst = zipOpenTvSubst [tv] [ty]
-           ; eqs'               <- mapM (substEq eq coSubst tySubst) eqs
-           ; res'               <- mapM (substEq eq coSubst tySubst) res
-           ; (lbinds, locals')  <- mapAndUnzipM 
-                                     (substDict eq coSubst tySubst False) 
-                                     locals
+
+             -- substitute into all other equalities
+           ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
+           ; res' <- mapM (substEq eq coSubst tySubst) res
+
+             -- only substitute local equalities into local dictionaries
+           ; (lbinds, locals')  <- if not (isWantedCo co)
+                                   then 
+                                     mapAndUnzipM 
+                                       (substDict eq coSubst tySubst False) 
+                                       locals
+                                   else
+                                     return ([], locals)
+
+              -- substitute all equalities into wanteds dictionaries
             ; (wbinds, wanteds') <- mapAndUnzipM 
                                       (substDict eq coSubst tySubst True) 
                                       wanteds
             ; (wbinds, wanteds') <- mapAndUnzipM 
                                       (substDict eq coSubst tySubst True) 
                                       wanteds
+
             ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
             ; subst eqs' (eq:res') binds' locals' wanteds'
             }
             ; let binds' = unionManyBags $ binds : lbinds ++ wbinds
             ; subst eqs' (eq:res') binds' locals' wanteds'
             }
+
+    -- co ::^w F t1..tn ~ alpha
+    subst (eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty, 
+                           rwi_co = co}):eqs) 
+          res binds locals wanteds
+      | Just tv <- tcGetTyVar_maybe ty
+      , isMetaTyVar tv
+      , isWantedCo co
+      = do { traceTc $ ptext (sLit "TcTyFuns.substitute[RewriteFam]:") <+> 
+                       ppr eq
+
+             -- create the substitution
+           ; let coSubst = zipOpenTvSubst [tv] [mkSymCoercion $ eqInstCoType co]
+                 tySubst = zipOpenTvSubst [tv] [mkTyConApp fam args]
+
+             -- substitute into other wanted equalities (`substEq' makes sure
+             -- that we only substitute into wanteds)
+           ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
+           ; res' <- mapM (substEq eq coSubst tySubst) res
+
+           ; subst eqs' (eq:res') binds locals wanteds
+           }
+
      subst (eq:eqs) res binds locals wanteds
        = subst eqs (eq:res) binds locals wanteds
  
        -- We have, co :: tv ~ ty 
        -- => apply [ty/tv] to right-hand side of eq2
      subst (eq:eqs) res binds locals wanteds
        = subst eqs (eq:res) binds locals wanteds
  
        -- We have, co :: tv ~ ty 
        -- => apply [ty/tv] to right-hand side of eq2
-      --    (but only if tv actually occurs in the right-hand side of eq2)
+      --    (but only if tv actually occurs in the right-hand side of eq2
+      --    and if eq2 is a local, co :: tv ~ ty needs to be a local, too)
      substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) 
              coSubst tySubst eq2
      substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) 
              coSubst tySubst eq2
-      | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
+      |  tv `elemVarSet` tyVarsOfType (rwi_right eq2)
+      && (isWantedRewriteInst eq2 || not (isWantedCo co))
        = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
                   right2'  = substTy tySubst (rwi_right eq2)
                   left2    = case eq2 of
        = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
                   right2'  = substTy tySubst (rwi_right eq2)
                   left2    = case eq2 of
@@ -1031,6 +1322,44 @@ substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
                 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
             }
  
                 _ -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
             }
  
+      -- We have, co ::^w F t1..tn ~ tv
+      -- => apply [F t1..tn/tv] to eq2
+      --    (but only if tv actually occurs in eq2
+      --    and eq2 is a wanted equality
+      --    and we are either in checking mode or eq2 is a family equality)
+    substEq (RewriteFam {rwi_args = args, rwi_right = ty}) 
+            coSubst tySubst eq2
+      | Just tv <- tcGetTyVar_maybe ty
+      , tv `elemVarSet` tyVarsOfRewriteInst eq2
+      , isWantedRewriteInst eq2
+      , checkingMode || not (isRewriteVar eq2)
+      = do { -- substitute into the right-hand side
+           ; let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
+                 right2'  = substTy tySubst (rwi_right eq2)
+                 left2    = case eq2 of
+                              RewriteVar {rwi_var = tv2}   -> mkTyVarTy tv2
+                              RewriteFam {rwi_fam = fam,
+                                          rwi_args = args} -> mkTyConApp fam args
+           ; co2' <- mkLeftTransEqInstCo (rwi_co eq2) co1Subst (left2, right2')
+           ; case eq2 of
+               RewriteVar {rwi_var = tv2} 
+                 -- variable equality: perform an occurs check
+                 | tv2 `elemVarSet` tyVarsOfTypes args
+                 -> occurCheckErr left2 right2'
+                 | otherwise
+                 -> return $ eq2 {rwi_right = right2', rwi_co = co2'}
+               RewriteFam {rwi_fam = fam}
+                 -- family equality: substitute also into the left-hand side
+                 -> do { let co1Subst = substTy coSubst left2
+                             args2'   = substTys tySubst (rwi_args  eq2)
+                             left2'   = mkTyConApp fam args2'
+                       ; co2'' <- mkRightTransEqInstCo co2' co1Subst 
+                                                       (left2', right2')
+                       ; return $ eq2 {rwi_args = args2', rwi_right = right2', 
+                                       rwi_co = co2''}
+                       }
+           }
+
        -- unchanged
      substEq _ _ _ eq2
        = return eq2
        -- unchanged
      substEq _ _ _ eq2
        = return eq2
@@ -1038,12 +1367,10 @@ substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
        -- We have, co :: tv ~ ty 
        -- => apply [ty/tv] to dictionary predicate
        --    (but only if tv actually occurs in the predicate)
        -- We have, co :: tv ~ ty 
        -- => apply [ty/tv] to dictionary predicate
        --    (but only if tv actually occurs in the predicate)
-    substDict (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) 
-              coSubst tySubst isWanted dict
+    substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict
        | isClassDict dict
        , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
        | isClassDict dict
        , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
-      = do { let co1Subst = mkSymCoercion $ 
-                              PredTy (substPred coSubst (tci_pred dict))
+      = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
                   pred'    = substPred tySubst (tci_pred dict)
             ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
             ; return (binds, dict')
                   pred'    = substPred tySubst (tci_pred dict)
             ; (dict', binds) <- mkDictBind dict isWanted co1Subst pred'
             ; return (binds, dict')
@@ -1056,135 +1383,183 @@ substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
  \end{code}
  
  For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
  \end{code}
  
  For any *wanted* variable equality of the form co :: alpha ~ t or co :: a ~
-alpha, we instantiate alpha with t or a, respectively, and set co := id.
-Return all remaining wanted equalities.  The Boolean result component is True
-if at least one instantiation of a flexible was performed.
+alpha, we record a binding of alpha with t or a, respectively, and for co :=
+id.  We do the same for equalities of the form co :: F t1..tn ~ alpha unless
+we are in inference mode and alpha appears in the environment - i.e., it is
+not a flexible introduced by flattening locals or it is local, but was
+propagated into the environment by the instantiation of a variable equality.
+
+We proceed in two phases: (1) first we consider all variable equalities and then
+(2) we consider all family equalities.  The two phase structure is required as
+the recorded variable equalities determine which skolems flexibles escape, and
+hence, which family equalities may be recorded as bindings.
+
+We return all wanted equalities for which we did not generate a binding.
+(These can be skolem variable equalities, cyclic variable equalities, and
+family equalities.)
+
+We don't update any meta variables.  Instead, instantiation simply implies
+putting a type variable binding into the binding pool of TcM.
+
+NB:
+ * We may encounter filled flexibles due to the instant filling of local
+   skolems in local-given constraints during flattening.
+ * Be careful with SigTVs.  They can only be instantiated with other SigTVs or
+   rigid skolems.
  
  \begin{code}
  
  \begin{code}
-instantiateAndExtract :: [RewriteInst] -> TcM ([Inst], Bool)
-instantiateAndExtract eqs
-  = do { let wanteds = filter (isWantedCo . rwi_co) eqs
-       ; wanteds' <- mapM inst wanteds
-       ; let residuals = catMaybes wanteds'
-             improved  = length wanteds /= length residuals
-       ; return (map rewriteInstToInst residuals, improved)
+bindAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM [Inst]
+bindAndExtract eqs checkingMode freeFlexibles
+  = do { traceTc $ hang (ptext (sLit "bindAndExtract:"))
+                     4 (ppr eqs $$ ppr freeFlexibles)
+       ; residuals1 <- mapMaybeM instVarEq (filter isWantedRewriteInst eqs)
+       ; escapingSkolems <- getEscapingSkolems
+       ; let newFreeFlexibles = freeFlexibles `unionVarSet` escapingSkolems
+       ; residuals2 <- mapMaybeM (instFamEq newFreeFlexibles) residuals1
+       ; mapM rewriteInstToInst residuals2
         }
    where
         }
    where
-    inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
-
-        -- co :: alpha ~ t
-      | isMetaTyVar tv1
-      = doInst tv1 ty2 co eq
+    -- NB: we don't have to transitively chase the relation as the substitution
+    --     process applied before generating the bindings was exhaustive
+    getEscapingSkolems
+      = do { tybinds_rel <- getTcTyVarBindsRelation
+           ; return (unionVarSets . map snd . filter isFree $ tybinds_rel)
+           }
+      where
+        isFree (tv, _) = tv `elemVarSet` freeFlexibles
+
+        -- co :: alpha ~ t or co :: a ~ alpha
+    instVarEq eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
+      = do { flexi_tv1       <- isFlexible   tv1
+           ; maybe_flexi_tv2 <- isFlexibleTy ty2
+           ; case (flexi_tv1, maybe_flexi_tv2) of
+               (True, Just tv2)
+                 | isSigTyVar tv1 && isSigTyVar tv2
+                 -> -- co :: alpha ~ beta, where both a SigTvs
+                    doInst (rwi_swapped eq) tv1 ty2 co eq
+               (True, Nothing) 
+                 | Just tv2 <- tcGetTyVar_maybe ty2
+                 , isSigTyVar tv1
+                 , isSkolemTyVar tv2
+                 -> -- co :: alpha ~ a, where alpha is a SigTv
+                    doInst (rwi_swapped eq) tv1 ty2 co eq
+               (True, _) 
+                 | not (isSigTyVar tv1)
+                 -> -- co :: alpha ~ t, where alpha is not a SigTv
+                    doInst (rwi_swapped eq) tv1 ty2 co eq
+               (False, Just tv2) 
+                 | isSigTyVar tv2
+                 , isSkolemTyVar tv1
+                 -> -- co :: a ~ alpha, where alpha is a SigTv
+                    doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
+                 | not (isSigTyVar tv2)
+                 -> -- co :: a ~ alpha, where alpha is not a SigTv 
+                    --                        ('a' may be filled)
+                    doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
+               _ -> return $ Just eq
+           }
+    instVarEq eq = return $ Just eq
  
  
-        -- co :: a ~ alpha
+        -- co :: F args ~ alpha, 
+        -- and we are either in checking mode or alpha is a skolem flexible that
+        --     doesn't escape
+    instFamEq newFreeFlexibles eq@(RewriteFam {rwi_fam = fam, rwi_args = args, 
+                                               rwi_right = ty2, rwi_co = co})
        | Just tv2 <- tcGetTyVar_maybe ty2
        | Just tv2 <- tcGetTyVar_maybe ty2
-      , isMetaTyVar tv2
-      = doInst tv2 (mkTyVarTy tv1) co eq
-
-    inst eq = return $ Just eq
-
-    doInst _  _  (Right ty)  _eq = pprPanic "TcTyFuns.doInst: local eq: " 
-                                           (ppr ty)
-    doInst tv ty (Left cotv) eq  = do { lookupTV <- lookupTcTyVar tv
-                                      ; uMeta False tv lookupTV ty cotv
-                                      }
+      , checkingMode || not (tv2 `elemVarSet` newFreeFlexibles)
+      = do { flexi_tv2 <- isFlexible tv2
+           ; if flexi_tv2
+             then
+               doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
+             else
+               return $ Just eq
+           }
+    instFamEq _ eq = return $ Just eq
+
+    -- tv is a meta var, but not a SigTV and not filled
+    isFlexible tv
+      | isMetaTyVar tv = liftM isFlexi $ readMetaTyVar tv
+      | otherwise      = return False
+
+    -- type is a tv that is a meta var, but not a SigTV and not filled
+    isFlexibleTy ty
+      | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible tv
+                                            ; if flexi then return $ Just tv 
+                                                       else return Nothing
+                                            }
+      | otherwise                      = return Nothing
+
+    doInst _swapped _tv _ty (Right ty) _eq 
+      = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)
+    doInst swapped tv ty (Left cotv) eq
+      = do { lookupTV <- lookupTcTyVar tv
+           ; bMeta swapped tv lookupTV ty cotv
+           }
        where
        where
+        -- Try to create a binding for a meta variable.  There is *no* need to
+        -- consider reorienting the underlying equality; `checkOrientation'
+        -- makes sure that we get variable-variable equalities only in the
+        -- appropriate orientation.
+        --
+        bMeta :: Bool                    -- is this a swapped equality?
+              -> TcTyVar                 -- tyvar to instantiate
+              -> LookupTyVarResult       -- lookup result of that tyvar
+              -> TcType                  -- to to instantiate tyvar with
+              -> TcTyVar                 -- coercion tyvar of current equality
+              -> TcM (Maybe RewriteInst) -- returns the original equality if
+                                         -- the tyvar could not be instantiated,
+                                         -- and hence, the equality must be kept
+
          -- meta variable has been filled already
          -- meta variable has been filled already
-        -- => ignore (must be a skolem that was introduced by flattening locals)
-        uMeta _swapped _tv (IndirectTv _) _ty _cotv
-          = return Nothing
+        -- => this should never happen due to the use of `isFlexible' above
+        bMeta _swapped tv (IndirectTv fill_ty) ty _cotv
+          = pprPanic "TcTyFuns.bMeta" $ 
+              ptext (sLit "flexible") <+> ppr tv <+>
+              ptext (sLit "already filled with") <+> ppr fill_ty <+>
+              ptext (sLit "meant to fill with") <+> ppr ty
  
          -- type variable meets type variable
  
          -- type variable meets type variable
-        -- => check that tv2 hasn't been updated yet and choose which to update
-        uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
-          | tv1 == tv2
-          = panic "TcTyFuns.uMeta: normalisation shouldn't allow x ~ x"
-
-          | otherwise
+        -- => `checkOrientation' already ensures that it is fine to instantiate
+        --    tv1 with tv2, but chase tv2's instantiations if necessary, so that
+        --    we eventually can perform a kinds check in bMetaInst
+        -- NB: tv's instantiations won't alter the orientation in which we
+        --     want to instantiate as they either constitute a family 
+        --     application or are themselves due to a properly oriented
+        --     instantiation
+        bMeta swapped tv1 details1@(DoneTv (MetaTv _ _)) ty@(TyVarTy tv2) cotv
            = do { lookupTV2 <- lookupTcTyVar tv2
                 ; case lookupTV2 of
            = do { lookupTV2 <- lookupTcTyVar tv2
                 ; case lookupTV2 of
-                   IndirectTv ty   -> 
-                     uMeta swapped tv1 (DoneTv details1) ty cotv
-                   DoneTv details2 -> 
-                     uMetaVar swapped tv1 details1 tv2 details2 cotv
+                   IndirectTv ty' -> bMeta swapped tv1 details1 ty' cotv
+                   DoneTv _       -> bMetaInst swapped tv1 ty cotv
                 }
  
                 }
  
-        ------ Beyond this point we know that ty2 is not a type variable
+        -- updatable meta variable meets non-variable type
+        -- => occurs check, monotype check, and kinds match check, then bind
+        bMeta swapped tv (DoneTv (MetaTv _ _ref)) non_tv_ty cotv
+          = bMetaInst swapped tv non_tv_ty cotv
  
  
-        -- signature skolem meets non-variable type
-        -- => cannot update (retain the equality)!
-        uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
-          = return $ Just eq
+        bMeta _ _ _ _ _ = panic "TcTyFuns.bMeta"
  
  
-        -- updatable meta variable meets non-variable type
-        -- => occurs check, monotype check, and kinds match check, then update
-        uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
+        -- We know `tv' can be instantiated; check that `ty' is alright for
+        -- instantiating `tv' with and then record a binding; we return the
+        -- original equality if it is cyclic through a synonym family
+        bMetaInst swapped tv ty cotv
            = do {   -- occurs + monotype check
            = do {   -- occurs + monotype check
-               ; mb_ty' <- checkTauTvUpdate tv non_tv_ty    
+               ; mb_ty' <- checkTauTvUpdate tv ty    
                               
                 ; case mb_ty' of
                     Nothing  -> 
                               
                 ; case mb_ty' of
                     Nothing  -> 
-                     -- normalisation shouldn't leave families in non_tv_ty
-                     panic "TcTyFuns.uMeta: unexpected synonym family"
+                     -- there may be a family in non_tv_ty due to an unzonked,
+                     -- but updated skolem for a local equality 
+                     -- (cf `wantedToLocal')
+                     return $ Just eq
                     Just ty' ->
                     Just ty' ->
-                     do { checkUpdateMeta swapped tv ref ty'  -- update meta var
-                        ; writeMetaTyVar cotv ty'             -- update co var
+                     do { checkKinds swapped tv ty'
+                        ; bindMetaTyVar tv ty'          -- bind meta var
+                        ; bindMetaTyVar cotv ty'        -- bind co var
                          ; return Nothing
                          }
                 }
                          ; return Nothing
                          }
                 }
-
-        uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
-
-        -- uMetaVar: unify two type variables
-        -- meta variable meets skolem 
-        -- => just update
-        uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
-          = do { checkUpdateMeta swapped tv1 ref (mkTyVarTy tv2)
-               ; writeMetaTyVar cotv (mkTyVarTy tv2)
-               ; return Nothing
-               }
-
-        -- meta variable meets meta variable 
-        -- => be clever about which of the two to update 
-        --   (from TcUnify.uUnfilledVars minus boxy stuff)
-        uMetaVar swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) cotv
-          = do { case (info1, info2) of
-                   -- Avoid SigTvs if poss
-                   (SigTv _, _      ) | k1_sub_k2 -> update_tv2
-                   (_,       SigTv _) | k2_sub_k1 -> update_tv1
-
-                   (_,   _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1
-                                           then update_tv1     -- Same kinds
-                                           else update_tv2
-                            | k2_sub_k1 -> update_tv1
-                            | otherwise -> kind_err
-              -- Update the variable with least kind info
-              -- See notes on type inference in Kind.lhs
-              -- The "nicer to" part only applies if the two kinds are the same,
-              -- so we can choose which to do.
-
-               ; writeMetaTyVar cotv (mkTyVarTy tv2)
-               ; return Nothing
-               }
-          where
-                -- Kinds should be guaranteed ok at this point
-            update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2)
-            update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1)
-
-            kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $
-                       unifyKindMisMatch k1 k2
-
-            k1 = tyVarKind tv1
-            k2 = tyVarKind tv2
-            k1_sub_k2 = k1 `isSubKind` k2
-            k2_sub_k1 = k2 `isSubKind` k1
-
-            nicer_to_update_tv1 = isSystemName (Var.varName tv1)
-                -- Try to update sys-y type variables in preference to ones
-                -- gotten (say) by instantiating a polymorphic function with
-                -- a user-written type sig 
-
-        uMetaVar _ _ _ _ _ _ = panic "uMetaVar"
  \end{code}
  
  
  \end{code}
  
  
@@ -1256,7 +1631,9 @@ warnDroppingLoopyEquality ty1 ty2
    = do { env0 <- tcInitTidyEnv
         ; ty1 <- zonkTcType ty1
         ; ty2 <- zonkTcType ty2
    = do { env0 <- tcInitTidyEnv
         ; ty1 <- zonkTcType ty1
         ; ty2 <- zonkTcType ty2
+       ; let (env1 , tidy_ty1) = tidyOpenType env0 ty1
+            (_env2, tidy_ty2) = tidyOpenType env1 ty2
         ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
         ; addWarnTc $ hang (ptext (sLit "Dropping loopy given equality"))
-                      2 (ppr ty1 <+> text "~" <+> ppr ty2)
+                      2 (quotes (ppr tidy_ty1 <+> text "~" <+> ppr tidy_ty2))
         }
  \end{code}
         }
  \end{code}