[project @ 2002-02-28 12:17:19 by simonpj]
authorsimonpj <unknown>
Thu, 28 Feb 2002 12:17:22 +0000 (12:17 +0000)
committersimonpj <unknown>
Thu, 28 Feb 2002 12:17:22 +0000 (12:17 +0000)
---------------------------------
Fix a rather obscure bug in tcGen
---------------------------------

This bug concerns deciding when a type variable "escapes",
and hence we can't generalise it.  Our new subsumption-checking
machinery for higher-ranked types requires a slightly
more general approach than I had before.  The main excitement
is in TcUnify.checkSigTyVars and its friends.

As usual, I moved functions around and cleaned things up a bit;
hence the multi-module commit.

12 files changed:
ghc/compiler/typecheck/TcBinds.lhs
ghc/compiler/typecheck/TcClassDcl.lhs
ghc/compiler/typecheck/TcEnv.lhs
ghc/compiler/typecheck/TcExpr.lhs
ghc/compiler/typecheck/TcForeign.lhs
ghc/compiler/typecheck/TcHsSyn.lhs
ghc/compiler/typecheck/TcInstDcls.lhs
ghc/compiler/typecheck/TcMType.lhs
ghc/compiler/typecheck/TcMatches.lhs
ghc/compiler/typecheck/TcPat.lhs
ghc/compiler/typecheck/TcType.lhs
ghc/compiler/typecheck/TcUnify.lhs

index 8dad853..b677fe9 100644 (file)
@@ -26,7 +26,7 @@ import Inst           ( LIE, emptyLIE, mkLIE, plusLIE, InstOrigin(..),
                          newDicts, instToId
                        )
 import TcEnv           ( tcExtendLocalValEnv, newLocalName )
