X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSMonad.lhs;h=240abc9cb6fda51d74479bc93657606708874967;hb=44674ca1081895c95e04707d74779d3f887c430e;hp=26f52d9fa49b930a9d9b1f4b898d5f7be706e2e1;hpb=5231445e104fa0227978909b47066ed1f012d325;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 26f52d9..240abc9 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -4,12 +4,12 @@ module TcSMonad (
 
        -- Canonical constraints
     CanonicalCts, emptyCCan, andCCan, andCCans, 
-    singleCCan, extendCCans, isEmptyCCan,
+    singleCCan, extendCCans, isEmptyCCan, isEqCCan, 
     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals,
     mkWantedConstraints, deCanonicaliseWanted, 
     makeGivens, makeSolved,
 
-    CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, 
+    CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, canSolve,
     combineCtLoc, mkGivenFlavor,
 
     TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0,  -- Basic functionality 
@@ -100,7 +100,6 @@ import FunDeps
 
 import TcRnTypes
 
-import Control.Monad
 import Data.IORef
 \end{code}
 
@@ -142,8 +141,8 @@ data CanonicalCt
   | CTyEqCan {  -- tv ~ xi	(recall xi means function free)
        -- Invariant: 
        --   * tv not in tvs(xi)   (occurs check)
-       --   * If tv is a MetaTyVar, then typeKind xi <: typeKind tv 
-       --              a skolem,    then typeKind xi =  typeKind tv 
+       --   * If constraint is given then typeKind xi ==  typeKind tv 
+       --                See Note [Spontaneous solving and kind compatibility] 
       cc_id     :: EvVar, 
       cc_flavor :: CtFlavor, 
       cc_tyvar :: TcTyVar, 
@@ -154,7 +153,8 @@ data CanonicalCt
                  -- Invariant: * isSynFamilyTyCon cc_fun 
                  --            * cc_rhs is not a touchable unification variable 
                  --                   See Note [No touchables as FunEq RHS]
-                 --            * typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
+                 --            * If constraint is given then 
+                 --                 typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs
       cc_id     :: EvVar,
       cc_flavor :: CtFlavor, 
       cc_fun    :: TyCon,	-- A type function
@@ -254,6 +254,12 @@ emptyCCan = emptyBag
 
 isEmptyCCan :: CanonicalCts -> Bool
 isEmptyCCan = isEmptyBag
+
+isEqCCan :: CanonicalCt -> Bool 
+isEqCCan (CTyEqCan {})  = True 
+isEqCCan (CFunEqCan {}) = True 
+isEqCCan _              = False 
+
 \end{code}
 
 %************************************************************************
@@ -289,14 +295,25 @@ isDerived :: CtFlavor -> Bool
 isDerived (Derived {}) = True
 isDerived _            = False
 
+canSolve :: CtFlavor -> CtFlavor -> Bool 
+-- canSolve ctid1 ctid2 
+-- The constraint ctid1 can be used to solve ctid2 
+-- "to solve" means a reaction where the active parts of the two constraints match.
+--  active(F xis ~ xi) = F xis 
+--  active(tv ~ xi)    = tv 
+--  active(D xis)      = D xis 
+--  active(IP nm ty)   = nm 
+-----------------------------------------
+canSolve (Given {})   _            = True 
+canSolve (Derived {}) (Wanted {})  = True 
+canSolve (Derived {}) (Derived {}) = True 
+canSolve (Wanted {})  (Wanted {})  = True
+canSolve _ _ = False
+
 canRewrite :: CtFlavor -> CtFlavor -> Bool 
 -- canRewrite ctid1 ctid2 
--- The constraint ctid1 can be used to rewrite ctid2 
-canRewrite (Given {})   _            = True 
-canRewrite (Derived {}) (Wanted {})  = True 
-canRewrite (Derived {}) (Derived {}) = True 
-canRewrite (Wanted {})  (Wanted {})  = True
-canRewrite _ _ = False
+-- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
+canRewrite = canSolve 
 
 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
 -- Precondition: At least one of them should be wanted 
@@ -567,40 +584,58 @@ pprEq :: TcType -> TcType -> SDoc
 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
 
 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
--- is touchable variable!
 isTouchableMetaTyVar tv 
-  | isMetaTyVar tv = do { untch <- getUntouchables
-                        ; return (inTouchableRange untch tv) }
-  | otherwise      = return False
+  = case tcTyVarDetails tv of
+      MetaTv TcsTv _ -> return True	-- See Note [Touchable meta type variables]
+      MetaTv {}      -> do { untch <- getUntouchables
+                           ; return (inTouchableRange untch tv) }
+      _              -> return False
+\end{code}
+
+Note [Touchable meta type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Meta type variables allocated *by the constraint solver itself* are always
+touchable.  Example: 
+   instance C a b => D [a] where...
+if we use this instance declaration we "make up" a fresh meta type
+variable for 'b', which we must later guess.  (Perhaps C has a
+functional dependency.)  But since we aren't in the constraint *generator*
+we can't allocate a Unique in the touchable range for this implication
+constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
 
 
+\begin{code}
 -- Flatten skolems
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 newFlattenSkolemTy :: TcType -> TcS TcType
 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
-  where newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
-        newFlattenSkolemTyVar ty
-            = wrapTcS $ do { uniq <- TcM.newUnique
-                           ; let name = mkSysTvName uniq (fsLit "f")
-                           ; return $ 
-                             mkTcTyVar name (typeKind ty) (FlatSkol ty) 
-                           }
+
+newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
+newFlattenSkolemTyVar ty
+  = wrapTcS $ do { uniq <- TcM.newUnique
+                 ; let name = mkSysTvName uniq (fsLit "f")
+                 ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) }
 
 -- Instantiations 
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
-instDFunTypes mb_inst_tys = 
-  let inst_tv :: Either TyVar TcType -> TcS Type
-      inst_tv (Left tv)  = wrapTcS $ TcM.tcInstTyVar tv >>= return . mkTyVarTy
-      inst_tv (Right ty) = return ty 
-  in mapM inst_tv mb_inst_tys
-
+instDFunTypes mb_inst_tys 
+  = mapM inst_tv mb_inst_tys
+  where
+    inst_tv :: Either TyVar TcType -> TcS Type
+    inst_tv (Left tv)  = mkTyVarTy <$> newFlexiTcS tv
+    inst_tv (Right ty) = return ty 
 
 instDFunConstraints :: TcThetaType -> TcS [EvVar] 
 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 
 
+newFlexiTcS :: TyVar -> TcS TcTyVar
+-- Make a TcsTv meta tyvar; it is always touchable,
+-- but we are supposed to guess its instantiation
+-- See Note [Touchable meta type variables]
+newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv
 
 -- Superclasses and recursive dictionaries 
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -801,11 +836,13 @@ mkWantedFunDepEqns loc eqns
   where
     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
     to_work_item ((qtvs, pairs), _, _)
-      = do { (_, _, tenv) <- wrapTcS $ TcM.tcInstTyVars (varSetElems qtvs)
-           ; mapM (do_one tenv) pairs }
+      = do { let tvs = varSetElems qtvs
+           ; tvs' <- mapM newFlexiTcS tvs
+           ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
+           ; mapM (do_one subst) pairs }
 
-    do_one tenv (ty1, ty2) = do { let sty1 = substTy tenv ty1 
-                                      sty2 = substTy tenv ty2 
+    do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1 
+                                       sty2 = substTy subst ty2 
                                 ; ev <- newWantedCoVar sty1 sty2
                                 ; return (WantedEvVar ev loc) }