Typechecker performance fixes and flatten skolem bugfixing
authordimitris@microsoft.com <unknown>
Mon, 4 Oct 2010 13:02:00 +0000 (13:02 +0000)
committerdimitris@microsoft.com <unknown>
Mon, 4 Oct 2010 13:02:00 +0000 (13:02 +0000)
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs

index 415365f..2001c1e 100644 (file)
@@ -1,6 +1,7 @@
 \begin{code}
 module TcCanonical(
-    mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck 
+    mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck, 
+    canEq
  ) where
 
 #include "HsVersions.h"
index b079368..c3d7a9e 100644 (file)
@@ -7,10 +7,12 @@ module TcInteract (
 
 #include "HsVersions.h"
 
+
 import BasicTypes 
 import TcCanonical
 import VarSet
 import Type
+import TypeRep 
 
 import Id 
 import Var
@@ -34,6 +36,9 @@ import TcRnTypes
 import TcErrors
 import TcSMonad 
 import qualified Bag as Bag
+import qualified Data.Map as Map 
+import Maybes 
+
 import Control.Monad( zipWithM, unless )
 import FastString ( sLit ) 
 import DynFlags
@@ -79,37 +84,95 @@ implication constraint (when in top-level inference mode).
 \begin{code}
 
 -- See Note [InertSet invariants]
-
-newtype InertSet = IS (Bag.Bag CanonicalCt)
+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 
+
+-- newtype InertSet = IS (Bag.Bag CanonicalCt)
 instance Outputable InertSet where
-  ppr (IS cts) = vcat (map ppr (Bag.bagToList cts))
+  ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_cts is))
+                , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest)) 
+                       (Map.toList $ inert_fsks is)
+                       )
+                ]
+                       
 
-{- TODO: Later ...
-data Inert = IS { class_inerts :: FiniteMap Class Atomics
-                 ip_inerts    :: FiniteMap Class Atomics
-                 tyfun_inerts :: FiniteMap TyCon Atomics
-                 tyvar_inerts :: FiniteMap TyVar Atomics
-                }
-
-Later should we also separate out givens and wanteds?
--}
 
 emptyInert :: InertSet
-emptyInert = IS Bag.emptyBag
+emptyInert = IS { inert_cts = Bag.emptyBag, inert_fsks = Map.empty } 
+
 
 extendInertSet :: InertSet -> AtomicInert -> InertSet
-extendInertSet (IS cts) item = IS (cts `Bag.snocBag` item)
+-- 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 })  
+            item@(CTyEqCan { cc_id    = cv
+                           , cc_tyvar = tv1 
+                           , cc_rhs   = xi })
+  | Just tv2 <- tcGetTyVar_maybe xi,
+    FlatSkol {} <- tcTyVarDetails tv1, 
+    FlatSkol {} <- tcTyVarDetails tv2 
+  = let cts'  = cts `Bag.snocBag` item 
+        fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks
+    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 cts) = Bag.foldlBagM k z cts
+foldlInertSetM k z (IS { inert_cts = cts }) 
+  = Bag.foldlBagM k z cts
 
 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
