Template Haskell: support for kind annotations

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

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index 8d2d69e..1e65471 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

@@ -38,7 +37,9 @@ import Name
 import Bag
 import Outputable
 import SrcLoc  ( Located(..) )
 import Bag
 import Outputable
 import SrcLoc  ( Located(..) )

+import Util    ( debugIsOn )

 import Maybes
 import Maybes

+import MonadUtils

 import FastString
 
 -- standard
 import FastString
 
 -- standard

@@ -70,21 +71,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}
 

@@ -232,9 +228,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.
 --

@@ -269,6 +262,10 @@ emptyEqConfig = EqConfig
                 , binds   = emptyBag
                 , skolems = emptyVarSet
                 }
                 , 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,8 +280,16 @@ no further propoagation is possible.
 --
 normaliseEqs :: [Inst] -> TcM EqConfig
 normaliseEqs eqs 
 --
 normaliseEqs :: [Inst] -> TcM EqConfig
 normaliseEqs eqs 

-  = do { ASSERTM2( allM isValidWantedEqInst eqs, ppr eqs )
-       ; traceTc $ ptext (sLit "normaliseEqs")
+  = do { if debugIsOn then do { all_unsolved <- allM wantedEqInstIsUnsolved eqs
+                                     ; let msg = ptext (sLit "(This warning is harmless; for Simon & Manuel)")
+                                     ; WARN( not all_unsolved, msg $$ ppr eqs ) return () }
+                     else return ()
+           -- This is just a warning (not an error) because a current
+           -- harmless bug means that we sometimes solve the same
+           -- equality more than once It'll go away with the new
+           -- solver. See Trac #2999 for example
+
+       ; traceTc $ ptext (sLit "Entering normaliseEqs")

 
        ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
        ; return $ emptyEqConfig { eqs = concat eqss
 
        ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
        ; return $ emptyEqConfig { eqs = concat eqss

@@ -300,10 +305,15 @@ normaliseEqs eqs
 --
 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
 normaliseDicts isWanted insts
 --
 normaliseDicts :: Bool -> [Inst] -> TcM EqConfig
 normaliseDicts isWanted insts

-  = do { traceTc $ ptext (sLit "normaliseDicts") <+>
-                   ptext (if isWanted then sLit "[Wanted]" else sLit "[Local]")
+  = do { traceTc $ hang (ptext (sLit "Entering normaliseDicts") <+>
+                         ptext (if isWanted then sLit "[Wanted] for" 
+                                            else sLit "[Local] for"))
+                     4 (ppr insts)

        ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (normDict isWanted) 
                                                            insts
        ; (insts', eqss, bindss, skolemss) <- mapAndUnzip4M (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 []
        ; return $ emptyEqConfig { eqs     = concat eqss
                                 , locals  = if isWanted then [] else insts'
                                 , wanteds = if isWanted then insts' else []

@@ -316,7 +326,9 @@ normaliseDicts isWanted insts
 --
 propagateEqs :: EqConfig -> TcM EqConfig
 propagateEqs eqCfg@(EqConfig {eqs = todoEqs}) 
 --
 propagateEqs :: EqConfig -> TcM EqConfig
 propagateEqs eqCfg@(EqConfig {eqs = todoEqs}) 

-  = do { traceTc $ ptext (sLit "propagateEqs")
+  = do { traceTc $ hang (ptext (sLit "Entering propagateEqs:"))
+                     4 (ppr eqCfg)
+

        ; propagate todoEqs (eqCfg {eqs = []})
        }
 
        ; propagate todoEqs (eqCfg {eqs = []})
        }
 

@@ -327,35 +339,26 @@ propagateEqs eqCfg@(EqConfig {eqs = todoEqs})
 -- set of instances are the locals (without equalities) and the second set are
 -- all residual wanteds, including equalities. 
 --
 -- set of instances are the locals (without equalities) and the second set are
 -- all residual wanteds, including equalities. 
 --

--- 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
 finaliseEqsAndDicts :: EqConfig 
                     -> TcM ([Inst], [Inst], TcDictBinds, Bool)
 finaliseEqsAndDicts (EqConfig { eqs     = eqs
                               , locals  = locals
                               , wanteds = wanteds
                               , binds   = binds

+                              , skolems = skolems

                               })
   = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
        ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds
                               })
   = do { traceTc $ ptext (sLit "finaliseEqsAndDicts")
        ; (eqs', subst_binds, locals', wanteds') <- substitute eqs locals wanteds

-       ; (eqs'', improved) <- instantiateAndExtract eqs'
-       ; final_binds <- filterM nonTrivialDictBind $
-                          bagToList (subst_binds `unionBags` binds)
-
-       ; ASSERTM2( allM isValidWantedEqInst eqs'', ppr eqs'' )
-       ; return (locals', eqs'' ++ wanteds', listToBag final_binds, improved)
+       ; (eqs'', improved) <- instantiateAndExtract eqs' (null locals) skolems
+       ; 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, improved)

        }
        }

-  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

 \end{code}
 
 
 \end{code}
 
 

@@ -367,7 +370,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)

@@ -380,11 +383,10 @@ 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
 
 \begin{code}
 data RewriteInst

@@ -433,6 +435,24 @@ deriveEqInst rewrite ty1 ty2 co
   where
     swapped       = rwi_swapped rewrite
     (left, right) = if not swapped then (ty1, ty2) else (ty2, ty1)
   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

@@ -456,22 +476,29 @@ normEqInst :: Inst -> TcM ([RewriteInst], TyVarSet)
 -- 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
+    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 
       = mkRewriteFam False con args ty2 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)
            ; mkRewriteFam True con args ty1 co'
            }
       = do { co' <- mkSymEqInstCo co (ty2, ty1)
            ; mkRewriteFam True con args ty1 co'
            }

@@ -481,9 +508,9 @@ normEqInst inst
       = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
            ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
            ; let ty12_eqs  = ty1_eqs ++ ty2_eqs
       = do { (ty1', co1, ty1_eqs, ty1_skolems) <- flattenType inst ty1
            ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
            ; 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)

@@ -503,11 +530,11 @@ normEqInst inst
       = do { (args', cargs, args_eqss, args_skolemss) 
                <- mapAndUnzip4M (flattenType inst) args
            ; (ty2', co2, ty2_eqs, ty2_skolems) <- flattenType inst ty2
       = 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
+           ; 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 
                                   { rwi_fam     = con
                                   , rwi_args    = args'
            ; let thisRewriteFam = RewriteFam 
                                   { rwi_fam     = con
                                   , rwi_args    = args'

@@ -549,7 +576,7 @@ normDict isWanted inst@(Dict {tci_pred = ClassP clas args})
        ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
        ; return (inst', eqs', bind, unionVarSets args_skolemss)
        }}
        ; eqs' <- if isWanted then return eqs else mapM wantedToLocal eqs
        ; return (inst', eqs', bind, unionVarSets args_skolemss)
        }}

-normDict isWanted inst
+normDict _isWanted inst

   = return (inst, [], emptyBag, emptyVarSet)
 -- !!!TODO: Still need to normalise IP constraints.
 
   = return (inst, [], emptyBag, emptyVarSet)
 -- !!!TODO: Still need to normalise IP constraints.
 

@@ -572,15 +599,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 False tv1 ty2 co
-
-      -- two tvs, right greater => swap
-      | otherwise
-      = do { co' <- mkSymEqInstCo co (ty2, ty1)
-           ; mkRewriteVar True 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

@@ -599,6 +625,26 @@ checkOrientation ty1 ty2 co inst
            ; mkRewriteVar True 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
     go ty1 ty2 
       | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1   -- won't split fam apps
       -- type applications => decompose
     go ty1 ty2 
       | Just (ty1_l, ty1_r) <- repSplitAppTy_maybe ty1   -- won't split fam apps

@@ -608,8 +654,6 @@ 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
 
       -- inconsistency => type error
     go ty1 ty2

@@ -625,6 +669,55 @@ checkOrientation ty1 ty2 co inst
                                             , rwi_swapped = swapped
                                             }]
 
                                             , 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
 flattenType :: Inst     -- context to get location  & name
             -> Type     -- the type to flatten
             -> TcM (Type,           -- the flattened type

@@ -636,16 +729,23 @@ flattenType inst ty
   = go ty
   where
       -- look through synonyms
   = go ty
   where
       -- look through synonyms

-    go ty | Just ty' <- tcView ty = go ty'
+    go ty | Just ty' <- tcView ty 
+      = do { (ty_flat, co, eqs, skolems) <- go ty'
+           ; if null eqs
+             then     -- unchanged, keep the old type with folded synonyms
+               return (ty, ty, [], emptyVarSet)
+             else 
+               return (ty_flat, co, eqs, skolems)
+           }

 
       -- type variable => nothing to do
     go ty@(TyVarTy _)
       = return (ty, ty, [] , emptyVarSet)
 
 
       -- type variable => nothing to do
     go ty@(TyVarTy _)
       = return (ty, ty, [] , emptyVarSet)
 

-      -- 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
+      | isOpenSynTyConApp ty   -- only if not oversaturated

       = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
            ; alpha <- newFlexiTyVar (typeKind ty)
            ; let alphaTy = mkTyVarTy alpha
       = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
            ; alpha <- newFlexiTyVar (typeKind ty)
            ; let alphaTy = mkTyVarTy alpha

@@ -667,34 +767,49 @@ flattenType inst ty
 
       -- 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)
+    go ty@(TyConApp con args)
+      | not (isOpenSynTyCon con)   -- don't match oversaturated family apps

       = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
       = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args

-           ; return (mkTyConApp con args', 
-                     mkTyConApp con cargs,
-                     concat args_eqss,
-                     unionVarSets args_skolemss)
+           ; if null args_eqss
+             then     -- unchanged, keep the old type with folded synonyms
+               return (ty, ty, [], emptyVarSet)
+             else 
+               return (mkTyConApp con args', 
+                       mkTyConApp con cargs,
+                       concat args_eqss,
+                       unionVarSets args_skolemss)

            }
 
       -- 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)
+    go ty@(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
       = 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)
+           ; if null eqs_l && null eqs_r
+             then     -- unchanged, keep the old type with folded synonyms
+               return (ty, ty, [], emptyVarSet)
+             else 
+               return (mkFunTy ty_l' ty_r', 
+                       mkFunTy co_l co_r,
+                       eqs_l ++ eqs_r, 
+                       skolems_l `unionVarSet` skolems_r)

            }
 
       -- type application => flatten subtypes
            }
 
       -- type application => flatten subtypes

-    go (AppTy ty_l ty_r)
---      | Just (ty_l, ty_r) <- repSplitAppTy_maybe ty
+    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, skolems_l) <- go ty_l
            ; (ty_r', co_r, eqs_r, skolems_r) <- go 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 (mkAppTy ty_l' ty_r', 
-                     mkAppTy co_l co_r, 
-                     eqs_l ++ eqs_r, 
-                     skolems_l `unionVarSet` skolems_r)
+           ; if null eqs_l && null eqs_r
+             then     -- unchanged, keep the old type with folded synonyms
+               return (ty, ty, [], emptyVarSet)
+             else 
+               return (mkAppTy ty_l' ty_r', 
+                       mkAppTy co_l co_r, 
+                       eqs_l ++ eqs_r, 
+                       skolems_l `unionVarSet` skolems_r)

            }
 
       -- forall type => panic if the body contains a type family
            }
 
       -- forall type => panic if the body contains a type family

@@ -711,8 +826,11 @@ flattenType inst ty
     go (PredTy _)
       = panic "TcTyFuns.flattenType: unexpected PredType"
 
     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

@@ -720,17 +838,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
+       ; writeMetaTyVar 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')
        }

@@ -763,17 +881,23 @@ 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.
+--

 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}

@@ -827,8 +951,11 @@ mapSubstRules eq eqs
        }
   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
                Just (eqs, skolems) -> return (eqs, [], skolems)
                Nothing             -> do 
            ; case optEqs of
                Just (eqs, skolems) -> return (eqs, [], skolems)
                Nothing             -> do 

