[project @ 2005-02-25 13:06:31 by simonpj]
authorsimonpj <unknown>
Fri, 25 Feb 2005 13:07:54 +0000 (13:07 +0000)
committersimonpj <unknown>
Fri, 25 Feb 2005 13:07:54 +0000 (13:07 +0000)
---------------------------------------------
Type signatures are no longer instantiated with skolem constants
---------------------------------------------

Merge to STABLE

Consider

  p :: a
  q :: b
  (p,q,r) = (r,r,p)

Here, 'a' and 'b' end up being the same, because they are both bound
to the type for 'r', which is just a meta type variable.  So 'a' and 'b'
can't be skolems.

Sigh.  This commit goes back to an earlier way of doing things, by
arranging that type signatures get instantiated with *meta* type
variables; then at the end we must check that they have not been
unified with types, nor with each other.

This is a real bore.  I had to do quite a bit of related fiddling around
to make error messages come out right.  Improved one or two.

Also a small unrelated fix to make
:i (:+)
print with parens in ghci.  Sorry this got mixed up in the same commit.

19 files changed:
ghc/compiler/Makefile
ghc/compiler/basicTypes/Id.lhs
ghc/compiler/basicTypes/MkId.lhs
ghc/compiler/basicTypes/Name.lhs
ghc/compiler/basicTypes/OccName.lhs
ghc/compiler/compMan/CompManager.lhs
ghc/compiler/ghci/ByteCodeGen.lhs
ghc/compiler/ghci/InteractiveUI.hs
ghc/compiler/iface/IfaceSyn.lhs
ghc/compiler/iface/IfaceType.lhs
ghc/compiler/typecheck/Inst.lhs
ghc/compiler/typecheck/TcBinds.lhs
ghc/compiler/typecheck/TcEnv.lhs
ghc/compiler/typecheck/TcHsSyn.lhs
ghc/compiler/typecheck/TcMType.lhs
ghc/compiler/typecheck/TcSimplify.lhs
ghc/compiler/typecheck/TcType.lhs
ghc/compiler/typecheck/TcUnify.lhs
ghc/compiler/types/TypeRep.lhs

index 4cff048..bc3ab8a 100644 (file)
@@ -515,6 +515,11 @@ utils/Binary_HC_OPTS               += -O
 utils/FastMutInt_HC_OPTS       += -O
 
 
+# ---- Profiling ----
+#simplCore/Simplify_HC_OPTS = -auto-all
+#simplCore/SimplEnv_HC_OPTS = -auto-all
+#simplCore/SimplUtils_HC_OPTS = -auto-all
+
 # CSE interacts badly with top-level IORefs (reportedly in DriverState and
 # DriverMkDepend), causing some of them to be commoned up.  We have a fix for
 # this in 5.00+, but earlier versions of the compiler will need CSE turned off.
index cb848a1..63ef83f 100644 (file)
@@ -103,7 +103,7 @@ import qualified Demand     ( Demand )
 import DataCon         ( isUnboxedTupleCon )
 import NewDemand       ( Demand, StrictSig, topDmd, topSig, isBottomingSig )
 import Name            ( Name, OccName, nameIsLocalOrFrom, 
-                         mkSystemName, mkSystemNameEncoded, mkInternalName,
+                         mkSystemVarName, mkSystemVarNameEncoded, mkInternalName,
                          getOccName, getSrcLoc
                        ) 
 import Module          ( Module )
@@ -168,10 +168,10 @@ mkVanillaGlobal :: Name -> Type -> IdInfo -> Id
 
 -- for SysLocal, we assume the base name is already encoded, to avoid
 -- re-encoding the same string over and over again.
-mkSysLocal          fs uniq ty = mkLocalId (mkSystemNameEncoded uniq fs) ty
+mkSysLocal fs uniq ty = mkLocalId (mkSystemVarNameEncoded uniq fs) ty
 
 -- version to use when the faststring needs to be encoded
-mkSysLocalUnencoded fs uniq ty = mkLocalId (mkSystemName uniq fs)        ty
+mkSysLocalUnencoded fs uniq ty = mkLocalId (mkSystemVarName uniq fs)  ty
 
 mkUserLocal occ uniq ty loc = mkLocalId (mkInternalName    uniq occ loc) ty
 mkVanillaGlobal            = mkGlobalId VanillaGlobal
index 46e957f..50e981b 100644 (file)
@@ -51,7 +51,7 @@ import TcType         ( Type, ThetaType, mkDictTy, mkPredTys, mkPredTy,
                          tcSplitFunTys, tcSplitForAllTys
                        )
 import CoreUtils       ( exprType )
-import CoreUnfold      ( mkTopUnfolding, mkCompulsoryUnfolding, mkOtherCon )
+import CoreUnfold      ( mkTopUnfolding, mkCompulsoryUnfolding )
 import Literal         ( nullAddrLit, mkStringLit )
 import TyCon           ( TyCon, isNewTyCon, tyConTyVars, tyConDataCons,
                           tyConStupidTheta, isProductTyCon, isDataTyCon, isRecursiveTyCon )
@@ -85,7 +85,6 @@ import CoreSyn
 import Unique          ( mkBuiltinUnique, mkPrimOpIdUnique )
 import Maybes
 import PrelNames
-import Maybe            ( isJust )
 import Util             ( dropList, isSingleton )
 import Outputable
 import FastString
index f0ef363..4ea51b6 100644 (file)
@@ -11,8 +11,8 @@ module Name (
        -- The Name type
        Name,                                   -- Abstract
        BuiltInSyntax(..), 
-       mkInternalName, mkSystemName, 
-       mkSystemNameEncoded, mkSysTvName, 
+       mkInternalName, mkSystemName,
+       mkSystemVarName, mkSystemVarNameEncoded, mkSysTvName, 
        mkFCallName, mkIPName,
        mkExternalName, mkWiredInName,
 
@@ -206,21 +206,20 @@ mkWiredInName mod occ uniq mb_parent thing built_in
           n_sort = WiredIn mod mb_parent thing built_in,
           n_occ = occ, n_loc = wiredInSrcLoc }
 
-mkSystemName :: Unique -> UserFS -> Name
-mkSystemName uniq fs = Name { n_uniq = uniq, n_sort = System, 
-                             n_occ = mkVarOcc fs, n_loc = noSrcLoc }
+mkSystemName :: Unique -> OccName -> Name
+mkSystemName uniq occ = Name { n_uniq = uniq, n_sort = System, 
+                              n_occ = occ, n_loc = noSrcLoc }
+
+mkSystemVarName :: Unique -> UserFS -> Name
+mkSystemVarName uniq fs = mkSystemName uniq (mkVarOcc fs)
 
 -- Use this version when the string is already encoded.  Avoids duplicating
 -- the string each time a new name is created.
-mkSystemNameEncoded :: Unique -> EncodedFS -> Name
-mkSystemNameEncoded uniq fs = Name { n_uniq = uniq, n_sort = System, 
-                                    n_occ = mkSysOccFS varName fs, 
-                                    n_loc = noSrcLoc }
+mkSystemVarNameEncoded :: Unique -> EncodedFS -> Name
+mkSystemVarNameEncoded uniq fs = mkSystemName uniq (mkSysOccFS varName fs) 
 
 mkSysTvName :: Unique -> EncodedFS -> Name
-mkSysTvName uniq fs = Name { n_uniq = uniq, n_sort = System, 
-                            n_occ = mkSysOccFS tvName fs, 
-                            n_loc = noSrcLoc }
+mkSysTvName uniq fs = mkSystemName uniq (mkSysOccFS tvName fs) 
 
 mkFCallName :: Unique -> EncodedString -> Name
        -- The encoded string completely describes the ccall
@@ -299,7 +298,6 @@ instance NamedThing Name where
 
 \begin{code}
 instance Outputable Name where
-       -- When printing interfaces, all Internals have been given nice print-names
     ppr name = pprName name
 
 instance OutputableBndr Name where