-extractUnsolved (IS cts)
-  = (IS cts', unsolved)
+extractUnsolved is@(IS {inert_cts = cts}) 
+  = (is { inert_cts = cts'}, unsolved)
   where (unsolved, cts') = Bag.partitionBag isWantedCt cts
 
+
+getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)] 
+-- Precondition: tv is a FlatSkol 
+getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv 
+  = case lkpTyEqCanByLhs of
+      Nothing  -> fromMaybe [] (Map.lookup tv fsks)  
+      Just ceq -> 
+        case tcGetTyVar_maybe (cc_rhs ceq) of 
+          Just tv_rhs | FlatSkol {} <- tcTyVarDetails tv_rhs
+            -> let ceq_co = mkSymCoercion $ mkCoVarCoercion (cc_id ceq)
+                   mk_co (v,c) = (v, mkTransCoercion c ceq_co)
+               in (tv_rhs, ceq_co): map mk_co (fromMaybe [] $ Map.lookup tv fsks) 
+          _ -> []
+  where lkpTyEqCanByLhs = Bag.foldlBag lkp Nothing cts 
+        lkp :: Maybe CanonicalCt -> CanonicalCt -> Maybe CanonicalCt 
+        lkp Nothing ct@(CTyEqCan {cc_tyvar = tv'}) | tv' == tv = Just ct 
+        lkp other _ct = other 
+
+
 isWantedCt :: CanonicalCt -> Bool 
 isWantedCt ct = isWanted (cc_flavor ct)
+
+{- TODO: Later ...
+data Inert = IS { class_inerts :: FiniteMap Class Atomics
+                 ip_inerts    :: FiniteMap Class Atomics
+                 tyfun_inerts :: FiniteMap TyCon Atomics
+                 tyvar_inerts :: FiniteMap TyVar Atomics
+                }
+
+Later should we also separate out givens and wanteds?
+-}
+
 \end{code}
 
 Note [Touchables and givens]
@@ -172,9 +235,9 @@ Note [Basic plan]
 
 type AtomicInert = CanonicalCt     -- constraint pulled from InertSet
 type WorkItem    = CanonicalCt     -- constraint pulled from WorkList
-type SWorkItem   = WorkItem        -- a work item we know is solved
 
 type WorkList    = CanonicalCts    -- A mixture of Given, Wanted, and Solved
+type SWorkList   = WorkList        -- A worklist of solved 
                    
 
 listToWorkList :: [WorkItem] -> WorkList
@@ -192,6 +255,9 @@ isEmptyWorkList = Bag.isEmptyBag
 emptyWorkList :: WorkList
 emptyWorkList = Bag.emptyBag
 
+singletonWorkList :: CanonicalCt -> WorkList 
+singletonWorkList ct = singleCCan ct 
+
 data StopOrContinue 
   = Stop                       -- Work item is consumed
   | ContinueWith WorkItem      -- Not consumed
@@ -238,7 +304,7 @@ runSolverPipeline pipeline inerts workItem
        ; let new_inert 
               = case sr_stop itr_out of 
                          Stop              -> sr_inerts itr_out
-                  ContinueWith item -> sr_inerts itr_out `extendInertSet` item
+                  ContinueWith item -> sr_inerts itr_out `updInertSet` item
        ; return (new_inert, sr_new_work itr_out) }
   where 
     run_pipeline :: [(String, SimplifierStage)]
@@ -349,14 +415,19 @@ thePipeline = [ ("interact with inerts", interactWithInertsStage)
 \begin{code}
 spontaneousSolveStage :: SimplifierStage 
 spontaneousSolveStage workItem inerts 
-  = do { mSolve <- trySpontaneousSolve workItem 
+  = do { mSolve <- trySpontaneousSolve workItem inerts 
        ; case mSolve of 
            Nothing -> -- no spontaneous solution for him, keep going
                return $ SR { sr_new_work   = emptyWorkList 
                            , sr_inerts     = inerts 
                            , sr_stop       = ContinueWith workItem }
 
-           Just workItem' -- He has been solved; workItem' is a Given
+           Just workList' -> -- He has been solved; workList' are all givens 
+               return $ SR { sr_new_work = workList'
+                           , sr_inerts   = inerts 
+                           , sr_stop     = Stop } 
+       }
+{--
                | isWantedCt workItem 
                            -- Original was wanted we have now made him given so 
                            -- we have to ineract him with the inerts again because 
@@ -382,54 +453,56 @@ spontaneousSolveStage workItem inerts
                    -> return $ SR { sr_new_work   = emptyWorkList 
                                   , sr_inerts     = inerts `extendInertSet` workItem' 
                                   , sr_stop       = Stop } }
+--} 
 
 -- @trySpontaneousSolve wi@ solves equalities where one side is a
 -- touchable unification variable. Returns:
 --   * Nothing if we were not able to solve it
 --   * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
 --                 See Note [Touchables and givens] 
-trySpontaneousSolve :: WorkItem -> TcS (Maybe SWorkItem)
-trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) 
+-- Note, just passing the inerts through for the skolem equivalence classes
+trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList)
+trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts 
   | Just tv2 <- tcGetTyVar_maybe xi
   = do { tch1 <- isTouchableMetaTyVar tv1
        ; tch2 <- isTouchableMetaTyVar tv2
        ; case (tch1, tch2) of
-           (True,  True)  -> trySpontaneousEqTwoWay cv gw tv1 tv2
-           (True,  False) -> trySpontaneousEqOneWay cv gw tv1 xi
+           (True,  True)  -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
+           (True,  False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
            (False, True)  | tyVarKind tv1 `isSubKind` tyVarKind tv2
-                          -> trySpontaneousEqOneWay cv gw tv2 (mkTyVarTy tv1)
+                          -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
           _ -> return Nothing }
   | otherwise
   = do { tch1 <- isTouchableMetaTyVar tv1
-       ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
+       ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
                  else return Nothing }
 
   -- No need for 
   --      trySpontaneousSolve (CFunEqCan ...) = ...
   -- See Note [No touchables as FunEq RHS] in TcSMonad
-trySpontaneousSolve _ = return Nothing 
+trySpontaneousSolve _ = return Nothing 
 
 ----------------
-trySpontaneousEqOneWay :: CoVar -> CtFlavor -> TcTyVar -> Xi
-                       -> TcS (Maybe SWorkItem)
+trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
+                       -> TcS (Maybe SWorkList)
 -- tv is a MetaTyVar, not untouchable
 -- Precondition: kind(xi) is a sub-kind of kind(tv)
-trySpontaneousEqOneWay cv gw tv xi     
+trySpontaneousEqOneWay inerts cv gw tv xi      
   | not (isSigTyVar tv) || isTyVarTy xi
-  = solveWithIdentity cv gw tv xi
+  = solveWithIdentity inerts cv gw tv xi
   | otherwise
   = return Nothing
 
 ----------------
-trySpontaneousEqTwoWay :: CoVar -> CtFlavor -> TcTyVar -> TcTyVar
-                       -> TcS (Maybe SWorkItem)
+trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
+                       -> TcS (Maybe SWorkList)
 -- Both tyvars are *touchable* MetaTyvars
 -- By the CTyEqCan invariant, k2 `isSubKind` k1
-trySpontaneousEqTwoWay cv gw tv1 tv2
+trySpontaneousEqTwoWay inerts cv gw tv1 tv2
   | k1 `eqKind` k2
-  , nicer_to_update_tv2 = solveWithIdentity cv gw tv2 (mkTyVarTy tv1)
+  , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1)
   | otherwise           = ASSERT( k2 `isSubKind` k1 )
-                          solveWithIdentity cv gw tv1 (mkTyVarTy tv2)
+                          solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
   where
     k1 = tyVarKind tv1
     k2 = tyVarKind tv2
@@ -478,53 +551,166 @@ all about unifying or spontaneously solving (F xis ~ alpha) by unification.
 
 \begin{code}
 ----------------
-solveWithIdentity :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS (Maybe SWorkItem)
+solveWithIdentity :: InertSet 
+                  -> CoVar -> CtFlavor -> TcTyVar -> Xi 
+                  -> TcS (Maybe SWorkList)
 -- Solve with the identity coercion 
 -- Precondition: kind(xi) is a sub-kind of kind(tv)
 -- See [New Wanted Superclass Work] to see why we do this for *given* as well
-solveWithIdentity cv gw tv xi 
-  | tv `elemVarSet` tyVarsOfUnflattenedType xi 
-                           -- Beware of Note [Loopy spontaneous solving] 
-                    -- Can't spontaneously solve loopy equalities
-                    -- though they are not a type error 
-  = return Nothing 
-  | not (isGiven gw) -- Wanted or Derived 
-  = do { traceTcS "Sneaky unification:" $ 
-         vcat [text "Coercion variable:  " <+> ppr gw, 
-               text "Coercion:           " <+> pprEq (mkTyVarTy tv) xi,
-               text "Left  Kind is     : " <+> ppr (typeKind (mkTyVarTy tv)),
-               text "Right Kind is     : " <+> ppr (typeKind xi)
-              ]
-       ; setWantedTyBind tv xi                  -- Set tv := xi
-       ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi  
-                                                -- Create new given with identity evidence
-
-       ; case gw of 
-           Wanted  {} -> setWantedCoBind  cv xi 
-           Derived {} -> setDerivedCoBind cv xi 
-           _          -> pprPanic "Can't spontaneously solve *given*" empty 
+solveWithIdentity inerts cv gw tv xi 
+  | not (isGiven gw)
+  = do { m <- passOccursCheck inerts tv xi 
+       ; case m of 
+           Nothing -> return Nothing 
+           Just (xi_unflat,coi) -- coi : xi_unflat ~ xi  
+               -> do { traceTcS "Sneaky unification:" $ 
+                       vcat [text "Coercion variable:  " <+> ppr gw, 
+                             text "Coercion:           " <+> pprEq (mkTyVarTy tv) xi,
+                             text "Left  Kind is     : " <+> ppr (typeKind (mkTyVarTy tv)),
+                             text "Right Kind is     : " <+> ppr (typeKind xi)
+                            ]
+                     ; setWantedTyBind tv xi_unflat        -- Set tv := xi_unflat
+                     ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
+                     ; let flav = mkGivenFlavor gw UnkSkol 
+                     ; (cts, co) <- case coi of 
+                         ACo co  -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
+                                       ; return (can_eqs, co) }
+                         IdCo co -> return $ 
+                                    (singleCCan (CTyEqCan { cc_id = cv_given 
+                                                          , cc_flavor = mkGivenFlavor gw UnkSkol
+                                                          , cc_tyvar = tv, cc_rhs = xi }
+                                                          -- xi, *not* xi_unflat! 
+                                                ), co)
+                     ; case gw of 
+                         Wanted  {} -> setWantedCoBind  cv co
+                         Derived {} -> setDerivedCoBind cv co 
+                         _          -> pprPanic "Can't spontaneously solve *given*" empty 
 
-       ; let solved = CTyEqCan { cc_id = cv_given
-                               , cc_flavor = mkGivenFlavor gw UnkSkol
-                               , cc_tyvar = tv, cc_rhs = 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 solved) }
-  | otherwise        -- Given 
+                     ; return (Just cts) } 
+       }
+  | otherwise 
   = return Nothing 
 
-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 
+
+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. 
+--} 
+
+
+
 \end{code}
 
 
