Major bugfixing pass through the type checker

6 files changed, 319 insertions, 208 deletions

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 2001c1ee35..f834a4c328 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -259,6 +259,31 @@ canEq fl cv ty1 (TyConApp fn tys)
   | isSynFamilyTyCon fn, length tys == tyConArity fn
   = canEqLeaf fl cv (classify ty1) (FunCls fn tys) 
 
+canEq fl cv s1 s2
+  | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe s1, 
+    Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2
+  = do { (v1,v2,v3) <- if isWanted fl then 
+                         do { v1 <- newWantedCoVar t1a t2a
+                            ; v2 <- newWantedCoVar t1b t2b 
+                            ; v3 <- newWantedCoVar t1c t2c 
+                            ; let res_co = mkCoPredCo (mkCoVarCoercion v1) 
+                                                      (mkCoVarCoercion v2) (mkCoVarCoercion v3)
+                            ; setWantedCoBind cv res_co
+                            ; return (v1,v2,v3) }
+                       else let co_orig = mkCoVarCoercion cv 
+                                coa = mkCsel1Coercion co_orig
+                                cob = mkCsel2Coercion co_orig
+                                coc = mkCselRCoercion co_orig
+                            in do { v1 <- newGivOrDerCoVar t1a t2a coa
+                                  ; v2 <- newGivOrDerCoVar t1b t2b cob
+                                  ; v3 <- newGivOrDerCoVar t1c t2c coc 
+                                  ; return (v1,v2,v3) }
+       ; cc1 <- canEq fl v1 t1a t2a 
+       ; cc2 <- canEq fl v2 t1b t2b 
+       ; cc3 <- canEq fl v3 t1c t2c 
+       ; return (cc1 `andCCan` cc2 `andCCan` cc3) }
+
+
 -- Split up an equality between function types into two equalities.
 canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
   = do { (argv, resv) <- 
@@ -276,6 +301,34 @@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
        ; cc2 <- canEq fl resv t1 t2
        ; return (cc1 `andCCan` cc2) }
 
+canEq fl cv (PredTy p1) (PredTy p2) = canEqPred p1 p2 
+  where canEqPred (IParam n1 t1) (IParam n2 t2) 
+          | n1 == n2 
+          = if isWanted fl then 
+                do { v <- newWantedCoVar t1 t2 
+                   ; setWantedCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv)
+                   ; canEq fl v t1 t2 } 
+            else return emptyCCan -- DV: How to decompose given IP coercions? 
+
+        canEqPred (ClassP c1 tys1) (ClassP c2 tys2) 
+          | c1 == c2 
+          = if isWanted fl then 
+               do { vs <- zipWithM newWantedCoVar tys1 tys2 
+                  ; setWantedCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs) 
+                  ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2
+                  }
+            else return emptyCCan 
+          -- How to decompose given dictionary (and implicit parameter) coercions? 
+          -- You may think that the following is right: 
+          --    let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) 
+          --    in  zipWith3M newGivOrDerCoVar tys1 tys2 cos
+          -- But this assumes that the coercion is a type constructor-based 
+          -- coercion, and not a PredTy (ClassP cn cos) coercion. So we chose
+          -- to not decompose these coercions. We have to get back to this 
+          -- when we clean up the Coercion API.
+
+        canEqPred p1 p2 = misMatchErrorTcS fl (mkPredTy p1) (mkPredTy p2) 
+
 
 canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
   | isAlgTyCon tc1 && isAlgTyCon tc2
@@ -312,9 +365,10 @@ canEq fl cv ty1 ty2
          ; cc2 <- canEq fl cv2 t1 t2 
          ; return (cc1 `andCCan` cc2) } 
 
-canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) 
- | Wanted {} <- fl 
- = misMatchErrorTcS fl s1 s2
+canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {})  
+ | tcIsForAllTy s1, tcIsForAllTy s2, 
+   Wanted {} <- fl 
+ = misMatchErrorTcS fl s1 s2 
  | otherwise 
  = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2)
       ; return emptyCCan }
@@ -322,9 +376,10 @@ canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {})
 -- Finally expand any type synonym applications.
 canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2
 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2'
-
 canEq fl _ ty1 ty2 
   = misMatchErrorTcS fl ty1 ty2
+
+
 \end{code}
 
 Note [Equality between type applications]
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index c3d7a9e3aa..807dd61ba5 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -1,7 +1,7 @@
 \begin{code}
 module TcInteract ( 
      solveInteract, AtomicInert, 
-     InertSet, emptyInert, extendInertSet, extractUnsolved, solveOne,
+     InertSet, emptyInert, updInertSet, extractUnsolved, solveOne,
      listToWorkList
   ) where  
 
@@ -44,7 +44,7 @@ import FastString ( sLit )
 import DynFlags
 \end{code}
 
-Note [InsertSet invariants]
+Note [InertSet invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 An InertSet is a bag of canonical constraints, with the following invariants:
@@ -81,18 +81,39 @@ now we do not distinguish between given and solved constraints.
 Note that we must switch wanted inert items to given when going under an
 implication constraint (when in top-level inference mode).
 
+Note [InertSet FlattenSkolemEqClass] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The inert_fsks field of the inert set contains an "inverse map" of all the 
+flatten skolem equalities in the inert set. For instance, if inert_cts looks
+like this: 
+ 
+    fsk1 ~ fsk2 
+    fsk3 ~ fsk2 
+    fsk4 ~ fsk5 
+
+Then, the inert_fsks fields holds the following map: 
+    fsk2 |-> { fsk1, fsk3 } 
+    fsk5 |-> { fsk4 } 
+Along with the necessary coercions to convert fsk1 and fsk3 back to fsk2 
+and fsk4 back to fsk5. Hence, the invariants of the inert_fsks field are: 
+  
+   (a) All TcTyVars in the domain and range of inert_fsks are flatten skolems
+   (b) All TcTyVars in the domain of inert_fsk occur naked as rhs in some 
+       equalities of inert_cts 
+   (c) For every mapping  fsk1 |-> { (fsk2,co), ... } it must be: 
+         co : fsk2 ~ fsk1 
+
+The role of the inert_fsks is to make it easy to maintain the equivalence
+class of each flatten skolem, which is much needed to correctly do spontaneous
+solving. See Note [Loopy Spontaneous Solving] 
 \begin{code}
 
 -- See Note [InertSet invariants]
 data InertSet 
   = IS { inert_cts  :: Bag.Bag CanonicalCt 
        , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] }
--- inert_fsks contains the *FlattenSkolem* equivalence classes. 
--- inert_fsks extra invariants: 
---    (a) all TcTyVars in the domain and range of inert_fsks are flatten skolems
---    (b) for every mapping tv1 |-> (tv2,co), co : tv2 ~ tv1 
+       -- See Note [InertSet FlattenSkolemEqClass] 
 
--- newtype InertSet = IS (Bag.Bag CanonicalCt)
 instance Outputable InertSet where
   ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_cts is))
                 , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest)) 
@@ -100,20 +121,9 @@ instance Outputable InertSet where
                        )
                 ]
                        
-
-
 emptyInert :: InertSet
 emptyInert = IS { inert_cts = Bag.emptyBag, inert_fsks = Map.empty } 
 
-
-extendInertSet :: InertSet -> AtomicInert -> InertSet
--- Simply extend the bag of constraints rebuilding an inert set
-extendInertSet (IS { inert_cts  = cts
-                   , inert_fsks = fsks }) item 
-  = IS { inert_cts  = cts `Bag.snocBag` item 
-       , inert_fsks = fsks }
-
-
 updInertSet :: InertSet -> AtomicInert -> InertSet 
 -- Introduces an element in the inert set for the first time 
 updInertSet (IS { inert_cts = cts, inert_fsks = fsks })  
@@ -125,13 +135,13 @@ updInertSet (IS { inert_cts = cts, inert_fsks = fsks })
     FlatSkol {} <- tcTyVarDetails tv2 
   = let cts'  = cts `Bag.snocBag` item 
         fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks
+        -- See Note [InertSet FlattenSkolemEqClass] 
     in IS { inert_cts = cts', inert_fsks = fsks' }
 updInertSet (IS { inert_cts = cts
                 , inert_fsks = fsks }) item 
   = let cts' = cts `Bag.snocBag` item
     in IS { inert_cts = cts', inert_fsks = fsks } 
 
-
 foldlInertSetM :: (Monad m) => (a -> AtomicInert -> m a) -> a -> InertSet -> m a 
 foldlInertSetM k z (IS { inert_cts = cts }) 
   = Bag.foldlBagM k z cts
@@ -143,7 +153,7 @@ extractUnsolved is@(IS {inert_cts = cts})
 
 
 getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)] 