@@ -896,20 +1023,26 @@ applySubstFam :: RewriteInst
               -> TcM (Maybe ([RewriteInst], TyVarSet))
 applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
               eq2@(RewriteFam {rwi_fam = fam2, rwi_args = args2})
               -> TcM (Maybe ([RewriteInst], TyVarSet))
 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)
        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
        ; liftM Just $ normEqInst eq2'
        }
   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
        ; 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], emptyVarSet)
+

   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}
 

@@ -931,17 +1064,26 @@ applySubstVarVar :: RewriteInst
                  -> TcM (Maybe ([RewriteInst], TyVarSet))
 applySubstVarVar eq1@(RewriteVar {rwi_var = tv1})
                  eq2@(RewriteVar {rwi_var = tv2})
                  -> TcM (Maybe ([RewriteInst], TyVarSet))
 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)
        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
        ; liftM Just $ normEqInst eq2'
        }
   | tv1 == tv2 &&
     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
   = do { co2' <- mkRightTransEqInstCo co2 co1 (lhs, rhs)
        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
        ; 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], emptyVarSet)
+

   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}
 

@@ -959,6 +1101,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

@@ -973,6 +1117,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}
 

@@ -992,10 +1143,26 @@ implied by one variable equality exhaustively before turning to the next and
 We also apply the same substitutions to the local and wanted class and IP
 dictionaries.
 
 We also apply the same substitutions to the local and wanted class and IP
 dictionaries.
 