@@ -586,13 +772,14 @@ interactWithInertsStage workItem inert
                  , sr_new_work = emptyCCan
                  , sr_stop     = ContinueWith workItem }
 
+
     interactNext :: StageResult -> AtomicInert -> TcS StageResult 
     interactNext it inert  
       | ContinueWith workItem <- sr_stop it
         = do { ir <- interactWithInert inert workItem 
              ; let inerts = sr_inerts it 
              ; return $ SR { sr_inerts   = if ir_inert_action ir == KeepInert
-                                           then inerts `extendInertSet` inert
+                                           then inerts `updInertSet` inert
                                            else inerts
                            , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
                            , sr_stop     = ir_stop ir } }
@@ -600,7 +787,7 @@ interactWithInertsStage workItem inert
     
                              
     itrAddInert :: AtomicInert -> StageResult -> StageResult
-    itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `extendInertSet` inert }
+    itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert }
 
 -- Do a single interaction of two constraints.
 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
@@ -766,21 +953,14 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
   where
     lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) 
 
-doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) 
+doInteractWithInert 
+           inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) 
            workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
 -- Check for matching LHS 
   | fl1 `canRewrite` fl2 && tv1 == tv2 
   = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) 
        ; mkIRStop KeepInert cans } 
 
-{-
-  | fl1 `canRewrite` fl2                       -- If at all possible, keep the inert, 
-  , Just tv1_rhs <- tcGetTyVar_maybe xi1       -- special case of inert a~b
-  , tv1_rhs == tv2
-  = do { cans <- rewriteEqLHS (mkSymCoercion (mkCoVarCoercion cv1), mkTyVarTy tv1) 
-                              (cv2,fl2,xi2) 
-       ; mkIRStop KeepInert cans } 
--}
   | fl2 `canRewrite` fl1 && tv1 == tv2 
   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) 
        ; mkIRContinue workItem DropInert cans } 