index 2de02e7..29a6bbc 100644 (file)
@@ -35,7 +35,7 @@ module OccName (
        mkDataConWrapperOcc, mkDataConWorkerOcc,
        
        isVarOcc, isTvOcc, isTcOcc, isDataOcc, isDataSymOcc, isSymOcc, isValOcc,
-       reportIfUnused,
+       parenSymOcc, reportIfUnused,
 
        occNameFS, occNameString, occNameUserString, occNameSpace, 
        occNameFlavour, briefOccNameFlavour,
@@ -402,9 +402,15 @@ isDataOcc other                   = False
 
 -- Any operator (data constructor or variable)
 -- Pretty inefficient!
-isSymOcc (OccName DataName s) = isLexConSym (decodeFS s)
-isSymOcc (OccName VarName s)  = isLexSym (decodeFS s)
-isSymOcc other               = False
+isSymOcc (OccName DataName s)  = isLexConSym (decodeFS s)
+isSymOcc (OccName TcClsName s) = isLexConSym (decodeFS s)
+isSymOcc (OccName VarName s)   = isLexSym (decodeFS s)
+isSymOcc other                = False
+
+parenSymOcc :: OccName -> SDoc -> SDoc
+-- Wrap parens around an operator
+parenSymOcc occ doc | isSymOcc occ = parens doc
+                   | otherwise    = doc
 \end{code}
 
 
index 5bb0a98..829664d 100644 (file)
@@ -61,8 +61,7 @@ import HscMain                ( newHscEnv )
 import DriverState     ( v_Output_file, v_NoHsMain, v_MainModIs )
 import DriverPhases    ( HscSource(..), isHsBoot, hscSourceString, isHaskellSrcFilename )
 import Finder          ( findModule, findLinkable, addHomeModuleToFinder,
-                         flushFinderCache, findPackageModule,
-                         mkHomeModLocation, FindResult(..), cantFindError )
+                         flushFinderCache, mkHomeModLocation, FindResult(..), cantFindError )
 import HscTypes                ( ModSummary(..), HomeModInfo(..), ModIface(..), msHsFilePath,
                          HscEnv(..), GhciMode(..), 
                          InteractiveContext(..), emptyInteractiveContext, 
@@ -78,17 +77,17 @@ import ErrUtils             ( showPass )
 import SysTools                ( cleanTempFilesExcept )
 import BasicTypes      ( SuccessFlag(..), succeeded )
 import StringBuffer    ( hGetStringBuffer )
-import Type            ( dropForAlls )
 import Util
 import Outputable
 import Panic
-import CmdLineOpts     ( DynFlags(..), dopt )
+import CmdLineOpts     ( DynFlags(..) )
 import Maybes          ( expectJust, orElse, mapCatMaybes )
 import FiniteMap
 
 import DATA_IOREF      ( readIORef )
 
 #ifdef GHCI
+import Finder          ( findPackageModule )
 import HscMain         ( hscGetInfo, GetInfoResult, hscStmt, hscTcExpr, hscKcType )
 import HscTypes                ( TyThing(..), icPrintUnqual, showModMsg )
 import TcRnDriver      ( mkExportEnv, getModuleContents )
@@ -97,13 +96,13 @@ import RdrName              ( GlobalRdrEnv, plusGlobalRdrEnv )
 import Name            ( Name )
 import NameEnv
 import Id              ( idType )
-import Type            ( tidyType )
+import Type            ( tidyType, dropForAlls )
 import VarEnv          ( emptyTidyEnv )
 import Linker          ( HValue, unload, extendLinkEnv )
 import GHC.Exts                ( unsafeCoerce# )
 import Foreign
 import Control.Exception as Exception ( Exception, try )
-import CmdLineOpts     ( DynFlag(..), dopt_unset )
+import CmdLineOpts     ( DynFlag(..), dopt_unset, dopt )
 #endif
 
 import EXCEPTION       ( throwDyn )
index 5964884..5f9fe00 100644 (file)
@@ -15,7 +15,7 @@ import ByteCodeAsm    ( CompiledByteCode(..), UnlinkedBCO,
 import ByteCodeLink    ( lookupStaticPtr )
 
 import Outputable
-import Name            ( Name, getName, mkSystemName )
+import Name            ( Name, getName, mkSystemVarName )
 import Id
 import FiniteMap
 import ForeignCall     ( ForeignCall(..), CCallTarget(..), CCallSpec(..) )
@@ -102,7 +102,7 @@ coreExprToBCOs dflags expr
 
       -- create a totally bogus name for the top-level BCO; this
       -- should be harmless, since it's never used for anything
-      let invented_name  = mkSystemName (mkPseudoUniqueE 0) FSLIT("ExprTopLevel")
+      let invented_name  = mkSystemVarName (mkPseudoUniqueE 0) FSLIT("ExprTopLevel")
           invented_id    = mkLocalId invented_name (panic "invented_id's type")
          
       (BcM_State final_ctr mallocd, proto_bco) 
index 42f6b1b..a686e43 100644 (file)
@@ -1,6 +1,6 @@
 {-# OPTIONS -#include "Linker.h" #-}
 -----------------------------------------------------------------------------
--- $Id: InteractiveUI.hs,v 1.190 2005/02/23 15:38:52 simonmar Exp $
+-- $Id: InteractiveUI.hs,v 1.191 2005/02/25 13:07:10 simonpj Exp $
 --
 -- GHC Interactive User Interface
 --
@@ -27,7 +27,7 @@ import DriverUtil     ( remove_spaces )
 import Linker          ( showLinkerState, linkPackages )
 import Util
 import Name            ( Name, NamedThing(..) )
-import OccName         ( OccName, isSymOcc, occNameUserString )
+import OccName         ( OccName, parenSymOcc, occNameUserString )
 import BasicTypes      ( StrictnessMark(..), defaultFixity, SuccessFlag(..) )
 import Outputable
 import CmdLineOpts     ( DynFlags(..), DynFlag(..), dopt )
@@ -622,8 +622,7 @@ ppr_trim show xs
 
 ppr_bndr :: OccName -> SDoc
 -- Wrap operators in ()
-ppr_bndr occ | isSymOcc occ = parens (ppr occ)
-            | otherwise    = ppr occ
+ppr_bndr occ = parenSymOcc occ (ppr occ)
 
 
 -----------------------------------------------------------------------------
index d4f5545..a538823 100644 (file)
@@ -58,7 +58,7 @@ import DataCon                ( dataConName, dataConSig, dataConFieldLabels, dataConStrictMark
                          dataConTyCon, dataConIsInfix, isVanillaDataCon )
 import Class           ( FunDep, DefMeth, classExtraBigSig, classTyCon )
 import OccName         ( OccName, OccEnv, emptyOccEnv, 
-                         lookupOccEnv, extendOccEnv, 
+                         lookupOccEnv, extendOccEnv, parenSymOcc,
                          OccSet, unionOccSets, unitOccSet )
 import Name            ( Name, NamedThing(..), nameOccName, isExternalName )
 import NameSet         ( NameSet, elemNameSet )
@@ -290,7 +290,7 @@ instance Outputable IfaceClassOp where
 
 pprIfaceDeclHead :: IfaceContext -> OccName -> [IfaceTvBndr] -> SDoc
 pprIfaceDeclHead context thing tyvars 
-  = hsep [pprIfaceContext context, ppr thing, pprIfaceTvBndrs tyvars]
+  = hsep [pprIfaceContext context, parenSymOcc thing (ppr thing), pprIfaceTvBndrs tyvars]
 
 pp_condecls tc IfAbstractTyCon    = ptext SLIT("{- abstract -}")
 pp_condecls tc (IfNewTyCon c)     = equals <+> pprIfaceConDecl tc c
index 19226e9..b713908 100644 (file)
@@ -30,7 +30,7 @@ import TypeRep                ( Type(..), TyNote(..), PredType(..), ThetaType )
 import TyCon           ( TyCon, isTupleTyCon, tyConArity, tupleTyConBoxity )
 import Var             ( isId, tyVarKind, idType )
 import TysWiredIn      ( listTyConName, parrTyConName, tupleTyCon, intTyConName, charTyConName, boolTyConName )
-import OccName         ( OccName )
+import OccName         ( OccName, parenSymOcc )
 import Name            ( Name, getName, getOccName, nameModule, nameOccName )
 import Module          ( Module )
 import BasicTypes      ( IPName(..), Arity, Version, mapIPName, tupleParens, Boxity )
@@ -72,6 +72,12 @@ isLocalIfaceExtName other          = False
 mkIfaceExtName name = ExtPkg (nameModule name) (nameOccName name)
        -- Local helper for wired-in names
 
+ifaceExtOcc :: IfaceExtName -> OccName
+ifaceExtOcc (ExtPkg _ occ)     = occ
+ifaceExtOcc (HomePkg _ occ _)  = occ
+ifaceExtOcc (LocalTop occ)     = occ
+ifaceExtOcc (LocalTopSub occ _) = occ
+
 interactiveExtNameFun :: PrintUnqualified -> Name-> IfaceExtName
 interactiveExtNameFun print_unqual name
   | print_unqual mod occ = LocalTop occ
@@ -272,7 +278,7 @@ pprIfaceForAllPart tvs ctxt doc
            | otherwise = ptext SLIT("forall") <+> pprIfaceTvBndrs tvs <> dot
 
 -------------------
-ppr_tc_app ctxt_prec tc         []   = ppr tc
+ppr_tc_app ctxt_prec tc         []   = ppr_tc tc
 ppr_tc_app ctxt_prec IfaceListTc [ty] = brackets   (pprIfaceType ty)
 ppr_tc_app ctxt_prec IfacePArrTc [ty] = pabrackets (pprIfaceType ty)
 ppr_tc_app ctxt_prec (IfaceTupTc bx arity) tys
@@ -280,13 +286,19 @@ ppr_tc_app ctxt_prec (IfaceTupTc bx arity) tys
   = tupleParens bx (sep (punctuate comma (map pprIfaceType tys)))
 ppr_tc_app ctxt_prec tc tys 
   = maybeParen ctxt_prec tYCON_PREC 
-              (sep [ppr tc, nest 4 (sep (map pprParendIfaceType tys))])
+              (sep [ppr_tc tc, nest 4 (sep (map pprParendIfaceType tys))])
+
+ppr_tc :: IfaceTyCon -> SDoc
+-- Wrap infix type constructors in parens
+ppr_tc tc@(IfaceTc ext_nm) = parenSymOcc (ifaceExtOcc ext_nm) (ppr tc)
+ppr_tc tc                 = ppr tc
 
 -------------------
 instance Outputable IfacePredType where
        -- Print without parens
   ppr (IfaceIParam ip ty)  = hsep [ppr ip, dcolon, ppr ty]
-  ppr (IfaceClassP cls ts) = ppr cls <+> sep (map pprParendIfaceType ts)
+  ppr (IfaceClassP cls ts) = parenSymOcc (ifaceExtOcc cls) (ppr cls)
+                            <+> sep (map pprParendIfaceType ts)
 
 instance Outputable IfaceTyCon where
   ppr (IfaceTc ext) = ppr ext
index 4fb3f87..f75d1d3 100644 (file)
@@ -50,11 +50,11 @@ import TcRnMonad
 import TcEnv   ( tcLookupId, checkWellStaged, topIdLvl, tcMetaTy )
 import InstEnv ( DFunId, InstEnv, lookupInstEnv, checkFunDeps, extendInstEnv )
 import TcIface ( loadImportedInsts )
-import TcMType ( zonkTcType, zonkTcTypes, zonkTcPredType, 
-                 zonkTcThetaType, tcInstTyVar, tcInstType
+import TcMType ( zonkTcType, zonkTcTypes, zonkTcPredType, zonkTcThetaType, 
+                 tcInstTyVar, tcInstType, tcSkolType
                )
 import TcType  ( Type, TcType, TcThetaType, TcTyVarSet, TcTyVar, TcPredType,
-                 PredType(..), typeKind, mkSigmaTy,
+                 PredType(..), SkolemInfo(..), typeKind, mkSigmaTy,
                  tcSplitForAllTys, tcSplitForAllTys, 
                  tcSplitPhiTy, tcIsTyVarTy, tcSplitDFunTy, tcSplitDFunHead,
                  isIntTy,isFloatTy, isIntegerTy, isDoubleTy,
@@ -71,27 +71,25 @@ import Type ( TvSubst, substTy, substTyVar, substTyWith, substTheta, zipTopTvSub
 import Unify   ( tcMatchTys )
 import Kind    ( isSubKind )
 import Packages        ( isHomeModule )
-import HscTypes        ( HscEnv( hsc_HPT ), ExternalPackageState(..), 
-                 ModDetails( md_insts ), HomeModInfo( hm_details )  )
+import HscTypes        ( ExternalPackageState(..) )
 import CoreFVs ( idFreeTyVars )
 import DataCon ( DataCon, dataConTyVars, dataConStupidTheta, dataConName )
 import Id      ( Id, idName, idType, mkUserLocal, mkLocalId )
 import PrelInfo        ( isStandardClass, isNoDictClass )
 import Name    ( Name, mkMethodOcc, getOccName, getSrcLoc, nameModule,
-                 isInternalName, setNameUnique, mkSystemNameEncoded )
+                 isInternalName, setNameUnique, mkSystemVarNameEncoded )
 import NameSet ( addOneToNameSet )
 import Literal ( inIntRange )
 import Var     ( TyVar, tyVarKind, setIdType )
 import VarEnv  ( TidyEnv, emptyTidyEnv )
 import VarSet  ( elemVarSet, emptyVarSet, unionVarSet, mkVarSet )
-import Module  ( moduleEnvElts, elemModuleEnv, lookupModuleEnv )
 import TysWiredIn ( floatDataCon, doubleDataCon )
 import PrelNames       ( integerTyConName, fromIntegerName, fromRationalName, rationalTyConName )
 import BasicTypes( IPName(..), mapIPName, ipNameName )
 import UniqSupply( uniqsFromSupply )
 import SrcLoc  ( mkSrcSpan, noLoc, unLoc, Located(..) )
 import CmdLineOpts( DynFlags )
-import Maybes  ( isJust, fromJust )
+import Maybes  ( isJust )
 import Outputable
 \end{code}
 
@@ -402,7 +400,7 @@ newLitInst orig lit expected_ty
   = getInstLoc orig            `thenM` \ loc ->
     newUnique                  `thenM` \ new_uniq ->
     let
-       lit_nm   = mkSystemNameEncoded new_uniq FSLIT("lit")
+       lit_nm   = mkSystemVarNameEncoded new_uniq FSLIT("lit")
                -- The "encoded" bit means that we don't need to z-encode
                -- the string every time we call this!
        lit_inst = LitInst lit_nm lit expected_ty loc
@@ -571,7 +569,12 @@ addInst :: DynFlags -> InstEnv -> DFunId -> TcM InstEnv
 addInst dflags home_ie dfun
   = do {       -- Instantiate the dfun type so that we extend the instance
                -- envt with completely fresh template variables
-         (tvs', theta', tau') <- tcInstType (idType dfun)
+               -- This is important because the template variables must
+               -- not overlap with anything in the things being looked up
+               -- (since we do unification).  
+               -- We use tcSkolType because we don't want to allocate fresh
+               -- *meta* type variables.  
+         (tvs', theta', tau') <- tcSkolType (InstSkol dfun) (idType dfun)
        ; let   (cls, tys') = tcSplitDFunHead tau'
                dfun'       = setIdType dfun (mkSigmaTy tvs' theta' tau')           
 
@@ -704,8 +707,13 @@ lookupInst (Dict _ _ _) = returnM NoInstance
 instantiate_dfun :: TvSubst -> DFunId -> TcPredType -> InstLoc -> TcM LookupInstResult
 instantiate_dfun tenv dfun_id pred loc
   = -- tenv is a substitution that instantiates the dfun_id 
-    -- to match the requested result type.   However, the dfun
-    -- might have some tyvars that only appear in arguments
+    -- to match the requested result type.   
+    -- 
+    -- We ASSUME that the dfun is quantified over the very same tyvars 
+    -- that are bound by the tenv.
+    -- 
+    -- However, the dfun
+    -- might have some tyvars that *only* appear in arguments
     -- dfun :: forall a b. C a b, Ord b => D [a]
     -- We instantiate b to a flexi type variable -- it'll presumably
     -- become fixed later via functional dependencies
@@ -731,7 +739,7 @@ instantiate_dfun tenv dfun_id pred loc
     mappM tcInstTyVar open_tvs `thenM` \ open_tvs' ->
     let
        tenv' = extendTvSubstList tenv open_tvs (mkTyVarTys open_tvs')
-               -- Since the tyvars are freshly made, they cannot possibly be captured by
+               -- Since the open_tvs' are freshly made, they cannot possibly be captured by
                -- any nested for-alls in rho.  So the in-scope set is unchanged
        dfun_rho   = substTy tenv' rho
        (theta, _) = tcSplitPhiTy dfun_rho
index f0de50a..a16cddc 100644 (file)
@@ -23,8 +23,10 @@ import TcHsSyn               ( TcId, TcDictBinds, zonkId, mkHsLet )
 import TcRnMonad
 import Inst            ( InstOrigin(..), newDictsAtLoc, newIPDict, instToId )
 import TcEnv           ( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv2, 
-                         newLocalName, tcLookupLocalIds, pprBinders )
-import TcUnify         ( Expected(..), tcInfer, checkSigTyVars, sigCtxt )
+                         newLocalName, tcLookupLocalIds, pprBinders,
+                         tcGetGlobalTyVars )
+import TcUnify         ( Expected(..), tcInfer, unifyTheta, 
+                         bleatEscapedTvs, sigCtxt )
 import TcSimplify      ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted, 
                          tcSimplifyToDicts, tcSimplifyIPs )
 import TcHsType                ( tcHsSigType, UserTypeCtxt(..), tcAddLetBoundTyVars,
@@ -32,16 +34,15 @@ import TcHsType             ( tcHsSigType, UserTypeCtxt(..), tcAddLetBoundTyVars,
                        )
 import TcPat           ( tcPat, PatCtxt(..) )
 import TcSimplify      ( bindInstsOfLocalFuns )
-import TcMType         ( newTyFlexiVarTy, tcSkolType, zonkQuantifiedTyVar, zonkTcTypes )
+import TcMType         ( newTyFlexiVarTy, zonkQuantifiedTyVar, 
+                         tcInstSigType, zonkTcTypes, zonkTcTyVar )
 import TcType          ( TcTyVar, SkolemInfo(SigSkol), 
                          TcTauType, TcSigmaType, 
-                         TvSubstEnv, mkOpenTvSubst, substTheta, substTy, 
                          mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType, 
                          mkForAllTy, isUnLiftedType, tcGetTyVar_maybe, 
-                         mkTyVarTys )
-import Unify           ( tcMatchPreds )
+                         mkTyVarTys, tidyOpenTyVar, tidyOpenType )
 import Kind            ( argTypeKind )
-import VarEnv          ( lookupVarEnv ) 
+import VarEnv          ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv, emptyTidyEnv ) 
 import TysPrim         ( alphaTyVar )
 import Id              ( mkLocalId, mkSpecPragmaId, setInlinePragma )
 import Var             ( idType, idName )
@@ -51,7 +52,6 @@ import VarSet
 import SrcLoc          ( Located(..), unLoc, noLoc, getLoc )
 import Bag
 import Util            ( isIn )
-import Maybes          ( orElse )
 import BasicTypes      ( TopLevelFlag(..), RecFlag(..), isNonRec, isRec, 
                          isNotTopLevel, isAlwaysActive )
 import FiniteMap       ( listToFM, lookupFM )
@@ -464,6 +464,7 @@ tcMonoBinds binds lookup_sig is_rec
 
        ; binds' <- tcExtendTyVarEnv2 rhs_tvs   $
                    tcExtendIdEnv2   rhs_id_env $
+                   traceTc (text "tcMonoBinds" <+> vcat [ppr n <+> ppr id <+> ppr (idType id) | (n,id) <- rhs_id_env]) `thenM_`
                    mapBagM (wrapLocM tcRhs) tc_binds
        ; return (binds', mono_info) }
    where
@@ -560,6 +561,27 @@ getMonoBindInfo tc_binds
 %*                                                                     *
 %************************************************************************
 
+Type signatures are tricky.  Consider
+
+  x :: [a]
+  y :: b
+  (x,y,z) = ([y,z], z, head x)
+
+Here, x and y have type sigs, which go into the environment.  We used to
+instantiate their types with skolem constants, and push those types into
+the RHS, so we'd typecheck the RHS with type
+       ( [a*], b*, c )
+where a*, b* are skolem constants, and c is an ordinary meta type varible.
+
+The trouble is that the occurrences of z in the RHS force a* and b* to 
+be the *same*, so we can't make them into skolem constants that don't unify
+with each other.  Alas.
+
+Current solution: don't use skolems at all.  Instead, instantiate the type
+signatures with ordinary meta type variables, and check at the end that
+each group has remained distinct.
+
+
 \begin{code}
 tcTySigs :: [LSig Name] -> TcM [TcSigInfo]
 -- The trick here is that all the signatures should have the same
@@ -570,8 +592,21 @@ tcTySigs [] = return []
 
 tcTySigs sigs
   = do { (tc_sig1 : tc_sigs) <- mappM tcTySig sigs
-       ; tc_sigs'            <- mapM (checkSigCtxt tc_sig1) tc_sigs
-        ; return (tc_sig1 : tc_sigs') }
+       ; mapM (check_ctxt tc_sig1) tc_sigs
+        ; return (tc_sig1 : tc_sigs) }
+  where
+       -- Check tha all the signature contexts are the same
+       -- The type signatures on a mutually-recursive group of definitions
+       -- must all have the same context (or none).
+       --
+       -- We unify them because, with polymorphic recursion, their types
+       -- might not otherwise be related.  This is a rather subtle issue.
+    check_ctxt :: TcSigInfo -> TcSigInfo -> TcM ()
+    check_ctxt sig1@(TcSigInfo { sig_theta = theta1 }) sig@(TcSigInfo { sig_theta = theta })
+       = setSrcSpan (instLocSrcSpan (sig_loc sig))     $
+         addErrCtxt (sigContextsCtxt sig1 sig)         $
+         unifyTheta theta1 theta
+
 
 tcTySig :: LSig Name -> TcM TcSigInfo
 tcTySig (L span (Sig (L _ name) ty))
@@ -587,51 +622,11 @@ tcTySig (L span (Sig (L _ name) ty))
                                L _ (HsForAllTy _ tvs _ _) -> hsLTyVarNames tvs
                                other                      -> []
 
-       ; (tvs, theta, tau) <- tcSkolType rigid_info sigma_ty
+       ; (tvs, theta, tau) <- tcInstSigType sigma_ty
        ; loc <- getInstLoc (SigOrigin rigid_info)
        ; return (TcSigInfo { sig_id = poly_id, sig_scoped = scoped_names,
                              sig_tvs = tvs, sig_theta = theta, sig_tau = tau, 
                              sig_loc = loc }) }
-
-checkSigCtxt :: TcSigInfo -> TcSigInfo -> TcM TcSigInfo
-checkSigCtxt sig1 sig@(TcSigInfo { sig_tvs = tvs, sig_theta = theta, sig_tau = tau })
-  =    -- Try to match the context of this signature with 
-       -- that of the first signature
-    case tcMatchPreds (sig_tvs sig) (sig_theta sig) (sig_theta sig1) of {
-       Nothing   -> bale_out ;
-       Just tenv ->
-
-    case check_tvs tenv tvs of {
-       Nothing   -> bale_out ;
-       Just tvs' -> 
-
-    let 
-       subst  = mkOpenTvSubst tenv
-    in
-    return (sig { sig_tvs   = tvs', 
-                 sig_theta = substTheta subst theta, 
-                 sig_tau   = substTy subst tau }) }}
-
-  where
-    bale_out = setSrcSpan (instLocSrcSpan (sig_loc sig)) $
-               failWithTc $
-               sigContextsErr (sig_id sig1) (sig_id sig)
-
-       -- Rather tedious check that the type variables
-       -- have been matched only with another type variable,
-       -- and that two type variables have not been matched
-       -- with the same one
-       -- A return of Nothing indicates that one of the bad
-       -- things has happened
-    check_tvs :: TvSubstEnv -> [TcTyVar] -> Maybe [TcTyVar]
-    check_tvs tenv [] = Just []
-    check_tvs tenv (tv:tvs) 
-       = do { let ty = lookupVarEnv tenv tv `orElse` mkTyVarTy tv
-            ; tv'  <- tcGetTyVar_maybe ty
-            ; tvs' <- check_tvs tenv tvs
-            ; if tv' `elem` tvs'
-              then Nothing
-              else Just (tv':tvs') }
 \end{code}
 
 \begin{code}
@@ -680,34 +675,74 @@ generalise top_lvl is_unrestricted mono_infos sigs lie_req
     is_mono_sig sig = null (sig_theta sig)
     doc = ptext SLIT("type signature(s) for") <+> pprBinders bndr_names
 
-mkMethInst (TcSigInfo { sig_id = poly_id, sig_tvs = tvs, 
-                       sig_theta = theta, sig_tau = tau, sig_loc = loc }) mono_id
-  = Method mono_id poly_id (mkTyVarTys tvs) theta tau loc
+    mkMethInst (TcSigInfo { sig_id = poly_id, sig_tvs = tvs, 
+                           sig_theta = theta, sig_tau = tau, sig_loc = loc }) mono_id
+      = Method mono_id poly_id (mkTyVarTys tvs) theta tau loc
 
 checkSigsTyVars :: [TcTyVar] -> [TcSigInfo] -> TcM [TcTyVar]
 checkSigsTyVars qtvs sigs 
-  = mappM check_one sigs       `thenM` \ sig_tvs_s ->
-    let
-       -- Sigh.  Make sure that all the tyvars in the type sigs
-       -- appear in the returned ty var list, which is what we are
-       -- going to generalise over.  Reason: we occasionally get
-       -- silly types like
-       --      type T a = () -> ()
-       --      f :: T a
-       --      f () = ()
-       -- Here, 'a' won't appear in qtvs, so we have to add it
-
-       sig_tvs = foldl extendVarSetList emptyVarSet sig_tvs_s
-       all_tvs = extendVarSetList sig_tvs qtvs
-    in
-    returnM (varSetElems all_tvs)
+  = do { gbl_tvs <- tcGetGlobalTyVars
+       ; sig_tvs_s <- mappM (check_sig gbl_tvs) sigs
+
+       ; let   -- Sigh.  Make sure that all the tyvars in the type sigs
+               -- appear in the returned ty var list, which is what we are
+               -- going to generalise over.  Reason: we occasionally get
+               -- silly types like
+               --      type T a = () -> ()
+               --      f :: T a
+               --      f () = ()
+               -- Here, 'a' won't appear in qtvs, so we have to add it
+               sig_tvs = foldl extendVarSetList emptyVarSet sig_tvs_s
+               all_tvs = varSetElems (extendVarSetList sig_tvs qtvs)
+       ; returnM all_tvs }
   where
-    check_one (TcSigInfo {sig_id = id, sig_tvs = tvs, sig_theta = theta, sig_tau = tau})
-      = addErrCtxt (ptext SLIT("In the type signature for") 
-                     <+> quotes (ppr id))              $
-       addErrCtxtM (sigCtxt id tvs theta tau)          $
-       do { checkSigTyVars tvs; return tvs }
-\end{code}
+    check_sig gbl_tvs (TcSigInfo {sig_id = id, sig_tvs = tvs, 
+                                 sig_theta = theta, sig_tau = tau})
+      = addErrCtxt (ptext SLIT("In the type signature for") <+> quotes (ppr id))       $
+       addErrCtxtM (sigCtxt id tvs theta tau)                                          $
+       do { tvs' <- checkDistinctTyVars tvs
+          ; ifM (any (`elemVarSet` gbl_tvs) tvs')
+                (bleatEscapedTvs gbl_tvs tvs tvs') 
+          ; return tvs' }
+
+checkDistinctTyVars :: [TcTyVar] -> TcM [TcTyVar]
+-- (checkDistinctTyVars tvs) checks that the tvs from one type signature
+-- are still all type variables, and all distinct from each other.  
+-- It returns a zonked set of type variables.
+-- For example, if the type sig is
+--     f :: forall a b. a -> b -> b
+-- we want to check that 'a' and 'b' haven't 
+--     (a) been unified with a non-tyvar type
+--     (b) been unified with each other (all distinct)
+
+checkDistinctTyVars sig_tvs
+  = do { zonked_tvs <- mapM zonk_one sig_tvs
+       ; foldlM check_dup emptyVarEnv (sig_tvs `zip` zonked_tvs)
+       ; return zonked_tvs }
+  where
+    zonk_one sig_tv = do { ty <- zonkTcTyVar sig_tv
+                        ; case tcGetTyVar_maybe ty of
+                            Just tv' -> return tv'
+                            Nothing  -> bomb_out sig_tv "a type" ty }
+
+    check_dup :: TyVarEnv TcTyVar -> (TcTyVar, TcTyVar) -> TcM (TyVarEnv TcTyVar)
+       -- The TyVarEnv maps each zonked type variable back to its
+       -- corresponding user-written signature type variable
+    check_dup acc (sig_tv, zonked_tv)
+       = case lookupVarEnv acc zonked_tv of
+               Just sig_tv' -> bomb_out sig_tv "another quantified type variable" 
+                                               (mkTyVarTy sig_tv')
+
+               Nothing -> return (extendVarEnv acc zonked_tv sig_tv)
+
+    bomb_out sig_tv doc ty 
+       = failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv) 
+                    <+> ptext SLIT("is unified with") <+> text doc <+> ppr tidy_ty)
+       where
+        (env1,  tidy_tv) = tidyOpenTyVar emptyTidyEnv sig_tv
+        (_env2, tidy_ty) = tidyOpenType  env1         ty
+\end{code}    
+
 
 @getTyVarsToGen@ decides what type variables to generalise over.
 
@@ -865,11 +900,14 @@ valSpecSigCtxt v ty
         nest 4 (ppr v <+> dcolon <+> ppr ty)]
 
 -----------------------------------------------
-sigContextsErr id1 id2
-  = vcat [ptext SLIT("Mis-match between the contexts of the signatures for"), 
+sigContextsCtxt sig1 sig2
+  = vcat [ptext SLIT("When matching the contexts of the signatures for"), 
          nest 2 (vcat [ppr id1 <+> dcolon <+> ppr (idType id1),
                        ppr id2 <+> dcolon <+> ppr (idType id2)]),
          ptext SLIT("The signature contexts in a mutually recursive group should all be identical")]
+  where
+    id1 = sig_id sig1
+    id2 = sig_id sig2
 
 
 -----------------------------------------------
index fe2cc1e..12192a9 100644 (file)
@@ -345,13 +345,13 @@ find_thing ignore_it tidy_env (ATyVar tv ty)
     else let
        -- The name tv is scoped, so we don't need to tidy it
        (tidy_env1, tidy_ty) = tidyOpenType  tidy_env tv_ty
-       msg = sep [ppr tv <+> eq_stuff, nest 2 bound_at]
+       msg = sep [ptext SLIT("Scoped type variable") <+> quotes (ppr tv) <+> eq_stuff, nest 2 bound_at]
 
        eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, 
-                  tv == tyVarName tv' = empty
+                  getOccName tv == getOccName tv' = empty
                 | otherwise = equals <+> ppr tidy_ty
                -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
-       bound_at = ptext SLIT("bound at:") <+> ppr (getSrcLoc tv)
+       bound_at = parens $ ptext SLIT("bound at:") <+> ppr (getSrcLoc tv)
     in
     returnM (tidy_env1, Just msg)
 \end{code}
index cf4fad9..59dfa9c 100644 (file)
@@ -36,11 +36,10 @@ import Id   ( idType, setIdType, Id )
 
 import TcRnMonad
 import Type      ( Type )
-import TcType    ( TcType, TcTyVar, mkTyVarTy, mkTyConApp, isImmutableTyVar )
+import TcType    ( TcType, TcTyVar, mkTyVarTy, mkTyConApp, isImmutableTyVar, tcGetTyVar )
 import Kind      ( isLiftedTypeKind, liftedTypeKind, isSubKind )
 import qualified  Type
-import TcMType   ( zonkQuantifiedTyVar, zonkType, zonkTcType, 
-                   putMetaTyVar )
+import TcMType   ( zonkQuantifiedTyVar, zonkType, zonkTcType, zonkTcTyVars, putMetaTyVar )
 import TysPrim   ( charPrimTy, intPrimTy, floatPrimTy,
                    doublePrimTy, addrPrimTy
                  )
@@ -318,9 +317,14 @@ zonk_bind env (AbsBinds tyvars dicts exports inlines val_binds)
     returnM (AbsBinds tyvars new_dicts new_exports inlines new_val_bind)
   where
     zonkExport env (tyvars, global, local)
-       = ASSERT( all isImmutableTyVar tyvars )
+       = zonkTcTyVars tyvars           `thenM` \ tys ->
+         let
+               new_tyvars = map (tcGetTyVar "zonkExport") tys
+               -- This isn't the binding occurrence of these tyvars
+               -- but they should *be* tyvars.  Hence tcGetTyVar.
+         in
          zonkIdBndr env global         `thenM` \ new_global ->
-         returnM (tyvars, new_global, zonkIdOcc env local)
+         returnM (new_tyvars, new_global, zonkIdOcc env local)
 \end{code}
 
 %************************************************************************
index 4db7ae3..2a3dc75 100644 (file)
@@ -21,7 +21,7 @@ module TcMType (
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstType, 
-  tcSkolType, tcSkolTyVars,
+  tcSkolType, tcSkolTyVars, tcInstSigType,
   tcSkolSigType, tcSkolSigTyVars,
 
   --------------------------------
@@ -77,7 +77,7 @@ import Var            ( TyVar, tyVarKind, tyVarName,
 -- others:
 import TcRnMonad          -- TcType, amongst others
 import FunDeps         ( grow )
-import Name            ( Name, setNameUnique, mkSysTvName )
+import Name            ( Name, setNameUnique, mkSysTvName, mkSystemName, getOccName )
 import VarSet
 import VarEnv
 import CmdLineOpts     ( dopt, DynFlag(..) )
@@ -177,11 +177,12 @@ tcInstTyVars tyvars
                -- they cannot possibly be captured by
                -- any existing for-alls.  Hence zipTopTvSubst
 
-tcInstTyVar tyvar
+tcInstTyVar tyvar      -- Use the OccName of the tyvar we are instantiating
+                       -- but make a System Name, so that it's updated in 
+                       -- preference to a tcInstSigTyVar
   = do { uniq <- newUnique
-       ; let name = setNameUnique (tyVarName tyvar) uniq
-               -- See Note [TyVarName]
-       ; newMetaTyVar name (tyVarKind tyvar) Flexi }
+        ; newMetaTyVar (mkSystemName uniq (getOccName tyvar)) 
+                      (tyVarKind tyvar) Flexi }
 
 tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- tcInstType instantiates the outer-level for-alls of a TcType with
@@ -191,6 +192,28 @@ tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
 
 
 ---------------------------------------------
+tcInstSigType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh meta type variables, but
+-- ones which have the same Name as the original type 
+-- variable.  This is used for type signatures, where we must
+-- instantiate with meta type variables, but we'd like to avoid
+-- instantiating them were possible; and the unifier unifies
+-- tyvars with System Names by preference
+-- 
+-- We don't need a fresh unique, because the renamer has made them
+-- unique, and it's better not to do so because we extend the envt
+-- with them as scoped type variables, and we'd like to avoid spurious
+-- 's = s' bindings in error messages
+tcInstSigType ty = tc_inst_type tcInstSigTyVars ty
+
+tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
+tcInstSigTyVars tyvars
+  = mapM new_tv tyvars
+  where
+    new_tv tv = newMetaTyVar (tyVarName tv) (tyVarKind tv) Flexi
+                           
+
+---------------------------------------------
 tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type with fresh skolem constants
 tcSkolType info ty = tc_inst_type (tcSkolTyVars info) ty
@@ -410,7 +433,7 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
 -- bound occurences of the original type variable will get zonked to 
 -- the immutable version.
 --
--- We leave skolem TyVars alone; they are imutable.
+-- We leave skolem TyVars alone; they are immutable.
 zonkQuantifiedTyVar tv
   | isSkolemTyVar tv = return tv
        -- It might be a skolem type variable, 
@@ -533,7 +556,7 @@ zonkTyVar :: (TcTyVar -> TcM Type)          -- What to do for an unbound mutable variabl
          -> TcTyVar -> TcM TcType
 zonkTyVar unbound_var_fn rflag tyvar 
   | not (isTcTyVar tyvar)      -- When zonking (forall a.  ...a...), the occurrences of 
-                               -- the quantified variable a are TyVars not TcTyVars
+                               -- the quantified variable 'a' are TyVars not TcTyVars
   = returnM (TyVarTy tyvar)
 
   | otherwise
index 4c0ca4b..dd4d215 100644 (file)
@@ -1984,8 +1984,17 @@ tc_simplify_top is_interactive wanteds
     strangeTopIPErrs bad_ips                           `thenM_`
 
        -- Deal with ambiguity errors, but only if
-       -- if there has not been an error so far; errors often
-       -- give rise to spurious ambiguous Insts
+       -- if there has not been an error so far:
+       -- errors often give rise to spurious ambiguous Insts.
+       -- For example:
+       --   f = (*)    -- Monomorphic
+       --   g :: Num a => a -> a
+       --   g x = f x x
+       -- Here, we get a complaint when checking the type signature for g,
+       -- that g isn't polymorphic enough; but then we get another one when
+       -- 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
     ifErrsM (returnM []) (
        
        -- Complain about the ones that don't fall under
index d31866d..ce31dd5 100644 (file)
@@ -104,7 +104,7 @@ module TcType (
   isPrimitiveType, 
 
   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
-  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
+  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
   typeKind, 
 
   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
@@ -159,7 +159,7 @@ import Type         (       -- Re-exports
 import TyCon           ( TyCon, isUnLiftedTyCon, tyConUnique )
 import DataCon         ( DataCon )
 import Class           ( Class )
-import Var             ( TyVar, Id, isTcTyVar, tcTyVarDetails )
+import Var             ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
 import ForeignCall     ( Safety, playSafe, DNType(..) )
 import VarSet
 
@@ -167,6 +167,7 @@ import VarSet
 import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
 import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc )
 import NameSet
+import VarEnv          ( TidyEnv )
 import OccName         ( OccName, mkDictOcc )
 import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
 import TysWiredIn      ( unitTyCon, charTyCon, listTyCon )
@@ -266,7 +267,8 @@ data SkolemInfo
                        -- variable for 'a'.  
   | ArrowSkol SrcSpan  -- An arrow form (see TcArrows)
 
-  | GenSkol TcType     -- Bound when doing a subsumption check for this type
+  | GenSkol [TcTyVar]  -- Bound when doing a subsumption check for 
+           TcType      --      (forall tvs. ty)
            SrcSpan
 
 data MetaDetails
@@ -276,6 +278,19 @@ data MetaDetails
   | Indirect TcType  -- Type indirections, treated as wobbly 
                      -- for the purpose of GADT unification.
 
+tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
+-- Tidy the type inside a GenSkol, preparatory to printing it
+tidySkolemTyVar env tv
+  = ASSERT( isSkolemTyVar tv )
+    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info1))
+  where
+    (env1, info1) = case skolemTvInfo tv of
+                     GenSkol tvs ty loc -> (env2, GenSkol tvs1 ty1 loc)
+                           where
+                             (env1, tvs1) = tidyOpenTyVars env tvs
+                             (env2, ty1)  = tidyOpenType env1 ty
+                     info -> (env, info)
+                    
 pprSkolemTyVar :: TcTyVar -> SDoc
 pprSkolemTyVar tv
   = ASSERT( isSkolemTyVar tv )
@@ -288,8 +303,9 @@ instance Outputable SkolemInfo where
   ppr (ArrowSkol loc)  = ptext SLIT("the arrow form at") <+> ppr loc
   ppr (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
                            nest 2 (ptext SLIT("at") <+> ppr loc)]
-  ppr (GenSkol ty loc) = sep [ptext SLIT("the polymorphic type") <+> quotes (ppr ty),
-                           nest 2 (ptext SLIT("at") <+> ppr loc)]
+  ppr (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type") 
+                                 <+> quotes (ppr (mkForAllTys tvs ty)),
+                                 nest 2 (ptext SLIT("at") <+> ppr loc)]
 
 instance Outputable MetaDetails where
   ppr Flexi        = ptext SLIT("Flexi")
index 655a0bb..395df1e 100644 (file)
@@ -7,10 +7,10 @@
 module TcUnify (
        -- Full-blown subsumption
   tcSubPat, tcSubExp, tcGen, 
-  checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals,
+  checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt, 
 
        -- Various unifications
-  unifyTauTy, unifyTauTyList, 
+  unifyTauTy, unifyTauTyList, unifyTheta,
   unifyKind, unifyKinds, unifyFunKind, 
   checkExpectedKind,
 
@@ -38,10 +38,10 @@ import TcType               ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
                          SkolemInfo( GenSkol ), MetaDetails(..), 
                          pprSkolemTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
                          tcSplitAppTy_maybe, tcSplitTyConApp_maybe, 
-                         tyVarsOfType, mkPhiTy, mkTyVarTy, 
+                         tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
                          typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
                          tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
-                         pprType, isSkolemTyVar )
+                         pprType, tidySkolemTyVar, isSkolemTyVar )
 import Kind            ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
                          openTypeKind, liftedTypeKind, mkArrowKind, kindFunResult,
                          isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
@@ -49,8 +49,7 @@ import Kind           ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
 import Inst            ( newDicts, instToId, tcInstCall )
 import TcMType         ( condLookupTcTyVar, LookupTyVarResult(..),
                           putMetaTyVar, tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
-                         newTyFlexiVarTy, zonkTcKind, 
-                          zonkType, zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, 
+                         newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType,  zonkTcTyVarsAndFV, 
                          readKindVar, writeKindVar )
 import TcSimplify      ( tcSimplifyCheck )
 import TcEnv           ( tcGetGlobalTyVars, findGlobals )
@@ -58,14 +57,13 @@ import TyCon                ( TyCon, tyConArity, tyConTyVars )
 import TysWiredIn      ( listTyCon )
 import Id              ( Id, mkSysLocal )
 import Var             ( Var, varName, tyVarKind )
-import VarSet          ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, 
-                          varSetElems, intersectsVarSet, mkVarSet )
+import VarSet          ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
 import VarEnv
 import Name            ( isSystemName, mkSysTvName )
 import ErrUtils                ( Message )
 import SrcLoc          ( noLoc )
 import BasicTypes      ( Arity )
-import Util            ( notNull )
+import Util            ( notNull, equalLength )
 import Outputable
 \end{code}
 
@@ -556,12 +554,26 @@ tcGen :: TcSigmaType                              -- expected_ty
 
 tcGen expected_ty extra_tvs thing_inside       -- We expect expected_ty to be a forall-type
                                                -- If not, the call is a no-op
-  = do { span <- getSrcSpanM
-       ; let rigid_info = GenSkol expected_ty span
-       ; (forall_tvs, theta, phi_ty) <- tcSkolType rigid_info expected_ty
+  = do {       -- We want the GenSkol info in the skolemised type variables to 
+               -- mention the *instantiated* tyvar names, so that we get a
+               -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
+               -- Hence the tiresome but innocuous fixM
+         ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) ->
+               do { (forall_tvs, theta, rho_ty) <- tcSkolType skol_info expected_ty
+                  ; span <- getSrcSpanM
+                  ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span
+                  ; return ((forall_tvs, theta, rho_ty), skol_info) })
+
+#ifdef DEBUG
+       ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
+                                   text "expected_ty" <+> ppr expected_ty,
+                                   text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty,
+                                   text "free_tvs" <+> ppr free_tvs,
+                                   text "forall_tvs" <+> ppr forall_tvs])
+#endif
 
        -- Type-check the arg and unify with poly type
-       ; (result, lie) <- getLIE (thing_inside phi_ty)
+       ; (result, lie) <- getLIE (thing_inside rho_ty)
 
        -- Check that the "forall_tvs" havn't been constrained
        -- The interesting bit here is that we must include the free variables
@@ -574,18 +586,9 @@ tcGen expected_ty extra_tvs thing_inside   -- We expect expected_ty to be a forall
        -- Conclusion: include the free vars of the expected_ty in the
        -- list of "free vars" for the signature check.
 
-       ; dicts <- newDicts (SigOrigin rigid_info) theta
+       ; dicts <- newDicts (SigOrigin skol_info) theta
        ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
 
-#ifdef DEBUG
-       ; forall_tys <- zonkTcTyVars forall_tvs
-       ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
-                                   text "expected_ty" <+> ppr expected_ty,
-                                   text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr phi_ty,
-                                   text "free_tvs" <+> ppr free_tvs,
-                                   text "forall_tys" <+> ppr forall_tys])
-#endif
-
        ; checkSigTyVarsWrt free_tvs forall_tvs
        ; traceTc (text "tcGen:done")
 
@@ -623,6 +626,12 @@ unifyTauTy ty1 ty2         -- ty1 expected, ty2 inferred
     ASSERT2( isTauTy ty2, ppr ty2 )
     addErrCtxtM (unifyCtxt "type" ty1 ty2) $
     uTys True ty1 ty1 True ty2 ty2
+
+unifyTheta :: TcThetaType -> TcThetaType -> TcM ()
+unifyTheta theta1 theta2
+  = do { checkTc (equalLength theta1 theta2)
+                (ptext SLIT("Contexts differ in length"))
+       ; unifyTauTyLists True (map mkPredTy theta1) True (map mkPredTy theta2) }
 \end{code}
 
 @unifyTauTyList@ unifies corresponding elements of two lists of
@@ -1176,9 +1185,11 @@ ppr_ty env ty
             simple_result  = (env1, quotes (ppr tidy_ty), empty)
        ; case tidy_ty of
           TyVarTy tv 
-               | isSkolemTyVar tv -> return (env1, pp_rigid tv,
-                                             pprSkolemTyVar tv)
+               | isSkolemTyVar tv -> return (env2, pp_rigid tv',
+                                             pprSkolemTyVar tv')
                | otherwise -> return simple_result
+               where
+                 (env2, tv') = tidySkolemTyVar env1 tv
           other -> return simple_result }
   where
     pp_rigid tv = ptext SLIT("the rigid variable") <+> quotes (ppr tv)
@@ -1261,18 +1272,10 @@ checkExpectedKind ty act_kind exp_kind
 %*                                                                     *
 %************************************************************************
 
-@checkSigTyVars@ is used after the type in a type signature has been unified with
-the actual type found.  It then checks that the type variables of the type signature
-are
-       (a) Still all type variables
-               eg matching signature [a] against inferred type [(p,q)]
-               [then a will be unified to a non-type variable]
+@checkSigTyVars@ checks that a set of universally quantified type varaibles
+are not mentioned in the environment.  In particular:
 
-       (b) Still all distinct
-               eg matching signature [(a,b)] against inferred type [(p,p)]
-               [then a and b will be unified together]
-
-       (c) Not mentioned in the environment
+       (a) Not mentioned in the type of a variable in the envt
                eg the signature for f in this:
 
                        g x = ... where
@@ -1295,28 +1298,6 @@ are
 
 Before doing this, the substitution is applied to the signature type variable.
 
-We used to have the notion of a "DontBind" type variable, which would
-only be bound to itself or nothing.  Then points (a) and (b) were 
-self-checking.  But it gave rise to bogus consequential error messages.
-For example:
-
-   f = (*)     -- Monomorphic
-
-   g :: Num a => a -> a
-   g x = f x x
-
-Here, we get a complaint when checking the type signature for g,
-that g isn't polymorphic enough; but then we get another one when
-dealing with the (Num x) context arising from f's definition;
-we try to unify x with Int (to default it), but find that x has already
-been unified with the DontBind variable "a" from g's signature.
-This is really a problem with side-effecting unification; we'd like to
-undo g's effects when its type signature fails, but unification is done
-by side effect, so we can't (easily).
-
-So we revert to ordinary type variables for signatures, and try to
-give a helpful message in checkSigTyVars.
-
 \begin{code}
 checkSigTyVars :: [TcTyVar] -> TcM ()
 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
@@ -1331,82 +1312,60 @@ check_sig_tyvars
                        --      tyvars should not mention any of these
                        --      Guaranteed already zonked.
        -> [TcTyVar]    -- Universally-quantified type variables in the signature
-                       --      Not guaranteed zonked.
+                       --      Guaranteed to be skolems
        -> TcM ()
-
 check_sig_tyvars extra_tvs []
   = returnM ()
 check_sig_tyvars extra_tvs sig_tvs 
-  = do { gbl_tvs <- tcGetGlobalTyVars
+  = ASSERT( all isSkolemTyVar sig_tvs )
+    do { gbl_tvs <- tcGetGlobalTyVars
        ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
                                      text "gbl_tvs" <+> ppr gbl_tvs,
                                      text "extra_tvs" <+> ppr extra_tvs]))
 
-       -- Check that that the signature type vars are not free in the envt
        ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
-       ; checkM (not (mkVarSet sig_tvs `intersectsVarSet` env_tvs))
-                (complain sig_tvs env_tvs)
+       ; ifM (any (`elemVarSet` env_tvs) sig_tvs)
+             (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
+       }
 
-       ; ASSERT( all isSkolemTyVar sig_tvs )
-         return () }
+bleatEscapedTvs :: TcTyVarSet  -- The global tvs
+               -> [TcTyVar]    -- The possibly-escaping type variables
+               -> [TcTyVar]    -- The zonked versions thereof
+               -> TcM ()
+-- Complain about escaping type variables
+-- We pass a list of type variables, at least one of which
+-- escapes.  The first list contains the original signature type variable,
+-- while the second  contains the type variable it is unified to (usually itself)
+bleatEscapedTvs globals sig_tvs zonked_tvs
+  = do { (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs)
+       ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) }
   where
-    complain sig_tvs globals
-      = -- "check" checks each sig tyvar in turn
-        foldlM check
-              (env, emptyVarEnv, [])
-              tidy_tvs `thenM` \ (env2, _, msgs) ->
-
-        failWithTcM (env2, main_msg $$ nest 2 (vcat msgs))
-      where
-       (env, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
-
-       main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
-
-       check (tidy_env, acc, msgs) tv
-               -- sig_tyvar is from the signature;
-               -- ty is what you get if you zonk sig_tyvar and then tidy it
-               --
-               -- acc maps a zonked type variable back to a signature type variable
-         = case lookupVarEnv acc tv of {
-               Just sig_tyvar' ->      -- Error (b)!
-                       returnM (tidy_env, acc, unify_msg tv thing : msgs)
-                   where
-                       thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
-
-             ; Nothing ->
-
-           if tv `elemVarSet` globals  -- Error (c) or (d)! Type variable escapes
-                                       -- The least comprehensible, so put it last
-                       -- Game plan: 
-                       --       get the local TcIds and TyVars from the environment,
-                       --       and pass them to find_globals (they might have tv free)
-           then   
-                   findGlobals (unitVarSet tv) tidy_env        `thenM` \ (tidy_env1, globs) ->
-                       -- This rigid type variable has escaped into the envt
-                       -- We make it flexi so that subequent uses of these 
-                       -- variables don't give rise to a cascade of further errors
-                  returnM (tidy_env1, acc, escape_msg tv globs : msgs)
-
-           else        -- All OK
-           returnM (tidy_env, extendVarEnv acc tv tv, msgs)
-           }
-\end{code}
+    (env1, tidy_tvs)         = tidyOpenTyVars emptyTidyEnv sig_tvs
+    (env2, tidy_zonked_tvs) = tidyOpenTyVars env1        zonked_tvs
 
+    main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
+
+    check (tidy_env, msgs) (sig_tv, zonked_tv)
+      | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
+      | otherwise
+      = do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env
+          ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
 
-\begin{code}
 -----------------------
-escape_msg sig_tv globs
-  = mk_msg sig_tv <+> ptext SLIT("escapes") $$
-    if notNull globs then
-       vcat [ptext SLIT("It is mentioned in the environment:"), 
-             nest 2 (vcat globs)]
-     else
-       empty   -- Sigh.  It's really hard to give a good error message
-               -- all the time.   One bad case is an existential pattern match.
-               -- We rely on the "When..." context to help.
-
-unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
-mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
+escape_msg sig_tv zonked_tv globs
+  | notNull globs 
+  = vcat [sep [msg, ptext SLIT("is mentioned in the environment:")], 
+         nest 2 (vcat globs)]
+  | otherwise
+  = msg <+> ptext SLIT("escapes")
+       -- Sigh.  It's really hard to give a good error message
+       -- all the time.   One bad case is an existential pattern match.
+       -- We rely on the "When..." context to help.
+  where
+    msg = ptext SLIT("Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to
+    is_bound_to 
+       | sig_tv == zonked_tv = empty
+       | otherwise = ptext SLIT("is unified with") <+> quotes (ppr zonked_tv) <+> ptext SLIT("which")
 \end{code}
 
 These two context are used with checkSigTyVars
index a3487a4..45cd457 100644 (file)
@@ -33,7 +33,7 @@ import Kind
 import Var       ( Var, Id, TyVar, tyVarKind )
 import VarSet     ( TyVarSet )
 import Name      ( Name, NamedThing(..), BuiltInSyntax(..), mkWiredInName )
-import OccName   ( mkOccFS, tcName )
+import OccName   ( mkOccFS, tcName, parenSymOcc )
 import BasicTypes ( IPName, tupleParens )
 import TyCon     ( TyCon, mkFunTyCon, tyConArity, tupleTyConBoxity, isTupleTyCon, isRecursiveTyCon, isNewTyCon )
 import Class     ( Class )
@@ -317,7 +317,8 @@ pprPred (ClassP cls tys) = pprClassPred cls tys
 pprPred (IParam ip ty)   = ppr ip <> dcolon <> pprType ty
 
 pprClassPred :: Class -> [Type] -> SDoc
-pprClassPred clas tys = ppr clas <+> sep (map pprParendType tys)
+pprClassPred clas tys = parenSymOcc (getOccName clas) (ppr clas) 
+                       <+> sep (map pprParendType tys)
 
 pprTheta :: ThetaType -> SDoc
 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
@@ -394,13 +395,13 @@ ppr_tc_app p tc tys
     ppr_tc tc <+> sep (map (ppr_type TyConPrec) tys)
 
 ppr_tc :: TyCon -> SDoc
-ppr_tc tc
-  | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc 
-                               then ptext SLIT("<recnt>")
-                               else ptext SLIT("<nt>")
-                   ) <> ppr tc
-  | otherwise = ppr tc
-                              
+ppr_tc tc = parenSymOcc (getOccName tc) (pp_nt_debug <> ppr tc)
+  where
+   pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc 
+                                            then ptext SLIT("<recnt>")
+                                            else ptext SLIT("<nt>"))
+              | otherwise     = empty
+
 -------------------
 pprForAll []  = empty
 pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot