From 95a15c7e7659505e4d70a004f567a05a7ccf41b2 Mon Sep 17 00:00:00 2001 From: Matthew Pickering Date: Fri, 12 May 2023 16:11:39 +0100 Subject: WIP --- compiler/GHC/Tc/Errors/Ppr.hs | 4 +- compiler/GHC/Tc/Errors/Types.hs | 46 +-- compiler/GHC/Tc/Errors/Types/PromotionErr.hs | 47 +++ compiler/GHC/Tc/Types.hs | 520 +-------------------------- compiler/GHC/Tc/Types.hs-boot | 8 - compiler/GHC/Tc/Types/Constraint.hs | 7 +- compiler/GHC/Tc/Types/LclEnv.hs | 261 ++++++++++++++ compiler/GHC/Tc/Types/TH.hs | 108 ++++++ compiler/GHC/Tc/Types/TcIdSigInfo.hs | 209 +++++++++++ compiler/GHC/Tc/Types/TcRef.hs | 8 + compiler/GHC/Tc/Types/TcTyThing.hs | 252 +++++++++++++ compiler/GHC/Tc/Utils/Monad.hs | 5 +- compiler/GHC/Types/LclEnv.hs | 0 compiler/ghc.cabal.in | 6 + 14 files changed, 913 insertions(+), 568 deletions(-) create mode 100644 compiler/GHC/Tc/Errors/Types/PromotionErr.hs create mode 100644 compiler/GHC/Tc/Types/LclEnv.hs create mode 100644 compiler/GHC/Tc/Types/TH.hs create mode 100644 compiler/GHC/Tc/Types/TcIdSigInfo.hs create mode 100644 compiler/GHC/Tc/Types/TcRef.hs create mode 100644 compiler/GHC/Tc/Types/TcTyThing.hs create mode 100644 compiler/GHC/Types/LclEnv.hs diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs index 269063ae65..bc59436bc4 100644 --- a/compiler/GHC/Tc/Errors/Ppr.hs +++ b/compiler/GHC/Tc/Errors/Ppr.hs @@ -56,7 +56,8 @@ import GHC.Hs import GHC.Tc.Errors.Types import GHC.Tc.Types.Constraint -import {-# SOURCE #-} GHC.Tc.Types( getLclEnvLoc, lclEnvInGeneratedCode, TcTyThing ) +import {-# SOURCE #-} GHC.Tc.Types( getLclEnvLoc, lclEnvInGeneratedCode ) +import GHC.Tc.Types.TcTyThing import GHC.Tc.Types.Origin import GHC.Tc.Types.Rank (Rank(..)) import GHC.Tc.Utils.TcType @@ -103,7 +104,6 @@ import Data.List ( groupBy, sortBy, tails import Data.Ord ( comparing ) import Data.Bifunctor import qualified Language.Haskell.TH as TH -import {-# SOURCE #-} GHC.Tc.Types (pprTcTyThingCategory) import GHC.Iface.Errors.Types import GHC.Iface.Errors.Ppr diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs index 68c5ca2869..772c5fdbb8 100644 --- a/compiler/GHC/Tc/Errors/Types.hs +++ b/compiler/GHC/Tc/Errors/Types.hs @@ -124,7 +124,7 @@ module GHC.Tc.Errors.Types ( import GHC.Prelude import GHC.Hs -import {-# SOURCE #-} GHC.Tc.Types (TcIdSigInfo, TcTyThing) +import GHC.Tc.Types.TcTyThing -- (TcIdSigInfo, TcTyThing) import {-# SOURCE #-} GHC.Tc.Errors.Hole.FitTypes (HoleFit) import GHC.Tc.Types.Constraint import GHC.Tc.Types.Evidence (EvBindsVar) @@ -178,6 +178,10 @@ import GHC.Unit.Module.ModIface import GHC.Generics ( Generic ) import GHC.Types.Name.Env (NameEnv) import GHC.Iface.Errors.Types +import GHC.Tc.Errors.Types.PromotionErr +import GHC.Tc.Types.TcIdSigInfo + + {- Note [Migrating TcM Messages] @@ -5186,46 +5190,6 @@ discardMsg :: SDoc discardMsg = text "(Some bindings suppressed;" <+> text "use -fmax-relevant-binds=N or -fno-max-relevant-binds)" -data PromotionErr - = TyConPE -- TyCon used in a kind before we are ready - -- data T :: T -> * where ... - | ClassPE -- Ditto Class - - | FamDataConPE -- Data constructor for a data family - -- See Note [AFamDataCon: not promoting data family constructors] - -- in GHC.Tc.Utils.Env. - | ConstrainedDataConPE ThetaType -- Data constructor with a context - -- See Note [No constraints in kinds] in GHC.Tc.Validity - | PatSynPE -- Pattern synonyms - -- See Note [Don't promote pattern synonyms] in GHC.Tc.Utils.Env - - | RecDataConPE -- Data constructor in a recursive loop - -- See Note [Recursion and promoting data constructors] in GHC.Tc.TyCl - | TermVariablePE -- See Note [Promoted variables in types] - | NoDataKindsDC -- -XDataKinds not enabled (for a datacon) - -instance Outputable PromotionErr where - ppr ClassPE = text "ClassPE" - ppr TyConPE = text "TyConPE" - ppr PatSynPE = text "PatSynPE" - ppr FamDataConPE = text "FamDataConPE" - ppr (ConstrainedDataConPE theta) = text "ConstrainedDataConPE" <+> parens (ppr theta) - ppr RecDataConPE = text "RecDataConPE" - ppr NoDataKindsDC = text "NoDataKindsDC" - ppr TermVariablePE = text "TermVariablePE" - -pprPECategory :: PromotionErr -> SDoc -pprPECategory = text . capitalise . peCategory - -peCategory :: PromotionErr -> String -peCategory ClassPE = "class" -peCategory TyConPE = "type constructor" -peCategory PatSynPE = "pattern synonym" -peCategory FamDataConPE = "data constructor" -peCategory ConstrainedDataConPE{} = "data constructor" -peCategory RecDataConPE = "data constructor" -peCategory NoDataKindsDC = "data constructor" -peCategory TermVariablePE = "term variable" -- | Stores the information to be reported in a representation-polymorphism -- error message. diff --git a/compiler/GHC/Tc/Errors/Types/PromotionErr.hs b/compiler/GHC/Tc/Errors/Types/PromotionErr.hs new file mode 100644 index 0000000000..2de61c5aa3 --- /dev/null +++ b/compiler/GHC/Tc/Errors/Types/PromotionErr.hs @@ -0,0 +1,47 @@ +module GHC.Tc.Errors.Types.PromotionErr where + +import GHC.Prelude +import GHC.Core.Type (ThetaType) +import GHC.Utils.Outputable +import GHC.Utils.Misc + +data PromotionErr + = TyConPE -- TyCon used in a kind before we are ready + -- data T :: T -> * where ... + | ClassPE -- Ditto Class + + | FamDataConPE -- Data constructor for a data family + -- See Note [AFamDataCon: not promoting data family constructors] + -- in GHC.Tc.Utils.Env. + | ConstrainedDataConPE ThetaType -- Data constructor with a context + -- See Note [No constraints in kinds] in GHC.Tc.Validity + | PatSynPE -- Pattern synonyms + -- See Note [Don't promote pattern synonyms] in GHC.Tc.Utils.Env + + | RecDataConPE -- Data constructor in a recursive loop + -- See Note [Recursion and promoting data constructors] in GHC.Tc.TyCl + | TermVariablePE -- See Note [Promoted variables in types] + | NoDataKindsDC -- -XDataKinds not enabled (for a datacon) + +instance Outputable PromotionErr where + ppr ClassPE = text "ClassPE" + ppr TyConPE = text "TyConPE" + ppr PatSynPE = text "PatSynPE" + ppr FamDataConPE = text "FamDataConPE" + ppr (ConstrainedDataConPE theta) = text "ConstrainedDataConPE" <+> parens (ppr theta) + ppr RecDataConPE = text "RecDataConPE" + ppr NoDataKindsDC = text "NoDataKindsDC" + ppr TermVariablePE = text "TermVariablePE" + +pprPECategory :: PromotionErr -> SDoc +pprPECategory = text . capitalise . peCategory + +peCategory :: PromotionErr -> String +peCategory ClassPE = "class" +peCategory TyConPE = "type constructor" +peCategory PatSynPE = "pattern synonym" +peCategory FamDataConPE = "data constructor" +peCategory ConstrainedDataConPE{} = "data constructor" +peCategory RecDataConPE = "data constructor" +peCategory NoDataKindsDC = "data constructor" +peCategory TermVariablePE = "term variable" \ No newline at end of file diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs index a6bab74fc0..f30e891753 100644 --- a/compiler/GHC/Tc/Types.hs +++ b/compiler/GHC/Tc/Types.hs @@ -177,6 +177,12 @@ import qualified Language.Haskell.TH as TH import GHC.Driver.Env.KnotVars import GHC.Linker.Types +import GHC.Tc.Types.TcTyThing +import GHC.Tc.Types.TcIdSigInfo +import GHC.Tc.Types.TH +import GHC.Tc.Types.TcRef +import GHC.Tc.Types.LclEnv () + -- | A 'NameShape' is a substitution on 'Name's that can be used -- to refine the identities of a hole while we are renaming interfaces -- (see "GHC.Iface.Rename"). Specifically, a 'NameShape' for @@ -899,10 +905,6 @@ pass it inwards. -} --- | Type alias for 'IORef'; the convention is we'll use this for mutable --- bits of data in 'TcGblEnv' which are updated during typechecking and --- returned at the end. -type TcRef a = IORef a -- ToDo: when should I refer to it as a 'TcId' instead of an 'Id'? type TcId = Id type TcIdSet = IdSet @@ -969,103 +971,6 @@ removeBindingShadowing bindings = reverse $ fst $ foldl getPlatform :: TcRnIf a b Platform getPlatform = targetPlatform <$> getDynFlags ---------------------------- --- Template Haskell stages and levels ---------------------------- - -data SpliceType = Typed | Untyped - -data ThStage -- See Note [Template Haskell state diagram] - -- and Note [Template Haskell levels] in GHC.Tc.Gen.Splice - -- Start at: Comp - -- At bracket: wrap current stage in Brack - -- At splice: currently Brack: return to previous stage - -- currently Comp/Splice: compile and run - = Splice SpliceType -- Inside a top-level splice - -- This code will be run *at compile time*; - -- the result replaces the splice - -- Binding level = 0 - - | RunSplice (TcRef [ForeignRef (TH.Q ())]) - -- Set when running a splice, i.e. NOT when renaming or typechecking the - -- Haskell code for the splice. See Note [RunSplice ThLevel]. - -- - -- Contains a list of mod finalizers collected while executing the splice. - -- - -- 'addModFinalizer' inserts finalizers here, and from here they are taken - -- to construct an @HsSpliced@ annotation for untyped splices. See Note - -- [Delaying modFinalizers in untyped splices] in GHC.Rename.Splice. - -- - -- For typed splices, the typechecker takes finalizers from here and - -- inserts them in the list of finalizers in the global environment. - -- - -- See Note [Collecting modFinalizers in typed splices] in "GHC.Tc.Gen.Splice". - - | Comp -- Ordinary Haskell code - -- Binding level = 1 - - | Brack -- Inside brackets - ThStage -- Enclosing stage - PendingStuff - -data PendingStuff - = RnPendingUntyped -- Renaming the inside of an *untyped* bracket - (TcRef [PendingRnSplice]) -- Pending splices in here - - | RnPendingTyped -- Renaming the inside of a *typed* bracket - - | TcPending -- Typechecking the inside of a typed bracket - (TcRef [PendingTcSplice]) -- Accumulate pending splices here - (TcRef WantedConstraints) -- and type constraints here - QuoteWrapper -- A type variable and evidence variable - -- for the overall monad of - -- the bracket. Splices are checked - -- against this monad. The evidence - -- variable is used for desugaring - -- `lift`. - - -topStage, topAnnStage, topSpliceStage :: ThStage -topStage = Comp -topAnnStage = Splice Untyped -topSpliceStage = Splice Untyped - -instance Outputable ThStage where - ppr (Splice _) = text "Splice" - ppr (RunSplice _) = text "RunSplice" - ppr Comp = text "Comp" - ppr (Brack s _) = text "Brack" <> parens (ppr s) - -type ThLevel = Int - -- NB: see Note [Template Haskell levels] in GHC.Tc.Gen.Splice - -- Incremented when going inside a bracket, - -- decremented when going inside a splice - -- NB: ThLevel is one greater than the 'n' in Fig 2 of the - -- original "Template meta-programming for Haskell" paper - -impLevel, outerLevel :: ThLevel -impLevel = 0 -- Imported things; they can be used inside a top level splice -outerLevel = 1 -- Things defined outside brackets - -thLevel :: ThStage -> ThLevel -thLevel (Splice _) = 0 -thLevel Comp = 1 -thLevel (Brack s _) = thLevel s + 1 -thLevel (RunSplice _) = panic "thLevel: called when running a splice" - -- See Note [RunSplice ThLevel]. - -{- Note [RunSplice ThLevel] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The 'RunSplice' stage is set when executing a splice, and only when running a -splice. In particular it is not set when the splice is renamed or typechecked. - -'RunSplice' is needed to provide a reference where 'addModFinalizer' can insert -the finalizer (see Note [Delaying modFinalizers in untyped splices]), and -'addModFinalizer' runs when doing Q things. Therefore, It doesn't make sense to -set 'RunSplice' when renaming or typechecking the splice, where 'Splice', -'Brack' or 'Comp' are used instead. - --} --------------------------- -- Arrow-notation context @@ -1107,234 +1012,6 @@ from further out in the ArrowCtxt that we push inwards. data ArrowCtxt -- Note [Escaping the arrow scope] = NoArrowCtxt | ArrowCtxt LocalRdrEnv (TcRef WantedConstraints) - - ---------------------------- --- TcTyThing ---------------------------- - --- | A typecheckable thing available in a local context. Could be --- 'AGlobal' 'TyThing', but also lexically scoped variables, etc. --- See "GHC.Tc.Utils.Env" for how to retrieve a 'TyThing' given a 'Name'. -data TcTyThing - = AGlobal TyThing -- Used only in the return type of a lookup - - | ATcId -- Ids defined in this module; may not be fully zonked - { tct_id :: TcId - , tct_info :: IdBindingInfo -- See Note [Meaning of IdBindingInfo] - } - - | ATyVar Name TcTyVar -- See Note [Type variables in the type environment] - - | ATcTyCon TyCon -- Used temporarily, during kind checking, for the - -- tycons and classes in this recursive group - -- The TyCon is always a TcTyCon. Its kind - -- can be a mono-kind or a poly-kind; in TcTyClsDcls see - -- Note [Type checking recursive type and class declarations] - - | APromotionErr PromotionErr - --- | Matches on either a global 'TyCon' or a 'TcTyCon'. -tcTyThingTyCon_maybe :: TcTyThing -> Maybe TyCon -tcTyThingTyCon_maybe (AGlobal (ATyCon tc)) = Just tc -tcTyThingTyCon_maybe (ATcTyCon tc_tc) = Just tc_tc -tcTyThingTyCon_maybe _ = Nothing - -instance Outputable TcTyThing where -- Debugging only - ppr (AGlobal g) = ppr g - ppr elt@(ATcId {}) = text "Identifier" <> - brackets (ppr (tct_id elt) <> dcolon - <> ppr (varType (tct_id elt)) <> comma - <+> ppr (tct_info elt)) - ppr (ATyVar n tv) = text "Type variable" <+> quotes (ppr n) <+> equals <+> ppr tv - <+> dcolon <+> ppr (varType tv) - ppr (ATcTyCon tc) = text "ATcTyCon" <+> ppr tc <+> dcolon <+> ppr (tyConKind tc) - ppr (APromotionErr err) = text "APromotionErr" <+> ppr err - --- | IdBindingInfo describes how an Id is bound. --- --- It is used for the following purposes: --- a) for static forms in 'GHC.Tc.Gen.Expr.checkClosedInStaticForm' and --- b) to figure out when a nested binding can be generalised, --- in 'GHC.Tc.Gen.Bind.decideGeneralisationPlan'. --- -data IdBindingInfo -- See Note [Meaning of IdBindingInfo] - = NotLetBound - | ClosedLet - | NonClosedLet - RhsNames -- Used for (static e) checks only - ClosedTypeId -- Used for generalisation checks - -- and for (static e) checks - --- | IsGroupClosed describes a group of mutually-recursive bindings -data IsGroupClosed - = IsGroupClosed - (NameEnv RhsNames) -- Free var info for the RHS of each binding in the group - -- Used only for (static e) checks - - ClosedTypeId -- True <=> all the free vars of the group are - -- imported or ClosedLet or - -- NonClosedLet with ClosedTypeId=True. - -- In particular, no tyvars, no NotLetBound - -type RhsNames = NameSet -- Names of variables, mentioned on the RHS of - -- a definition, that are not Global or ClosedLet - -type ClosedTypeId = Bool - -- See Note [Meaning of IdBindingInfo] - -{- Note [Meaning of IdBindingInfo] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -NotLetBound means that - the Id is not let-bound (e.g. it is bound in a - lambda-abstraction or in a case pattern) - -ClosedLet means that - - The Id is let-bound, - - Any free term variables are also Global or ClosedLet - - Its type has no free variables (NB: a top-level binding subject - to the MR might have free vars in its type) - These ClosedLets can definitely be floated to top level; and we - may need to do so for static forms. - - Property: ClosedLet - is equivalent to - NonClosedLet emptyNameSet True - -(NonClosedLet (fvs::RhsNames) (cl::ClosedTypeId)) means that - - The Id is let-bound - - - The fvs::RhsNames contains the free names of the RHS, - excluding Global and ClosedLet ones. - - - For the ClosedTypeId field see Note [Bindings with closed types: ClosedTypeId] - -For (static e) to be valid, we need for every 'x' free in 'e', -that x's binding is floatable to the top level. Specifically: - * x's RhsNames must be empty - * x's type has no free variables -See Note [Grand plan for static forms] in "GHC.Iface.Tidy.StaticPtrTable". -This test is made in GHC.Tc.Gen.Expr.checkClosedInStaticForm. -Actually knowing x's RhsNames (rather than just its emptiness -or otherwise) is just so we can produce better error messages - -Note [Bindings with closed types: ClosedTypeId] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - - f x = let g ys = map not ys - in ... - -Can we generalise 'g' under the OutsideIn algorithm? Yes, -because all g's free variables are top-level; that is they themselves -have no free type variables, and it is the type variables in the -environment that makes things tricky for OutsideIn generalisation. - -Here's the invariant: - If an Id has ClosedTypeId=True (in its IdBindingInfo), then - the Id's type is /definitely/ closed (has no free type variables). - Specifically, - a) The Id's actual type is closed (has no free tyvars) - b) Either the Id has a (closed) user-supplied type signature - or all its free variables are Global/ClosedLet - or NonClosedLet with ClosedTypeId=True. - In particular, none are NotLetBound. - -Why is (b) needed? Consider - \x. (x :: Int, let y = x+1 in ...) -Initially x::alpha. If we happen to typecheck the 'let' before the -(x::Int), y's type will have a free tyvar; but if the other way round -it won't. So we treat any let-bound variable with a free -non-let-bound variable as not ClosedTypeId, regardless of what the -free vars of its type actually are. - -But if it has a signature, all is well: - \x. ...(let { y::Int; y = x+1 } in - let { v = y+2 } in ...)... -Here the signature on 'v' makes 'y' a ClosedTypeId, so we can -generalise 'v'. - -Note that: - - * A top-level binding may not have ClosedTypeId=True, if it suffers - from the MR - - * A nested binding may be closed (eg 'g' in the example we started - with). Indeed, that's the point; whether a function is defined at - top level or nested is orthogonal to the question of whether or - not it is closed. - - * A binding may be non-closed because it mentions a lexically scoped - *type variable* Eg - f :: forall a. blah - f x = let g y = ...(y::a)... - -Under OutsideIn we are free to generalise an Id all of whose free -variables have ClosedTypeId=True (or imported). This is an extension -compared to the JFP paper on OutsideIn, which used "top-level" as a -proxy for "closed". (It's not a good proxy anyway -- the MR can make -a top-level binding with a free type variable.) - -Note [Type variables in the type environment] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The type environment has a binding for each lexically-scoped -type variable that is in scope. For example - - f :: forall a. a -> a - f x = (x :: a) - - g1 :: [a] -> a - g1 (ys :: [b]) = head ys :: b - - g2 :: [Int] -> Int - g2 (ys :: [c]) = head ys :: c - -* The forall'd variable 'a' in the signature scopes over f's RHS. - -* The pattern-bound type variable 'b' in 'g1' scopes over g1's - RHS; note that it is bound to a skolem 'a' which is not itself - lexically in scope. - -* The pattern-bound type variable 'c' in 'g2' is bound to - Int; that is, pattern-bound type variables can stand for - arbitrary types. (see - GHC proposal #128 "Allow ScopedTypeVariables to refer to types" - https://github.com/ghc-proposals/ghc-proposals/pull/128, - and the paper - "Type variables in patterns", Haskell Symposium 2018. - - -This is implemented by the constructor - ATyVar Name TcTyVar -in the type environment. - -* The Name is the name of the original, lexically scoped type - variable - -* The TcTyVar is sometimes a skolem (like in 'f'), and sometimes - a unification variable (like in 'g1', 'g2'). We never zonk the - type environment so in the latter case it always stays as a - unification variable, although that variable may be later - unified with a type (such as Int in 'g2'). --} - -instance Outputable IdBindingInfo where - ppr NotLetBound = text "NotLetBound" - ppr ClosedLet = text "TopLevelLet" - ppr (NonClosedLet fvs closed_type) = - text "TopLevelLet" <+> ppr fvs <+> ppr closed_type - --------------- -pprTcTyThingCategory :: TcTyThing -> SDoc -pprTcTyThingCategory = text . capitalise . tcTyThingCategory - -tcTyThingCategory :: TcTyThing -> String -tcTyThingCategory (AGlobal thing) = tyThingCategory thing -tcTyThingCategory (ATyVar {}) = "type variable" -tcTyThingCategory (ATcId {}) = "local identifier" -tcTyThingCategory (ATcTyCon {}) = "local tycon" -tcTyThingCategory (APromotionErr pe) = peCategory pe - {- ************************************************************************ * * @@ -1429,191 +1106,6 @@ instance Outputable WhereFrom where ppr ImportByPlugin = text "{- PLUGIN -}" -{- ********************************************************************* -* * - Type signatures -* * -********************************************************************* -} - --- These data types need to be here only because --- GHC.Tc.Solver uses them, and GHC.Tc.Solver is fairly --- low down in the module hierarchy - -type TcSigFun = Name -> Maybe TcSigInfo - -data TcSigInfo = TcIdSig TcIdSigInfo - | TcPatSynSig TcPatSynInfo - -data TcIdSigInfo -- See Note [Complete and partial type signatures] - = CompleteSig -- A complete signature with no wildcards, - -- so the complete polymorphic type is known. - { sig_bndr :: TcId -- The polymorphic Id with that type - - , sig_ctxt :: UserTypeCtxt -- In the case of type-class default methods, - -- the Name in the FunSigCtxt is not the same - -- as the TcId; the former is 'op', while the - -- latter is '$dmop' or some such - - , sig_loc :: SrcSpan -- Location of the type signature - } - - | PartialSig -- A partial type signature (i.e. includes one or more - -- wildcards). In this case it doesn't make sense to give - -- the polymorphic Id, because we are going to /infer/ its - -- type, so we can't make the polymorphic Id ab-initio - { psig_name :: Name -- Name of the function; used when report wildcards - , psig_hs_ty :: LHsSigWcType GhcRn -- The original partial signature in - -- HsSyn form - , sig_ctxt :: UserTypeCtxt - , sig_loc :: SrcSpan -- Location of the type signature - } - - -{- Note [Complete and partial type signatures] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A type signature is partial when it contains one or more wildcards -(= type holes). The wildcard can either be: -* A (type) wildcard occurring in sig_theta or sig_tau. These are - stored in sig_wcs. - f :: Bool -> _ - g :: Eq _a => _a -> _a -> Bool -* Or an extra-constraints wildcard, stored in sig_cts: - h :: (Num a, _) => a -> a - -A type signature is a complete type signature when there are no -wildcards in the type signature, i.e. iff sig_wcs is empty and -sig_extra_cts is Nothing. --} - -data TcIdSigInst - = TISI { sig_inst_sig :: TcIdSigInfo - - , sig_inst_skols :: [(Name, InvisTVBinder)] - -- Instantiated type and kind variables, TyVarTvs - -- The Name is the Name that the renamer chose; - -- but the TcTyVar may come from instantiating - -- the type and hence have a different unique. - -- No need to keep track of whether they are truly lexically - -- scoped because the renamer has named them uniquely - -- See Note [Binding scoped type variables] in GHC.Tc.Gen.Sig - -- - -- NB: The order of sig_inst_skols is irrelevant - -- for a CompleteSig, but for a PartialSig see - -- Note [Quantified variables in partial type signatures] - - , sig_inst_theta :: TcThetaType - -- Instantiated theta. In the case of a - -- PartialSig, sig_theta does not include - -- the extra-constraints wildcard - - , sig_inst_tau :: TcSigmaType -- Instantiated tau - -- See Note [sig_inst_tau may be polymorphic] - - -- Relevant for partial signature only - , sig_inst_wcs :: [(Name, TcTyVar)] - -- Like sig_inst_skols, but for /named/ wildcards (_a etc). - -- The named wildcards scope over the binding, and hence - -- their Names may appear in type signatures in the binding - - , sig_inst_wcx :: Maybe TcType - -- Extra-constraints wildcard to fill in, if any - -- If this exists, it is surely of the form (meta_tv |> co) - -- (where the co might be reflexive). This is filled in - -- only from the return value of GHC.Tc.Gen.HsType.tcAnonWildCardOcc - } - -{- Note [sig_inst_tau may be polymorphic] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Note that "sig_inst_tau" might actually be a polymorphic type, -if the original function had a signature like - forall a. Eq a => forall b. Ord b => .... -But that's ok: tcMatchesFun (called by tcRhs) can deal with that -It happens, too! See Note [Polymorphic methods] in GHC.Tc.TyCl.Class. - -Note [Quantified variables in partial type signatures] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - f :: forall a b. _ -> a -> _ -> b - f (x,y) p q = q - -Then we expect f's final type to be - f :: forall {x,y}. forall a b. (x,y) -> a -> b -> b - -Note that x,y are Inferred, and can't be use for visible type -application (VTA). But a,b are Specified, and remain Specified -in the final type, so we can use VTA for them. (Exception: if -it turns out that a's kind mentions b we need to reorder them -with scopedSort.) - -The sig_inst_skols of the TISI from a partial signature records -that original order, and is used to get the variables of f's -final type in the correct order. - - -Note [Wildcards in partial signatures] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The wildcards in psig_wcs may stand for a type mentioning -the universally-quantified tyvars of psig_ty - -E.g. f :: forall a. _ -> a - f x = x -We get sig_inst_skols = [a] - sig_inst_tau = _22 -> a - sig_inst_wcs = [_22] -and _22 in the end is unified with the type 'a' - -Moreover the kind of a wildcard in sig_inst_wcs may mention -the universally-quantified tyvars sig_inst_skols -e.g. f :: t a -> t _ -Here we get - sig_inst_skols = [k:*, (t::k ->*), (a::k)] - sig_inst_tau = t a -> t _22 - sig_inst_wcs = [ _22::k ] --} - -data TcPatSynInfo - = TPSI { - patsig_name :: Name, - patsig_implicit_bndrs :: [InvisTVBinder], -- Implicitly-bound kind vars (Inferred) and - -- implicitly-bound type vars (Specified) - -- See Note [The pattern-synonym signature splitting rule] in GHC.Tc.TyCl.PatSyn - patsig_univ_bndrs :: [InvisTVBinder], -- Bound by explicit user forall - patsig_req :: TcThetaType, - patsig_ex_bndrs :: [InvisTVBinder], -- Bound by explicit user forall - patsig_prov :: TcThetaType, - patsig_body_ty :: TcSigmaType - } - -instance Outputable TcSigInfo where - ppr (TcIdSig idsi) = ppr idsi - ppr (TcPatSynSig tpsi) = text "TcPatSynInfo" <+> ppr tpsi - -instance Outputable TcIdSigInfo where - ppr (CompleteSig { sig_bndr = bndr }) - = ppr bndr <+> dcolon <+> ppr (idType bndr) - ppr (PartialSig { psig_name = name, psig_hs_ty = hs_ty }) - = text "psig" <+> ppr name <+> dcolon <+> ppr hs_ty - -instance Outputable TcIdSigInst where - ppr (TISI { sig_inst_sig = sig, sig_inst_skols = skols - , sig_inst_theta = theta, sig_inst_tau = tau }) - = hang (ppr sig) 2 (vcat [ ppr skols, ppr theta <+> darrow <+> ppr tau ]) - -instance Outputable TcPatSynInfo where - ppr (TPSI{ patsig_name = name}) = ppr name - -isPartialSig :: TcIdSigInst -> Bool -isPartialSig (TISI { sig_inst_sig = PartialSig {} }) = True -isPartialSig _ = False - --- | No signature or a partial signature -hasCompleteSig :: TcSigFun -> Name -> Bool -hasCompleteSig sig_fn name - = case sig_fn name of - Just (TcIdSig (CompleteSig {})) -> True - _ -> False - - {- Constraint Solver Plugins ------------------------- diff --git a/compiler/GHC/Tc/Types.hs-boot b/compiler/GHC/Tc/Types.hs-boot index 68902e98ae..7a96132e00 100644 --- a/compiler/GHC/Tc/Types.hs-boot +++ b/compiler/GHC/Tc/Types.hs-boot @@ -3,18 +3,11 @@ module GHC.Tc.Types where import GHC.Prelude import GHC.Tc.Utils.TcType import GHC.Types.SrcLoc -import GHC.Utils.Outputable data TcLclEnv data SelfBootInfo -data TcIdSigInfo -instance Outputable TcIdSigInfo - -data TcTyThing -instance Outputable TcTyThing - setLclEnvTcLevel :: TcLclEnv -> TcLevel -> TcLclEnv getLclEnvTcLevel :: TcLclEnv -> TcLevel @@ -22,4 +15,3 @@ setLclEnvLoc :: TcLclEnv -> RealSrcSpan -> TcLclEnv getLclEnvLoc :: TcLclEnv -> RealSrcSpan lclEnvInGeneratedCode :: TcLclEnv -> Bool -pprTcTyThingCategory :: TcTyThing -> SDoc diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index d99f9067df..f47fb1c147 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -68,7 +68,7 @@ module GHC.Tc.Types.Constraint ( ctLocTypeOrKind_maybe, ctLocDepth, bumpCtLocDepth, isGivenLoc, setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan, - pprCtLoc, + pprCtLoc, CtLocEnv(..), -- CtEvidence CtEvidence(..), TcEvDest(..), @@ -143,6 +143,7 @@ import Data.Word ( Word8 ) import Data.List ( intersperse ) + {- ************************************************************************ * * @@ -2417,10 +2418,12 @@ dictionaries don't appear in the original source code. -} data CtLoc = CtLoc { ctl_origin :: CtOrigin - , ctl_env :: TcLclEnv + , ctl_env :: CtLocEnv , ctl_t_or_k :: Maybe TypeOrKind -- OK if we're not sure , ctl_depth :: !SubGoalDepth } +data CtLocEnv = CtLocEnv { ct_ctxt :: [()], ctl_loc :: RealSrcSpan, ctl_bndrs :: TcBinderStack, ctl_tclvl :: TcLevel } + -- The TcLclEnv includes particularly -- source location: tcl_loc :: RealSrcSpan -- context: tcl_ctxt :: [ErrCtxt] diff --git a/compiler/GHC/Tc/Types/LclEnv.hs b/compiler/GHC/Tc/Types/LclEnv.hs new file mode 100644 index 0000000000..4f803244c7 --- /dev/null +++ b/compiler/GHC/Tc/Types/LclEnv.hs @@ -0,0 +1,261 @@ +module GHC.Tc.Types.LclEnv where + +import GHC.Prelude ( Bool, IO ) + + + +import GHC.Tc.Utils.TcType ( TcLevel, ExpType ) +import GHC.Tc.Types.Constraint ( WantedConstraints ) +import GHC.Tc.Errors.Types ( TcRnMessage ) + +import GHC.Core.Type ( TyVar ) +import GHC.Core.UsageEnv ( UsageEnv ) + +import GHC.Types.Id ( idName ) +import GHC.Types.Name.Reader ( LocalRdrEnv ) +import GHC.Types.Name ( Name, HasOccName(..) ) +import GHC.Types.Name.Env ( NameEnv ) +import GHC.Types.Var ( Id ) +import GHC.Types.Var.Env ( TidyEnv ) +import GHC.Types.SrcLoc ( RealSrcSpan ) +import GHC.Types.Basic ( TopLevelFlag ) + +import GHC.Data.IOEnv ( IORef ) + + +import GHC.Utils.Error ( Messages, SDoc ) +import GHC.Utils.Outputable + ( Outputable(..), IsLine((<+>), (<>)), brackets ) + + + +import GHC.Tc.Types.TcTyThing ( TcTyThing ) +import GHC.Tc.Types.TH ( ThStage, ThLevel ) + +{- +************************************************************************ +* * + The local typechecker environment +* * +************************************************************************ + +Note [The Global-Env/Local-Env story] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +During type checking, we keep in the tcg_type_env + * All types and classes + * All Ids derived from types and classes (constructors, selectors) + +At the end of type checking, we zonk the local bindings, +and as we do so we add to the tcg_type_env + * Locally defined top-level Ids + +Why? Because they are now Ids not TcIds. This final GlobalEnv is + a) fed back (via the knot) to typechecking the + unfoldings of interface signatures + b) used in the ModDetails of this module +-} + +data TcLclEnv -- Changes as we move inside an expression + -- Discarded after typecheck/rename; not passed on to desugarer + = TcLclEnv { + tcl_loc :: RealSrcSpan, -- Source span + tcl_ctxt :: [ErrCtxt], -- Error context, innermost on top + tcl_in_gen_code :: Bool, -- See Note [Rebindable syntax and HsExpansion] + tcl_tclvl :: TcLevel, + + tcl_th_ctxt :: ThStage, -- Template Haskell context + tcl_th_bndrs :: ThBindEnv, -- and binder info + -- The ThBindEnv records the TH binding level of in-scope Names + -- defined in this module (not imported) + -- We can't put this info in the TypeEnv because it's needed + -- (and extended) in the renamer, for untyped splices + + tcl_arrow_ctxt :: ArrowCtxt, -- Arrow-notation context + + tcl_rdr :: LocalRdrEnv, -- Local name envt + -- Maintained during renaming, of course, but also during + -- type checking, solely so that when renaming a Template-Haskell + -- splice we have the right environment for the renamer. + -- + -- Does *not* include global name envt; may shadow it + -- Includes both ordinary variables and type variables; + -- they are kept distinct because tyvar have a different + -- occurrence constructor (Name.TvOcc) + -- We still need the unsullied global name env so that + -- we can look up record field names + + tcl_env :: TcTypeEnv, -- The local type environment: + -- Ids and TyVars defined in this module + + tcl_usage :: TcRef UsageEnv, -- Required multiplicity of bindings is accumulated here. + + + tcl_bndrs :: TcBinderStack, -- Used for reporting relevant bindings, + -- and for tidying types + + tcl_lie :: TcRef WantedConstraints, -- Place to accumulate type constraints + tcl_errs :: TcRef (Messages TcRnMessage) -- Place to accumulate diagnostics + } + +setLclEnvTcLevel :: TcLclEnv -> TcLevel -> TcLclEnv +setLclEnvTcLevel env lvl = env { tcl_tclvl = lvl } + +getLclEnvTcLevel :: TcLclEnv -> TcLevel +getLclEnvTcLevel = tcl_tclvl + +setLclEnvLoc :: TcLclEnv -> RealSrcSpan -> TcLclEnv +setLclEnvLoc env loc = env { tcl_loc = loc } + +getLclEnvLoc :: TcLclEnv -> RealSrcSpan +getLclEnvLoc = tcl_loc + +lclEnvInGeneratedCode :: TcLclEnv -> Bool +lclEnvInGeneratedCode = tcl_in_gen_code + +type ErrCtxt = (Bool, TidyEnv -> IO (TidyEnv, SDoc)) + -- Monadic so that we have a chance + -- to deal with bound type variables just before error + -- message construction + + -- Bool: True <=> this is a landmark context; do not + -- discard it when trimming for display + +{- TODO move these into where CtLoc is defined. + + +-- These are here to avoid module loops: one might expect them +-- in GHC.Tc.Types.Constraint, but they refer to ErrCtxt which refers to TcM. +-- Easier to just keep these definitions here, alongside TcM. +pushErrCtxt :: CtOrigin -> ErrCtxt -> CtLoc -> CtLoc +pushErrCtxt o err loc@(CtLoc { ctl_env = lcl }) + = loc { ctl_origin = o, ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } } + +pushErrCtxtSameOrigin :: ErrCtxt -> CtLoc -> CtLoc +-- Just add information w/o updating the origin! +pushErrCtxtSameOrigin err loc@(CtLoc { ctl_env = lcl }) + = loc { ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } } + -} + + +type TcTypeEnv = NameEnv TcTyThing + +type ThBindEnv = NameEnv (TopLevelFlag, ThLevel) + -- Domain = all Ids bound in this module (ie not imported) + -- The TopLevelFlag tells if the binding is syntactically top level. + -- We need to know this, because the cross-stage persistence story allows + -- cross-stage at arbitrary types if the Id is bound at top level. + -- + -- Nota bene: a ThLevel of 'outerLevel' is *not* the same as being + -- bound at top level! See Note [Template Haskell levels] in GHC.Tc.Gen.Splice + +--------------------------- +-- Arrow-notation context +--------------------------- + +{- Note [Escaping the arrow scope] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In arrow notation, a variable bound by a proc (or enclosed let/kappa) +is not in scope to the left of an arrow tail (-<) or the head of (|..|). +For example + + proc x -> (e1 -< e2) + +Here, x is not in scope in e1, but it is in scope in e2. This can get +a bit complicated: + + let x = 3 in + proc y -> (proc z -> e1) -< e2 + +Here, x and z are in scope in e1, but y is not. + +We implement this by +recording the environment when passing a proc (using newArrowScope), +and returning to that (using escapeArrowScope) on the left of -< and the +head of (|..|). + +All this can be dealt with by the *renamer*. But the type checker needs +to be involved too. Example (arrowfail001) + class Foo a where foo :: a -> () + data Bar = forall a. Foo a => Bar a + get :: Bar -> () + get = proc x -> case x of Bar a -> foo -< a +Here the call of 'foo' gives rise to a (Foo a) constraint that should not +be captured by the pattern match on 'Bar'. Rather it should join the +constraints from further out. So we must capture the constraint bag +from further out in the ArrowCtxt that we push inwards. +-} + +data ArrowCtxt -- Note [Escaping the arrow scope] + = NoArrowCtxt + | ArrowCtxt LocalRdrEnv (IORef WantedConstraints) + + +--------------------------- +-- The TcBinderStack +--------------------------- + +type TcBinderStack = [TcBinder] + -- This is a stack of locally-bound ids and tyvars, + -- innermost on top + -- Used only in error reporting (relevantBindings in TcError), + -- and in tidying + -- We can't use the tcl_env type environment, because it doesn't + -- keep track of the nesting order + +type TcId = Id +type TcRef = IORef + +data TcBinder + = TcIdBndr + TcId + TopLevelFlag -- Tells whether the binding is syntactically top-level + -- (The monomorphic Ids for a recursive group count + -- as not-top-level for this purpose.) + + | TcIdBndr_ExpType -- Variant that allows the type to be specified as + -- an ExpType + Name + ExpType + TopLevelFlag + + | TcTvBndr -- e.g. case x of P (y::a) -> blah + Name -- We bind the lexical name "a" to the type of y, + TyVar -- which might be an utterly different (perhaps + -- existential) tyvar + +instance Outputable TcBinder where + ppr (TcIdBndr id top_lvl) = ppr id <> brackets (ppr top_lvl) + ppr (TcIdBndr_ExpType id _ top_lvl) = ppr id <> brackets (ppr top_lvl) + ppr (TcTvBndr name tv) = ppr name <+> ppr tv + +instance HasOccName TcBinder where + occName (TcIdBndr id _) = occName (idName id) + occName (TcIdBndr_ExpType name _ _) = occName name + occName (TcTvBndr name _) = occName name + + +{- +************************************************************************ +* * + CtLoc +* * +************************************************************************ + +The 'CtLoc' gives information about where a constraint came from. +This is important for decent error message reporting because +dictionaries don't appear in the original source code. + +-} + +{- +data CtLoc = CtLoc { ctl_origin :: CtOrigin + , ctl_env :: TcLclEnv + , ctl_t_or_k :: Maybe TypeOrKind -- OK if we're not sure + , ctl_depth :: !SubGoalDepth } + -} + + -- The TcLclEnv includes particularly + -- source location: tcl_loc :: RealSrcSpan + -- context: tcl_ctxt :: [ErrCtxt] + -- binder stack: tcl_bndrs :: TcBinderStack + -- level: tcl_tclvl :: TcLevel \ No newline at end of file diff --git a/compiler/GHC/Tc/Types/TH.hs b/compiler/GHC/Tc/Types/TH.hs new file mode 100644 index 0000000000..8e776f49b3 --- /dev/null +++ b/compiler/GHC/Tc/Types/TH.hs @@ -0,0 +1,108 @@ +module GHC.Tc.Types.TH where +import GHCi.RemoteTypes +import qualified Language.Haskell.TH as TH +import GHC.Hs.Expr +import GHC.Tc.Types.Constraint +import GHC.Tc.Types.Evidence +import GHC.Utils.Outputable +import GHC.Prelude +import GHC.Utils.Panic +import GHC.Tc.Types.TcRef +--------------------------- +-- Template Haskell stages and levels +--------------------------- + + +data SpliceType = Typed | Untyped + +data ThStage -- See Note [Template Haskell state diagram] + -- and Note [Template Haskell levels] in GHC.Tc.Gen.Splice + -- Start at: Comp + -- At bracket: wrap current stage in Brack + -- At splice: currently Brack: return to previous stage + -- currently Comp/Splice: compile and run + = Splice SpliceType -- Inside a top-level splice + -- This code will be run *at compile time*; + -- the result replaces the splice + -- Binding level = 0 + + | RunSplice (TcRef [ForeignRef (TH.Q ())]) + -- Set when running a splice, i.e. NOT when renaming or typechecking the + -- Haskell code for the splice. See Note [RunSplice ThLevel]. + -- + -- Contains a list of mod finalizers collected while executing the splice. + -- + -- 'addModFinalizer' inserts finalizers here, and from here they are taken + -- to construct an @HsSpliced@ annotation for untyped splices. See Note + -- [Delaying modFinalizers in untyped splices] in GHC.Rename.Splice. + -- + -- For typed splices, the typechecker takes finalizers from here and + -- inserts them in the list of finalizers in the global environment. + -- + -- See Note [Collecting modFinalizers in typed splices] in "GHC.Tc.Gen.Splice". + + | Comp -- Ordinary Haskell code + -- Binding level = 1 + + | Brack -- Inside brackets + ThStage -- Enclosing stage + PendingStuff + +data PendingStuff + = RnPendingUntyped -- Renaming the inside of an *untyped* bracket + (TcRef [PendingRnSplice]) -- Pending splices in here + + | RnPendingTyped -- Renaming the inside of a *typed* bracket + + | TcPending -- Typechecking the inside of a typed bracket + (TcRef [PendingTcSplice]) -- Accumulate pending splices here + (TcRef WantedConstraints) -- and type constraints here + QuoteWrapper -- A type variable and evidence variable + -- for the overall monad of + -- the bracket. Splices are checked + -- against this monad. The evidence + -- variable is used for desugaring + -- `lift`. + + +topStage, topAnnStage, topSpliceStage :: ThStage +topStage = Comp +topAnnStage = Splice Untyped +topSpliceStage = Splice Untyped + +instance Outputable ThStage where + ppr (Splice _) = text "Splice" + ppr (RunSplice _) = text "RunSplice" + ppr Comp = text "Comp" + ppr (Brack s _) = text "Brack" <> parens (ppr s) + +type ThLevel = Int + -- NB: see Note [Template Haskell levels] in GHC.Tc.Gen.Splice + -- Incremented when going inside a bracket, + -- decremented when going inside a splice + -- NB: ThLevel is one greater than the 'n' in Fig 2 of the + -- original "Template meta-programming for Haskell" paper + +impLevel, outerLevel :: ThLevel +impLevel = 0 -- Imported things; they can be used inside a top level splice +outerLevel = 1 -- Things defined outside brackets + +thLevel :: ThStage -> ThLevel +thLevel (Splice _) = 0 +thLevel Comp = 1 +thLevel (Brack s _) = thLevel s + 1 +thLevel (RunSplice _) = panic "thLevel: called when running a splice" + -- See Note [RunSplice ThLevel]. + +{- Note [RunSplice ThLevel] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The 'RunSplice' stage is set when executing a splice, and only when running a +splice. In particular it is not set when the splice is renamed or typechecked. + +'RunSplice' is needed to provide a reference where 'addModFinalizer' can insert +the finalizer (see Note [Delaying modFinalizers in untyped splices]), and +'addModFinalizer' runs when doing Q things. Therefore, It doesn't make sense to +set 'RunSplice' when renaming or typechecking the splice, where 'Splice', +'Brack' or 'Comp' are used instead. + +-} \ No newline at end of file diff --git a/compiler/GHC/Tc/Types/TcIdSigInfo.hs b/compiler/GHC/Tc/Types/TcIdSigInfo.hs new file mode 100644 index 0000000000..4b4bd265e1 --- /dev/null +++ b/compiler/GHC/Tc/Types/TcIdSigInfo.hs @@ -0,0 +1,209 @@ +module GHC.Tc.Types.TcIdSigInfo where + +import GHC.Prelude + + +import GHC.Hs + +import GHC.Tc.Utils.TcType +import GHC.Tc.Types.Origin + + +import GHC.Types.Id ( idType ) +import GHC.Types.Name +import GHC.Types.Var +import GHC.Types.SrcLoc + + + +import GHC.Utils.Outputable + + + + + + +{- ********************************************************************* +* * + Type signatures +* * +********************************************************************* -} + +-- These data types need to be here only because +-- GHC.Tc.Solver uses them, and GHC.Tc.Solver is fairly +-- low down in the module hierarchy + +type TcSigFun = Name -> Maybe TcSigInfo + +data TcSigInfo = TcIdSig TcIdSigInfo + | TcPatSynSig TcPatSynInfo + +data TcIdSigInfo -- See Note [Complete and partial type signatures] + = CompleteSig -- A complete signature with no wildcards, + -- so the complete polymorphic type is known. + { sig_bndr :: Id -- The polymorphic Id with that type + + , sig_ctxt :: UserTypeCtxt -- In the case of type-class default methods, + -- the Name in the FunSigCtxt is not the same + -- as the TcId; the former is 'op', while the + -- latter is '$dmop' or some such + + , sig_loc :: SrcSpan -- Location of the type signature + } + + | PartialSig -- A partial type signature (i.e. includes one or more + -- wildcards). In this case it doesn't make sense to give + -- the polymorphic Id, because we are going to /infer/ its + -- type, so we can't make the polymorphic Id ab-initio + { psig_name :: Name -- Name of the function; used when report wildcards + , psig_hs_ty :: LHsSigWcType GhcRn -- The original partial signature in + -- HsSyn form + , sig_ctxt :: UserTypeCtxt + , sig_loc :: SrcSpan -- Location of the type signature + } + + +{- Note [Complete and partial type signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A type signature is partial when it contains one or more wildcards +(= type holes). The wildcard can either be: +* A (type) wildcard occurring in sig_theta or sig_tau. These are + stored in sig_wcs. + f :: Bool -> _ + g :: Eq _a => _a -> _a -> Bool +* Or an extra-constraints wildcard, stored in sig_cts: + h :: (Num a, _) => a -> a + +A type signature is a complete type signature when there are no +wildcards in the type signature, i.e. iff sig_wcs is empty and +sig_extra_cts is Nothing. +-} + +data TcIdSigInst + = TISI { sig_inst_sig :: TcIdSigInfo + + , sig_inst_skols :: [(Name, InvisTVBinder)] + -- Instantiated type and kind variables, TyVarTvs + -- The Name is the Name that the renamer chose; + -- but the TcTyVar may come from instantiating + -- the type and hence have a different unique. + -- No need to keep track of whether they are truly lexically + -- scoped because the renamer has named them uniquely + -- See Note [Binding scoped type variables] in GHC.Tc.Gen.Sig + -- + -- NB: The order of sig_inst_skols is irrelevant + -- for a CompleteSig, but for a PartialSig see + -- Note [Quantified variables in partial type signatures] + + , sig_inst_theta :: TcThetaType + -- Instantiated theta. In the case of a + -- PartialSig, sig_theta does not include + -- the extra-constraints wildcard + + , sig_inst_tau :: TcSigmaType -- Instantiated tau + -- See Note [sig_inst_tau may be polymorphic] + + -- Relevant for partial signature only + , sig_inst_wcs :: [(Name, TcTyVar)] + -- Like sig_inst_skols, but for /named/ wildcards (_a etc). + -- The named wildcards scope over the binding, and hence + -- their Names may appear in type signatures in the binding + + , sig_inst_wcx :: Maybe TcType + -- Extra-constraints wildcard to fill in, if any + -- If this exists, it is surely of the form (meta_tv |> co) + -- (where the co might be reflexive). This is filled in + -- only from the return value of GHC.Tc.Gen.HsType.tcAnonWildCardOcc + } + +{- Note [sig_inst_tau may be polymorphic] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note that "sig_inst_tau" might actually be a polymorphic type, +if the original function had a signature like + forall a. Eq a => forall b. Ord b => .... +But that's ok: tcMatchesFun (called by tcRhs) can deal with that +It happens, too! See Note [Polymorphic methods] in GHC.Tc.TyCl.Class. + +Note [Quantified variables in partial type signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + f :: forall a b. _ -> a -> _ -> b + f (x,y) p q = q + +Then we expect f's final type to be + f :: forall {x,y}. forall a b. (x,y) -> a -> b -> b + +Note that x,y are Inferred, and can't be use for visible type +application (VTA). But a,b are Specified, and remain Specified +in the final type, so we can use VTA for them. (Exception: if +it turns out that a's kind mentions b we need to reorder them +with scopedSort.) + +The sig_inst_skols of the TISI from a partial signature records +that original order, and is used to get the variables of f's +final type in the correct order. + + +Note [Wildcards in partial signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The wildcards in psig_wcs may stand for a type mentioning +the universally-quantified tyvars of psig_ty + +E.g. f :: forall a. _ -> a + f x = x +We get sig_inst_skols = [a] + sig_inst_tau = _22 -> a + sig_inst_wcs = [_22] +and _22 in the end is unified with the type 'a' + +Moreover the kind of a wildcard in sig_inst_wcs may mention +the universally-quantified tyvars sig_inst_skols +e.g. f :: t a -> t _ +Here we get + sig_inst_skols = [k:*, (t::k ->*), (a::k)] + sig_inst_tau = t a -> t _22 + sig_inst_wcs = [ _22::k ] +-} + +data TcPatSynInfo + = TPSI { + patsig_name :: Name, + patsig_implicit_bndrs :: [InvisTVBinder], -- Implicitly-bound kind vars (Inferred) and + -- implicitly-bound type vars (Specified) + -- See Note [The pattern-synonym signature splitting rule] in GHC.Tc.TyCl.PatSyn + patsig_univ_bndrs :: [InvisTVBinder], -- Bound by explicit user forall + patsig_req :: TcThetaType, + patsig_ex_bndrs :: [InvisTVBinder], -- Bound by explicit user forall + patsig_prov :: TcThetaType, + patsig_body_ty :: TcSigmaType + } + +instance Outputable TcSigInfo where + ppr (TcIdSig idsi) = ppr idsi + ppr (TcPatSynSig tpsi) = text "TcPatSynInfo" <+> ppr tpsi + +instance Outputable TcIdSigInfo where + ppr (CompleteSig { sig_bndr = bndr }) + = ppr bndr <+> dcolon <+> ppr (idType bndr) + ppr (PartialSig { psig_name = name, psig_hs_ty = hs_ty }) + = text "psig" <+> ppr name <+> dcolon <+> ppr hs_ty + +instance Outputable TcIdSigInst where + ppr (TISI { sig_inst_sig = sig, sig_inst_skols = skols + , sig_inst_theta = theta, sig_inst_tau = tau }) + = hang (ppr sig) 2 (vcat [ ppr skols, ppr theta <+> darrow <+> ppr tau ]) + +instance Outputable TcPatSynInfo where + ppr (TPSI{ patsig_name = name}) = ppr name + +isPartialSig :: TcIdSigInst -> Bool +isPartialSig (TISI { sig_inst_sig = PartialSig {} }) = True +isPartialSig _ = False + +-- | No signature or a partial signature +hasCompleteSig :: TcSigFun -> Name -> Bool +hasCompleteSig sig_fn name + = case sig_fn name of + Just (TcIdSig (CompleteSig {})) -> True + _ -> False + diff --git a/compiler/GHC/Tc/Types/TcRef.hs b/compiler/GHC/Tc/Types/TcRef.hs new file mode 100644 index 0000000000..c6b28e6521 --- /dev/null +++ b/compiler/GHC/Tc/Types/TcRef.hs @@ -0,0 +1,8 @@ +module GHC.Tc.Types.TcRef where +import Data.IORef + + +-- | Type alias for 'IORef'; the convention is we'll use this for mutable +-- bits of data in 'TcGblEnv' which are updated during typechecking and +-- returned at the end. +type TcRef a = IORef a \ No newline at end of file diff --git a/compiler/GHC/Tc/Types/TcTyThing.hs b/compiler/GHC/Tc/Types/TcTyThing.hs new file mode 100644 index 0000000000..5b2ad427b1 --- /dev/null +++ b/compiler/GHC/Tc/Types/TcTyThing.hs @@ -0,0 +1,252 @@ +module GHC.Tc.Types.TcTyThing where + +import GHC.Prelude + + + +import GHC.Tc.Utils.TcType +--import GHC.Tc.Errors.Types () + +import GHC.Core.Type +import GHC.Core.TyCon ( TyCon, tyConKind ) + +import GHC.Types.Name +import GHC.Types.Name.Env +import GHC.Types.Name.Set +import GHC.Types.Var +import GHC.Types.TyThing + + + +import GHC.Utils.Error +import GHC.Utils.Outputable +import GHC.Utils.Misc +import GHC.Tc.Errors.Types.PromotionErr (PromotionErr, peCategory) + + + +--------------------------- +-- TcTyThing +--------------------------- + +-- | A typecheckable thing available in a local context. Could be +-- 'AGlobal' 'TyThing', but also lexically scoped variables, etc. +-- See "GHC.Tc.Utils.Env" for how to retrieve a 'TyThing' given a 'Name'. +data TcTyThing + = AGlobal TyThing -- Used only in the return type of a lookup + + | ATcId -- Ids defined in this module; may not be fully zonked + { tct_id :: Id + , tct_info :: IdBindingInfo -- See Note [Meaning of IdBindingInfo] + } + + | ATyVar Name TcTyVar -- See Note [Type variables in the type environment] + + | ATcTyCon TyCon -- Used temporarily, during kind checking, for the + -- tycons and classes in this recursive group + -- The TyCon is always a TcTyCon. Its kind + -- can be a mono-kind or a poly-kind; in TcTyClsDcls see + -- Note [Type checking recursive type and class declarations] + + | APromotionErr PromotionErr + +-- | Matches on either a global 'TyCon' or a 'TcTyCon'. +tcTyThingTyCon_maybe :: TcTyThing -> Maybe TyCon +tcTyThingTyCon_maybe (AGlobal (ATyCon tc)) = Just tc +tcTyThingTyCon_maybe (ATcTyCon tc_tc) = Just tc_tc +tcTyThingTyCon_maybe _ = Nothing + +instance Outputable TcTyThing where -- Debugging only + ppr (AGlobal g) = ppr g + ppr elt@(ATcId {}) = text "Identifier" <> + brackets (ppr (tct_id elt) <> dcolon + <> ppr (varType (tct_id elt)) <> comma + <+> ppr (tct_info elt)) + ppr (ATyVar n tv) = text "Type variable" <+> quotes (ppr n) <+> equals <+> ppr tv + <+> dcolon <+> ppr (varType tv) + ppr (ATcTyCon tc) = text "ATcTyCon" <+> ppr tc <+> dcolon <+> ppr (tyConKind tc) + ppr (APromotionErr err) = text "APromotionErr" <+> ppr err + +-- | IdBindingInfo describes how an Id is bound. +-- +-- It is used for the following purposes: +-- a) for static forms in 'GHC.Tc.Gen.Expr.checkClosedInStaticForm' and +-- b) to figure out when a nested binding can be generalised, +-- in 'GHC.Tc.Gen.Bind.decideGeneralisationPlan'. +-- +data IdBindingInfo -- See Note [Meaning of IdBindingInfo] + = NotLetBound + | ClosedLet + | NonClosedLet + RhsNames -- Used for (static e) checks only + ClosedTypeId -- Used for generalisation checks + -- and for (static e) checks + +-- | IsGroupClosed describes a group of mutually-recursive bindings +data IsGroupClosed + = IsGroupClosed + (NameEnv RhsNames) -- Free var info for the RHS of each binding in the group + -- Used only for (static e) checks + + ClosedTypeId -- True <=> all the free vars of the group are + -- imported or ClosedLet or + -- NonClosedLet with ClosedTypeId=True. + -- In particular, no tyvars, no NotLetBound + +type RhsNames = NameSet -- Names of variables, mentioned on the RHS of + -- a definition, that are not Global or ClosedLet + +type ClosedTypeId = Bool + -- See Note [Meaning of IdBindingInfo] + +{- Note [Meaning of IdBindingInfo] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +NotLetBound means that + the Id is not let-bound (e.g. it is bound in a + lambda-abstraction or in a case pattern) + +ClosedLet means that + - The Id is let-bound, + - Any free term variables are also Global or ClosedLet + - Its type has no free variables (NB: a top-level binding subject + to the MR might have free vars in its type) + These ClosedLets can definitely be floated to top level; and we + may need to do so for static forms. + + Property: ClosedLet + is equivalent to + NonClosedLet emptyNameSet True + +(NonClosedLet (fvs::RhsNames) (cl::ClosedTypeId)) means that + - The Id is let-bound + + - The fvs::RhsNames contains the free names of the RHS, + excluding Global and ClosedLet ones. + + - For the ClosedTypeId field see Note [Bindings with closed types: ClosedTypeId] + +For (static e) to be valid, we need for every 'x' free in 'e', +that x's binding is floatable to the top level. Specifically: + * x's RhsNames must be empty + * x's type has no free variables +See Note [Grand plan for static forms] in "GHC.Iface.Tidy.StaticPtrTable". +This test is made in GHC.Tc.Gen.Expr.checkClosedInStaticForm. +Actually knowing x's RhsNames (rather than just its emptiness +or otherwise) is just so we can produce better error messages + +Note [Bindings with closed types: ClosedTypeId] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + + f x = let g ys = map not ys + in ... + +Can we generalise 'g' under the OutsideIn algorithm? Yes, +because all g's free variables are top-level; that is they themselves +have no free type variables, and it is the type variables in the +environment that makes things tricky for OutsideIn generalisation. + +Here's the invariant: + If an Id has ClosedTypeId=True (in its IdBindingInfo), then + the Id's type is /definitely/ closed (has no free type variables). + Specifically, + a) The Id's actual type is closed (has no free tyvars) + b) Either the Id has a (closed) user-supplied type signature + or all its free variables are Global/ClosedLet + or NonClosedLet with ClosedTypeId=True. + In particular, none are NotLetBound. + +Why is (b) needed? Consider + \x. (x :: Int, let y = x+1 in ...) +Initially x::alpha. If we happen to typecheck the 'let' before the +(x::Int), y's type will have a free tyvar; but if the other way round +it won't. So we treat any let-bound variable with a free +non-let-bound variable as not ClosedTypeId, regardless of what the +free vars of its type actually are. + +But if it has a signature, all is well: + \x. ...(let { y::Int; y = x+1 } in + let { v = y+2 } in ...)... +Here the signature on 'v' makes 'y' a ClosedTypeId, so we can +generalise 'v'. + +Note that: + + * A top-level binding may not have ClosedTypeId=True, if it suffers + from the MR + + * A nested binding may be closed (eg 'g' in the example we started + with). Indeed, that's the point; whether a function is defined at + top level or nested is orthogonal to the question of whether or + not it is closed. + + * A binding may be non-closed because it mentions a lexically scoped + *type variable* Eg + f :: forall a. blah + f x = let g y = ...(y::a)... + +Under OutsideIn we are free to generalise an Id all of whose free +variables have ClosedTypeId=True (or imported). This is an extension +compared to the JFP paper on OutsideIn, which used "top-level" as a +proxy for "closed". (It's not a good proxy anyway -- the MR can make +a top-level binding with a free type variable.) + +Note [Type variables in the type environment] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The type environment has a binding for each lexically-scoped +type variable that is in scope. For example + + f :: forall a. a -> a + f x = (x :: a) + + g1 :: [a] -> a + g1 (ys :: [b]) = head ys :: b + + g2 :: [Int] -> Int + g2 (ys :: [c]) = head ys :: c + +* The forall'd variable 'a' in the signature scopes over f's RHS. + +* The pattern-bound type variable 'b' in 'g1' scopes over g1's + RHS; note that it is bound to a skolem 'a' which is not itself + lexically in scope. + +* The pattern-bound type variable 'c' in 'g2' is bound to + Int; that is, pattern-bound type variables can stand for + arbitrary types. (see + GHC proposal #128 "Allow ScopedTypeVariables to refer to types" + https://github.com/ghc-proposals/ghc-proposals/pull/128, + and the paper + "Type variables in patterns", Haskell Symposium 2018. + + +This is implemented by the constructor + ATyVar Name TcTyVar +in the type environment. + +* The Name is the name of the original, lexically scoped type + variable + +* The TcTyVar is sometimes a skolem (like in 'f'), and sometimes + a unification variable (like in 'g1', 'g2'). We never zonk the + type environment so in the latter case it always stays as a + unification variable, although that variable may be later + unified with a type (such as Int in 'g2'). +-} + +instance Outputable IdBindingInfo where + ppr NotLetBound = text "NotLetBound" + ppr ClosedLet = text "TopLevelLet" + ppr (NonClosedLet fvs closed_type) = + text "TopLevelLet" <+> ppr fvs <+> ppr closed_type + +-------------- +pprTcTyThingCategory :: TcTyThing -> SDoc +pprTcTyThingCategory = text . capitalise . tcTyThingCategory + +tcTyThingCategory :: TcTyThing -> String +tcTyThingCategory (AGlobal thing) = tyThingCategory thing +tcTyThingCategory (ATyVar {}) = "type variable" +tcTyThingCategory (ATcId {}) = "local identifier" +tcTyThingCategory (ATcTyCon {}) = "local tycon" +tcTyThingCategory (APromotionErr pe) = peCategory pe diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs index 75b74cbb35..0cd69c95bb 100644 --- a/compiler/GHC/Tc/Utils/Monad.hs +++ b/compiler/GHC/Tc/Utils/Monad.hs @@ -1275,10 +1275,13 @@ getCtLocM :: CtOrigin -> Maybe TypeOrKind -> TcM CtLoc getCtLocM origin t_or_k = do { env <- getLclEnv ; return (CtLoc { ctl_origin = origin - , ctl_env = env + , ctl_env = mkCtLocEnv env , ctl_t_or_k = t_or_k , ctl_depth = initialSubGoalDepth }) } +mkCtLocEnv :: TcLclEnv -> CtLocEnv +mkCtLocEnv lcl_env = CtLocEnv + setCtLocM :: CtLoc -> TcM a -> TcM a -- Set the SrcSpan and error context from the CtLoc setCtLocM (CtLoc { ctl_env = lcl }) thing_inside diff --git a/compiler/GHC/Types/LclEnv.hs b/compiler/GHC/Types/LclEnv.hs new file mode 100644 index 0000000000..e69de29bb2 diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in index fc2151f547..7735a28b44 100644 --- a/compiler/ghc.cabal.in +++ b/compiler/ghc.cabal.in @@ -708,6 +708,7 @@ Library GHC.Tc.Errors.Hole.FitTypes GHC.Tc.Errors.Ppr GHC.Tc.Errors.Types + GHC.Tc.Errors.Types.PromotionErr GHC.Tc.Gen.Annotation GHC.Tc.Gen.App GHC.Tc.Gen.Arrow @@ -740,6 +741,11 @@ Library GHC.Tc.Solver.Types GHC.Tc.TyCl GHC.Tc.TyCl.Build + GHC.Tc.Types.LclEnv + GHC.Tc.Types.TcIdSigInfo + GHC.Tc.Types.TH + GHC.Tc.Types.TcRef + GHC.Tc.Types.TcTyThing GHC.Tc.TyCl.Class GHC.Tc.TyCl.Instance GHC.Tc.TyCl.PatSyn -- cgit v1.2.1