Comments only

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

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index ba73891..77d7205 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

@@ -287,7 +286,7 @@ no further propoagation is possible.
 --
 normaliseEqs :: [Inst] -> TcM EqConfig
 normaliseEqs eqs 
 --
 normaliseEqs :: [Inst] -> TcM EqConfig
 normaliseEqs eqs 

-  = do { ASSERTM2( allM isValidWantedEqInst eqs, ppr eqs )
+  = do { ASSERTM2( allM wantedEqInstIsUnsolved eqs, ppr eqs )

        ; traceTc $ ptext (sLit "Entering normaliseEqs")
 
        ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs
        ; traceTc $ ptext (sLit "Entering normaliseEqs")
 
        ; (eqss, skolemss) <- mapAndUnzipM normEqInst eqs

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

-  = do { traceTc $ ptext (sLit "Entering 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 []

@@ -333,35 +337,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' (null locals)
-       ; 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}
 
 

@@ -480,22 +475,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'
            }

@@ -583,13 +585,7 @@ checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
 -- NB: We cannot assume that the two types already have outermost type
 --     synonyms expanded due to the recursion in the case of type applications.
 checkOrientation ty1 ty2 co inst
 -- NB: We cannot assume that the two types already have outermost type
 --     synonyms expanded due to the recursion in the case of type applications.
 checkOrientation ty1 ty2 co inst

-  = do { traceTc $ ptext (sLit "checkOrientation of ") <+> 
-                   pprEqInstCo co <+> text "::" <+> 
-                   ppr ty1 <+> text "~" <+> ppr ty2
-       ; eqs <- go ty1 ty2
-       ; traceTc $ ptext (sLit "checkOrientation returns") <+> ppr eqs
-       ; return eqs
-       }
+  = go ty1 ty2

   where
       -- look through synonyms
     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
   where
       -- look through synonyms
     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2

@@ -679,10 +675,10 @@ flattenType inst ty
     go ty@(TyVarTy _)
       = return (ty, ty, [] , emptyVarSet)
 
     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

@@ -705,6 +701,7 @@ flattenType inst ty
       -- data constructor application => flatten subtypes
       -- NB: Special cased for efficiency - could be handled as type application
     go ty@(TyConApp con args)
       -- data constructor application => flatten subtypes
       -- NB: Special cased for efficiency - could be handled as type application
     go ty@(TyConApp con args)

+      | not (isOpenSynTyCon con)   -- don't match oversaturated family apps

       = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
            ; if null args_eqss
              then     -- unchanged, keep the old type with folded synonyms
       = do { (args', cargs, args_eqss, args_skolemss) <- mapAndUnzip4M go args
            ; if null args_eqss
              then     -- unchanged, keep the old type with folded synonyms

@@ -732,7 +729,10 @@ flattenType inst ty
            }
 
       -- type application => flatten subtypes
            }
 
       -- type application => flatten subtypes

-    go ty@(AppTy ty_l ty_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, skolems_l) <- go ty_l
            ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
            ; if null eqs_l && null eqs_r
       = do { (ty_l', co_l, eqs_l, skolems_l) <- go ty_l
            ; (ty_r', co_r, eqs_r, skolems_r) <- go ty_r
            ; if null eqs_l && null eqs_r

@@ -759,6 +759,8 @@ 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
                 -> Coercion            -- coercion witnessing the left rewrite
                 -> Coercion            -- coercion witnessing the right rewrite
 adjustCoercions :: EqInstCo            -- coercion of original equality
                 -> Coercion            -- coercion witnessing the left rewrite
                 -> Coercion            -- coercion witnessing the right rewrite

@@ -812,17 +814,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}

@@ -876,8 +884,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 

@@ -945,6 +956,8 @@ 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))
 -- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms
   | fam1 == fam2 && tcEqTypes args1 args2 &&
     (isWantedRewriteInst eq2 || not (isWantedRewriteInst eq1))
 -- !!!TODO: tcEqTypes is insufficient as it does not look through type synonyms

@@ -954,11 +967,18 @@ applySubstFam eq1@(RewriteFam {rwi_fam = fam1, rwi_args = args1})
        ; eq2' <- deriveEqInst eq2 lhs rhs co2'
        ; liftM Just $ normEqInst eq2'
        }
        ; 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}
 

