Merge branch 'master' into type-nats
authorIavor S. Diatchki <iavor.diatchki@gmail.com>
Mon, 17 Jan 2011 00:26:23 +0000 (16:26 -0800)
committerIavor S. Diatchki <iavor.diatchki@gmail.com>
Mon, 17 Jan 2011 00:26:23 +0000 (16:26 -0800)
Conflicts:
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSMonad.lhs

14 files changed:
1  2 
compiler/basicTypes/OccName.lhs
compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcHsSyn.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcSplice.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcUnify.lhs
compiler/types/FamInstEnv.lhs
compiler/types/Unify.lhs

Simple merge
Simple merge
Simple merge
Simple merge
Simple merge
@@@ -22,12 -24,9 +24,10 @@@ import InstEn
  import Class
  import TyCon
  import Name
 -
 +import PrelNames (typeNatClassName,lessThanEqualClassName,
 +                  addTyFamName, mulTyFamName, expTyFamName)
  import FunDeps
  
- import Control.Monad ( when ) 
  import Coercion
  import Outputable
  
@@@ -977,10 -917,9 +921,9 @@@ doInteractWithInert (CDictCan { cc_id 
    = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
         ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
  
 --- Class constraint and given equality: use the equality to rewrite
 +-- Implicit parameter and given equality: use the equality to rewrite
  -- the class constraint.
- doInteractWithInert _fdimprs 
-                     (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) 
+ doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi }) 
                      (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty }) 
    | ifl `canRewrite` wfl
    , tv `elemVarSet` tyVarsOfType ty 
@@@ -1088,72 -1021,21 +1025,109 @@@ doInteractWithInert (CTyEqCan { cc_id 
    = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) 
         ; mkIRContinue workItem DropInert rewritten_eq } 
  
+ doInteractWithInert (CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
+                     (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
+   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
+   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
+        ; mkIRStop KeepInert rewritten_frozen }
+ doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
+            workItem@(CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
+   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
+   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
+        ; mkIRContinue workItem DropInert rewritten_frozen }
  -- Fall-through case for all other situations
- doInteractWithInert _fdimprs _ workItem = noInteraction workItem
+ doInteractWithInert _ workItem = noInteraction workItem
++-- XXX: Do something with the derived.
++-- Derived example:
++--
++--   class (1 <= n) => C n where f :: ...
++--
++-- Using "f" generates a wanted "C n" constraint which, in turn,
++-- results in a derived "1 <= n" constraint.
++--
++-- This is not something that we need to solve but, rather, we can use
++-- this fact when solvoing other goals (wanteds).
++--
++-- Derived constraints may interact with assumptions (givens).
++-- For example, if we were working in a context where we knew that
++-- "n <= 1" (e.g., from a type signature), then we can generate another
++-- derived constraint: "n ~ 1".
 +
 +
 +numericReactionsStage :: SimplifierStage
 +numericReactionsStage workItem inert
 +  | isNumWork =
 +    if isWanted (cc_flavor workItem) then
 +        do (val,new) <- solveNumWanted grelevant wrelevant workItem
 +           return
 +            SR { sr_stop = case val of
 +                             Nothing -> Stop
 +                             Just v  -> ContinueWith v
 +               , sr_new_work = new
 +               , sr_inerts = inert
 +               }
 +    else do (val,ins,new) <- addNumGiven grelevant wrelevant workItem
 +            return
 +              SR { sr_stop = case val of
 +                               Nothing -> Stop
 +                               Just v  -> ContinueWith v
 +                 , sr_new_work = new
 +                 , sr_inerts = foldrBag (flip updInertSet) inert_residual ins
 +                 }
 +
-   where (grelevant, wrelevant, inert_residual) = getNumInerts inert
++  where (grelevant, drelevant, wrelevant, inert_residual) = getNumInerts inert
 +
 +        isNumWork = case workItem of
 +                      CFunEqCan { cc_fun   = f }  -> isNumFun f
 +                      CDictCan  { cc_class = c }  -> isNumClass c
 +                      _                           -> False
 +
 +numericReactionsStage workItem inert = return
 +  SR { sr_inerts    = inert
 +     , sr_new_work  = emptyBag
 +     , sr_stop      = ContinueWith workItem
 +     }
 +
 +-- Extract constraints which may interact with numeric predicates.
- getNumInerts :: InertSet -> (CanonicalCts, CanonicalCts, InertSet)
++getNumInerts :: InertSet -> (CanonicalCts, CanonicalCts, CanonicalCts, InertSet)
 +getNumInerts i =
-   let (gfuns, wfuns, other_funs) = partitionCCanMap isNumFun (inert_funeqs i)
-       (gcls,  wcls, other_cls)   = partitionCCanMap isNumClass (inert_dicts i)
++  let (gfuns, dfuns, wfuns, other_funs) =
++                                    partitionCCanMap isNumFun (inert_funeqs i)
++      (gcls, dcls, wcls, other_cls) =
++                                    partitionCCanMap isNumClass (inert_dicts i)
 +  in ( unionWorkLists gfuns gcls
++     , unionWorkLists dfuns dcls
 +     , unionWorkLists wfuns wcls
 +     , i { inert_funeqs = other_funs, inert_dicts = other_cls }
 +     )
 +
 +
 +isNumFun :: TyCon -> Bool
 +isNumFun tc = tyConName tc `elem` [ addTyFamName, mulTyFamName, expTyFamName ]
 +
 +-- Does not include 'TypeNat' (it does not interact with numeric predicates).
 +isNumClass :: Class -> Bool
 +isNumClass cls  = className cls == lessThanEqualClassName
 +
 +partitionCCanMap ::
-   Ord a => (a -> Bool) -> CCanMap a -> (CanonicalCts, CanonicalCts, CCanMap a)
++  Ord a => (a -> Bool) -> CCanMap a ->
++                          (CanonicalCts, CanonicalCts, CanonicalCts, CCanMap a)
 +partitionCCanMap p cmap =
 +  let (relw,not_relw) = Map.partitionWithKey (\k _ -> p k) (cts_wanted cmap)
-       (relg,not_relg) = Map.partitionWithKey (\k _ -> p k) (cts_givder cmap)
-   in ( unionManyBags (Map.elems relg)
-      , unionManyBags (Map.elems relw)
-      , cmap { cts_wanted = not_relw, cts_givder = not_relg }
++      (reld,not_reld) = Map.partitionWithKey (\k _ -> p k) (cts_derived cmap)
++      (relg,not_relg) = Map.partitionWithKey (\k _ -> p k) (cts_given  cmap)
++  in ( unionManyBags (Map.elems relg)   -- These our assumptions.
++     , unionManyBags (Map.elems reld)   -- These are facts implied by the goals.
++     , unionManyBags (Map.elems relw)   -- These are our goals.
++     , cmap { cts_wanted  = not_relw
++            , cts_given   = not_relg
++            , cts_derived = not_reld
++            }
 +     )
 +
  -------------------------
  -- Equational Rewriting 
  rewriteDict  :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
@@@ -89,7 -93,7 +93,8 @@@ import BasicType
  import SrcLoc
  import Outputable
  import FastString
 +import PrelNames (typeNatClassName, lessThanEqualClassName)
+ import Unique( Unique )
  import Bag
  
  import Control.Monad
@@@ -509,12 -506,12 +507,13 @@@ zonkTcTypeAndSubst :: TvSubst -> TcTyp
  zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
    where
      zonk_tv tv 
 -      = case tcTyVarDetails tv of
 +      = ASSERT ( isTcTyVar tv )
 +        case tcTyVarDetails tv of
-                 SkolemTv {}    -> return (TyVarTy tv)
-                 FlatSkol ty    -> zonkType zonk_tv ty
-                 MetaTv _ ref   -> do { cts <- readMutVar ref
-                              ; case cts of    
+           SkolemTv {}   -> return (TyVarTy tv)
+           RuntimeUnk {} -> 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
@@@ -36,15 -36,9 +36,10 @@@ module TcSMonad 
  
      setWantedTyBind,
  
-     newTcEvBindsTcS,
-  
-     getInstEnvs, getFamInstEnvs,                -- Getting the environments 
+     getInstEnvs, getFamInstEnvs,                -- Getting the environments
      getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
-     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors,
-     getTcSErrorsBag, FrozenError (..),
-     addErrorTcS,
-     ErrorKind(..),
 +    tcsLookupClass, tcsLookupTyCon,
+     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
  
      newFlattenSkolemTy,                         -- Flatten skolems 
  
@@@ -1144,3 -1182,19 +1183,19 @@@ that g isn't polymorphic enough; but th
  dealing with the (Num a) context arising from f's definition;
  we try to unify a with Int (to default it), but find that it's
  already been unified with the rigid variable from g's type sig
 -\end{code}
+ *********************************************************************************
+ *                                                                               * 
+ *                   Utility functions
+ *                                                                               *
+ *********************************************************************************
+ \begin{code}
+ newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar)
+ newFlatWanteds orig theta
+   = do { loc <- getCtLoc orig
+        ; evs <- newWantedEvVars theta
+        ; return (listToBag [EvVarX w loc | w <- evs]) }
++\end{code}
Simple merge
Simple merge
Simple merge
Simple merge
Simple merge