-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.
+The treatment of flexibles in wanteds is quite subtle.  We absolutely want to
+substitute them into right-hand sides of equalities, to avoid getting two
+competing instantiations for a type variables; 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.
+
+However, there is no reason why we would want to *substitute* `alpha ~ t' into a
+class constraint.  We rather wait until `alpha' is instantiated to `t` and
+save the extra dictionary binding that substitution would introduce.
+Moreover, we may substitute wanted equalities only into wanted dictionaries.
+
+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
 
 \begin{code}
 substitute :: [RewriteInst]       -- equalities

@@ -1009,20 +1176,35 @@ substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
   where
     subst [] res binds locals wanteds 
       = return (res, binds, locals, wanteds)
   where
     subst [] res binds locals wanteds 
       = return (res, binds, locals, wanteds)

+

     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:") <+> ppr eq
+

            ; 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
-           ; (wbinds, wanteds') <- mapAndUnzipM 
-                                     (substDict eq coSubst tySubst True) 
-                                     wanteds
+           ; eqs' <- mapM (substEq eq coSubst tySubst) eqs
+           ; res' <- mapM (substEq eq coSubst tySubst) res
+
+             -- only susbtitute local equalities into local dictionaries
+           ; (lbinds, locals')  <- if not (isWantedCo co)
+                                   then 
+                                     mapAndUnzipM 
+                                       (substDict eq coSubst tySubst False) 
+                                       locals
+                                   else
+                                     return ([], locals)
+
+              -- flexible tvs in wanteds will be instantiated anyway, there is
+              -- no need to substitute them into dictionaries
+           ; (wbinds, wanteds') <- if not (isMetaTyVar tv && isWantedCo co)
+                                   then
+                                     mapAndUnzipM 
+                                       (substDict eq coSubst tySubst True) 
+                                       wanteds
+                                   else
+                                     return ([], 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'
            }

@@ -1032,7 +1214,7 @@ substitute eqs locals wanteds = subst eqs [] emptyBag 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)
       -- 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)

-    substEq (RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}) 
+    substEq (RewriteVar {rwi_var = tv, rwi_right = ty}) 

             coSubst tySubst eq2
       | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
       = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)
             coSubst tySubst eq2
       | tv `elemVarSet` tyVarsOfType (rwi_right eq2)
       = do { let co1Subst = mkSymCoercion $ substTy coSubst (rwi_right eq2)

@@ -1055,12 +1237,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')

@@ -1075,31 +1255,75 @@ substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
 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
 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.
+if at least one instantiation of a flexible that is *not* a skolem from
+flattening was performed.
+
+We need to instantiate all flexibles that arose as skolems during flattening
+of wanteds before we instantiate any other flexibles. Consider F delta ~
+alpha, F alpha ~ delta, where alpha is a skolem and delta a free 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.

 
 \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
+instantiateAndExtract :: [RewriteInst] -> Bool -> TyVarSet -> TcM ([Inst], Bool)
+instantiateAndExtract eqs localsEmpty skolems
+  = do { traceTc $ hang (ptext (sLit "instantiateAndExtract:"))
+                     4 (ppr eqs $$ ppr skolems)
+           -- start by *only* instantiating skolem flexibles from flattening
+       ; unflat_wanteds <- liftM catMaybes $ 
+                             mapM (inst (`elemVarSet` skolems)) wanteds
+           -- only afterwards instantiate free flexibles
+       ; residuals <- liftM catMaybes $ mapM (inst (const True)) unflat_wanteds
+       ; let improvement = length residuals < length unflat_wanteds

        ; residuals' <- mapM rewriteInstToInst residuals
        ; residuals' <- mapM rewriteInstToInst residuals

-       ; return (residuals', improved)
+       ; return (residuals', improvement)

        }
   where
        }
   where

-    inst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
-
-        -- co :: alpha ~ t
-      | isMetaTyVar tv1
-      = doInst (rwi_swapped eq) tv1 ty2 co eq
+    wanteds      = filter (isWantedCo . rwi_co) eqs
+    checkingMode = length eqs > length wanteds || not localsEmpty
+                     -- no local equalities or dicts => checking mode
+
+        -- co :: alpha ~ t or co :: a ~ alpha
+    inst mayInst eq@(RewriteVar {rwi_var = tv1, rwi_right = ty2, rwi_co = co})
+      = do { flexi_tv1       <- isFlexible mayInst tv1
+           ; maybe_flexi_tv2 <- isFlexibleTy mayInst ty2
+           ; case (flexi_tv1, maybe_flexi_tv2) of
+               (True, _) 
+                 -> -- co :: alpha ~ t
+                    doInst (rwi_swapped eq) tv1 ty2 co eq
+               (False, Just tv2) 
+                 -> -- co :: a ~ alpha                  
+                    doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
+               _ -> return $ Just eq
+           }

 
 

-        -- co :: a ~ alpha
+        -- co :: F args ~ alpha, and we are in checking mode (ie, no locals)
+    inst mayInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args, 
+                                 rwi_right = ty2, rwi_co = co})

       | Just tv2 <- tcGetTyVar_maybe ty2
       , isMetaTyVar tv2
       | Just tv2 <- tcGetTyVar_maybe ty2
       , isMetaTyVar tv2

