From 8e67f5502e2e316245806ee3735a2f41a844b611 Mon Sep 17 00:00:00 2001 From: simonpj Date: Fri, 25 Feb 2005 13:07:54 +0000 Subject: [PATCH] [project @ 2005-02-25 13:06:31 by simonpj] --------------------------------------------- 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. --- ghc/compiler/Makefile | 5 + ghc/compiler/basicTypes/Id.lhs | 6 +- ghc/compiler/basicTypes/MkId.lhs | 3 +- ghc/compiler/basicTypes/Name.lhs | 24 ++-- ghc/compiler/basicTypes/OccName.lhs | 14 ++- ghc/compiler/compMan/CompManager.lhs | 11 +- ghc/compiler/ghci/ByteCodeGen.lhs | 4 +- ghc/compiler/ghci/InteractiveUI.hs | 7 +- ghc/compiler/iface/IfaceSyn.lhs | 4 +- ghc/compiler/iface/IfaceType.lhs | 20 +++- ghc/compiler/typecheck/Inst.lhs | 34 +++--- ghc/compiler/typecheck/TcBinds.lhs | 192 ++++++++++++++++++------------- ghc/compiler/typecheck/TcEnv.lhs | 6 +- ghc/compiler/typecheck/TcHsSyn.lhs | 14 ++- ghc/compiler/typecheck/TcMType.lhs | 39 +++++-- ghc/compiler/typecheck/TcSimplify.lhs | 13 ++- ghc/compiler/typecheck/TcType.lhs | 26 ++++- ghc/compiler/typecheck/TcUnify.lhs | 199 +++++++++++++-------------------- ghc/compiler/types/TypeRep.lhs | 19 ++-- 19 files changed, 358 insertions(+), 282 deletions(-) diff --git a/ghc/compiler/Makefile b/ghc/compiler/Makefile index 4cff048..bc3ab8a 100644 --- a/ghc/compiler/Makefile +++ b/ghc/compiler/Makefile @@ -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. diff --git a/ghc/compiler/basicTypes/Id.lhs b/ghc/compiler/basicTypes/Id.lhs index cb848a1..63ef83f 100644 --- a/ghc/compiler/basicTypes/Id.lhs +++ b/ghc/compiler/basicTypes/Id.lhs @@ -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 diff --git a/ghc/compiler/basicTypes/MkId.lhs b/ghc/compiler/basicTypes/MkId.lhs index 46e957f..50e981b 100644 --- a/ghc/compiler/basicTypes/MkId.lhs +++ b/ghc/compiler/basicTypes/MkId.lhs @@ -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 diff --git a/ghc/compiler/basicTypes/Name.lhs b/ghc/compiler/basicTypes/Name.lhs index f0ef363..4ea51b6 100644 --- a/ghc/compiler/basicTypes/Name.lhs +++ b/ghc/compiler/basicTypes/Name.lhs @@ -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 diff --git a/ghc/compiler/basicTypes/OccName.lhs b/ghc/compiler/basicTypes/OccName.lhs index 2de02e7..29a6bbc 100644 --- a/ghc/compiler/basicTypes/OccName.lhs +++ b/ghc/compiler/basicTypes/OccName.lhs @@ -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} diff --git a/ghc/compiler/compMan/CompManager.lhs b/ghc/compiler/compMan/CompManager.lhs index 5bb0a98..829664d 100644 --- a/ghc/compiler/compMan/CompManager.lhs +++ b/ghc/compiler/compMan/CompManager.lhs @@ -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 ) diff --git a/ghc/compiler/ghci/ByteCodeGen.lhs b/ghc/compiler/ghci/ByteCodeGen.lhs index 5964884..5f9fe00 100644 --- a/ghc/compiler/ghci/ByteCodeGen.lhs +++ b/ghc/compiler/ghci/ByteCodeGen.lhs @@ -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) diff --git a/ghc/compiler/ghci/InteractiveUI.hs b/ghc/compiler/ghci/InteractiveUI.hs index 42f6b1b..a686e43 100644 --- a/ghc/compiler/ghci/InteractiveUI.hs +++ b/ghc/compiler/ghci/InteractiveUI.hs @@ -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) ----------------------------------------------------------------------------- diff --git a/ghc/compiler/iface/IfaceSyn.lhs b/ghc/compiler/iface/IfaceSyn.lhs index d4f5545..a538823 100644 --- a/ghc/compiler/iface/IfaceSyn.lhs +++ b/ghc/compiler/iface/IfaceSyn.lhs @@ -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 diff --git a/ghc/compiler/iface/IfaceType.lhs b/ghc/compiler/iface/IfaceType.lhs index 19226e9..b713908 100644 --- a/ghc/compiler/iface/IfaceType.lhs +++ b/ghc/compiler/iface/IfaceType.lhs @@ -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 diff --git a/ghc/compiler/typecheck/Inst.lhs b/ghc/compiler/typecheck/Inst.lhs index 4fb3f87..f75d1d3 100644 --- a/ghc/compiler/typecheck/Inst.lhs +++ b/ghc/compiler/typecheck/Inst.lhs @@ -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 diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs index f0de50a..a16cddc 100644 --- a/ghc/compiler/typecheck/TcBinds.lhs +++ b/ghc/compiler/typecheck/TcBinds.lhs @@ -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 ----------------------------------------------- diff --git a/ghc/compiler/typecheck/TcEnv.lhs b/ghc/compiler/typecheck/TcEnv.lhs index fe2cc1e..12192a9 100644 --- a/ghc/compiler/typecheck/TcEnv.lhs +++ b/ghc/compiler/typecheck/TcEnv.lhs @@ -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} diff --git a/ghc/compiler/typecheck/TcHsSyn.lhs b/ghc/compiler/typecheck/TcHsSyn.lhs index cf4fad9..59dfa9c 100644 --- a/ghc/compiler/typecheck/TcHsSyn.lhs +++ b/ghc/compiler/typecheck/TcHsSyn.lhs @@ -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} %************************************************************************ diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index 4db7ae3..2a3dc75 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -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 diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs index 4c0ca4b..dd4d215 100644 --- a/ghc/compiler/typecheck/TcSimplify.lhs +++ b/ghc/compiler/typecheck/TcSimplify.lhs @@ -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 diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index d31866d..ce31dd5 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -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") diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index 655a0bb..395df1e 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -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 diff --git a/ghc/compiler/types/TypeRep.lhs b/ghc/compiler/types/TypeRep.lhs index a3487a4..45cd457 100644 --- a/ghc/compiler/types/TypeRep.lhs +++ b/ghc/compiler/types/TypeRep.lhs @@ -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("") - else ptext SLIT("") - ) <> 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("") + else ptext SLIT("")) + | otherwise = empty + ------------------- pprForAll [] = empty pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot -- 1.7.10.4