@@ -980,17 +1000,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}
 

@@ -1008,6 +1037,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

@@ -1022,6 +1053,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}
 

@@ -1041,10 +1079,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

@@ -1058,19 +1112,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
       = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr eq
     subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs) 
           res binds locals wanteds
       = 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'
            }

@@ -1103,8 +1173,7 @@ 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}) 
-              coSubst tySubst isWanted dict
+    substDict (RewriteVar {rwi_var = tv}) coSubst tySubst isWanted dict

       | isClassDict dict
       , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
       = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))
       | isClassDict dict
       , tv `elemVarSet` tyVarsOfPred (tci_pred dict)
       = do { let co1Subst = PredTy (substPred coSubst (tci_pred dict))

@@ -1122,42 +1191,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] -> Bool -> TcM ([Inst], Bool)
-instantiateAndExtract eqs localsEmpty
-  = do { 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
     wanteds      = filter (isWantedCo . rwi_co) eqs
     checkingMode = length eqs > length wanteds || not localsEmpty
                      -- no local equalities or dicts => checking mode
 
        }
   where
     wanteds      = filter (isWantedCo . rwi_co) eqs
     checkingMode = length eqs > length wanteds || not localsEmpty
                      -- no local equalities or dicts => checking mode
 

-    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
-
-        -- co :: a ~ alpha
-      | Just tv2 <- tcGetTyVar_maybe ty2
-      , isMetaTyVar tv2
-      = doInst (not $ rwi_swapped eq) tv2 (mkTyVarTy tv1) co eq
+        -- 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 :: F args ~ alpha, and we are in checking mode (ie, no locals)
 
         -- co :: F args ~ alpha, and we are in checking mode (ie, no locals)

-    inst eq@(RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = ty2, 
-                         rwi_co = co})
-      | checkingMode
-      , Just tv2 <- tcGetTyVar_maybe ty2
+    inst mayInst eq@(RewriteFam {rwi_fam = fam, rwi_args = args, 
+                                 rwi_right = ty2, rwi_co = co})
+      | Just tv2 <- tcGetTyVar_maybe ty2

       , isMetaTyVar tv2
       , isMetaTyVar tv2

+      , mayInst tv2 && (checkingMode || tv2 `elemVarSet` skolems)
+                        -- !!!TODO: 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
 
       = doInst (not $ rwi_swapped eq) tv2 (mkTyConApp fam args) co eq
 

-    inst eq = return $ Just 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)

@@ -1167,9 +1269,14 @@ instantiateAndExtract eqs localsEmpty
            }
       where
         -- meta variable has been filled already
            }
       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
+        -- => 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
+               }

 
         -- type variable meets type variable
         -- => check that tv2 hasn't been updated yet and choose which to update
 
         -- type variable meets type variable
         -- => check that tv2 hasn't been updated yet and choose which to update

@@ -1201,8 +1308,9 @@ instantiateAndExtract eqs localsEmpty
                              
                ; 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
                    Just ty' ->
                      do { checkUpdateMeta swapped tv ref ty'  -- update meta var
                         ; writeMetaTyVar cotv ty'             -- update co var

@@ -1230,8 +1338,9 @@ instantiateAndExtract eqs localsEmpty
                    (SigTv _, _      ) | k1_sub_k2 -> update_tv2
                    (_,       SigTv _) | k2_sub_k1 -> update_tv1
 
                    (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
+                   (_,   _) | 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
                                            else update_tv2
                             | k2_sub_k1 -> update_tv1
                             | otherwise -> kind_err