-      = doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
-
-    inst eq = return $ Just eq
+      , mayInst tv2 && (checkingMode || tv2 `elemVarSet` skolems)
+                        -- !!!FIXME: this is too liberal, even if tv2 is in 
+                        -- skolems we shouldn't instantiate if tvs occurs 
+                        -- in other equalities that may propagate it into the
+                        -- environment
+      = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
+
+    inst _mayInst eq = return $ Just eq
+
+    -- tv is a meta var and not filled
+    isFlexible mayInst tv
+      | isMetaTyVar tv && mayInst tv = liftM isFlexi $ readMetaTyVar tv
+      | otherwise                    = return False
+
+    -- type is a tv that is a meta var and not filled
+    isFlexibleTy mayInst ty
+      | Just tv <- tcGetTyVar_maybe ty = do {flexi <- isFlexible mayInst 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 (Right ty) _eq 
       = pprPanic "TcTyFuns.doInst: local eq: " (ppr ty)

@@ -1108,102 +1332,76 @@ instantiateAndExtract eqs
            ; uMeta swapped tv lookupTV ty cotv
            }
       where
            ; uMeta swapped tv lookupTV ty cotv
            }
       where

-        -- 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
+        -- Try to fill in 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.
+        --
+        uMeta :: 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

 
 

-        -- 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
-          = 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
+        -- meta variable has been filled already
+        -- => keep the equality
+        uMeta _swapped tv (IndirectTv fill_ty) ty _cotv
+          = do { traceTc $ 
+                   ptext (sLit "flexible") <+> ppr tv <+>
+                   ptext (sLit "already filled with") <+> ppr fill_ty <+>
+                   ptext (sLit "meant to fill with") <+> ppr ty
+               ; return $ Just eq

                }
 
                }
 

-        ------ Beyond this point we know that ty2 is not a type variable
-
-        -- signature skolem meets non-variable type
+        -- signature skolem

         -- => cannot update (retain the equality)!
         uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
           = return $ Just eq
 
         -- => cannot update (retain the equality)!
         uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
           = return $ Just eq
 

+        -- type variable meets type variable
+        -- => `checkOrientation' already ensures that it is fine to instantiate
+        --    tv1 with tv2, but chase tv2's instantiations if necessary
+        -- 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
+        uMeta swapped tv1 details1@(DoneTv (MetaTv _ ref)) ty@(TyVarTy tv2) cotv
+          = do { lookupTV2 <- lookupTcTyVar tv2
+               ; case lookupTV2 of
+                   IndirectTv ty' -> 
+                     uMeta swapped tv1 details1 ty' cotv
+                   DoneTv _       -> 
+                     uMetaInst swapped tv1 ref ty cotv
+               }
+

         -- 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
         -- 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

+          = uMetaInst swapped tv ref non_tv_ty cotv
+
+        uMeta _ _ _ _ _ = panic "TcTyFuns.uMeta"
+
+        -- We know `tv' can be instantiated; check that `ty' is alright for
+        -- instantiating `tv' with and then do it; otherwise, return the original
+        -- equality.
+        uMetaInst swapped tv ref 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
+                     return $ Just eq

                    Just ty' ->
                      do { checkUpdateMeta swapped tv ref ty'  -- update meta var
                         ; writeMetaTyVar cotv ty'             -- update co var
                         ; return Nothing
                         }
                }
                    Just ty' ->
                      do { checkUpdateMeta swapped tv ref ty'  -- update meta var
                         ; writeMetaTyVar cotv ty'             -- update co var
                         ; 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}
 
 

@@ -1275,7 +1473,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}