@@ -792,6 +972,16 @@ doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc
   | 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. 
+
+  | not $ isGiven fl1,                  -- The inert is wanted or derived
+    isMetaTyVar tv1,                    -- and has a unification variable lhs
+    FlatSkol {} <- tcTyVarDetails tv2,  -- And workitem is a flatten skolem equality
+    Just tv2'   <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2' 
+  = mkIRContinue workItem DropInert (singletonWorkList inert)
 
 
 -- Fall-through case for all other cases
index 84fb1b8..b31a4cc 100644 (file)
@@ -497,12 +497,12 @@ zonkTcTypeCarefully ty
       | otherwise
       = ASSERT( isTcTyVar tv )
        case tcTyVarDetails tv of
-         SkolemTv {}  -> return (TyVarTy tv)
+         SkolemTv {}    -> return (TyVarTy tv)
          FlatSkol ty  -> zonkType (zonk_tv env_tvs) ty
-         MetaTv _ ref -> do { cts <- readMutVar ref
-                            ; case cts of    
-                                Flexi       -> return (TyVarTy tv)
-                                Indirect ty -> zonkType (zonk_tv env_tvs) ty }
+         MetaTv _ ref   -> do { cts <- readMutVar ref
+                              ; case cts of    
+                                  Flexi       -> return (TyVarTy tv)
+                                  Indirect ty -> zonkType (zonk_tv env_tvs) ty }
 
 zonkTcType :: TcType -> TcM TcType
 -- Simply look through all Flexis
