Fix kind quantification (again)
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 2 May 2013 16:28:20 +0000 (17:28 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 3 May 2013 06:44:03 +0000 (07:44 +0100)
We simply weren't quantifying kind variables at the points we
were claiming.  In paritcular, in
     forall (a:k). blah
we quantify the 'k' around the 'forall a', provided k isn't
already in scope

compiler/hsSyn/HsTypes.lhs
compiler/rename/RnTypes.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSMonad.lhs

index d0d9e1a..a95630d 100644 (file)
@@ -152,8 +152,8 @@ hsQTvBndrs :: LHsTyVarBndrs name -> [LHsTyVarBndr name]
 hsQTvBndrs = hsq_tvs
 
 data HsWithBndrs thing
-  = HsWB { hswb_cts :: thing           -- Main payload (type or list of types)
-         , hswb_kvs :: [Name]         -- Kind vars
+  = HsWB { hswb_cts :: thing         -- Main payload (type or list of types)
+         , hswb_kvs :: [Name]        -- Kind vars
          , hswb_tvs :: [Name]        -- Type vars
     }                  
   deriving (Data, Typeable)
@@ -280,7 +280,7 @@ Note [HsForAllTy tyvar binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 After parsing:
   * Implicit => empty
-    Explicit => the varibles the user wrote
+    Explicit => the variables the user wrote
 
 After renaming
   * Implicit => the *type* variables free in the type
index 95bdcb4..a230701 100644 (file)
@@ -1024,19 +1024,17 @@ extract_lty (L _ ty) acc
 extract_hs_tv_bndrs :: LHsTyVarBndrs RdrName -> FreeKiTyVars
                     -> FreeKiTyVars -> FreeKiTyVars
 extract_hs_tv_bndrs (HsQTvs { hsq_tvs = tvs }) 
-                    acc@(acc_kvs, acc_tvs)   -- Note accumulator comes first
+                    (acc_kvs, acc_tvs)   -- Note accumulator comes first
                     (body_kvs, body_tvs)
   | null tvs
   = (body_kvs ++ acc_kvs, body_tvs ++ acc_tvs)
   | otherwise
-  = (outer_kvs ++ body_kvs,
-     outer_tvs ++ filterOut (`elem` local_tvs) body_tvs)
+  = (acc_kvs ++ filterOut (`elem` local_kvs) body_kvs,
+     acc_tvs ++ filterOut (`elem` local_tvs) body_tvs)
   where
     local_tvs = map hsLTyVarName tvs
-        -- Currently we don't have a syntax to explicitly bind 
-        -- kind variables, so these are all type variables
-
-    (outer_kvs, outer_tvs) = foldr extract_lkind acc [k | L _ (KindedTyVar _ k) <- tvs]
+    (_, local_kvs) = foldr extract_lty ([], []) [k | L _ (KindedTyVar _ k) <- tvs]
+       -- These kind variables are bound here if not bound further out
 
 extract_tv :: RdrName -> FreeKiTyVars -> FreeKiTyVars
 extract_tv tv acc
index 7bfa518..703ab95 100644 (file)
@@ -195,7 +195,8 @@ tcHsInstHead :: UserTypeCtxt -> LHsType Name -> TcM ([TyVar], ThetaType, Class,
 tcHsInstHead user_ctxt lhs_ty@(L loc hs_ty)
   = setSrcSpan loc $    -- The "In the type..." context comes from the caller
     do { inst_ty <- tc_inst_head hs_ty
-       ; kvs     <- kindGeneralize (tyVarsOfType inst_ty) []
+       ; kvs     <- zonkTcTypeAndFV inst_ty
+       ; kvs     <- kindGeneralize kvs []
        ; inst_ty <- zonkTcType (mkForAllTys kvs inst_ty)
        ; checkValidInstance user_ctxt lhs_ty inst_ty }
 
@@ -304,7 +305,10 @@ tcCheckHsTypeAndGen :: HsType Name -> Kind -> TcM Type
 -- The result is not necessarily zonked, and has not been checked for validity
 tcCheckHsTypeAndGen hs_ty kind
   = do { ty  <- tc_hs_type hs_ty (EK kind expectedKindMsg)
-       ; kvs <- kindGeneralize (tyVarsOfType ty) []
+       ; traceTc "tcCheckHsTypeAndGen" (ppr hs_ty)
+       ; traceTc "tcCheckHsTypeAndGen" (ppr ty)
+       ; kvs <- zonkTcTypeAndFV ty 
+       ; kvs <- kindGeneralize kvs []
        ; return (mkForAllTys kvs ty) }
 \end{code}
 
@@ -895,22 +899,25 @@ kcHsTyVarBndrs full_kind_sig (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thin
                Just thing       -> pprPanic "check_in_scope" (ppr thing)
            ; return (n, kind) }
 
-tcScopedKindVars :: [Name] -> TcM a -> TcM a
--- Given some tyvar binders like [a (b :: k -> *) (c :: k)]
--- bind each scoped kind variable (k in this case) to a fresh
--- kind skolem variable
-tcScopedKindVars kv_ns thing_inside 
-  = tcExtendTyVarEnv (map mkKindSigVar kv_ns) thing_inside
-
 tcHsTyVarBndrs :: LHsTyVarBndrs Name 
               -> ([TcTyVar] -> TcM r)
               -> TcM r
--- Bind the type variables to skolems, each with a meta-kind variable kind
-tcHsTyVarBndrs (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
-  = tcScopedKindVars kvs $
-    do { tvs <- mapM tcHsTyVarBndr hs_tvs
-       ; traceTc "tcHsTyVarBndrs" (ppr hs_tvs $$ ppr tvs)
-       ; tcExtendTyVarEnv tvs (thing_inside tvs) }
+-- Bind the kind variables to fresh skolem variables
+-- and type variables to skolems, each with a meta-kind variable kind
+tcHsTyVarBndrs (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
+  = do { let kvs = map mkKindSigVar kv_ns
+       ; tcExtendTyVarEnv kvs $ do 
+       { tvs <- mapM tcHsTyVarBndr hs_tvs
+       ; traceTc "tcHsTyVarBndrs {" (vcat [ text "Hs kind vars:" <+> ppr kv_ns
+                                        , text "Hs type vars:" <+> ppr hs_tvs
+                                        , text "Kind vars:" <+> ppr kvs
+                                        , text "Type vars:" <+> ppr tvs ])
+       ; res <- tcExtendTyVarEnv tvs (thing_inside (kvs ++ tvs))
+       ; traceTc "tcHsTyVarBndrs }" (vcat [ text "Hs kind vars:" <+> ppr kv_ns
+                                        , text "Hs type vars:" <+> ppr hs_tvs
+                                        , text "Kind vars:" <+> ppr kvs
+                                        , text "Type vars:" <+> ppr tvs ])
+       ; return res  } }
 
 tcHsTyVarBndr :: LHsTyVarBndr Name -> TcM TcTyVar
 -- Return a type variable 
index 0a68584..39955e3 100644 (file)
@@ -1397,7 +1397,7 @@ doTopReact inerts workItem
        ; case workItem of
           CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis
                    , cc_loc = d }
-             -> doTopReactDict inerts workItem fl cls xis d
+             -> doTopReactDict inerts fl cls xis d
 
           CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args
                     , cc_rhs = xi, cc_loc = d }
@@ -1407,35 +1407,36 @@ doTopReact inerts workItem
                 return NoTopInt  }
 
 --------------------
-doTopReactDict :: InertSet -> WorkItem -> CtEvidence -> Class -> [Xi]
+doTopReactDict :: InertSet -> CtEvidence -> Class -> [Xi]
                -> CtLoc -> TcS TopInteractResult
-doTopReactDict inerts workItem fl cls xis loc
-  = do { instEnvs <- getInstEnvs 
+doTopReactDict inerts fl cls xis loc
+  = do {    -- Try functional dependencies with the instance environment
+         instEnvs <- getInstEnvs 
        ; let pred = mkClassPred cls xis
              fd_eqns = improveFromInstEnv instEnvs (pred, arising_sdoc)
-             
        ; fd_work <- rewriteWithFunDeps fd_eqns loc
-       ; if not (null fd_work) then
-            do { updWorkListTcS (extendWorkListEqs fd_work)
-               ; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
-                                   , tir_new_item = ContinueWith workItem } }
-         else if not (isWanted fl) then 
+       ; unless (null fd_work) (updWorkListTcS (extendWorkListEqs fd_work))
+       
+       ; if not (isWanted fl) then 
             return NoTopInt
-         else do
+         else 
 
-       { solved_dicts <- getTcSInerts >>= (return . inert_solved_dicts)
-       ; case lookupSolvedDict solved_dicts pred of {
+            -- Even if there *were* some functional dependencies against the
+            -- instance environment, there might be a unique match, and if 
+            -- so we should get on and solve it. See Note [Wierd fundeps]
+
+         case lookupSolvedDict inerts pred of {
             Just ev -> do { setEvBind dict_id (ctEvTerm ev); 
                           ; return $ 
                             SomeTopInt { tir_rule = "Dict/Top (cached)" 
                                        , tir_new_item = Stop } } ;
             Nothing -> do
 
-      { lkup_inst_res  <- matchClassInst inerts cls xis loc
+      { lkup_inst_res <- matchClassInst inerts cls xis loc
       ; case lkup_inst_res of
            GenInst wtvs ev_term -> do { addSolvedDict fl 
                                       ; doSolveFromInstance wtvs ev_term }
-           NoInstance -> return NoTopInt } } } }
+           NoInstance -> return NoTopInt } } }
    where 
      arising_sdoc = pprArisingAt loc
      dict_id = ctEvId fl
@@ -1592,6 +1593,25 @@ and now we need improvement between that derived superclass an the Given (L a b)
 Test typecheck/should_fail/FDsFromGivens also shows why it's a good idea to 
 emit Derived FDs for givens as well. 
 
+Note [Weird fundeps]
+~~~~~~~~~~~~~~~~~~~~
+Consider   class Het a b | a -> b where
+              het :: m (f c) -> a -> m b
+
+          class GHet (a :: * -> *) (b :: * -> *) | a -> b
+          instance            GHet (K a) (K [a])
+          instance Het a b => GHet (K a) (K b)
+
+The two instances don't actually conflict on their fundeps,
+although it's pretty strange.  So they are both accepted. Now
+try   [W] GHet (K Int) (K Bool)
+This triggers fudeps from both instance decls; but it also 
+matches a *unique* instance decl, and we should go ahead and
+pick that one right now.  Otherwise, if we don't, it ends up 
+unsolved in the inert set and is reported as an error.
+
+Trac #7875 is a case in point.
+
 Note [Overriding implicit parameters]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
index 7ac66d0..09e307a 100644 (file)
@@ -51,9 +51,9 @@ module TcMType (
   -- Zonking
   zonkTcPredType, 
   skolemiseSigTv, skolemiseUnboundMetaTyVar,
-  zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, 
+  zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
-  zonkTcType, zonkTcTypes, zonkTcThetaType,
+  zonkTcType, zonkTcTypes, zonkTcThetaType, 
 
   zonkTcKind, defaultKindVarToStar,
   zonkEvVar, zonkWC, zonkId, zonkCt, zonkCts, zonkSkolemInfo,
@@ -504,6 +504,15 @@ tcGetGlobalTyVars
 -----------------  Type variables
 
 \begin{code}
+zonkTcTypeAndFV :: TcType -> TcM TyVarSet
+-- Zonk a type and take its free variables
+-- With kind polymorphism it can be essential to zonk *first*
+-- so that we find the right set of free variables.  Eg
+--    forall k1. forall (a:k2). a
+-- where k2:=k1 is in the substitution.  We don't want
+-- k2 to look free in this type!
+zonkTcTypeAndFV ty = do { ty <- zonkTcType ty; return (tyVarsOfType ty) }
+
 zonkTyVar :: TyVar -> TcM TcType
 -- Works on TyVars and TcTyVars
 zonkTyVar tv | isTcTyVar tv = zonkTcTyVar tv
index 14ec1ba..f6bb4b7 100644 (file)
@@ -896,18 +896,19 @@ lookupFlatEqn fam_ty
 lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
 -- Is this exact predicate type cached in the solved or canonicals of the InertSet
 lookupInInerts pty
-  = do { IS { inert_solved_dicts = solved, inert_cans = ics } <- getTcSInerts
-       ; case lookupSolvedDict solved pty of
+  = do { inerts <- getTcSInerts
+       ; case lookupSolvedDict inerts pty of
            Just ctev -> return (Just ctev)
-           Nothing   -> return (lookupInInertCans ics pty) }
+           Nothing   -> return (lookupInInertCans inerts pty) }
 
-lookupSolvedDict :: PredMap CtEvidence -> TcPredType -> Maybe CtEvidence
+lookupSolvedDict :: InertSet -> TcPredType -> Maybe CtEvidence
 -- Returns just if exactly this predicate type exists in the solved.
-lookupSolvedDict tm pty = lookupTM pty $ unPredMap tm
+lookupSolvedDict (IS { inert_solved_dicts = solved }) pty 
+  = lookupTM pty (unPredMap solved)
 
-lookupInInertCans :: InertCans -> TcPredType -> Maybe CtEvidence
+lookupInInertCans :: InertSet -> TcPredType -> Maybe CtEvidence
 -- Returns Just if exactly this pred type exists in the inert canonicals
-lookupInInertCans ics pty
+lookupInInertCans (IS { inert_cans = ics }) pty
   = case (classifyPredType pty) of
       ClassPred cls _ 
          -> lookupCCanMap cls (\ct -> ctEvPred ct `eqType` pty) (inert_dicts ics)
@@ -1160,6 +1161,7 @@ getTcSInertsRef = TcS (return . tcs_inerts)
 
 getTcSWorkListRef :: TcS (IORef WorkList) 
 getTcSWorkListRef = TcS (return . tcs_worklist) 
+
 getTcSInerts :: TcS InertSet 
 getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)