-import TcUnify         ( unifyTauTyLists, checkSigTyVars, sigCtxt )
+import TcUnify         ( unifyTauTyLists, checkSigTyVarsWrt, sigCtxt )
 import TcSimplify      ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted, tcSimplifyToDicts )
 import TcMonoType      ( tcHsSigType, UserTypeCtxt(..), 
                          TcSigInfo(..), tcTySig, maybeSig, tcAddScopedTyVars
@@ -495,7 +495,7 @@ checkSigsTyVars sigs = mapTc_ check_one sigs
        tcAddErrCtxt (ptext SLIT("When checking the type signature for") 
                      <+> quotes (ppr id))                              $
        tcAddErrCtxtM (sigCtxt sig_tyvars sig_theta sig_tau)            $
-       checkSigTyVars sig_tyvars (idFreeTyVars id)
+       checkSigTyVarsWrt (idFreeTyVars id) sig_tyvars
 \end{code}
 
 @getTyVarsToGen@ decides what type variables to generalise over.
index a89895a..3f32e87 100644 (file)
@@ -25,8 +25,8 @@ import TcHsSyn                ( TcMonoBinds )
 
 import Inst            ( Inst, InstOrigin(..), LIE, emptyLIE, plusLIE, plusLIEs, 
                          instToId, newDicts, newMethod )
-import TcEnv           ( TyThingDetails(..), 
-                         tcLookupClass, tcExtendTyVarEnvForMeths, tcExtendGlobalTyVars,
+import TcEnv           ( TyThingDetails(..), tcExtendGlobalTyVars,
+                         tcLookupClass, tcExtendTyVarEnvForMeths, 
                          tcExtendLocalValEnv, tcExtendTyVarEnv
                        )
 import TcBinds         ( tcBindWithSigs, tcSpecSigs )
@@ -52,7 +52,6 @@ import NameEnv                ( NameEnv, lookupNameEnv, emptyNameEnv, unitNameEnv, plusNameEnv
 import NameSet         ( emptyNameSet )
 import Outputable
 import Var             ( TyVar )
-import VarSet          ( mkVarSet, emptyVarSet )
 import CmdLineOpts
 import ErrUtils                ( dumpIfSet )
 import Util            ( count, isSingleton, lengthIs, equalLength )
@@ -438,10 +437,10 @@ tcDefMeth clas tyvars binds_in prags op_item@(sel_id, DefMeth dm_name)
         (ptext SLIT("class") <+> ppr clas)
        clas_tyvars
         [this_dict]
-        insts_needed                           `thenTc` \ (const_lie, dict_binds) ->
+        insts_needed                   `thenTc` \ (const_lie, dict_binds) ->
 
        -- Simplification can do unification
-    checkSigTyVars clas_tyvars emptyVarSet     `thenTc` \ clas_tyvars' ->
+    checkSigTyVars clas_tyvars         `thenTc` \ clas_tyvars' ->
     
     let
         full_bind = AbsBinds
@@ -508,8 +507,9 @@ tcMethodBind clas origin inst_tyvars inst_tys inst_theta
     )                                                          `thenTc` \ meth_bind ->
      -- Check the bindings; first add inst_tyvars to the envt
      -- so that we don't quantify over them in nested places
-     -- The *caller* put the class/inst decl tyvars into the envt
-     tcExtendGlobalTyVars (mkVarSet inst_tyvars) 
+     -- The *caller* put the class/inst decl tyvars into the tyvar envt,
+     -- but not into the global tyvars, so that the call to checkSigTyVars below works ok
+     tcExtendGlobalTyVars inst_tyvars 
                    (tcAddErrCtxt (methodCtxt sel_id)           $
                     tcBindWithSigs NotTopLevel meth_bind 
                                    [sig_info] meth_prags NonRecursive 
@@ -531,9 +531,9 @@ tcMethodBind clas origin inst_tyvars inst_tys inst_theta
      -- ...and this is why the call to tcExtendGlobalTyVars must be here
      --    rather than in the caller
      tcAddErrCtxt (ptext SLIT("When checking the type of class method") 
-                  <+> quotes (ppr sel_id))                                     $
+                  <+> quotes (ppr sel_id))                             $
      tcAddErrCtxtM (sigCtxt inst_tyvars inst_theta (idType meth_id))   $
-     checkSigTyVars inst_tyvars emptyVarSet                                    `thenTc_` 
+     checkSigTyVars inst_tyvars                                                `thenTc_` 
 
      returnTc (binds `AndMonoBinds` prag_binds1 `AndMonoBinds` prag_binds2, 
               insts `plusLIE` prag_lie',
index 5dc8b8b..fdcd99f 100644 (file)
@@ -442,8 +442,8 @@ tcExtendLocalValEnv names_w_ids thing_inside
 
 \begin{code}
 tcExtendGlobalTyVars extra_global_tvs thing_inside
-  = tcGetEnv                                           `thenNF_Tc` \ env ->
-    tc_extend_gtvs (tcTyVars env) extra_global_tvs     `thenNF_Tc` \ gtvs' ->
+  = tcGetEnv                                                   `thenNF_Tc` \ env ->
+    tc_extend_gtvs (tcTyVars env) (mkVarSet extra_global_tvs)  `thenNF_Tc` \ gtvs' ->
     tcSetEnv (env {tcTyVars = gtvs'}) thing_inside
 
 tc_extend_gtvs gtvs extra_global_tvs
index 81614cb..252d995 100644 (file)
@@ -52,7 +52,7 @@ import DataCon                ( dataConFieldLabels, dataConSig,
 import Name            ( Name )
 import TyCon           ( TyCon, tyConTyVars, isAlgTyCon, tyConDataCons )
 import Subst           ( mkTopTyVarSubst, substTheta, substTy )
-import VarSet          ( elemVarSet )
+import VarSet          ( emptyVarSet, elemVarSet )
 import TysWiredIn      ( boolTy, mkListTy, mkPArrTy, listTyCon, parrTyCon )
 import PrelNames       ( cCallableClassName, 
                          cReturnableClassName, 
@@ -85,7 +85,9 @@ tcExpr expr expected_ty
   = tcMonoExpr expr expected_ty
 
   | otherwise
-  = tcGen expected_ty (tcMonoExpr expr)                `thenTc` \ (gen_fn, expr', lie) ->
+  = tcGen expected_ty emptyVarSet (
+       tcMonoExpr expr
+    )                                  `thenTc` \ (gen_fn, expr', lie) ->
     returnTc (gen_fn <$> expr', lie)
 \end{code}
 
@@ -129,12 +131,12 @@ tcMonoExpr (HsIPVar ip) res_ty
 \begin{code}
 tcMonoExpr in_expr@(ExprWithTySig expr poly_ty) res_ty
  = tcHsSigType ExprSigCtxt poly_ty     `thenTc` \ sig_tc_ty ->
-   tcAddErrCtxt (exprSigCtxt in_expr)  $
    tcExpr expr sig_tc_ty               `thenTc` \ (expr', lie1) ->
 
        -- Must instantiate the outer for-alls of sig_tc_ty
        -- else we risk instantiating a ? res_ty to a forall-type
        -- which breaks the invariant that tcMonoExpr only returns phi-types
+   tcAddErrCtxt (exprSigCtxt in_expr)  $
    tcInstCall SignatureOrigin sig_tc_ty        `thenNF_Tc` \ (inst_fn, lie2, inst_sig_ty) ->
    tcSub res_ty inst_sig_ty            `thenTc` \ (co_fn, lie3) ->
 
@@ -1011,7 +1013,7 @@ caseScrutCtxt expr
   = hang (ptext SLIT("In the scrutinee of a case expression:")) 4 (ppr expr)
 
 exprSigCtxt expr
-  = hang (ptext SLIT("In an expression with a type signature:"))
+  = hang (ptext SLIT("When checking the type signature of the expression:"))
         4 (ppr expr)
 
 listCtxt expr
index b5a2de9..c943b44 100644 (file)
@@ -26,7 +26,6 @@ import HsSyn          ( HsDecl(..), ForeignDecl(..), HsExpr(..),
 import RnHsSyn         ( RenamedHsDecl, RenamedForeignDecl )
 
 import TcMonad
-import TcEnv           ( newLocalName )
 import TcMonoType      ( tcHsSigType, UserTypeCtxt(..) )
 import TcHsSyn         ( TcMonoBinds, TypecheckedForeignDecl, TcForeignExportDecl )
 import TcExpr          ( tcExpr )                      
@@ -38,7 +37,7 @@ import PrimRep                ( getPrimRepSize, isFloatingRep )
 import Module          ( Module )
 import Type            ( typePrimRep )
 import OccName         ( mkForeignExportOcc )
-import Name            ( Name(..), NamedThing(..), mkGlobalName )
+import Name            ( NamedThing(..), mkGlobalName )
 import TcType          ( Type, tcSplitFunTys, tcSplitTyConApp_maybe,
                          tcSplitForAllTys, 
                          isFFIArgumentTy, isFFIImportResultTy, 
@@ -46,7 +45,7 @@ import TcType         ( Type, tcSplitFunTys, tcSplitTyConApp_maybe,
                          isFFIExternalTy, isFFIDynArgumentTy,
                          isFFIDynResultTy, isForeignPtrTy
                        )
-import ForeignCall     ( CCallSpec(..), CExportSpec(..), CCallTarget(..),
+import ForeignCall     ( CExportSpec(..), CCallTarget(..),
                          isDynamicTarget, isCasmTarget ) 
 import CStrings                ( CLabelString, isCLabelString )
 import PrelNames       ( hasKey, ioTyConKey )
index d691ab4..2d01c49 100644 (file)
@@ -48,8 +48,8 @@ import TcEnv  ( tcLookupGlobal_maybe, tcExtendGlobalValEnv, TcEnv, TcId )
 
 import TcMonad
 import Type      ( Type )
-import TcType    ( TcType )
-import TcMType   ( zonkTcTypeToType, zonkTcTyVarToTyVar, zonkTcType, zonkTcSigTyVars )
+import TcType    ( TcType, tcGetTyVar )
+import TcMType   ( zonkTcTypeToType, zonkTcTyVarToTyVar, zonkTcType, zonkTcTyVars )
 import TysPrim   ( charPrimTy, intPrimTy, floatPrimTy,
                    doublePrimTy, addrPrimTy
                  )
@@ -352,9 +352,12 @@ zonkMonoBinds (AbsBinds tyvars dicts exports inlines val_bind)
                 new_globals)
   where
     zonkExport (tyvars, global, local)
-       = zonkTcSigTyVars tyvars        `thenNF_Tc` \ new_tyvars ->
+       = zonkTcTyVars tyvars           `thenNF_Tc` \ tys ->
+         let
+               new_tyvars = map (tcGetTyVar "zonkExport") tys
                -- This isn't the binding occurrence of these tyvars
-               -- but they should *be* tyvars.  Hence zonkTcSigTyVars.
+               -- but they should *be* tyvars.  Hence tcGetTyVar.
+         in
          zonkIdBndr global             `thenNF_Tc` \ new_global ->
          zonkIdOcc local               `thenNF_Tc` \ new_local -> 
          returnNF_Tc (new_tyvars, new_global, new_local)
index d0335bc..97de0f2 100644 (file)
@@ -52,7 +52,6 @@ import Subst          ( substTheta )
 import DataCon         ( classDataCon )
 import Class           ( Class, classBigSig )
 import Var             ( idName, idType )
-import VarSet          ( emptyVarSet )
 import Id              ( setIdLocalExported )
 import MkId            ( mkDictFunId, unsafeCoerceId, eRROR_ID )
 import FunDeps         ( checkInstFDs )
@@ -612,9 +611,9 @@ tcInstDecl2 (InstInfo { iDFunId = dfun_id, iBinds = monobinds, iPrags = uprags }
                 dfun_arg_dicts         -- NB! Don't include this_dict here, else the sc_dicts
                                        -- get bound by just selecting from this_dict!!
                 (mkLIE sc_dicts)
-    )                                          `thenTc` \ (const_lie2, lie_binds2) ->
+    )                                  `thenTc` \ (const_lie2, lie_binds2) ->
 
-    checkSigTyVars inst_tyvars' emptyVarSet    `thenNF_Tc` \ zonked_inst_tyvars ->
+    checkSigTyVars inst_tyvars'        `thenNF_Tc` \ zonked_inst_tyvars ->
 
        -- Create the result bindings
     let
index 49ef3f9..d91312d 100644 (file)
@@ -31,7 +31,7 @@ module TcMType (
 
   --------------------------------
   -- Zonking
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
   zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
 
@@ -49,7 +49,7 @@ import TcType         ( TcType, TcThetaType, TcTauType, TcPredType,
                          tcEqType, tcCmpPred,
                          tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
                          tcSplitTyConApp_maybe, tcSplitForAllTys,
-                         tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, 
+                         tcIsTyVarTy, tcSplitSigmaTy, 
                          isUnLiftedType, isIPPred, 
 
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
@@ -343,14 +343,6 @@ zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars     `thenNF_Tc` \ tys ->
 
 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
-
-zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
--- This guy is to zonk the tyvars we're about to feed into tcSimplify
--- Usually this job is done by checkSigTyVars, but in a couple of places
--- that is overkill, so we use this simpler chap
-zonkTcSigTyVars tyvars
-  = zonkTcTyVars tyvars        `thenNF_Tc` \ tys ->
-    returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
 \end{code}
 
 -----------------  Types
index a99f936..7b02308 100644 (file)
@@ -23,17 +23,18 @@ import TcHsSyn              ( TcMatch, TcGRHSs, TcStmt, TcDictBinds, TypecheckedPat )
 import TcMonad
 import TcMonoType      ( tcAddScopedTyVars, tcHsSigType, UserTypeCtxt(..) )
 import Inst            ( LIE, isEmptyLIE, plusLIE, emptyLIE, plusLIEs, lieToList )
-import TcEnv           ( TcId, tcLookupLocalIds, tcExtendLocalValEnv, tcExtendGlobalTyVars )
+import TcEnv           ( TcId, tcLookupLocalIds, tcExtendLocalValEnv )
 import TcPat           ( tcPat, tcMonoPatBndr )
-import TcMType         ( newTyVarTy )
-import TcType          ( TcType, TcTyVar, tyVarsOfType,
+import TcMType         ( newTyVarTy, zonkTcType )
+import TcType          ( TcType, TcTyVar, tyVarsOfType, tidyOpenTypes, tidyOpenType,
                          mkFunTy, isOverloadedTy, liftedTypeKind, openTypeKind  )
 import TcBinds         ( tcBindsAndThen )
-import TcUnify         ( subFunTy, checkSigTyVars, tcSub, isIdCoercion, (<$>), sigPatCtxt )
+import TcUnify         ( subFunTy, checkSigTyVarsWrt, tcSub, isIdCoercion, (<$>) )
 import TcSimplify      ( tcSimplifyCheck, bindInstsOfLocalFuns )
 import Name            ( Name )
 import TysWiredIn      ( boolTy )
 import Id              ( idType )
+import CoreFVs         ( idFreeTyVars )
 import BasicTypes      ( RecFlag(..) )
 import VarSet
 import Var             ( Id )
@@ -109,11 +110,11 @@ tcMatches :: [(Name,Id)]
          -> TcType
          -> TcM ([TcMatch], LIE)
 
-tcMatches xve fun_or_case matches expected_ty
+tcMatches xve ctxt matches expected_ty
   = mapAndUnzipTc tc_match matches     `thenTc` \ (matches, lies) ->
     returnTc (matches, plusLIEs lies)
   where
-    tc_match match = tcMatch xve fun_or_case match expected_ty
+    tc_match match = tcMatch xve ctxt match expected_ty
 \end{code}
 
 
@@ -224,8 +225,8 @@ tcMatchPats pats expected_ty thing_inside
        in
        tcExtendLocalValEnv xve (thing_inside pats' rhs_ty)             `thenTc` \ (result, lie_req2) ->
 
-       returnTc (rhs_ty, lie_req1, ex_tvs, pat_ids, lie_avail, result, lie_req2)
-    ) `thenTc` \ (rhs_ty, lie_req1, ex_tvs, pat_ids, lie_avail, result, lie_req2) -> 
+       returnTc (lie_req1, ex_tvs, pat_ids, lie_avail, result, lie_req2)
+    ) `thenTc` \ (lie_req1, ex_tvs, pat_ids, lie_avail, result, lie_req2) -> 
 
        -- STEP 4: Check for existentially bound type variables
        -- Do this *outside* the scope of the tcAddScopedTyVars, else checkSigTyVars
@@ -260,8 +261,7 @@ tcCheckExistentialPat ids ex_tvs lie_avail lie_req match_ty
     returnTc (lie_req, EmptyMonoBinds)
 
   | otherwise
-  = tcExtendGlobalTyVars (tyVarsOfType match_ty)               $
-    tcAddErrCtxtM (sigPatCtxt tv_list ids)                     $
+  = tcAddErrCtxtM (sigPatCtxt tv_list ids match_ty)            $
 
        -- In case there are any polymorpic, overloaded binders in the pattern
        -- (which can happen in the case of rank-2 type signatures, or data constructors
@@ -270,7 +270,7 @@ tcCheckExistentialPat ids ex_tvs lie_avail lie_req match_ty
 
        -- Deal with overloaded functions bound by the pattern
     tcSimplifyCheck doc tv_list (lieToList lie_avail) lie1     `thenTc` \ (lie2, dict_binds) ->
-    checkSigTyVars tv_list emptyVarSet                         `thenTc_` 
+    checkSigTyVarsWrt (tyVarsOfType match_ty) tv_list          `thenTc_` 
 
     returnTc (lie2, dict_binds `AndMonoBinds` inst_binds)
   where
@@ -447,9 +447,26 @@ sameNoOfArgs matches = isSingleton (nub (map args_in_match matches))
 \end{code}
 
 \begin{code}
+varyingArgsErr name matches
+  = sep [ptext SLIT("Varying number of arguments for function"), quotes (ppr name)]
+
 matchCtxt ctxt  match  = hang (pprMatchContext ctxt     <> colon) 4 (pprMatch ctxt match)
 stmtCtxt do_or_lc stmt = hang (pprMatchContext do_or_lc <> colon) 4 (ppr stmt)
 
-varyingArgsErr name matches
-  = sep [ptext SLIT("Varying number of arguments for function"), quotes (ppr name)]
+sigPatCtxt bound_tvs bound_ids match_ty tidy_env 
+  = zonkTcType match_ty                `thenNF_Tc` \ match_ty' ->
+    let
+       (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
+       (env2, tidy_mty) = tidyOpenType  env1     match_ty'
+    in
+    returnNF_Tc (env1,
+                sep [ptext SLIT("When checking an existential match that binds"),
+                     nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
+                     ptext SLIT("and whose type is") <+> ppr tidy_mty])
+  where
+    show_ids = filter is_interesting bound_ids
+    is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
+
+    ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
+       -- Don't zonk the types so we get the separate, un-unified versions
 \end{code}
index 0e57a0c..a662f3c 100644 (file)
@@ -150,8 +150,9 @@ tcPat tc_bndr WildPatIn pat_ty
 tcPat tc_bndr (ParPatIn parend_pat) pat_ty
   = tcPat tc_bndr parend_pat pat_ty
 
-tcPat tc_bndr (SigPatIn pat sig) pat_ty
-  = tcHsSigType PatSigCtxt sig         `thenTc` \ sig_ty ->
+tcPat tc_bndr pat_in@(SigPatIn pat sig) pat_ty
+  = tcAddErrCtxt (patCtxt pat_in)      $
+    tcHsSigType PatSigCtxt sig         `thenTc` \ sig_ty ->
     tcSubPat sig_ty pat_ty             `thenTc` \ (co_fn, lie_sig) ->
     tcPat tc_bndr pat sig_ty           `thenTc` \ (pat', lie_req, tvs, ids, lie_avail) ->
     returnTc (co_fn <$> pat', lie_req `plusLIE` lie_sig, tvs, ids, lie_avail)
@@ -487,7 +488,7 @@ tcSubPat sig_ty exp_ty
 %************************************************************************
 
 \begin{code}
-patCtxt pat = hang (ptext SLIT("In the pattern:")) 
+patCtxt pat = hang (ptext SLIT("When checking the pattern:")) 
                 4 (ppr pat)
 
 badFieldCon :: Name -> Name -> SDoc
index b8f0878..1752026 100644 (file)
@@ -46,6 +46,7 @@ module TcType (
   isDoubleTy, isFloatTy, isIntTy,
   isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy, 
   isTauTy, tcIsTyVarTy, tcIsForAllTy,
+  allDistinctTyVars,
 
   ---------------------------------
   -- Misc type manipulators
@@ -74,7 +75,6 @@ module TcType (
   ---------------------------------
   -- Unifier and matcher  
   unifyTysX, unifyTyListsX, unifyExtendTysX,
-  allDistinctTyVars,
   matchTy, matchTys, match,
 
   --------------------------------
@@ -453,6 +453,31 @@ tcSplitDFunTy ty
     (tvs, theta, clas, tys) }}
 \end{code}
 
+(allDistinctTyVars tys tvs) = True 
+       iff 
+all the types tys are type variables, 
+distinct from each other and from tvs.
+
+This is useful when checking that unification hasn't unified signature
+type variables.  For example, if the type sig is
+       f :: forall a b. a -> b -> b
+we want to check that 'a' and 'b' havn't 
+       (a) been unified with a non-tyvar type
+       (b) been unified with each other (all distinct)
+       (c) been unified with a variable free in the environment
+
+\begin{code}
+allDistinctTyVars :: [Type] -> TyVarSet -> Bool
+
+allDistinctTyVars []       acc
+  = True
+allDistinctTyVars (ty:tys) acc 
+  = case tcGetTyVar_maybe ty of
+       Nothing                       -> False  -- (a)
+       Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
+               | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
+\end{code}    
+
 
 %************************************************************************
 %*                                                                     *
@@ -886,38 +911,6 @@ boxedMarshalableTyCon tc
 %*                                                                     *
 %************************************************************************
 
-(allDistinctTyVars tys tvs) = True 
-       iff 
-all the types tys are type variables, 
-distinct from each other and from tvs.
-
-This is useful when checking that unification hasn't unified signature
-type variables.  For example, if the type sig is
-       f :: forall a b. a -> b -> b
-we want to check that 'a' and 'b' havn't 
-       (a) been unified with a non-tyvar type
-       (b) been unified with each other (all distinct)
-       (c) been unified with a variable free in the environment
-
-\begin{code}
-allDistinctTyVars :: [Type] -> TyVarSet -> Bool
-
-allDistinctTyVars []       acc
-  = True
-allDistinctTyVars (ty:tys) acc 
-  = case tcGetTyVar_maybe ty of
-       Nothing                       -> False  -- (a)
-       Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
-               | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
-\end{code}    
-
-
-%************************************************************************
-%*                                                                     *
-\subsection{Unification with an explicit substitution}
-%*                                                                     *
-%************************************************************************
-
 Unify types with an explicit substitution and no monad.
 Ignore usage annotations.
 
index 593a735..2cf985e 100644 (file)
@@ -7,7 +7,7 @@
 module TcUnify (
        -- Full-blown subsumption
   tcSub, tcGen, subFunTy,
-  checkSigTyVars, sigCtxt, sigPatCtxt,
+  checkSigTyVars, checkSigTyVarsWrt, sigCtxt, 
 
        -- Various unifications
   unifyTauTy, unifyTauTyList, unifyTauTyLists, 
@@ -25,8 +25,7 @@ module TcUnify (
 
 
 import HsSyn           ( HsExpr(..) )
-import TcHsSyn         ( TypecheckedHsExpr, TcPat, 
-                         mkHsDictApp, mkHsTyApp, mkHsLet )
+import TcHsSyn         ( TypecheckedHsExpr, TcPat, mkHsLet )
 import TypeRep         ( Type(..), SourceType(..), TyNote(..),
                          openKindCon, typeCon )
 
@@ -36,34 +35,33 @@ import TcType               ( TcKind, TcType, TcSigmaType, TcPhiType, TcTyVar, TcTauType,
                          isTauTy, isSigmaTy, 
                          tcSplitAppTy_maybe, tcSplitTyConApp_maybe, 
                          tcGetTyVar_maybe, tcGetTyVar, 
-                         mkTyConApp, mkTyVarTys, mkFunTy, tyVarsOfType, mkRhoTy,
+                         mkTyConApp, mkFunTy, tyVarsOfType, mkRhoTy,
                          typeKind, tcSplitFunTy_maybe, mkForAllTys,
-                         isHoleTyVar, isSkolemTyVar, isUserTyVar, allDistinctTyVars, 
+                         isHoleTyVar, isSkolemTyVar, isUserTyVar, 
                          tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
                          eqKind, openTypeKind, liftedTypeKind, isTypeKind,
-                         hasMoreBoxityInfo, tyVarBindingInfo
+                         hasMoreBoxityInfo, tyVarBindingInfo, allDistinctTyVars
                        )
 import qualified Type  ( getTyVar_maybe )
-import Inst            ( LIE, emptyLIE, plusLIE, mkLIE, 
+import Inst            ( LIE, emptyLIE, plusLIE, 
                          newDicts, instToId, tcInstCall
                        )
 import TcMType         ( getTcTyVar, putTcTyVar, tcInstType, 
                          newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy,
-                         zonkTcType, zonkTcTyVars, zonkTcTyVar )
+                         zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcTyVar )
 import TcSimplify      ( tcSimplifyCheck )
 import TysWiredIn      ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy )
-import TcEnv           ( TcTyThing(..), tcExtendGlobalTyVars, tcGetGlobalTyVars, tcLEnvElts )
+import TcEnv           ( TcTyThing(..), tcGetGlobalTyVars, tcLEnvElts )
 import TyCon           ( tyConArity, isTupleTyCon, tupleTyConBoxity )
 import PprType         ( pprType )
-import CoreFVs         ( idFreeTyVars )
 import Id              ( mkSysLocal, idType )
 import Var             ( Var, varName, tyVarKind )
-import VarSet          ( elemVarSet, varSetElems )
+import VarSet          ( emptyVarSet, unionVarSet, elemVarSet, varSetElems )
 import VarEnv
 import Name            ( isSystemName, getSrcLoc )
 import ErrUtils                ( Message )
 import BasicTypes      ( Boxity, Arity, isBoxed )
-import Util            ( isSingleton, equalLength )
+import Util            ( equalLength )
 import Maybe           ( isNothing )
 import Outputable
 \end{code}
@@ -147,7 +145,9 @@ tc_sub _ (TyVarTy tv) act_sty act_ty
 
 tc_sub exp_sty expected_ty act_sty actual_ty
   | isSigmaTy expected_ty
-  = tcGen expected_ty (
+  = tcGen expected_ty (tyVarsOfType actual_ty) (
+       -- It's really important to check for escape wrt the free vars of
+       -- both expected_ty *and* actual_ty
        \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
     )                          `thenTc` \ (gen_fn, co_fn, lie) ->
     returnTc (gen_fn <.> co_fn, lie)
@@ -262,12 +262,15 @@ imitateFun tv ty
 
 \begin{code}
 tcGen :: TcSigmaType                           -- expected_ty
+      -> TcTyVarSet                            -- Extra tyvars that the universally
+                                               --      quantified tyvars of expected_ty
+                                               --      must not be unified
       -> (TcPhiType -> TcM (result, LIE))      -- spec_ty
       -> TcM (ExprCoFn, result, LIE)
        -- The expression has type: spec_ty -> expected_ty
 
-tcGen expected_ty thing_inside -- We expect expected_ty to be a forall-type
-                               -- If not, the call is a no-op
+tcGen expected_ty extra_tvs thing_inside       -- We expect expected_ty to be a forall-type
+                                               -- If not, the call is a no-op
   = tcInstType expected_ty             `thenNF_Tc` \ (forall_tvs, theta, phi_ty) ->
 
        -- Type-check the arg and unify with poly type
@@ -284,12 +287,9 @@ tcGen expected_ty thing_inside     -- We expect expected_ty to be a forall-type
        -- Conclusion: include the free vars of the expected_ty in the
        -- list of "free vars" for the signature check.
 
-    tcExtendGlobalTyVars free_tvs                              $
-    tcAddErrCtxtM (sigCtxt forall_tvs theta phi_ty)    $
-
     newDicts SignatureOrigin theta                     `thenNF_Tc` \ dicts ->
     tcSimplifyCheck sig_msg forall_tvs dicts lie       `thenTc` \ (free_lie, inst_binds) ->
-    checkSigTyVars forall_tvs free_tvs                 `thenTc` \ zonked_tvs ->
+    checkSigTyVarsWrt free_tvs forall_tvs              `thenTc` \ zonked_tvs ->
 
     let
            -- This HsLet binds any Insts which came out of the simplification.
@@ -300,7 +300,7 @@ tcGen expected_ty thing_inside      -- We expect expected_ty to be a forall-type
     in
     returnTc (mkCoercion co_fn, result, free_lie)
   where
-    free_tvs = tyVarsOfType expected_ty
+    free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
     sig_msg  = ptext SLIT("When generalising the type of an expression")
 \end{code}    
 
@@ -1000,20 +1000,32 @@ So we revert to ordinary type variables for signatures, and try to
 give a helpful message in checkSigTyVars.
 
 \begin{code}
-checkSigTyVars :: [TcTyVar]            -- Universally-quantified type variables in the signature
-              -> TcTyVarSet            -- Tyvars that are free in the type signature
-                                       --      Not necessarily zonked
-                                       --      These should *already* be in the free-in-env set, 
-                                       --      and are used here only to improve the error message
-              -> TcM [TcTyVar]         -- Zonked signature type variables
-
-checkSigTyVars [] free = returnTc []
-checkSigTyVars sig_tyvars free_tyvars
-  = zonkTcTyVars sig_tyvars            `thenNF_Tc` \ sig_tys ->
-    tcGetGlobalTyVars                  `thenNF_Tc` \ globals ->
-
-    checkTcM (allDistinctTyVars sig_tys globals)
-            (complain sig_tys globals) `thenTc_`
+checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar]
+checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
+
+checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar]
+checkSigTyVarsWrt extra_tvs sig_tvs
+  = zonkTcTyVarsAndFV (varSetElems extra_tvs)  `thenNF_Tc` \ extra_tvs' ->
+    check_sig_tyvars extra_tvs' sig_tvs
+
+check_sig_tyvars
+       :: TcTyVarSet           -- Global type variables. The universally quantified
+                               --      tyvars should not mention any of these
+                               --      Guaranteed already zonked.
+       -> [TcTyVar]            -- Universally-quantified type variables in the signature
+                               --      Not guaranteed zonked.
+       -> TcM [TcTyVar]        -- Zonked signature type variables
+
+check_sig_tyvars extra_tvs []
+  = returnTc []
+check_sig_tyvars extra_tvs sig_tvs 
+  = zonkTcTyVars sig_tvs       `thenNF_Tc` \ sig_tys ->
+    tcGetGlobalTyVars          `thenNF_Tc` \ gbl_tvs ->
+    let
+       env_tvs = gbl_tvs `unionVarSet` extra_tvs
+    in
+    checkTcM (allDistinctTyVars sig_tys env_tvs)
+            (complain sig_tys env_tvs)         `thenTc_`
 
     returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
 
@@ -1024,9 +1036,9 @@ checkSigTyVars sig_tyvars free_tyvars
                   (env2, emptyVarEnv, [])
                   (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
 
-        failWithTcM (env3, main_msg $$ vcat msgs)
+        failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
       where
-       (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
+       (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
        (env2, tidy_tys) = tidyOpenTypes  env1         sig_tys
 
        main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
@@ -1053,18 +1065,19 @@ checkSigTyVars sig_tyvars free_tyvars
            if tv `elemVarSet` globals  -- Error (c) or (d)! Type variable escapes
                                        -- The least comprehensible, so put it last
                        -- Game plan: 
-                       --    a) get the local TcIds and TyVars from the environment,
+                       --       get the local TcIds and TyVars from the environment,
                        --       and pass them to find_globals (they might have tv free)
-                       --    b) similarly, find any free_tyvars that mention tv
-           then   tcGetEnv                                                     `thenNF_Tc` \ ve ->
-                  find_globals tv tidy_env  (tcLEnvElts ve)                    `thenNF_Tc` \ (tidy_env1, globs) ->
-                  find_frees   tv tidy_env1 [] (varSetElems free_tyvars)       `thenNF_Tc` \ (tidy_env2, frees) ->
-                  returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
+           then   tcGetEnv                                     `thenNF_Tc` \ ve ->
+                  find_globals tv tidy_env  (tcLEnvElts ve)    `thenNF_Tc` \ (tidy_env1, globs) ->
+                  returnNF_Tc (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
 
            else        -- All OK
            returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
            }}
+\end{code}
+
 
+\begin{code}
 -----------------------
 -- find_globals looks at the value environment and finds values
 -- whose types mention the offending type variable.  It has to be 
@@ -1108,7 +1121,7 @@ find_thing ignore_it tidy_env (ATyVar tv)
     else let
        (tidy_env1, tv1)     = tidyOpenTyVar tidy_env  tv
        (tidy_env2, tidy_ty) = tidyOpenType  tidy_env1 tv_ty
-       msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
+       msg = sep [ppr tv1 <+> eq_stuff, nest 2 bound_at]
 
        eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
                 | otherwise                                        = equals <+> ppr tv_ty
@@ -1119,42 +1132,19 @@ find_thing ignore_it tidy_env (ATyVar tv)
     returnNF_Tc (tidy_env2, Just msg)
 
 -----------------------
-find_frees tv tidy_env acc []
-  = returnNF_Tc (tidy_env, acc)
-find_frees tv tidy_env acc (ftv:ftvs)
-  = zonkTcTyVar ftv    `thenNF_Tc` \ ty ->
-    if tv `elemVarSet` tyVarsOfType ty then
-       let
-           (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
-       in
-       find_frees tv tidy_env' (ftv':acc) ftvs
-    else
-       find_frees tv tidy_env  acc        ftvs
-
-
-escape_msg sig_tv tv globs frees
+escape_msg sig_tv tv globs
   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
     if not (null globs) then
        vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"), 
              nest 2 (vcat globs)]
-     else if not (null frees) then
-       vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
-             nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
-       ]
      else
        empty   -- Sigh.  It's really hard to give a good error message
-               -- all the time.   One bad case is an existential pattern match
+               -- all the time.   One bad case is an existential pattern match.
+               -- We rely on the "When..." context to help.
   where
-    is_are | isSingleton frees = ptext SLIT("is")
-          | otherwise         = ptext SLIT("are")
     pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
          | otherwise    = ptext SLIT("It")
 
-    vcat_first :: Int -> [SDoc] -> SDoc
-    vcat_first n []     = empty
-    vcat_first 0 (x:xs) = text "...others omitted..."
-    vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
-
 
 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
@@ -1165,29 +1155,16 @@ These two context are used with checkSigTyVars
 \begin{code}
 sigCtxt :: [TcTyVar] -> TcThetaType -> TcTauType
        -> TidyEnv -> NF_TcM (TidyEnv, Message)
-sigCtxt sig_tyvars sig_theta sig_tau tidy_env
+sigCtxt sig_tvs sig_theta sig_tau tidy_env
   = zonkTcType sig_tau         `thenNF_Tc` \ actual_tau ->
     let
-       (env1, tidy_sig_tyvars)  = tidyOpenTyVars tidy_env sig_tyvars
-       (env2, tidy_sig_rho)     = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
-       (env3, tidy_actual_tau)  = tidyOpenType env2 actual_tau
-       msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
-                   ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
+       (env1, tidy_sig_tvs)    = tidyOpenTyVars tidy_env sig_tvs
+       (env2, tidy_sig_rho)    = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
+       (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
+       sub_msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
+                       ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
                   ]
+       msg = ptext SLIT("When trying to generalise an inferred type") $$ nest 4 sub_msg
     in
     returnNF_Tc (env3, msg)
-
-sigPatCtxt bound_tvs bound_ids tidy_env
-  = returnNF_Tc (env1,
-                sep [ptext SLIT("When checking a pattern that binds"),
-                     nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
-  where
-    show_ids = filter is_interesting bound_ids
-    is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
-
-    (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
-    ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
-       -- Don't zonk the types so we get the separate, un-unified versions
 \end{code}
-
-