@@ -513,12 +513,12 @@ zonkTcTyVar :: TcTyVar -> TcM TcType
 zonkTcTyVar tv
   = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
-      SkolemTv {}  -> return (TyVarTy tv)
+      SkolemTv {}    -> return (TyVarTy tv)
       FlatSkol ty  -> zonkTcType ty
-      MetaTv _ ref -> do { cts <- readMutVar ref
-                        ; case cts of    
-                            Flexi       -> return (TyVarTy tv)
-                            Indirect ty -> zonkTcType ty }
+      MetaTv _ ref   -> do { cts <- readMutVar ref
+                          ; case cts of    
+                              Flexi       -> return (TyVarTy tv)
+                              Indirect ty -> zonkTcType ty }
 
 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
 -- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
@@ -526,12 +526,12 @@ zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
   where
     zonk_tv tv 
       = case tcTyVarDetails tv of
-         SkolemTv {}  -> return (TyVarTy tv)
-         FlatSkol ty  -> zonkType zonk_tv ty
-         MetaTv _ ref -> do { cts <- readMutVar ref
-                            ; case cts of    
-                                Flexi       -> zonk_flexi tv
-                                Indirect ty -> zonkType zonk_tv ty }
+         SkolemTv {}    -> return (TyVarTy tv)
+         FlatSkol ty    -> zonkType zonk_tv ty
+         MetaTv _ ref   -> do { cts <- readMutVar ref
+                              ; case cts of    
+                                  Flexi       -> zonk_flexi tv
+                                  Indirect ty -> zonkType zonk_tv ty }
     zonk_flexi tv
       = case lookupTyVar subst tv of
           Just ty -> zonkType zonk_tv ty
@@ -750,12 +750,12 @@ mkZonkTcTyVar :: (TcTyVar -> TcM Type)    -- What to do for an unbound mutable var
 mkZonkTcTyVar unbound_var_fn tyvar 
   = ASSERT( isTcTyVar tyvar )
     case tcTyVarDetails tyvar of