--- Precondition: tv is a FlatSkol 
+-- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass] 
 getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv 
   = case lkpTyEqCanByLhs of
       Nothing  -> fromMaybe [] (Map.lookup tv fsks)  
@@ -427,7 +437,15 @@ spontaneousSolveStage workItem inerts
                            , sr_inerts   = inerts 
                            , sr_stop     = Stop } 
        }
-{--
+
+{-- This is all old code, but does not quite work now. The problem is that due to 
+    Note [Loopy Spontaneous Solving] we may have unflattened a type, to be able to 
+    perform a sneaky unification. This unflattening means that we may have to recanonicalize
+    a given (solved) equality, this is why the result of trySpontaneousSolve is now a list
+    of constraints (instead of an atomic solved constraint). We would have to react all of 
+    them once again with the worklist but that is very tiresome. Instead we throw them back
+    in the worklist. 
+
                | isWantedCt workItem 
                            -- Original was wanted we have now made him given so 
                            -- we have to ineract him with the inerts again because 
@@ -522,8 +540,42 @@ where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
 it and keep it as wanted.  In inference mode we'll end up quantifying over
    (alpha ~ Maybe (E alpha))
 Hence, 'solveWithIdentity' performs a small occurs check before
-actually solving. But this occurs check *must look through* flatten
-skolems.
+actually solving. But this occurs check *must look through* flatten skolems.
+
+However, it may be the case that the flatten skolem in hand is equal to some other 
+flatten skolem whith *does not* mention our unification variable. Here's a typical example:
+
+Original wanteds: 
+   g: F alpha ~ F beta 
+   w: alpha ~ F alpha 
+After canonicalization: 
+   g: F beta ~ f1 
+   g: F alpha ~ f1 
+   w: alpha ~ f2 
+   g: F alpha ~ f2 
+After some reactions: 
+   g: f1 ~ f2 
+   g: F beta ~ f1 
+   w: alpha ~ f2 
+   g: F alpha ~ f2 
+At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved.
+We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However
+by looking at the equivalence class of the flatten skolems, we can see that it is fine to 
+unify (alpha ~ f1) which solves our goals! 
+
+A similar problem happens because of other spontaneous solving. Suppose we have the 
+following wanteds, arriving in this exact order:
+  (first)  w: beta ~ alpha 
+  (second) w: alpha ~ fsk 
+  (third)  g: F beta ~ fsk
+Then, we first spontaneously solve the first constraint, making (beta := alpha), and having
+(beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not 
+obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But 
+that is wrong since fsk mentions beta, which has already secretly been unified to alpha! 
+
+To avoid this problem, the same occurs check must unveil rewritings that can happen because 
+of spontaneously having solved other constraints. 
+
 
 Note [Avoid double unifications] 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -559,8 +611,8 @@ solveWithIdentity :: InertSet
 -- See [New Wanted Superclass Work] to see why we do this for *given* as well
 solveWithIdentity inerts cv gw tv xi 
   | not (isGiven gw)
-  = do { m <- passOccursCheck inerts tv xi 
-       ; case m of 
+  = do { tybnds <- getTcSTyBindsBag 
+       ; case occ_check_ok tybnds xi of 
            Nothing -> return Nothing 
            Just (xi_unflat,coi) -- coi : xi_unflat ~ xi  
                -> do { traceTcS "Sneaky unification:" $ 
@@ -579,7 +631,8 @@ solveWithIdentity inerts cv gw tv xi
                                     (singleCCan (CTyEqCan { cc_id = cv_given 
                                                           , cc_flavor = mkGivenFlavor gw UnkSkol
                                                           , cc_tyvar = tv, cc_rhs = xi }
-                                                          -- xi, *not* xi_unflat! 
+                                                          -- xi, *not* xi_unflat because 
+                                                          -- xi_unflat may require flattening!
                                                 ), co)
                      ; case gw of 
                          Wanted  {} -> setWantedCoBind  cv co
@@ -588,128 +641,83 @@ solveWithIdentity inerts cv gw tv xi
 
        -- See Note [Avoid double unifications] 
 
-       -- The reason that we create a new given variable (cv_given) instead of reusing cv
-       -- is because we do not want to end up with coercion unification variables in the givens.
-                     ; return (Just cts) } 
+                     ; return (Just cts) }
        }
   | otherwise 
   = return Nothing 
 
-
-passOccursCheck :: InertSet -> TcTyVar -> TcType -> TcS (Maybe (TcType,CoercionI))
--- passOccursCheck inerts tv ty 
--- Traverse the type and make sure that 'tv' does not appear under 
--- some flatten skolem. If it appears under some flatten skolem 
--- look in that flatten skolem equivalence class to see if you can 
--- find a different flatten skolem to use, which does not mention the 
--- variable.
--- Postcondition: Just (ty',coi) <- passOccursCheck tv ty 
---       coi :: ty' ~ ty 
--- NB: I believe there is no need to do the tcView thing here
-passOccursCheck is tv (TyConApp tc tys) 
-  = do { tys_mbs <- mapM (passOccursCheck is tv) tys 
-       ; case allMaybes tys_mbs of 
-           Nothing -> return Nothing 
-           Just tys_cois -> 
-               let (tys',cois') = unzip tys_cois
-               in return $ 
-                  Just (TyConApp tc tys', mkTyConAppCoI tc cois')
-       }
-passOccursCheck is tv (PredTy sty) 
-  = do { sty_mb <- passOccursCheckPred tv sty 
-       ; case sty_mb of 
-           Nothing -> return Nothing 
-           Just (sty',coi) -> return (Just (PredTy sty', coi))
-       }
-  where passOccursCheckPred tv (ClassP cn tys)
-          = do { tys_mbs <- mapM (passOccursCheck is tv) tys 
-               ; case allMaybes tys_mbs of 
-                   Nothing -> return Nothing 
-                   Just tys_cois -> 
-                       let (tys', cois') = unzip tys_cois 
-                       in return $ 
-                          Just (ClassP cn tys', mkClassPPredCoI cn cois') 
-               }
-        passOccursCheckPred tv (IParam nm ty)   
-          = do { mty <- passOccursCheck is tv ty 
-               ; case mty of 
-                   Nothing -> return Nothing 
-                   Just (ty',co') 
-                       -> return (Just (IParam nm ty', 
-                                               mkIParamPredCoI nm co')) 
-               }
-        passOccursCheckPred tv (EqPred ty1 ty2) 
-          = do { mty1 <- passOccursCheck is tv ty1 
-               ; mty2 <- passOccursCheck is tv ty2 
-               ; case (mty1,mty2) of 
-                   (Just (ty1',coi1), Just (ty2',coi2))
-                       -> return $ 
-                          Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
-                   _ -> return Nothing 
-               }
-                           
-passOccursCheck is tv (FunTy arg res) 
-  = do { arg_mb <- passOccursCheck is tv arg 
-       ; res_mb <- passOccursCheck is tv res
-       ; case (arg_mb,res_mb) of 
-           (Just (arg',coiarg), Just (res',coires)) 
-               -> return $ 
-                  Just (FunTy arg' res', mkFunTyCoI coiarg coires)
-           _ -> return Nothing 
-       }
-
-passOccursCheck is tv (AppTy fun arg) 
-  = do { fun_mb <- passOccursCheck is tv fun 
-       ; arg_mb <- passOccursCheck is tv arg 
-       ; case (fun_mb,arg_mb) of 
-           (Just (fun',coifun), Just (arg',coiarg)) 
-               -> return $ 
-                  Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
-           _ -> return Nothing 
-       }
-
-passOccursCheck is tv (ForAllTy tv1 ty1) 
-  = do { ty1_mb <- passOccursCheck is tv ty1 
-       ; case ty1_mb of 
-           Nothing -> return Nothing 
-           Just (ty1',coi) 
-               -> return $ 
-                  Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
-       }
-
-passOccursCheck _is tv (TyVarTy tv') 
-  | tv == tv' 
-  = return Nothing 
-
-passOccursCheck is tv (TyVarTy fsk) 
-  | FlatSkol ty <- tcTyVarDetails fsk 
-  = do { zty <- zonkFlattenedType ty -- Must zonk as it contains unif. vars
-       ; occ <- passOccursCheck is tv zty 
-       ; case occ of 
-           Nothing         -> go_down_eq_class $ getFskEqClass is fsk
-           Just (zty',ico) -> return $ Just (zty',ico) 
-       }
-  where go_down_eq_class [] = return Nothing 
-        go_down_eq_class ((fsk1,co1):rest) 
-          = do { occ1 <- passOccursCheck is tv (TyVarTy fsk1)
-               ; case occ1 of 
-                   Nothing -> go_down_eq_class rest 
-                   Just (ty1,co1i') 
-                     -> return $ Just (ty1, mkTransCoI co1i' (ACo co1)) }  
-passOccursCheck _is _tv ty 
-  = return (Just (ty,IdCo ty))  
-
-{-- 
-Problematic situation: 
-~~~~~~~~~~~~~~~~~~~~~~
- Suppose we have a flatten skolem f1 := F f6
- Suppose we are chasing for 'alpha', and: 
-       f6 := G alpha with eq.class f7,f8 
-
- Then we will return F f7 potentially. 
---} 
-
-
+  where occ_check_ok :: Bag.Bag (TcTyVar, TcType) -> TcType -> Maybe (TcType,CoercionI) 
+        occ_check_ok ty_binds_bag ty = ok ty 
+           where 
+           -- @ok ty@
+           -- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem. 
+           -- If it appears under some flatten skolem look in that flatten skolem equivalence class 
+           -- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you 
+           -- can find a different flatten skolem to use, that is, one that does not mention @tv@.
+           -- 
+           -- Postcondition: Just (ty',coi) <- ok ty 
+           --       coi :: ty' ~ ty 
+           -- 
+           -- NB: The returned type may not be flat!
+           --    
+           -- NB: There is no need to do the tcView thing here to expand synonyms, because
+           -- expanded synonyms have the same or fewer variables than their expanded definitions, 
+           -- but never more.
+           -- See Note [Type synonyms and the occur check] in TcUnify for the handling of type synonyms.
+                 ok this_ty@(TyConApp tc tys) 
+                   | Just tys_cois <- allMaybes (map ok tys) 
+                   = let (tys',cois') = unzip tys_cois
+                     in Just (TyConApp tc tys', mkTyConAppCoI tc cois') 
+                   | isSynTyCon tc, Just ty_expanded <- tcView this_ty
+                   = ok ty_expanded
+                 ok (PredTy sty) 
+                   | Just (sty',coi) <- ok_pred sty 
+                   = Just (PredTy sty', coi) 
+                   where ok_pred (ClassP cn tys)
+                           | Just tys_cois <- allMaybes $ map ok tys 
+                           = let (tys', cois') = unzip tys_cois 
+                             in Just (ClassP cn tys', mkClassPPredCoI cn cois')
+                         ok_pred (IParam nm ty)   
+                           | Just (ty',co') <- ok ty 
+                           = Just (IParam nm ty', mkIParamPredCoI nm co') 
+                         ok_pred (EqPred ty1 ty2) 
+                           | Just (ty1',coi1) <- ok ty1, Just (ty2',coi2) <- ok ty2
+                           = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2) 
+                         ok_pred _ = Nothing 
+                 ok (FunTy arg res) 
+                   | Just (arg', coiarg) <- ok arg, Just (res', coires) <- ok res
+                   = Just (FunTy arg' res', mkFunTyCoI coiarg coires) 
+                 ok (AppTy fun arg) 
+                   | Just (fun', coifun) <- ok fun, Just (arg', coiarg) <- ok arg 
+                   = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg) 
+                 ok (ForAllTy tv1 ty1) 
+                 -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment. 
+                   | Just (ty1', coi) <- ok ty1 
+                   = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi) 
+
+                 -- Variable cases 
+                 ok this_ty@(TyVarTy tv') 
+                   | not $ isTcTyVar tv' = Just (this_ty, IdCo this_ty) -- Bound variable
+                   | tv == tv'           = Nothing                      -- Occurs check error
+                 -- Flatten skolem 
+                 ok (TyVarTy fsk) | FlatSkol zty <- tcTyVarDetails fsk
+                   = case ok zty of 
+                       Nothing         -> go_down_eq_class $ getFskEqClass inerts fsk
+                       Just (zty',ico) -> Just (zty',ico) 
+                   where go_down_eq_class [] = Nothing 
+                         go_down_eq_class ((fsk1,co1):rest) 
+                           = case ok (TyVarTy fsk1) of 
+                               Nothing -> go_down_eq_class rest 
+                               Just (ty1,co1i') -> Just (ty1, mkTransCoI co1i' (ACo co1)) 
+                 -- Finally, check if bound already 
+                 ok this_ty@(TyVarTy tv0) 
+                   = case Bag.foldlBag find_bind Nothing ty_binds_bag of 
+                       Nothing -> Just (this_ty, IdCo this_ty)
+                       Just ty0 -> ok ty0 
+                   where find_bind Nothing (tvx,tyx) | tv0 == tvx = Just tyx
+                         find_bind m _ = m 
+                 -- Fall through
+                 ok _ty = Nothing 
 
 \end{code}
 
@@ -972,10 +980,12 @@ doInteractWithInert
   | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
   = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) 
        ; mkIRContinue workItem DropInert rewritten_eq } 
--- Finally, if workitem is a flatten equivalence class constraint and the 
--- inert is a wanted constraints, even when the workitem cannot rewrite the 
--- inert, drop the inert out because you may have to reconsider solving him 
--- using the equivalence class you created. 
+
+-- Finally, if workitem is a Flatten Equivalence Class constraint and the 
+-- inert is a wanted constraint, even when the workitem cannot rewrite the 
+-- inert, drop the inert out because you may have to reconsider solving the 
+-- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving]
+-- and [InertSet FlattenSkolemEqClass] 
 
   | not $ isGiven fl1,                  -- The inert is wanted or derived
     isMetaTyVar tv1,                    -- and has a unification variable lhs
@@ -984,7 +994,7 @@ doInteractWithInert
   = mkIRContinue workItem DropInert (singletonWorkList inert)
 
 
--- Fall-through case for all other cases
+-- Fall-through case for all other situations
 doInteractWithInert _ workItem = noInteraction workItem
 
 --------------------------------------------
@@ -1108,15 +1118,6 @@ rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
                         mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
        ; mkCanonical gw cv2' }
 
---                                              ->
--- if isWanted gw then 
---                      do { cv2' <- newWantedCoVar xi1 xi2 
---                         ; setWantedCoBind cv2 $ 
---                           co1 `mkTransCoercion` mkCoVarCoercion cv2'
---                         ; return cv2' } 
---                  else newGivOrDerCoVar xi1 xi2 $ 
---                       mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 
---        ; mkCanonical gw cv2' }
 
 
 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult 
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index c98681139d..f8b357a8d5 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -31,11 +31,10 @@ module TcSMonad (
  
     getInstEnvs, getFamInstEnvs,                -- Getting the environments 
     getTopEnv, getGblEnv, getTcEvBinds, getUntouchablesTcS,
-    getTcEvBindsBag, getTcSContext, getTcSTyBinds,
+    getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsBag,
 
 
     newFlattenSkolemTy,                         -- Flatten skolems 
-    zonkFlattenedType, 
 
 
     instDFunTypes,                              -- Instantiation
@@ -434,6 +433,7 @@ runTcS context untouch tcs
        ; return (res, evBindMapBinds ev_binds) }
   where
     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
+
        
 nestImplicTcS :: EvBindsVar -> TcTyVarSet -> TcS a -> TcS a 
 nestImplicTcS ref untouch tcs 
@@ -475,6 +475,10 @@ getTcEvBinds = TcS (return . tcs_ev_binds)
 getTcSTyBinds :: TcS (IORef (Bag (TcTyVar, TcType)))
 getTcSTyBinds = TcS (return . tcs_ty_binds)
 
+getTcSTyBindsBag :: TcS (Bag (TcTyVar, TcType)) 
+getTcSTyBindsBag = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
+
+
 getTcEvBindsBag :: TcS EvBindMap
 getTcEvBindsBag
   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
@@ -577,26 +581,6 @@ newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
                              mkTcTyVar name (typeKind ty) (FlatSkol ty) 
                            }
 
-
-zonkFlattenedType :: TcType -> TcS TcType 
-zonkFlattenedType ty = wrapTcS (TcM.zonkTcType ty) 
-
-
-{-- 
-tyVarsOfUnflattenedType :: TcType -> TcTyVarSet
--- A version of tyVarsOfType which looks through flatSkols
-tyVarsOfUnflattenedType ty
-  = foldVarSet (unionVarSet . do_tv) emptyVarSet (tyVarsOfType ty)
-  where
-    do_tv :: TyVar -> TcTyVarSet
-    do_tv tv = ASSERT( isTcTyVar tv)
-               case tcTyVarDetails tv of 
-                  FlatSkol _ ty -> tyVarsOfUnflattenedType ty
-                  _             -> unitVarSet tv 
---} 
-
-
-
 -- Instantiations 
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index d8be2d1178..48258ed011 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -405,7 +405,7 @@ simplifySuperClass self wanteds
        ; (unsolved, ev_binds) 
              <- runTcS SimplCheck emptyVarSet $
          	do { can_self <- canGivens loc [self]
-         	   ; let inert = foldlBag extendInertSet emptyInert can_self
+         	   ; let inert = foldlBag updInertSet emptyInert can_self
 	 	     -- No need for solveInteract; we know it's inert
 
 	 	   ; solveWanteds inert wanteds }
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index d73869f344..2b9838bcc7 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -46,6 +46,8 @@ import Name
 import ErrUtils
 import BasicTypes
 import Bag
+
+import Maybes ( allMaybes )  
 import Util
 import Outputable
 import FastString
@@ -575,7 +577,16 @@ uType_np origin orig_ty1 orig_ty2
         -- Predicates
     go origin (PredTy p1) (PredTy p2) = uPred origin p1 p2
 
-        -- Functions; just check the two parts
+        -- Coercion functions: (t1a ~ t1b) => t1c  ~  (t2a ~ t2b) => t2c
+    go origin ty1 ty2 
+      | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe ty1, 
+        Just (t2a,t2b,t2c) <- splitCoPredTy_maybe ty2
+      = do { co1 <- uType origin t1a t2a 
+           ; co2 <- uType origin t1b t2b
+           ; co3 <- uType origin t1c t2c 
+           ; return $ mkCoPredCoI co1 co2 co3 }
+
+        -- Functions (or predicate functions) just check the two parts
     go origin (FunTy fun1 arg1) (FunTy fun2 arg2)
       = do { coi_l <- uType origin fun1 fun2
            ; coi_r <- uType origin arg1 arg2
@@ -607,7 +618,8 @@ uType_np origin orig_ty1 orig_ty2
            ; return $ mkAppTyCoI coi_s coi_t }
 
     go _ ty1 ty2
-      | isSigmaTy ty1 || isSigmaTy ty2
+      | tcIsForAllTy ty1 || tcIsForAllTy ty2 
+{--      | isSigmaTy ty1 || isSigmaTy ty2 --} 
       = unifySigmaTy origin ty1 ty2
 
         -- Anything else fails
@@ -909,27 +921,65 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
 
 checkTauTvUpdate tv ty
   = do { ty' <- zonkTcType ty
-       ; if ok ty' && (typeKind ty' `isSubKind` tyVarKind tv) 
-         then return (Just ty')
+       ; if typeKind ty' `isSubKind` tyVarKind tv then
+           case ok ty' of 
+             Nothing -> return Nothing 
+             Just ty'' -> return (Just ty'')
          else return Nothing }
-  where ok :: TcType -> Bool 
-        -- Check that (a) tv is not among the free variables of 
-        -- the type and that (b) the type is type-family-free.
-        -- Reason: Note [Type family sharing]  
-        ok ty1 | Just ty1' <- tcView ty1 = ok ty1'  
-        ok (TyVarTy tv')      = not (tv == tv') 
-        ok (TyConApp tc tys)  = all ok tys && not (isSynFamilyTyCon tc)
-        ok (PredTy sty)       = ok_pred sty 
-        ok (FunTy arg res)    = ok arg && ok res 
-        ok (AppTy fun arg)    = ok fun && ok arg 
-        ok (ForAllTy _tv1 ty1) = ok ty1       
-
-        ok_pred (IParam _ ty)    = ok ty 
-        ok_pred (ClassP _ tys)   = all ok tys 
-        ok_pred (EqPred ty1 ty2) = ok ty1 && ok ty2 
+
+  where ok :: TcType -> Maybe TcType 
+        ok (TyVarTy tv') | not (tv == tv') = Just (TyVarTy tv') 
+        ok this_ty@(TyConApp tc tys) 
+          | not (isSynFamilyTyCon tc), Just tys' <- allMaybes (map ok tys) 
+          = Just (TyConApp tc tys') 
+          | isSynTyCon tc, Just ty_expanded <- tcView this_ty
+          = ok ty_expanded -- See Note [Type synonyms and the occur check] 
+        ok (PredTy sty) | Just sty' <- ok_pred sty = Just (PredTy sty') 
+        ok (FunTy arg res) | Just arg' <- ok arg, Just res' <- ok res
+                           = Just (FunTy arg' res') 
+        ok (AppTy fun arg) | Just fun' <- ok fun, Just arg' <- ok arg 
+                           = Just (AppTy fun' arg') 
+        ok (ForAllTy tv1 ty1) | Just ty1' <- ok ty1 = Just (ForAllTy tv1 ty1') 
+        -- Fall-through 
+        ok _ty = Nothing 
+       
+        ok_pred (IParam nm ty) | Just ty' <- ok ty = Just (IParam nm ty') 
+        ok_pred (ClassP cl tys) 
+          | Just tys' <- allMaybes (map ok tys) 
+          = Just (ClassP cl tys') 
+        ok_pred (EqPred ty1 ty2) 
+          | Just ty1' <- ok ty1, Just ty2' <- ok ty2 
+          = Just (EqPred ty1' ty2') 
+        -- Fall-through 
+        ok_pred _pty = Nothing 
 
 \end{code}
 
+Note [Type synonyms and the occur check]
+~~~~~~~~~~~~~~~~~~~~
+Generally speaking we need to update a variable with type synonyms not expanded, which
+improves later error messages, except for when looking inside a type synonym may help resolve
+a spurious occurs check error. Consider: 
+          type A a = ()
+
+          f :: (A a -> a -> ()) -> ()
+          f = \ _ -> ()
+
+          x :: ()
+          x = f (\ x p -> p x)
+
+We will eventually get a constraint of the form t ~ A t. The ok function above will 
+properly expand the type (A t) to just (), which is ok to be unified with t. If we had
+unified with the original type A t, we would lead the type checker into an infinite loop. 
+
+Hence, if the occurs check fails for a type synonym application, then (and *only* then), 
+the ok function expands the synonym to detect opportunities for occurs check success using
+the underlying definition of the type synonym. 
+
+The same applies later on in the constraint interaction code; see TcInteract, 
+function @occ_check_ok@. 
+
+
 Note [Type family sharing]
 ~~~~~~~~~~~~~~ 
 We must avoid eagerly unifying type variables to types that contain function symbols, 
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 8249ed9c8a..f7c48f4103 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -44,8 +44,9 @@ module Coercion (
         mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
         mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
         mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion, 
-                       
-        mkCoVarCoercion, 
+
+	mkClassPPredCo, mkIParamPredCo,
+        mkCoVarCoercion, mkCoPredCo, 
 
 
         unsafeCoercionTyCon, symCoercionTyCon,
@@ -68,7 +69,7 @@ module Coercion (
 	mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
 	mkForAllTyCoI,
 	fromCoI, 
-	mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI
+	mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI, mkCoPredCoI 
 
        ) where 
 
@@ -282,6 +283,11 @@ mkCoPredTy s t r = ASSERT( not (co_var `elemVarSet` tyVarsOfType r) )
   where
     co_var = mkWildCoVar (mkCoKind s t)
 
+mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion 
+-- Creates a coercion between (s1~t1) => r1  and (s2~t2) => r2 
+mkCoPredCo = mkCoPredTy 
+
+
 splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
 splitCoPredTy_maybe ty
   | Just (cv,r) <- splitForAllTy_maybe ty
@@ -347,7 +353,7 @@ mkTyConCoercion con cos = mkTyConApp con cos
 
 -- | Make a function 'Coercion' between two other 'Coercion's
 mkFunCoercion :: Coercion -> Coercion -> Coercion
-mkFunCoercion co1 co2 = mkFunTy co1 co2
+mkFunCoercion co1 co2 = mkFunTy co1 co2 -- NB: Handles correctly the forall for eqpreds!
 
 -- | Make a 'Coercion' which binds a variable within an inner 'Coercion'
 mkForAllCoercion :: Var -> Coercion -> Coercion
@@ -444,6 +450,16 @@ mkFamInstCoercion name tvs family inst_tys rep_tycon
     desc = CoAxiom { co_ax_tvs = tvs
                    , co_ax_lhs = mkTyConApp family inst_tys 
                    , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) }
+
+
+mkClassPPredCo :: Class -> [Coercion] -> Coercion
+mkClassPPredCo cls = (PredTy . ClassP cls)
+
+mkIParamPredCo :: (IPName Name) -> Coercion -> Coercion
+mkIParamPredCo ipn = (PredTy . IParam ipn)
+
+
+
 \end{code}
 
 
@@ -680,6 +696,11 @@ mkIParamPredCoI ipn = liftCoI (PredTy . IParam ipn)
 -- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI'
 mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
 mkEqPredCoI = liftCoI2 (\t1 t2 -> PredTy (EqPred t1 t2))
+
+mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI 
+mkCoPredCoI coi1 coi2 coi3 =   mkFunTyCoI (mkEqPredCoI coi1 coi2) coi3
+
+
 \end{code}
 
 %************************************************************************