-      SkolemTv {}  -> return (TyVarTy tyvar)
-      FlatSkol ty  -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
-      MetaTv _ ref -> do { cts <- readMutVar ref
-                        ; case cts of    
-                            Flexi       -> unbound_var_fn tyvar  
-                            Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
+      SkolemTv {}    -> return (TyVarTy tyvar)
+      FlatSkol ty    -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
+      MetaTv _ ref   -> do { cts <- readMutVar ref
+                          ; case cts of    
+                              Flexi       -> unbound_var_fn tyvar  
+                              Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
 
 -- Zonk the kind of a non-TC tyvar in case it is a coercion variable 
 -- (their kind contains types).
index 4965a93..c986811 100644 (file)
@@ -35,6 +35,8 @@ module TcSMonad (
 
 
     newFlattenSkolemTy,                         -- Flatten skolems 
+    zonkFlattenedType, 
+
 
     instDFunTypes,                              -- Instantiation
     instDFunConstraints,                        
@@ -63,7 +65,6 @@ module TcSMonad (
 
 import HscTypes
 import BasicTypes 
-import Type
 
 import Inst
 import InstEnv 
@@ -83,6 +84,8 @@ import DynFlags
 import Coercion
 import Class
 import TyCon
+import TypeRep 
+
 import Name
 import Var
 import Outputable
@@ -570,9 +573,30 @@ newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
         newFlattenSkolemTyVar ty
             = wrapTcS $ do { uniq <- TcM.newUnique
                            ; let name = mkSysTvName uniq (fsLit "f")
-                           ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty)
+                           ; return $ 
+                             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 
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
index dcc51ef..b49dbff 100644 (file)
@@ -274,17 +274,18 @@ TcBinds.tcInstSig, and its use_skols parameter.
 data TcTyVarDetails
   = SkolemTv SkolemInfo          -- A skolem constant
 
-  | FlatSkol TcType      -- The "skolem" obtained by flattening during
-                         -- constraint simplification
+  | FlatSkol TcType      
+           -- The "skolem" obtained by flattening during
+          -- constraint simplification
     
-                          -- In comments we will use the notation alpha[flat = ty]
-                          -- to represent a flattening skolem variable alpha
-                          -- identified with type ty.
-
+           -- In comments we will use the notation alpha[flat = ty]
+           -- to represent a flattening skolem variable alpha
+           -- identified with type ty.
+          
   | MetaTv MetaInfo (IORef MetaDetails)
 
 data MetaDetails
-  = Flexi      -- Flexi type variables unify to become Indirects  
+  = Flexi  -- Flexi type variables unify to become Indirects  
   | Indirect TcType
 
 data MetaInfo 
@@ -405,7 +406,7 @@ kind_var_occ = mkOccName tvName "k"
 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 -- For debugging
 pprTcTyVarDetails (SkolemTv _)         = ptext (sLit "sk")
-pprTcTyVarDetails (FlatSkol _)         = ptext (sLit "fsk")
+pprTcTyVarDetails (FlatSkol {})        = ptext (sLit "fsk")
 pprTcTyVarDetails (MetaTv TauTv _)     = ptext (sLit "tau")
 pprTcTyVarDetails (MetaTv (SigTv _) _) = ptext (sLit "sig")
 
@@ -431,7 +432,7 @@ pprSkolTvBinding tv
     quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
   where
     ppr_details (SkolemTv info)      = ppr_skol info
-    ppr_details (FlatSkol _)        = ptext (sLit "is a flattening type variable")
+    ppr_details (FlatSkol {})       = ptext (sLit "is a flattening type variable")
     ppr_details (MetaTv TauTv _)     = ptext (sLit "is a meta type variable")
     ppr_details (MetaTv (SigTv n) _) = ptext (sLit "is bound by the type signature for") <+> quotes (ppr n)
 
index 0fd7264..d73869f 100644 (file)
@@ -889,9 +889,8 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
 --    (checkTauTvUpdate tv ty)
 -- We are about to update the TauTv tv with ty.
 -- Check (a) that tv doesn't occur in ty (occurs check)
---       (b) that ty is a monotype
---      (c) that kind(ty) is a sub-kind of kind(tv)
---       (d) that ty does not contain any type families, see Note [SHARING]
+--      (b) that kind(ty) is a sub-kind of kind(tv)
+--       (c) that ty does not contain any type families, see Note [Type family sharing]
 -- 
 -- We have two possible outcomes:
 -- (1) Return the type to update the type variable with, 
@@ -914,8 +913,10 @@ checkTauTvUpdate tv ty
          then return (Just ty')
          else return Nothing }
   where ok :: TcType -> Bool 
-        -- Check that tv is not among the free variables of 
-        -- the type and that the type is type-family-free. 
+        -- 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 
@@ -929,7 +930,7 @@ checkTauTvUpdate tv ty
 
 \end{code}
 
-Note [SHARING]
+Note [Type family sharing]
 ~~~~~~~~~~~~~~ 
 We must avoid eagerly unifying type variables to types that contain function symbols, 
 because this may lead to loss of sharing, and in turn, in very poor performance of the