-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Liquid Types for Haskell -- -- This package provides a plugin to verify Haskell programs. But most -- likely you should be using the liquidhaskell package instead, -- which rexports this plugin together with necessary specifications for -- definitions in the boot libraries. @package liquidhaskell-boot @version 0.9.6.3 -- | This module provides a drop-in replacement for Cabal's -- defaultMain, to be used inside hs modules of packages -- that wants to use the "dev mode". For more information, visit the -- documentation, especially the "Developers' guide". module Language.Haskell.Liquid.Cabal liquidHaskellMain :: IO () module Language.Haskell.Liquid.GHC.Plugin.Tutorial -- | Deriving instances of Hashable and Binary, generically. module Language.Haskell.Liquid.Types.Generics instance (GHC.Classes.Eq (GHC.Generics.Generically a), GHC.Generics.Generic a, Data.Hashable.Class.GHashable Data.Hashable.Class.Zero (GHC.Generics.Rep a)) => Data.Hashable.Class.Hashable (GHC.Generics.Generically a) instance (GHC.Generics.Generic a, Data.Binary.Class.GBinaryPut (GHC.Generics.Rep a), Data.Binary.Class.GBinaryGet (GHC.Generics.Rep a)) => Data.Binary.Class.Binary (GHC.Generics.Generically a) instance (GHC.Generics.Generic a, GHC.Classes.Eq (GHC.Generics.Rep a ())) => GHC.Classes.Eq (GHC.Generics.Generically a) module Language.Haskell.Liquid.Types.Names lenLocSymbol :: Located Symbol anyTypeSymbol :: Symbol functionComposisionSymbol :: Symbol selfSymbol :: Symbol -- | Command Line Configuration Options -- ---------------------------------------- module Language.Haskell.Liquid.UX.Config data Config Config :: Verbosity -> [FilePath] -> [FilePath] -> Bool -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Bool -> Bool -> [String] -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Bool -> Maybe Int -> Int -> Int -> Int -> Maybe SMTSolver -> Bool -> Bool -> Bool -> [String] -> [String] -> Eliminate -> Int -> Bool -> Bool -> [String] -> Bool -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Maybe Int -> Bool -> Bool -> Bool -> Bool -> [String] -> Config -- | the logging verbosity to use (defaults to Quiet) [loggingVerbosity] :: Config -> Verbosity -- | source files to check [files] :: Config -> [FilePath] -- | path to directory for including specs [idirs] :: Config -> [FilePath] -- | check subset of binders modified (+ dependencies) since last check [diffcheck] :: Config -> Bool -- | uninterpreted integer multiplication and division [linear] :: Config -> Bool -- | interpretation of string theory in the logic [stringTheory] :: Config -> Bool -- | allow higher order binders into the logic [higherorder] :: Config -> Bool -- | allow higher order qualifiers [higherorderqs] :: Config -> Bool -- | smt timeout [smtTimeout] :: Config -> Maybe Int -- | check all binders (overrides diffcheck) [fullcheck] :: Config -> Bool -- | save fixpoint query [saveQuery] :: Config -> Bool -- | set of binders to check [checks] :: Config -> [String] -- | whether to complain about specifications for unexported and unused -- values [noCheckUnknown] :: Config -> Bool -- | disable termination check [notermination] :: Config -> Bool -- | disable positivity check [nopositivity] :: Config -> Bool -- | Adds precise reasoning on presence of rankNTypes [rankNTypes] :: Config -> Bool -- | disable checking class instances , structuralTerm :: Bool -- ^ use -- structural termination checker [noclasscheck] :: Config -> Bool -- | disable structural termination check [nostructuralterm] :: Config -> Bool -- | enable gradual type checking [gradual] :: Config -> Bool -- | scope of the outer binders on the inner refinements [bscope] :: Config -> Bool -- | depth of gradual concretization [gdepth] :: Config -> Int -- | interactive gradual solving [ginteractive] :: Config -> Bool -- | Check for termination and totality, Overrides no-termination flags [totalHaskell] :: Config -> Bool -- | disable warnings output (only show errors) [nowarnings] :: Config -> Bool -- | disable creation of intermediate annotation files [noannotations] :: Config -> Bool -- | check internal (GHC-derived) binders [checkDerived] :: Config -> Bool -- | maximum case expand nesting depth. [caseExpandDepth] :: Config -> Int -- | disable truing top level types [notruetypes] :: Config -> Bool -- | disable totality check in definitions [nototality] :: Config -> Bool -- | enable prunning unsorted Refinements [pruneUnsorted] :: Config -> Bool -- | number of cores used to solve constraints [cores] :: Config -> Maybe Int -- | Minimum size of a partition [minPartSize] :: Config -> Int -- | Maximum size of a partition. Overrides minPartSize [maxPartSize] :: Config -> Int -- | the maximum number of parameters to accept when mining qualifiers [maxParams] :: Config -> Int -- | name of smtsolver to use [default: try z3, cvc4, mathsat in order] [smtsolver] :: Config -> Maybe SMTSolver -- | drop module qualifers from pretty-printed names. [shortNames] :: Config -> Bool -- | don't show subtyping errors and contexts. [shortErrors] :: Config -> Bool -- | find and use .cabal file to include paths to sources for imported -- modules [cabalDir] :: Config -> Bool -- | command-line options to pass to GHC [ghcOptions] :: Config -> [String] -- | .c files to compile and link against (for GHC) [cFiles] :: Config -> [String] -- | eliminate (i.e. don't use qualifs for) for "none", "cuts" or "all" -- kvars [eliminate] :: Config -> Eliminate -- | port at which lhi should listen [port] :: Config -> Int -- | Automatically generate singleton types for data constructors [exactDC] :: Config -> Bool -- | Disable ADTs (only used with exactDC) [noADT] :: Config -> Bool -- | expect failure from Liquid with at least one of the following messages [expectErrorContaining] :: Config -> [String] -- | expect failure from Liquid with any message [expectAnyError] :: Config -> Bool -- | scrape qualifiers from imported specifications [scrapeImports] :: Config -> Bool -- | scrape qualifiers from auto specifications [scrapeInternals] :: Config -> Bool -- | scrape qualifiers from used, imported specifications [scrapeUsedImports] :: Config -> Bool -- | print eliminate stats [elimStats] :: Config -> Bool -- | eliminate upto given depth of KVar chains [elimBound] :: Config -> Maybe Int -- | print results (safe/errors) as JSON [json] :: Config -> Bool -- | attempt to generate counter-examples to type errors [counterExamples] :: Config -> Bool -- | check and time each (asserted) type-sig separately [timeBinds] :: Config -> Bool -- | treat code patterns (e.g. e1 >>= x -> e2) specially for -- inference [noPatternInline] :: Config -> Bool -- | print full blown core (with untidy names) in verbose mode [untidyCore] :: Config -> Bool -- | simplify GHC core before constraint-generation PLE-OPT , autoInst -- ntiate :: Instantiate -- ^ How to instantiate axioms [noSimplifyCore] :: Config -> Bool -- | Disable non-concrete KVar slicing [noslice] :: Config -> Bool -- | Disable loading lifted specifications (for "legacy" libs) [noLiftedImport] :: Config -> Bool -- | Enable proof-by-logical-evaluation [proofLogicEval] :: Config -> Bool -- | Unfold invocations with undecided guards in PLE [pleWithUndecidedGuards] :: Config -> Bool -- | Enable proof-by-logical-evaluation [oldPLE] :: Config -> Bool -- | Use an interpreter to assist PLE [interpreter] :: Config -> Bool -- | Enable proof-by-logical-evaluation locally, per function [proofLogicEvalLocal] :: Config -> Bool -- | Enable extensional interpretation of function equality [extensionality] :: Config -> Bool -- | No inference of polymorphic type application. [nopolyinfer] :: Config -> Bool -- | Allow "reflection"; switches on "--higherorder" and "--exactdc" [reflection] :: Config -> Bool -- | Only "compile" the spec -- into .bspec file -- don't do any checking. [compileSpec] :: Config -> Bool -- | Do not check the transitive imports [noCheckImports] :: Config -> Bool -- | enable typeclass support. [typeclass] :: Config -> Bool [auxInline] :: Config -> Bool -- | Enable termination checking for rewriting [rwTerminationCheck] :: Config -> Bool -- | Skip this module entirely (don't even compile any specs in it) [skipModule] :: Config -> Bool [noLazyPLE] :: Config -> Bool -- | Maximum PLE "fuel" (unfold depth) (default=infinite) [fuel] :: Config -> Maybe Int -- | Perform environment reduction [environmentReduction] :: Config -> Bool -- | Don't perform environment reduction [noEnvironmentReduction] :: Config -> Bool -- | Inline ANF bindings. Sometimes improves performance and sometimes -- worsens it. [inlineANFBindings] :: Config -> Bool -- | Use pandoc to generate html [pandocHtml] :: Config -> Bool [excludeAutomaticAssumptionsFor] :: Config -> [String] class HasConfig t getConfig :: HasConfig t => t -> Config allowPLE :: Config -> Bool allowLocalPLE :: Config -> Bool allowGlobalPLE :: Config -> Bool patternFlag :: HasConfig t => t -> Bool higherOrderFlag :: HasConfig t => t -> Bool pruneFlag :: HasConfig t => t -> Bool maxCaseExpand :: HasConfig t => t -> Int exactDCFlag :: HasConfig t => t -> Bool hasOpt :: HasConfig t => t -> (Config -> Bool) -> Bool totalityCheck :: HasConfig t => t -> Bool terminationCheck :: HasConfig t => t -> Bool structuralTerm :: HasConfig a => a -> Bool instance GHC.Classes.Eq Language.Haskell.Liquid.UX.Config.Config instance GHC.Show.Show Language.Haskell.Liquid.UX.Config.Config instance Data.Data.Data Language.Haskell.Liquid.UX.Config.Config instance GHC.Generics.Generic Language.Haskell.Liquid.UX.Config.Config instance Language.Haskell.Liquid.UX.Config.HasConfig Language.Haskell.Liquid.UX.Config.Config module Language.Haskell.Liquid.UX.SimpleVersion -- | Generate a string like Version 1.2, Git revision 1234. -- -- $(simpleVersion …) :: String Taken from -- https://hackage.haskell.org/package/optparse-simple-0.1.1.4/docs/Options-Applicative-Simple.html#v:simpleVersion -- so we can drop the dependency on optparse-simple. simpleVersion :: Version -> Q Exp module Liquid.GHC.API.StableModule -- | A newtype wrapper around a Module which: -- --
-- <location>: <error> -- ---- -- If the location is on the command line, or in GHC itself, then -- <location>="ghc". All of the error types below correspond to a -- <location> of "ghc", except for ProgramError (where the string -- is assumed to contain a location already, so we don't print one). data () => GhcException -- | A problem with the command line arguments, but don't print usage. CmdLineError :: String -> GhcException -- | An error in the user's code, probably. ProgramError :: String -> GhcException -- | Represents a pretty-printable document. -- -- To display an SDoc, use printSDoc, printSDocLn, -- bufLeftRenderSDoc, or renderWithContext. Avoid calling -- runSDoc directly as it breaks the abstraction layer. data () => SDoc -- | Represents an annotation after it has been sufficiently desugared from -- it's initial form of AnnDecl data () => Annotation Annotation :: CoreAnnTarget -> AnnPayload -> Annotation -- | The target of the annotation [ann_target] :: Annotation -> CoreAnnTarget [ann_value] :: Annotation -> AnnPayload -- | A Haskell expression. data () => HsExpr p -- | Variable See Note [Located RdrNames] HsVar :: XVar p -> LIdP p -> HsExpr p -- | Overloaded literals HsOverLit :: XOverLitE p -> HsOverLit p -> HsExpr p -- | Expression with an explicit type signature. e :: type -- --
-- `bar` -- ( ~ ) ---- --
-- handleSourceError printExceptionAndWarnings $ do -- ... api calls that may fail ... ---- -- The SourceErrors error messages can be accessed via -- srcErrorMessages. This list may be empty if the compiler failed -- due to -Werror (Opt_WarnIsError). -- -- See printExceptionAndWarnings for more information on what to -- take care of when writing a custom error handler. data () => SourceError -- | Plugin is the compiler plugin data type. Try to avoid -- constructing one of these directly, and just modify some fields of -- defaultPlugin instead: this is to try and preserve source-code -- compatibility when we add fields to this. -- -- Nonetheless, this API is preliminary and highly likely to change in -- the future. data () => Plugin Plugin :: CorePlugin -> TcPlugin -> DefaultingPlugin -> HoleFitPlugin -> ([CommandLineOption] -> HscEnv -> IO HscEnv) -> ([CommandLineOption] -> IO PluginRecompile) -> ([CommandLineOption] -> ModSummary -> ParsedResult -> Hsc ParsedResult) -> ([CommandLineOption] -> TcGblEnv -> HsGroup GhcRn -> TcM (TcGblEnv, HsGroup GhcRn)) -> ([CommandLineOption] -> ModSummary -> TcGblEnv -> TcM TcGblEnv) -> ([CommandLineOption] -> LHsExpr GhcTc -> TcM (LHsExpr GhcTc)) -> (forall lcl. () => [CommandLineOption] -> ModIface -> IfM lcl ModIface) -> Plugin -- | Modify the Core pipeline that will be used for compilation. This is -- called as the Core pipeline is built for every module being compiled, -- and plugins get the opportunity to modify the pipeline in a -- nondeterministic order. [installCoreToDos] :: Plugin -> CorePlugin -- | An optional typechecker plugin, which may modify the behaviour of the -- constraint solver. [tcPlugin] :: Plugin -> TcPlugin -- | An optional defaulting plugin, which may specify the additional -- type-defaulting rules. [defaultingPlugin] :: Plugin -> DefaultingPlugin -- | An optional plugin to handle hole fits, which may re-order or change -- the list of valid hole fits and refinement hole fits. [holeFitPlugin] :: Plugin -> HoleFitPlugin -- | An optional plugin to update HscEnv, right after plugin -- loading. This can be used to register hooks or tweak any field of -- DynFlags before doing actual work on a module. [driverPlugin] :: Plugin -> [CommandLineOption] -> HscEnv -> IO HscEnv -- | Specify how the plugin should affect recompilation. [pluginRecompile] :: Plugin -> [CommandLineOption] -> IO PluginRecompile -- | Modify the module when it is parsed. This is called by -- GHC.Driver.Main when the parser has produced no or only -- non-fatal errors. Compilation will fail if the messages produced by -- this function contain any errors. [parsedResultAction] :: Plugin -> [CommandLineOption] -> ModSummary -> ParsedResult -> Hsc ParsedResult -- | Modify each group after it is renamed. This is called after each -- HsGroup has been renamed. [renamedResultAction] :: Plugin -> [CommandLineOption] -> TcGblEnv -> HsGroup GhcRn -> TcM (TcGblEnv, HsGroup GhcRn) -- | Modify the module when it is type checked. This is called at the very -- end of typechecking. [typeCheckResultAction] :: Plugin -> [CommandLineOption] -> ModSummary -> TcGblEnv -> TcM TcGblEnv -- | Modify the TH splice or quasiqoute before it is run. [spliceRunAction] :: Plugin -> [CommandLineOption] -> LHsExpr GhcTc -> TcM (LHsExpr GhcTc) -- | Modify an interface that have been loaded. This is called by -- GHC.Iface.Load when an interface is successfully loaded. Not -- applied to the loading of the plugin interface. Tools that rely on -- information from modules other than the currently compiled one should -- implement this function. [interfaceLoadAction] :: Plugin -> forall lcl. () => [CommandLineOption] -> ModIface -> IfM lcl ModIface -- | A FastString is a UTF-8 encoded string together with a unique -- ID. All FastStrings are stored in a global hashtable to support -- fast O(1) comparison. -- -- It is also associated with a lazy reference to the Z-encoding of this -- string which is used by the compiler internally. data () => FastString -- | See Note [Roles] in GHC.Core.Coercion -- -- Order of constructors matters: the Ord instance coincides with the -- *super*typing relation on roles. data () => Role data () => Boxity Boxed :: Boxity -- | Maps the "normal" id type for a given pass type family IdP p -- | Occurrence Name -- -- In this context that means: "classified (i.e. as a type name, value -- name, etc) but not qualified and not yet resolved" data () => OccName -- | Indicates whether a module name is referring to a boot interface -- (hs-boot file) or regular module (hs file). We need to treat boot -- modules specially when building compilation graphs, since they break -- cycles. Regular source files and signature files are treated -- equivalently. data () => IsBootInterface NotBoot :: IsBootInterface IsBoot :: IsBootInterface -- | A class of types that represent a single logical line of text, with -- support for horizontal composition. -- -- See Note [HLine versus HDoc] and Note [The outputable class hierarchy] -- for more details. class IsOutput doc => IsLine doc char :: IsLine doc => Char -> doc text :: IsLine doc => String -> doc ftext :: IsLine doc => FastString -> doc ztext :: IsLine doc => FastZString -> doc -- | Join two docs together horizontally with a gap between them. (<+>) :: IsLine doc => doc -> doc -> doc -- | Separate: is either like hsep or like vcat, depending on -- what fits. sep :: IsLine doc => [doc] -> doc -- | A paragraph-fill combinator. It's much like sep, only it keeps -- fitting things on one line until it can't fit any more. fsep :: IsLine doc => [doc] -> doc -- | Concatenate docs horizontally without gaps. hcat :: IsLine doc => [doc] -> doc -- | Concatenate docs horizontally with a space between each one. hsep :: IsLine doc => [doc] -> doc -- | Prints as either the given SDoc or the given HLine, -- depending on which type the result is instantiated to. This should -- generally be avoided; see Note [dualLine and dualDoc] for details. dualLine :: IsLine doc => SDoc -> HLine -> doc -- | A superclass for IsLine and IsDoc that provides an -- identity, empty, as well as access to the shared -- SDocContext. -- -- See Note [The outputable class hierarchy] for more details. class () => IsOutput doc empty :: IsOutput doc => doc docWithContext :: IsOutput doc => (SDocContext -> doc) -> doc -- | Represents a (possibly empty) sequence of lines that can be -- efficiently printed directly to a Handle (actually a -- BufHandle). See Note [SDoc versus HDoc] and Note [HLine versus -- HDoc] for more details. data () => HDoc -- | Represents a single line of output that can be efficiently printed -- directly to a Handle (actually a BufHandle). See Note -- [SDoc versus HDoc] and Note [HLine versus HDoc] for more details. data () => HLine -- | When we print a binder, we often want to print its type too. The -- OutputableBndr class encapsulates this idea. class Outputable a => OutputableBndr a pprBndr :: OutputableBndr a => BindingSite -> a -> SDoc pprPrefixOcc :: OutputableBndr a => a -> SDoc pprInfixOcc :: OutputableBndr a => a -> SDoc bndrIsJoin_maybe :: OutputableBndr a => a -> Maybe Int -- | BindingSite is used to tell the thing that prints binder what -- language construct is binding the identifier. This can be used to -- decide how much info to print. Also see Note [Binding-site specific -- printing] in GHC.Core.Ppr data () => BindingSite -- | The x in (x. e) LambdaBind :: BindingSite -- | The x in case scrut of x { (y,z) -> ... } CaseBind :: BindingSite -- | The y,z in case scrut of x { (y,z) -> ... } CasePatBind :: BindingSite -- | The x in (let x = rhs in e) LetBind :: BindingSite -- | Wrapper for types having a Outputable instance when an OutputableP -- instance is required. newtype () => PDoc a PDoc :: a -> PDoc a -- | Outputable class with an additional environment value -- -- See Note [The OutputableP class] class () => OutputableP env a pdoc :: OutputableP env a => env -> a -> SDoc data () => SDocContext SDC :: !PprStyle -> !Scheme -> !PprColour -> !Bool -> !Int -> !Int -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !FastString -> SDoc -> SDocContext [sdocStyle] :: SDocContext -> !PprStyle [sdocColScheme] :: SDocContext -> !Scheme -- | The most recently used colour. This allows nesting colours. [sdocLastColour] :: SDocContext -> !PprColour [sdocShouldUseColor] :: SDocContext -> !Bool [sdocDefaultDepth] :: SDocContext -> !Int [sdocLineLength] :: SDocContext -> !Int -- | True if Unicode encoding is supported and not disabled by -- GHC_NO_UNICODE environment variable [sdocCanUseUnicode] :: SDocContext -> !Bool [sdocHexWordLiterals] :: SDocContext -> !Bool [sdocPprDebug] :: SDocContext -> !Bool [sdocPrintUnicodeSyntax] :: SDocContext -> !Bool [sdocPrintCaseAsLet] :: SDocContext -> !Bool [sdocPrintTypecheckerElaboration] :: SDocContext -> !Bool [sdocPrintAxiomIncomps] :: SDocContext -> !Bool [sdocPrintExplicitKinds] :: SDocContext -> !Bool [sdocPrintExplicitCoercions] :: SDocContext -> !Bool [sdocPrintExplicitRuntimeReps] :: SDocContext -> !Bool [sdocPrintExplicitForalls] :: SDocContext -> !Bool [sdocPrintPotentialInstances] :: SDocContext -> !Bool [sdocPrintEqualityRelations] :: SDocContext -> !Bool [sdocSuppressTicks] :: SDocContext -> !Bool [sdocSuppressTypeSignatures] :: SDocContext -> !Bool [sdocSuppressTypeApplications] :: SDocContext -> !Bool [sdocSuppressIdInfo] :: SDocContext -> !Bool [sdocSuppressCoercions] :: SDocContext -> !Bool [sdocSuppressCoercionTypes] :: SDocContext -> !Bool [sdocSuppressUnfoldings] :: SDocContext -> !Bool [sdocSuppressVarKinds] :: SDocContext -> !Bool [sdocSuppressUniques] :: SDocContext -> !Bool [sdocSuppressModulePrefixes] :: SDocContext -> !Bool [sdocSuppressStgExts] :: SDocContext -> !Bool [sdocSuppressStgReps] :: SDocContext -> !Bool [sdocErrorSpans] :: SDocContext -> !Bool [sdocStarIsType] :: SDocContext -> !Bool [sdocLinearTypes] :: SDocContext -> !Bool [sdocListTuplePuns] :: SDocContext -> !Bool [sdocPrintTypeAbbreviations] :: SDocContext -> !Bool -- | Used to map UnitIds to more friendly "package-version:component" -- strings while pretty-printing. -- -- Use pprWithUnitState to set it. Users should never have to set -- it to pretty-print SDocs emitted by GHC, otherwise it's a bug. It's an -- internal field used to thread the UnitState so that the Outputable -- instance of UnitId can use it. -- -- See Note [Pretty-printing UnitId] in GHC.Unit for more details. -- -- Note that we use FastString instead of UnitId to avoid -- boring module inter-dependency issues. [sdocUnitIdForUser] :: SDocContext -> !FastString -> SDoc data () => QualifyName NameUnqual :: QualifyName NameQual :: ModuleName -> QualifyName NameNotInScope1 :: QualifyName NameNotInScope2 :: QualifyName newtype () => IsEmptyOrSingleton IsEmptyOrSingleton :: Bool -> IsEmptyOrSingleton data () => PromotedItem PromotedItemListSyntax :: IsEmptyOrSingleton -> PromotedItem PromotedItemTupleSyntax :: PromotedItem PromotedItemDataCon :: OccName -> PromotedItem -- | Flags that affect whether a promotion tick is printed. data () => PromotionTickContext PromTickCtx :: !Bool -> !Bool -> PromotionTickContext [ptcListTuplePuns] :: PromotionTickContext -> !Bool [ptcPrintRedundantPromTicks] :: PromotionTickContext -> !Bool -- | Given a promoted data constructor, decide whether to print a tick to -- disambiguate the namespace. type QueryPromotionTick = PromotedItem -> Bool -- | For a given package, we need to know whether to print it with the -- component id to disambiguate it. type QueryQualifyPackage = Unit -> Bool -- | For a given module, we need to know whether to print it with a package -- name to disambiguate it. type QueryQualifyModule = Module -> Bool -- | Given a Name's Module and OccName, decide -- whether and how to qualify it. type QueryQualifyName = Module -> OccName -> QualifyName -- | When printing code that contains original names, we need to map the -- original names back to something the user understands. This is the -- purpose of the triple of functions that gets passed around when -- rendering SDoc. data () => NamePprCtx QueryQualify :: QueryQualifyName -> QueryQualifyModule -> QueryQualifyPackage -> QueryPromotionTick -> NamePprCtx [queryQualifyName] :: NamePprCtx -> QueryQualifyName [queryQualifyModule] :: NamePprCtx -> QueryQualifyModule [queryQualifyPackage] :: NamePprCtx -> QueryQualifyPackage [queryPromotionTick] :: NamePprCtx -> QueryPromotionTick data () => Depth AllTheWay :: Depth -- | 0 => stop PartWay :: Int -> Depth -- | Use sdocDefaultDepth field as depth DefaultDepth :: Depth data () => PprStyle PprUser :: NamePprCtx -> Depth -> Coloured -> PprStyle PprDump :: NamePprCtx -> PprStyle -- | Print code; either C or assembler PprCode :: PprStyle -- | Identifier Details -- -- The IdDetails of an Id give stable, and necessary, -- information about the Id. data () => IdDetails VanillaId :: IdDetails -- | The Id for a record selector RecSelId :: RecSelParent -> Bool -> IdDetails -- | The Id is for a data constructor worker DataConWorkId :: DataCon -> IdDetails -- | The Id is for a data constructor wrapper DataConWrapId :: DataCon -> IdDetails -- | Identifier Information -- -- An IdInfo gives optional information about an -- Id. If present it never lies, but it may not be present, in -- which case there is always a conservative assumption which can be -- made. -- -- Two Ids may have different info even though they have the -- same Unique (and are hence the same Id); for -- example, one might lack the properties attached to the other. -- -- Most of the IdInfo gives information about the value, or -- definition, of the Id, independent of its usage. Exceptions -- to this are demandInfo, occInfo, oneShotInfo and -- callArityInfo. -- -- Performance note: when we update IdInfo, we have to reallocate -- this entire record, so it is a good idea not to let this data -- structure get too big. data () => IdInfo -- | Class of things that we can obtain a Unique from class () => Uniquable a getUnique :: Uniquable a => a -> Unique -- | A class allowing convenient access to the Name of various -- datatypes class () => NamedThing a getOccName :: NamedThing a => a -> OccName getName :: NamedThing a => a -> Name -- | Type or kind Variable type TyVar = Var -- | Whether an Invisible argument may appear in source Haskell. data () => Specificity -- | the argument may appear in source Haskell, but isn't required. SpecifiedSpec :: Specificity data () => VarBndr var argf Bndr :: var -> argf -> VarBndr var argf -- | The non-dependent version of ForAllTyFlag. See Note [FunTyFlag] -- Appears here partly so that it's together with its friends -- ForAllTyFlag and ForallVisFlag, but also because it is used in -- IfaceType, rather early in the compilation chain data () => FunTyFlag FTF_T_T :: FunTyFlag -- | ForAllTyFlag -- -- Is something required to appear in source Haskell (Required), -- permitted by request (Specified) (visible type application), or -- prohibited entirely from appearing in source Haskell -- (Inferred)? See Note [VarBndrs, ForAllTyBinders, TyConBinders, -- and visibility] in GHC.Core.TyCo.Rep data () => ForAllTyFlag Required :: ForAllTyFlag -- | Expressions where binders are CoreBndrs type CoreExpr = Expr CoreBndr -- | The common case for the type of binders and variables when we are -- manipulating the Core language within GHC type CoreBndr = Var -- | This is the data type that represents GHCs core intermediate language. -- Currently GHC uses System FC -- https://www.microsoft.com/en-us/research/publication/system-f-with-type-equality-coercions/ -- for this purpose, which is closely related to the simpler and better -- known System F http://en.wikipedia.org/wiki/System_F. -- -- We get from Haskell source to this Core language in a number of -- stages: -- --
-- f x = let f x = x + 1 -- in f (x - 2) ---- -- Would be renamed by having Uniques attached so it looked -- something like this: -- --
-- f_1 x_2 = let f_3 x_4 = x_4 + 1 -- in f_3 (x_2 - 2) ---- -- But see Note [Shadowing] below. -- --
-- f :: (Eq a) => a -> Int
-- g :: (?x :: Int -> Int) => a -> Int
-- h :: (r\l) => {r} => {l::Int | r}
--
--
-- Here the Eq a and ?x :: Int -> Int and
-- rl are all called "predicates"
type PredType = Type
data () => TyLit
NumTyLit :: Integer -> TyLit
StrTyLit :: FastString -> TyLit
CharTyLit :: Char -> TyLit
-- | For simplicity, we have just one UnivCo that represents a coercion
-- from some type to some other type, with (in general) no restrictions
-- on the type. The UnivCoProvenance specifies more exactly what the
-- coercion really is and why a program should (or shouldn't!) trust the
-- coercion. It is reasonable to consider each constructor of
-- UnivCoProvenance as a totally independent coercion form; their
-- only commonality is that they don't tell you what types they coercion
-- between. (That info is in the UnivCo constructor of
-- Coercion.
data () => UnivCoProvenance
-- | See Note [Phantom coercions]. Only in Phantom roled coercions
PhantomProv :: KindCoercion -> UnivCoProvenance
-- | From the fact that any two coercions are considered equivalent. See
-- Note [ProofIrrelProv]. Can be used in Nominal or Representational
-- coercions
ProofIrrelProv :: KindCoercion -> UnivCoProvenance
-- | A monad for generating unique identifiers
class Monad m => MonadUnique (m :: Type -> Type)
-- | Get a new unique identifier
getUniqueM :: MonadUnique m => m Unique
type Located = GenLocated SrcSpan
-- | We attach SrcSpans to lots of things, so let's have a datatype for it.
data () => GenLocated l e
L :: l -> e -> GenLocated l e
data () => UnhelpfulSpanReason
UnhelpfulNoLocationInfo :: UnhelpfulSpanReason
UnhelpfulWiredIn :: UnhelpfulSpanReason
UnhelpfulInteractive :: UnhelpfulSpanReason
UnhelpfulGenerated :: UnhelpfulSpanReason
UnhelpfulOther :: !FastString -> UnhelpfulSpanReason
-- | Source Span
--
-- A SrcSpan identifies either a specific portion of a text file
-- or a human-readable description of a location.
data () => SrcSpan
RealSrcSpan :: !RealSrcSpan -> !Maybe BufSpan -> SrcSpan
UnhelpfulSpan :: !UnhelpfulSpanReason -> SrcSpan
-- | A RealSrcSpan delimits a portion of a text file. It could be
-- represented by a pair of (line,column) coordinates, but in fact we
-- optimise slightly by using more compact representations for
-- single-line and zero-length spans, both of which are quite common.
--
-- The end position is defined to be the column after the end of
-- the span. That is, a span of (1,1)-(1,2) is one character long, and a
-- span of (1,1)-(1,1) is zero characters long.
--
-- Real Source Span
data () => RealSrcSpan
-- | Real Source Location
--
-- Represents a single point within a file
data () => RealSrcLoc
data () => SourceText
SourceText :: String -> SourceText
-- | For when code is generated, e.g. TH, deriving. The pretty printer will
-- then make its own representation of the item.
NoSourceText :: SourceText
-- | Fields in an algebraic record type; see Note [FieldLabel].
data () => FieldLabel
data () => Bag a
-- | Captures the fixity of declarations as they are parsed. This is not
-- necessarily the same as the fixity declaration, as the normal fixity
-- may be overridden using parens or backticks.
data () => LexicalFixity
Prefix :: LexicalFixity
data () => FixityDirection
InfixR :: FixityDirection
InfixN :: FixityDirection
-- | Enumerates the simple on-or-off dynamic flags
data () => GeneralFlag
Opt_Haddock :: GeneralFlag
Opt_DeferTypedHoles :: GeneralFlag
-- | -- -fPIC --Opt_PIC :: GeneralFlag Opt_ImplicitImportQualified :: GeneralFlag Opt_KeepRawTokenStream :: GeneralFlag type ModuleNameWithIsBoot = GenWithIsBoot ModuleName -- | This data type just pairs a value mod with an IsBootInterface -- flag. In practice, mod is usually a Module or -- ModuleName'. data () => GenWithIsBoot mod -- | Module Location -- -- Where a module lives on the file system: the actual locations of the -- .hs, .hi, .dyn_hi, .o, .dyn_o and .hie files, if we have them. -- -- For a module in another unit, the ml_hs_file and ml_obj_file -- components of ModLocation are undefined. -- -- The locations specified by a ModLocation may or may not correspond to -- actual files yet: for example, even if the object file doesn't exist, -- the ModLocation still contains the path to where the object file will -- reside if/when it is created. -- -- The paths of anything which can affect recompilation should be placed -- inside ModLocation. -- -- When a ModLocation is created none of the filepaths will have -boot -- suffixes. This is because in --make mode the ModLocation is put in the -- finder cache which is indexed by ModuleName, when a ModLocation is -- retrieved from the FinderCache the boot suffixes are appended. The -- other case is in -c mode, there the ModLocation immediately gets given -- the boot suffixes in mkOneShotModLocation. data () => ModLocation -- | Package-qualifier after renaming -- -- Renaming detects if "this" or the unit-id of the home-unit was used as -- a package qualifier. data () => PkgQual -- | No package qualifier NoPkgQual :: PkgQual -- | Located Haskell Expression type LHsExpr p = XRec p HsExpr p -- | Is a TyCon a promoted data constructor or just a normal type -- constructor? data () => PromotionFlag NotPromoted :: PromotionFlag data () => InlinePragma -- | Untyped Phase description data () => Phase StopLn :: Phase -- | A general-purpose pretty-printing precedence type. data () => PprPrec data () => TopLevelFlag NotTopLevel :: TopLevelFlag -- | A data constructor -- --
-- AvailTC Eq [Eq, ==, \/=] --AvailTC :: Name -> [GreName] -> AvailInfo -- | Import Item Specification -- -- Describes import info a particular Name data () => ImpItemSpec -- | The import had no import list, or had a hiding list ImpAll :: ImpItemSpec -- | Import Declaration Specification -- -- Describes a particular import declaration and is shared among all the -- Provenances for that decl data () => ImpDeclSpec ImpDeclSpec :: ModuleName -> ModuleName -> Bool -> SrcSpan -> ImpDeclSpec -- | Module imported, e.g. import Muggle Note the Muggle -- may well not be the defining module for this thing! [is_mod] :: ImpDeclSpec -> ModuleName -- | Import alias, e.g. from as M (or Muggle if there is -- no as clause) [is_as] :: ImpDeclSpec -> ModuleName -- | Was this import qualified? [is_qual] :: ImpDeclSpec -> Bool -- | The location of the entire import declaration [is_dloc] :: ImpDeclSpec -> SrcSpan -- | Import Specification -- -- The ImportSpec of something says how it came to be imported -- It's quite elaborate so that we can give accurate unused-name -- warnings. data () => ImportSpec ImpSpec :: ImpDeclSpec -> ImpItemSpec -> ImportSpec type LocatedN = GenLocated SrcSpanAnnN type GhcRn = GhcPass 'Renamed type GhcPs = GhcPass 'Parsed -- | Located Import Declaration type LImportDecl pass = XRec pass ImportDecl pass -- | An annotation target data () => AnnTarget name -- | We are annotating a particular module ModuleTarget :: Module -> AnnTarget name type AnnPayload = Serialized -- | For now, we work only with nominal equality. data () => CoAxiomRule CoAxiomRule :: FastString -> [Role] -> Role -> ([TypeEqn] -> Maybe TypeEqn) -> CoAxiomRule -- | A CoAxiom is a "coercion constructor", i.e. a named equality -- axiom. data () => CoAxiom (br :: BranchFlag) type Branched = 'Branched data () => Class data () => TyConBndrVis AnonTCB :: FunTyFlag -> TyConBndrVis type TyConBinder = VarBndr TyVar TyConBndrVis data () => GenTickish (pass :: TickishPass) -- | An {-# SCC #-} profiling annotation, either automatically -- added by the desugarer as a result of -auto-all, or added by the user. ProfNote :: CostCentre -> !Bool -> !Bool -> GenTickish (pass :: TickishPass) -- | the cost centre [profNoteCC] :: GenTickish (pass :: TickishPass) -> CostCentre -- | bump the entry count? [profNoteCount] :: GenTickish (pass :: TickishPass) -> !Bool -- | scopes over the enclosed expression (i.e. not just a tick) [profNoteScope] :: GenTickish (pass :: TickishPass) -> !Bool -- | A "tick" used by HPC to track the execution of each subexpression in -- the original source code. HpcTick :: Module -> !Int -> GenTickish (pass :: TickishPass) [tickModule] :: GenTickish (pass :: TickishPass) -> Module [tickId] :: GenTickish (pass :: TickishPass) -> !Int -- | A breakpoint for the GHCi debugger. This behaves like an HPC tick, but -- has a list of free variables which will be available for inspection in -- GHCi when the program stops at the breakpoint. -- -- NB. we must take account of these Ids when (a) counting free -- variables, and (b) substituting (don't substitute for them) Breakpoint :: XBreakpoint pass -> !Int -> [XTickishId pass] -> GenTickish (pass :: TickishPass) [breakpointExt] :: GenTickish (pass :: TickishPass) -> XBreakpoint pass [breakpointId] :: GenTickish (pass :: TickishPass) -> !Int -- | the order of this list is important: it matches the order of the lists -- in the appropriate entry in ModBreaks. -- -- Careful about substitution! See Note [substTickish] in -- GHC.Core.Subst. [breakpointFVs] :: GenTickish (pass :: TickishPass) -> [XTickishId pass] -- | A source note. -- -- Source notes are pure annotations: Their presence should neither -- influence compilation nor execution. The semantics are given by -- causality: The presence of a source note means that a local change in -- the referenced source code span will possibly provoke the generated -- code to change. On the flip-side, the functionality of annotated code -- *must* be invariant against changes to all source code *except* the -- spans referenced in the source notes (see "Causality of optimized -- Haskell" paper for details). -- -- Therefore extending the scope of any given source note is always -- valid. Note that it is still undesirable though, as this reduces their -- usefulness for debugging and profiling. Therefore we will generally -- try only to make use of this property where it is necessary to enable -- optimizations. SourceNote :: RealSrcSpan -> String -> GenTickish (pass :: TickishPass) -- | Source covered [sourceSpan] :: GenTickish (pass :: TickishPass) -> RealSrcSpan -- | Name for source location (uses same names as CCs) [sourceName] :: GenTickish (pass :: TickishPass) -> String type CoreTickish = GenTickish 'TickishPassCore -- | Numeric literal type data () => LitNumType -- | Int# - according to target machine LitNumInt :: LitNumType -- | So-called Literals are one of: -- --
-- f :: Num a => a -> a ---- -- After renaming, this list of Names contains the named wildcards -- brought into scope by this signature. For a signature _ -> _a -- -> Bool, the renamer will leave the unnamed wildcard -- _ untouched, and the named wildcard _a is then -- replaced with fresh meta vars in the type. Their names are stored in -- the type signature that brought them into scope, in this third field -- to be more specific. -- --
-- infixl 8 *** ---- --
-- {#- INLINE f #-}
--
--
-- -- import Control.Monad.Trans.State -- from the "transformers" library -- -- printState :: Show s => StateT s IO () -- printState = do -- state <- get -- liftIO $ print state ---- -- Had we omitted liftIO, we would have ended up with -- this error: -- --
-- • Couldn't match type ‘IO’ with ‘StateT s IO’ -- Expected type: StateT s IO () -- Actual type: IO () ---- -- The important part here is the mismatch between StateT s IO -- () and IO (). -- -- Luckily, we know of a function that takes an IO a and -- returns an (m a): liftIO, enabling us to run -- the program and see the expected results: -- --
-- > evalStateT printState "hello" -- "hello" -- -- > evalStateT printState 3 -- 3 --liftIO :: MonadIO m => IO a -> m a getEnv :: IOEnv env env -- | Gives the filename of the RealSrcLoc srcLocFile :: RealSrcLoc -> FastString parens :: IsLine doc => doc -> doc -- | Module name (e.g. A.B.C) moduleName :: GenModule unit -> ModuleName -- | Unit the module belongs to moduleUnit :: GenModule unit -> unit mkFunTy :: HasDebugCallStack => FunTyFlag -> Mult -> Type -> Type -> Type infixr 3 `mkFunTy` -- | Attempts to tease a type apart into a type constructor and the -- application of a number of arguments to that constructor. Panics if -- that is not possible. See also splitTyConApp_maybe splitTyConApp :: Type -> (TyCon, [Type]) newUnique :: TcRnIf gbl lcl Unique isEmpty :: SDocContext -> SDoc -> Bool -- | Construct an expression which represents the application of a number -- of expressions to another. The leftmost expression in the list is -- applied first mkCoreApps :: CoreExpr -> [CoreExpr] -> CoreExpr infixl 4 `mkCoreApps` -- | Construct an expression which represents the application of a number -- of expressions to that of a data constructor expression. The leftmost -- expression in the list is applied first mkCoreConApps :: DataCon -> [CoreExpr] -> CoreExpr -- | Create a lambda where the given expression has a number of variables -- bound over it. The leftmost binder is that bound by the outermost -- lambda in the result mkCoreLams :: [CoreBndr] -> CoreExpr -> CoreExpr -- | Bind a list of binding groups over an expression. The leftmost binding -- group becomes the outermost group in the resulting expression mkCoreLets :: [CoreBind] -> CoreExpr -> CoreExpr -- | Expand out all type synonyms. Actually, it'd suffice to expand out -- just the ones that discard type variables (e.g. type Funny a = Int) -- But we don't know which those are currently, so we just expand all. -- -- expandTypeSynonyms only expands out type synonyms mentioned in -- the type, not in the kinds of any TyCon or TyVar mentioned in the -- type. -- -- Keep this synchronized with synonymTyConsOfType expandTypeSynonyms :: Type -> Type simplifyInfer :: TcLevel -> InferMode -> [TcIdSigInst] -> [(Name, TcTauType)] -> WantedConstraints -> TcM ([TcTyVar], [EvVar], TcEvBinds, Bool) -- | Panics and asserts. panic :: HasCallStack => String -> a -- | Gives the Modified UTF-8 encoded bytes corresponding to a -- FastString bytesFS :: FastString -> ByteString -- | Create a FastString by copying an existing ByteString mkFastStringByteString :: ByteString -> FastString -- | Creates a UTF-8 encoded FastString from a String mkFastString :: String -> FastString -- | Lazily unpacks and decodes the FastString unpackFS :: FastString -> String concatFS :: [FastString] -> FastString -- | Wrap an unboxed address into a PtrString. mkPtrString# :: Addr# -> PtrString fsLit :: String -> FastString ptext :: PtrString -> SDoc semi :: IsLine doc => doc equals :: IsLine doc => doc lparen :: IsLine doc => doc rparen :: IsLine doc => doc lbrack :: IsLine doc => doc rbrack :: IsLine doc => doc lbrace :: IsLine doc => doc rbrace :: IsLine doc => doc quotes :: SDoc -> SDoc doubleQuotes :: IsLine doc => doc -> doc brackets :: IsLine doc => doc -> doc braces :: IsLine doc => doc -> doc -- | Indent SDoc some specified amount nest :: Int -> SDoc -> SDoc hang :: SDoc -> Int -> SDoc -> SDoc -- | This behaves like hang, but does not indent the second document -- when the header is empty. hangNotEmpty :: SDoc -> Int -> SDoc -> SDoc punctuate :: IsLine doc => doc -> [doc] -> [doc] -- | Join two SDoc together vertically ($+$) :: SDoc -> SDoc -> SDoc -- | A paragraph-fill combinator. It's much like sep, only it keeps fitting -- things on one line until it can't fit any more. cat :: [SDoc] -> SDoc -- | This behaves like fsep, but it uses <> for -- horizontal composition rather than <+> fcat :: [SDoc] -> SDoc -- | Used when constructing a term with an unused extension point. noExtField :: NoExtField moduleNameFS :: ModuleName -> FastString moduleNameString :: ModuleName -> String mkModuleName :: String -> ModuleName mkModuleNameFS :: FastString -> ModuleName mkVarOccFS :: FastString -> OccName isListEmptyOrSingleton :: [a] -> IsEmptyOrSingleton reallyAlwaysQualifyNames :: QueryQualifyName -- | NB: This won't ever show package IDs alwaysQualifyNames :: QueryQualifyName neverQualifyNames :: QueryQualifyName alwaysQualifyModules :: QueryQualifyModule neverQualifyModules :: QueryQualifyModule alwaysQualifyPackages :: QueryQualifyPackage neverQualifyPackages :: QueryQualifyPackage alwaysPrintPromTick :: QueryPromotionTick reallyAlwaysQualify :: NamePprCtx alwaysQualify :: NamePprCtx neverQualify :: NamePprCtx defaultUserStyle :: PprStyle defaultDumpStyle :: PprStyle mkDumpStyle :: NamePprCtx -> PprStyle -- | Default style for error messages, when we don't know NamePprCtx It's a -- bit of a hack because it doesn't take into account what's in scope -- Only used for desugarer warnings, and typechecker errors in interface -- sigs defaultErrStyle :: PprStyle -- | Style for printing error messages mkErrStyle :: NamePprCtx -> PprStyle cmdlineParserStyle :: PprStyle mkUserStyle :: NamePprCtx -> Depth -> PprStyle withUserStyle :: NamePprCtx -> Depth -> SDoc -> SDoc withErrStyle :: NamePprCtx -> SDoc -> SDoc setStyleColoured :: Bool -> PprStyle -> PprStyle runSDoc :: SDoc -> SDocContext -> Doc -- | Default pretty-printing options defaultSDocContext :: SDocContext traceSDocContext :: SDocContext withPprStyle :: PprStyle -> SDoc -> SDoc pprDeeper :: SDoc -> SDoc -- | Truncate a list that is longer than the current depth. pprDeeperList :: ([SDoc] -> SDoc) -> [SDoc] -> SDoc pprSetDepth :: Depth -> SDoc -> SDoc getPprStyle :: (PprStyle -> SDoc) -> SDoc sdocWithContext :: (SDocContext -> SDoc) -> SDoc sdocOption :: (SDocContext -> a) -> (a -> SDoc) -> SDoc updSDocContext :: (SDocContext -> SDocContext) -> SDoc -> SDoc qualName :: PprStyle -> QueryQualifyName qualModule :: PprStyle -> QueryQualifyModule qualPackage :: PprStyle -> QueryQualifyPackage promTick :: PprStyle -> QueryPromotionTick queryQual :: PprStyle -> NamePprCtx codeStyle :: PprStyle -> Bool dumpStyle :: PprStyle -> Bool userStyle :: PprStyle -> Bool -- | Indicate if -dppr-debug mode is enabled getPprDebug :: IsOutput doc => (Bool -> doc) -> doc -- | Says what to do with and without -dppr-debug ifPprDebug :: IsOutput doc => doc -> doc -> doc -- | Says what to do with -dppr-debug; without, return empty whenPprDebug :: IsOutput doc => doc -> doc -- | The analog of printDoc_ for SDoc, which tries to make -- sure the terminal doesn't get screwed up by the ANSI color codes if an -- exception is thrown during pretty-printing. printSDoc :: SDocContext -> Mode -> Handle -> SDoc -> IO () -- | Like printSDoc but appends an extra newline. printSDocLn :: SDocContext -> Mode -> Handle -> SDoc -> IO () -- | An efficient variant of printSDoc specialized for -- LeftMode that outputs to a BufHandle. bufLeftRenderSDoc :: SDocContext -> BufHandle -> SDoc -> IO () pprCode :: SDoc -> SDoc renderWithContext :: SDocContext -> SDoc -> String showSDocOneLine :: SDocContext -> SDoc -> String showSDocUnsafe :: SDoc -> String showPprUnsafe :: Outputable a => a -> String pprDebugAndThen :: SDocContext -> (String -> a) -> SDoc -> SDoc -> a docToSDoc :: Doc -> SDoc -- | doublePrec p n shows a floating point number n with -- p digits of precision after the decimal point. doublePrec :: Int -> Double -> SDoc angleBrackets :: IsLine doc => doc -> doc cparen :: Bool -> SDoc -> SDoc blankLine :: SDoc dcolon :: SDoc arrow :: SDoc lollipop :: SDoc larrow :: SDoc darrow :: SDoc arrowt :: SDoc larrowt :: SDoc arrowtt :: SDoc larrowtt :: SDoc lambda :: SDoc underscore :: IsLine doc => doc dot :: IsLine doc => doc vbar :: IsLine doc => doc forAllLit :: SDoc bullet :: SDoc unicodeSyntax :: SDoc -> SDoc -> SDoc ppWhen :: IsOutput doc => Bool -> doc -> doc ppUnless :: IsOutput doc => Bool -> doc -> doc ppWhenOption :: (SDocContext -> Bool) -> SDoc -> SDoc ppUnlessOption :: IsLine doc => (SDocContext -> Bool) -> doc -> doc -- | Apply the given colour/style for the argument. -- -- Only takes effect if colours are enabled. coloured :: PprColour -> SDoc -> SDoc keyword :: SDoc -> SDoc pprModuleName :: IsLine doc => ModuleName -> doc -- | Special combinator for showing character literals. pprHsChar :: Char -> SDoc -- | Special combinator for showing string literals. pprHsString :: FastString -> SDoc -- | Special combinator for showing bytestring literals. pprHsBytes :: ByteString -> SDoc primCharSuffix :: SDoc primFloatSuffix :: SDoc primIntSuffix :: SDoc primDoubleSuffix :: SDoc primWordSuffix :: SDoc primInt8Suffix :: SDoc primWord8Suffix :: SDoc primInt16Suffix :: SDoc primWord16Suffix :: SDoc primInt32Suffix :: SDoc primWord32Suffix :: SDoc primInt64Suffix :: SDoc primWord64Suffix :: SDoc -- | Special combinator for showing unboxed literals. pprPrimChar :: Char -> SDoc pprPrimInt :: Integer -> SDoc pprPrimWord :: Integer -> SDoc pprPrimInt8 :: Integer -> SDoc pprPrimInt16 :: Integer -> SDoc pprPrimInt32 :: Integer -> SDoc pprPrimInt64 :: Integer -> SDoc pprPrimWord8 :: Integer -> SDoc pprPrimWord16 :: Integer -> SDoc pprPrimWord32 :: Integer -> SDoc pprPrimWord64 :: Integer -> SDoc pprPrefixVar :: Bool -> SDoc -> SDoc pprInfixVar :: Bool -> SDoc -> SDoc pprFastFilePath :: FastString -> SDoc -- | Normalise, escape and render a string representing a path -- -- e.g. "c:\whatever" pprFilePathString :: IsLine doc => FilePath -> doc pprWithCommas :: (a -> SDoc) -> [a] -> SDoc pprWithBars :: (a -> SDoc) -> [a] -> SDoc spaceIfSingleQuote :: SDoc -> SDoc -- | Returns the separated concatenation of the pretty printed things. interppSP :: Outputable a => [a] -> SDoc -- | Returns the comma-separated concatenation of the pretty printed -- things. interpp'SP :: Outputable a => [a] -> SDoc interpp'SP' :: (a -> SDoc) -> [a] -> SDoc -- | Returns the comma-separated concatenation of the quoted pretty printed -- things. -- --
-- [x,y,z] ==> `x', `y', `z' --pprQuotedList :: Outputable a => [a] -> SDoc quotedListWithOr :: [SDoc] -> SDoc quotedListWithNor :: [SDoc] -> SDoc intWithCommas :: Integral a => a -> SDoc -- | Converts an integer to a verbal index: -- --
-- speakNth 1 = text "first" -- speakNth 5 = text "fifth" -- speakNth 21 = text "21st" --speakNth :: Int -> SDoc -- | Converts an integer to a verbal multiplicity: -- --
-- speakN 0 = text "none" -- speakN 5 = text "five" -- speakN 10 = text "10" --speakN :: Int -> SDoc -- | Converts an integer and object description to a statement about the -- multiplicity of those objects: -- --
-- speakNOf 0 (text "melon") = text "no melons" -- speakNOf 1 (text "melon") = text "one melon" -- speakNOf 3 (text "melon") = text "three melons" --speakNOf :: Int -> SDoc -> SDoc -- | Determines the pluralisation suffix appropriate for the length of a -- list: -- --
-- plural [] = char 's' -- plural ["Hello"] = empty -- plural ["Hello", "World"] = char 's' --plural :: [a] -> SDoc -- | Determines the singular verb suffix appropriate for the length of a -- list: -- --
-- singular [] = empty -- singular["Hello"] = char 's' -- singular ["Hello", "World"] = empty --singular :: [a] -> SDoc -- | Determines the form of to be appropriate for the length of a list: -- --
-- isOrAre [] = text "are" -- isOrAre ["Hello"] = text "is" -- isOrAre ["Hello", "World"] = text "are" --isOrAre :: [a] -> SDoc -- | Determines the form of to do appropriate for the length of a list: -- --
-- doOrDoes [] = text "do" -- doOrDoes ["Hello"] = text "does" -- doOrDoes ["Hello", "World"] = text "do" --doOrDoes :: [a] -> SDoc -- | Determines the form of possessive appropriate for the length of a -- list: -- --
-- itsOrTheir [x] = text "its" -- itsOrTheir [x,y] = text "their" -- itsOrTheir [] = text "their" -- probably avoid this --itsOrTheir :: [a] -> SDoc -- | Determines the form of subject appropriate for the length of a list: -- --
-- thisOrThese [x] = text "This" -- thisOrThese [x,y] = text "These" -- thisOrThese [] = text "These" -- probably avoid this --thisOrThese :: [a] -> SDoc -- | "has" or "have" depending on the length of a list. hasOrHave :: [a] -> SDoc bPutHDoc :: BufHandle -> SDocContext -> HDoc -> IO () throwGhcException :: GhcException -> a throwGhcExceptionIO :: GhcException -> IO a -- | Basic IdInfo that carries no useful information whatsoever vanillaIdInfo :: IdInfo emptyPlugins :: Plugins getKey :: Unique -> Int mkUnique :: Char -> Int -> Unique hasKey :: Uniquable a => a -> Unique -> Bool nameOccName :: Name -> OccName -- | Does this TyCon represent a tuple? -- -- NB: when compiling Data.Tuple, the tycons won't reply -- True to isTupleTyCon, because they are built as -- AlgTyCons. However they get spat into the interface file as -- tuple tycons, so I don't think it matters. isTupleTyCon :: TyCon -> Bool mkSrcLoc :: FastString -> Int -> Int -> SrcLoc mkRealSrcLoc :: FastString -> Int -> Int -> RealSrcLoc -- | Raises an error when used on a "bad" RealSrcLoc srcLocLine :: RealSrcLoc -> Int -- | Raises an error when used on a "bad" RealSrcLoc srcLocCol :: RealSrcLoc -> Int -- | Built-in "bad" SrcSpans for common sources of location -- uncertainty noSrcSpan :: SrcSpan -- | Create a "bad" SrcSpan that has not location information mkGeneralSrcSpan :: FastString -> SrcSpan -- | Create a SrcSpan between two points in a file mkRealSrcSpan :: RealSrcLoc -> RealSrcLoc -> RealSrcSpan -- | Create a SrcSpan between two points in a file mkSrcSpan :: SrcLoc -> SrcLoc -> SrcSpan -- | Combines two SrcSpan into one that spans at least all the -- characters within both spans. Returns UnhelpfulSpan if the files -- differ. combineSrcSpans :: SrcSpan -> SrcSpan -> SrcSpan -- | Test if a SrcSpan is "good", i.e. has precise location -- information isGoodSrcSpan :: SrcSpan -> Bool srcSpanStartLine :: RealSrcSpan -> Int srcSpanEndLine :: RealSrcSpan -> Int srcSpanStartCol :: RealSrcSpan -> Int srcSpanEndCol :: RealSrcSpan -> Int realSrcSpanStart :: RealSrcSpan -> RealSrcLoc -- | Obtains the filename for a SrcSpan if it is "good" srcSpanFileName_maybe :: SrcSpan -> Maybe FastString srcSpanToRealSrcSpan :: SrcSpan -> Maybe RealSrcSpan unLoc :: GenLocated l e -> e mkUniqSet :: Uniquable a => [a] -> UniqSet a mkIntegralLit :: Integral a => a -> IntegralLit mkTHFractionalLit :: Rational -> FractionalLit bagToList :: Bag a -> [a] -- | Create a new simple unit identifier from a FastString. -- Internally, this is primarily used to specify wired-in unit -- identifiers. fsToUnit :: FastString -> Unit unitString :: IsUnitId u => u -> String -- | Return the UnitId of the Unit. For on-the-fly instantiated units, -- return the UnitId of the indefinite unit this unit is an instance of. toUnitId :: Unit -> UnitId -- | Get a string representation of a GenModule that's unique and -- stable across recompilations. eg. -- "$aeson_70dylHtv1FFGeai1IoxcQr$Data.Aeson.Types.Internal" moduleStableString :: Module -> String topPrec :: PprPrec funPrec :: PprPrec noOccInfo :: OccInfo isStrongLoopBreaker :: OccInfo -> Bool isDeadOcc :: OccInfo -> Bool -- | Returns an Id which looks like the Haskell-source constructor by using -- the wrapper if it exists (see dataConWrapId_maybe) and failing -- over to the worker (see dataConWorkId) dataConWrapId :: DataCon -> Id -- | The "full signature" of the DataCon returns, in order: -- -- 1) The result of dataConUnivTyVars -- -- 2) The result of dataConExTyCoVars -- -- 3) The non-dependent GADT equalities. Dependent GADT equalities are -- implied by coercion variables in return value (2). -- -- 4) The other constraints of the data constructor type, excluding GADT -- equalities -- -- 5) The original argument types to the DataCon (i.e. before any -- change of the representation of the type) with linearity annotations -- -- 6) The original result type of the DataCon dataConFullSig :: DataCon -> ([TyVar], [TyCoVar], [EqSpec], ThetaType, [Scaled Type], Type) -- | The labels for the fields of this particular DataCon dataConFieldLabels :: DataCon -> [FieldLabel] -- | The existentially-quantified type/coercion variables of the -- constructor including dependent (kind-) GADT equalities dataConExTyCoVars :: DataCon -> [TyCoVar] -- | The type constructor that we are building via this data constructor dataConTyCon :: DataCon -> TyCon -- | Get the Id of the DataCon worker: a function that is the -- "actual" constructor and has no top level binding in the program. The -- type may be different from the obvious one written in the source -- program. Panics if there is no such Id for this DataCon dataConWorkId :: DataCon -> Id -- | The Name of the DataCon, giving it a unique, rooted -- identification dataConName :: DataCon -> Name tupleTyCon :: Boxity -> Arity -> TyCon tupleDataCon :: Boxity -> Arity -> DataCon naturalTy :: Type liftedTypeKind :: Type typeSymbolKind :: Kind listTyCon :: TyCon mkVarOcc :: String -> OccName mkTyVarOcc :: String -> OccName mkTcOcc :: String -> OccName occNameString :: OccName -> String nameSrcLoc :: Name -> SrcLoc nameSrcSpan :: Name -> SrcSpan isExternalName :: Name -> Bool isInternalName :: Name -> Bool nameModule :: HasDebugCallStack => Name -> Module nameModule_maybe :: Name -> Maybe Module isSystemName :: Name -> Bool -- | Create a name which is (for now at least) local to the current module -- and hence does not need a GenModule to disambiguate it from -- other Names mkInternalName :: Unique -> OccName -> SrcSpan -> Name -- | Create a name brought into being by the compiler mkSystemName :: Unique -> OccName -> Name -- | Compare Names lexicographically This only works for Names that -- originate in the source code or have been tidied. stableNameCmp :: Name -> Name -> Ordering -- | Get a string representation of a Name that's unique and stable -- across recompilations. Used for deterministic generation of binds for -- derived instances. eg. -- "$aeson_70dylHtv1FFGeai1IoxcQr$Data.Aeson.Types.Internal$String" nameStableString :: Name -> String getSrcSpan :: NamedThing a => a -> SrcSpan getOccString :: NamedThing a => a -> String varUnique :: Var -> Unique setVarUnique :: Var -> Unique -> Var setVarName :: Var -> Name -> Var setVarType :: Var -> Type -> Var binderVar :: VarBndr tv argf -> tv tyVarKind :: TyVar -> Kind mkTyVar :: Name -> Kind -> TyVar idInfo :: HasDebugCallStack => Id -> IdInfo idDetails :: Id -> IdDetails mkLocalVar :: IdDetails -> Name -> Mult -> Type -> IdInfo -> Id -- | Is this a value-level (i.e., computationally relevant) -- Varentifier? Satisfies isId = not . isTyVar. isId :: Var -> Bool -- | Is this a coercion variable? Satisfies isId v ==> -- isCoVar v == not (isNonCoVarId v). isCoVar :: Var -> Bool isLocalId :: Var -> Bool -- | The same as fst . splitTyConApp We can short-cut the FunTy -- case tyConAppTyCon_maybe :: Type -> Maybe TyCon -- | Attempts to tease a type apart into a type constructor and the -- application of a number of arguments to that constructor splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) -- | A key function: builds a TyConApp or FunTy as -- appropriate to its arguments. Applies its arguments to the constructor -- from left to right. mkTyConApp :: TyCon -> [Type] -> Type emptyVarSet :: VarSet unitVarSet :: Var -> VarSet extendVarSet :: VarSet -> Var -> VarSet extendVarSetList :: VarSet -> [Var] -> VarSet elemVarSet :: Var -> VarSet -> Bool emptyInScopeSet :: InScopeSet mkRnEnv2 :: InScopeSet -> RnEnv2 -- | All names made available by the availability information (excluding -- overloaded selectors) availNames :: AvailInfo -> [Name] -- | A Name for internal use, but not for output to the user. For -- fields, the OccName will be the selector. See Note [GreNames] -- in GHC.Types.Name.Reader. greNameMangledName :: GreName -> Name mkUnqual :: NameSpace -> FastString -> RdrName mkVarUnqual :: FastString -> RdrName -- | Make a qualified RdrName in the given namespace and where the -- ModuleName and the OccName are taken from the first and -- second elements of the tuple respectively mkQual :: NameSpace -> (FastString, FastString) -> RdrName getRdrName :: NamedThing thing => thing -> RdrName nameRdrName :: Name -> RdrName -- | make a GlobalRdrEnv where all the elements point to the same -- Provenance (useful for "hiding" imports, or imports with no details). gresFromAvails :: Maybe ImportSpec -> [AvailInfo] -> [GlobalRdrElt] -- | A Name for the GRE for internal use. Careful: the -- OccName of this Name is not necessarily the same as the -- greOccName (see Note [GreNames]). greMangledName :: GlobalRdrElt -> Name globalRdrEnvElts :: GlobalRdrEnv -> [GlobalRdrElt] -- | Look for this RdrName in the global environment. Omits record -- fields without selector functions (see Note [NoFieldSelectors] in -- GHC.Rename.Env). lookupGRE_RdrName :: RdrName -> GlobalRdrEnv -> [GlobalRdrElt] mkGlobalRdrEnv :: [GlobalRdrElt] -> GlobalRdrEnv getLocA :: GenLocated (SrcSpanAnn' a) e -> SrcSpan noLocA :: a -> LocatedAn an a noAnnSrcSpan :: SrcSpan -> SrcAnn ann -- | Short form for EpAnnNotUsed noAnn :: EpAnn a -- | Module name. ideclName :: ImportDecl pass -> XRec pass ModuleName -- | as Module ideclAs :: ImportDecl pass -> Maybe (XRec pass ModuleName) itName :: Unique -> SrcSpan -> Name dATA_FOLDABLE :: Module gHC_REAL :: Module ge_RDR :: RdrName le_RDR :: RdrName lt_RDR :: RdrName gt_RDR :: RdrName minus_RDR :: RdrName times_RDR :: RdrName plus_RDR :: RdrName and_RDR :: RdrName not_RDR :: RdrName varQual_RDR :: Module -> FastString -> RdrName eqClassName :: Name ordClassName :: Name bindMName :: Name negateName :: Name isStringClassName :: Name eqClassKey :: Unique fractionalClassKey :: Unique ordClassKey :: Unique dollarIdKey :: Unique numericClassKeys :: [Unique] fractionalClassKeys :: [Unique] -- | Find the annotations attached to the given target as Typeable -- values of your choice. If no deserializer is specified, only transient -- annotations will be returned. findAnns :: Typeable a => ([Word8] -> a) -> AnnEnv -> CoreAnnTarget -> [a] coAxiomTyCon :: forall (br :: BranchFlag). CoAxiom br -> TyCon -- | If it is the case that -- --
-- c :: (t1 ~ t2) ---- -- i.e. the kind of c relates t1 and t2, then -- coercionKind c = Pair t1 t2. coercionKind :: Coercion -> Pair Type classAllSelIds :: Class -> [Id] classSCSelIds :: Class -> [Id] classMethods :: Class -> [Id] classSCTheta :: Class -> [PredType] classBigSig :: Class -> ([TyVar], [PredType], [Id], [ClassOpItem]) -- | Create an primitive TyCon, such as Int#, Type -- or RealWorld# Primitive TyCons are marshalable iff not -- lifted. If you'd like to change this, modify marshalablePrimTyCon. mkPrimTyCon :: Name -> [TyConBinder] -> Kind -> [Role] -> TyCon -- | Does this TyCon represent something that cannot be defined in -- Haskell? isPrimTyCon :: TyCon -> Bool -- | Returns True if the supplied TyCon resulted from -- either a data or newtype declaration isAlgTyCon :: TyCon -> Bool -- | Returns True for vanilla AlgTyCons -- that is, those created -- with a data or newtype declaration. isVanillaAlgTyCon :: TyCon -> Bool -- | Is this TyCon that for a newtype isNewTyCon :: TyCon -> Bool -- | Is this a TyCon representing a regular H98 type synonym -- (type)? isTypeSynonymTyCon :: TyCon -> Bool -- | Is this an algebraic TyCon declared with the GADT syntax? isGadtSyntaxTyCon :: TyCon -> Bool -- | Is this a TyCon, synonym or otherwise, that defines a family? isFamilyTyCon :: TyCon -> Bool -- | Is this the TyCon for a boxed tuple? isBoxedTupleTyCon :: TyCon -> Bool -- | Is this a PromotedDataCon? isPromotedDataCon :: TyCon -> Bool -- | As tyConDataCons_maybe, but returns the empty list of -- constructors if no constructors could be found tyConDataCons :: TyCon -> [DataCon] -- | Determine the DataCons originating from the given TyCon, -- if the TyCon is the sort that can have any constructors (note: -- this does not include abstract algebraic types) tyConDataCons_maybe :: TyCon -> Maybe [DataCon] -- | If the given TyCon has a single data constructor, i.e. -- it is a data type with one alternative, a tuple type or a -- newtype then that constructor is returned. If the -- TyCon has more than one constructor, or represents a primitive -- or function type constructor then Nothing is returned. tyConSingleDataCon_maybe :: TyCon -> Maybe DataCon -- | Extract the bound type variables and type expansion of a type synonym -- TyCon. Panics if the TyCon is not a synonym newTyConRhs :: TyCon -> ([TyVar], Type) -- | Extract the TyVars bound by a vanilla type synonym and the -- corresponding (unsubstituted) right hand side. synTyConDefn_maybe :: TyCon -> Maybe ([TyVar], Type) -- | Extract the information pertaining to the right hand side of a type -- synonym (type) declaration. synTyConRhs_maybe :: TyCon -> Maybe Type -- | Is this TyCon that for a class instance? isClassTyCon :: TyCon -> Bool -- | If this TyCon is that for a class instance, return the class it -- is for. Otherwise returns Nothing tyConClass_maybe :: TyCon -> Maybe Class -- | Is this TyCon that for a data family instance? isFamInstTyCon :: TyCon -> Bool -- | If this TyCon is that of a data family instance, return the -- family in question and the instance types. Otherwise, return -- Nothing tyConFamInst_maybe :: TyCon -> Maybe (TyCon, [Type]) mkTyVarTy :: TyVar -> Type mkTyVarTys :: [TyVar] -> [Type] -- | Wraps foralls over the type using the provided TyCoVars from -- left to right mkForAllTys :: [ForAllTyBinder] -> Type -> Type primTyCons :: [TyCon] isArrowTyCon :: TyCon -> Bool eqPrimTyCon :: TyCon eqReprPrimTyCon :: TyCon emptyTvSubstEnv :: TvSubstEnv emptySubst :: Subst -- | Add a substitution from a CoVar to a Coercion to the -- Subst: you must ensure that the in-scope set satisfies Note -- [The substitution invariant] after extending the substitution like -- this extendCvSubst :: Subst -> CoVar -> Coercion -> Subst -- | Generates the in-scope set for the TCvSubst from the types in -- the incoming environment. No CoVars, please! The InScopeSet is just a -- thunk so with a bit of luck it'll never be evaluated mkTvSubstPrs :: [(TyVar, Type)] -> Subst -- | Type substitution, see zipTvSubst substTyWith :: HasDebugCallStack => [TyVar] -> [Type] -> Type -> Type -- | Substitute within a Type The substitution has to satisfy the -- invariants described in Note [The substitution invariant]. substTy :: HasDebugCallStack => Subst -> Type -> Type isTyVarTy :: Type -> Bool -- | Recursively splits a type as far as is possible, leaving a residual -- type being applied to and the type arguments applied to it. Never -- fails, even if that means returning an empty list of type -- applications. splitAppTys :: Type -> (Type, [Type]) -- | Attempts to extract the multiplicity, argument and result types from a -- type splitFunTy_maybe :: Type -> Maybe (FunTyFlag, Mult, Type, Type) splitFunTys :: Type -> ([Scaled Type], Type) -- | (piResultTys f_ty [ty1, .., tyn]) gives the type of (f ty1 .. tyn) -- where f :: f_ty piResultTys is interesting because: 1. -- f_ty may have more for-alls than there are args 2. Less -- obviously, it may have fewer for-alls For case 2. think of: -- piResultTys (forall a.a) [forall b.b, Int] This really can happen, but -- only (I think) in situations involving undefined. For example: -- undefined :: forall a. a Term: undefined (forall b. b->b) -- Int This term should have type (Int -> Int), but notice that -- there are more type args than foralls in undefineds type. piResultTys :: HasDebugCallStack => Type -> [Type] -> Type -- | The same as snd . splitTyConApp tyConAppArgs_maybe :: Type -> Maybe [Type] -- | Unwrap one layer of newtype on a type constructor and its -- arguments, using an eta-reduced version of the newtype if -- possible. This requires tys to have at least newTyConInstArity -- tycon elements. newTyConInstRhs :: TyCon -> [Type] -> Type -- | Take a ForAllTy apart, returning the list of tycovars and the result -- type. This always succeeds, even if it returns only an empty list. -- Note that the result type returned may have free variables that were -- bound by a forall. splitForAllTyCoVars :: Type -> ([TyCoVar], Type) -- | Is this a function? isFunTy :: Type -> Bool -- | Drops all ForAllTys dropForAlls :: Type -> Type -- | Does this classify a type allowed to have values? Responds True to -- things like *, TYPE Lifted, TYPE IntRep, TYPE v, Constraint. -- -- True of a kind `TYPE _` or `CONSTRAINT _` isTYPEorCONSTRAINT :: Kind -> Bool irrelevantMult :: Scaled a -> a -- | Type equality on source types. Does not look through -- newtypes, PredTypes or type families, but it does look -- through type synonyms. This first checks that the kinds of the types -- are equal and then checks whether the types are equal, ignoring casts -- and coercions. (The kind check is a recursive call, but since all -- kinds have type Type, there is no need to check the types of -- kinds.) See also Note [Non-trivial definitional equality] in -- GHC.Core.TyCo.Rep. eqType :: Type -> Type -> Bool nonDetCmpType :: Type -> Type -> Ordering -- | Find the Haskell Type the literal occupies literalType :: Literal -> Type -- | Make a representational reflexive coercion mkRepReflCo :: Type -> Coercion -- | Create an error DiagnosticMessage holding just a single -- SDoc mkPlainError :: [GhcHint] -> SDoc -> DiagnosticMessage -- | Are there any errors or -Werror warnings here? errorsOrFatalWarningsFound :: Messages e -> Bool getLogger :: HasLogger m => m Logger -- | Log something putLogMsg :: Logger -> LogAction pprLocMsgEnvelope :: Diagnostic e => DiagnosticOpts e -> MsgEnvelope e -> SDoc -- | Time a compilation phase. -- -- When timings are enabled (e.g. with the -v2 flag), the -- allocations and CPU time used by the phase will be reported to stderr. -- Consider a typical usage: withTiming getDynFlags (text "simplify") -- force PrintTimings pass. When timings are enabled the following -- costs are included in the produced accounting, -- --
-- T :: forall a b. a -> b -> T [a] ---- -- rather than: -- --
-- T :: forall a c. forall b. (c~[a]) => a -> b -> T c ---- -- The type variables are quantified in the order that the user wrote -- them. See Note [DataCon user type variable binders]. -- -- NB: If the constructor is part of a data instance, the result type -- mentions the family tycon, not the internal one. dataConWrapperType :: DataCon -> Type -- | Finds the instantiated types of the arguments required to construct a -- DataCon representation NB: these INCLUDE any dictionary args -- but EXCLUDE the data-declaration context, which is discarded It's all -- post-flattening etc; this is a representation type dataConInstArgTys :: DataCon -> [Type] -> [Scaled Type] -- | Returns the argument types of the wrapper, excluding all dictionary -- arguments and without substituting for any type variables dataConOrigArgTys :: DataCon -> [Scaled Type] -- | Returns the arg types of the worker, including *all* non-dependent -- evidence, after any flattening has been done and without substituting -- for any type variables dataConRepArgTys :: DataCon -> [Scaled Type] isTupleDataCon :: DataCon -> Bool -- | Vanilla DataCons are those that are nice boring Haskell 98 -- constructors isVanillaDataCon :: DataCon -> Bool classDataCon :: Class -> DataCon -- | Retrieves the template of an unfolding if possible -- maybeUnfoldingTemplate is used mainly when specialising, and we do -- want to specialise DFuns, so it's important to return a template for -- DFunUnfoldings maybeUnfoldingTemplate :: Unfolding -> Maybe CoreExpr cmpAlt :: Alt a -> Alt a -> Ordering -- | Apply a list of argument expressions to a function expression in a -- nested fashion. Prefer to use mkCoreApps if possible mkApps :: Expr b -> [Arg b] -> Expr b infixl 4 `mkApps` -- | Apply a list of type argument expressions to a function expression in -- a nested fashion mkTyApps :: Expr b -> [Type] -> Expr b infixl 4 `mkTyApps` mkTyArg :: Type -> Expr b -- | Bind all supplied binders over an expression in a nested lambda -- expression. Prefer to use mkCoreLams if possible mkLams :: [b] -> Expr b -> Expr b -- | Extract every variable by this group bindersOf :: Bind b -> [b] -- | Collapse all the bindings in the supplied groups into a single list of -- lhs/rhs pairs suitable for binding in a Rec binding group flattenBinds :: [Bind b] -> [(b, Expr b)] -- | We often want to strip off leading lambdas before getting down to -- business. Variants are collectTyBinders, -- collectValBinders, and collectTyAndValBinders collectBinders :: Expr b -> ([b], Expr b) collectTyBinders :: CoreExpr -> ([TyVar], CoreExpr) collectTyAndValBinders :: CoreExpr -> ([TyVar], [Id], CoreExpr) -- | Takes a nested application expression and returns the function being -- applied and the arguments to which it is applied collectArgs :: Expr b -> (Expr b, [Arg b]) -- | Returns True iff the expression is a Type expression -- at its top level. Note this does NOT include Coercions. isTypeArg :: Expr b -> Bool -- | Id CAF info cafInfo :: IdInfo -> CafInfo setOccInfo :: IdInfo -> OccInfo -> IdInfo infixl 1 `setOccInfo` setCafInfo :: IdInfo -> CafInfo -> IdInfo infixl 1 `setCafInfo` mayHaveCafRefs :: CafInfo -> Bool idType :: Id -> Kind setIdInfo :: Id -> IdInfo -> Id modifyIdInfo :: HasDebugCallStack => (IdInfo -> IdInfo) -> Id -> Id -- | Create a local Id that is marked as exported. This prevents -- things attached to it from being removed as dead code. See Note -- [Exported LocalIds] mkExportedLocalId :: IdDetails -> Name -> Type -> Id -- | Create a user local Id. These are local Ids (see -- GHC.Types.Var#globalvslocal) with a name and location that the -- user might recognize mkUserLocal :: OccName -> Unique -> Mult -> Type -> SrcSpan -> Id isRecordSelector :: Id -> Bool isClassOpId_maybe :: Id -> Maybe Class isDFunId :: Id -> Bool -- | Get from either the worker or the wrapper Id to the -- DataCon. Currently used only in the desugarer. -- -- INVARIANT: idDataCon (dataConWrapId d) = d: remember, -- dataConWrapId can return either the wrapper or the worker idDataCon :: Id -> DataCon -- | Expose the unfolding if there is one, including for loop breakers realIdUnfolding :: Id -> Unfolding idOccInfo :: Id -> OccInfo isConLikeId :: Id -> Bool intTyConName :: Name boolTyConName :: Name listTyConName :: Name anyTy :: Type true_RDR :: RdrName charTyCon :: TyCon charDataCon :: DataCon stringTy :: Type intTy :: Type intTyCon :: TyCon intDataCon :: DataCon boolTy :: Type boolTyCon :: TyCon falseDataCon :: DataCon trueDataCon :: DataCon falseDataConId :: Id trueDataConId :: Id nilDataCon :: DataCon consDataCon :: DataCon -- | Find all locally-defined free Ids or type variables in an expression -- returning a deterministically ordered list. exprFreeVarsList :: CoreExpr -> [Var] emptyFamInstEnv :: FamInstEnv famInstEnvElts :: FamInstEnv -> [FamInst] -- | Get rid of *outermost* (or toplevel) * type function redex * data -- family redex * newtypes returning an appropriate Representational -- coercion. Specifically, if topNormaliseType_maybe env ty = Just (co, -- ty') then (a) co :: ty ~R ty' (b) ty' is not a newtype, and is not a -- type-family or data-family redex -- -- However, ty' can be something like (Maybe (F ty)), where (F ty) is a -- redex. -- -- Always operates homogeneously: the returned type has the same kind as -- the original type, and the returned coercion is always homogeneous. topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe Reduction -- | Recover the type of a well-typed Core expression. Fails when applied -- to the actual Type expression as it cannot really be said to -- have a type exprType :: HasDebugCallStack => CoreExpr -> Type -- | Add a substitution for an Id to the Subst: you must -- ensure that the in-scope set is such that TyCoSubst Note [The -- substitution invariant] holds after extending the substitution like -- this extendIdSubst :: Subst -> Id -> CoreExpr -> Subst -- | substExpr applies a substitution to an entire CoreExpr. -- Remember, you may only apply the substitution once: See Note -- [Substitutions apply only once] in GHC.Core.TyCo.Subst -- -- Do *not* attempt to short-cut in the case of an empty substitution! -- See Note [Extending the IdSubstEnv] substExpr :: HasDebugCallStack => Subst -> CoreExpr -> CoreExpr occurAnalysePgm :: Module -> (Id -> Bool) -> (Activation -> Bool) -> [CoreRule] -> CoreProgram -> CoreProgram pAT_ERROR_ID :: Id mkHsForAllInvisTele :: forall (p :: Pass). EpAnnForallTy -> [LHsTyVarBndr Specificity (GhcPass p)] -> HsForAllTelescope (GhcPass p) getDynFlags :: HasDynFlags m => m DynFlags -- | Test whether a GeneralFlag is set -- -- Note that dynamicNow (i.e., dynamic objects built with -- `-dynamic-too`) always implicitly enables Opt_PIC, -- Opt_ExternalDynamicRefs, and disables Opt_SplitSections. gopt :: GeneralFlag -> DynFlags -> Bool -- | Set a GeneralFlag gopt_set :: DynFlags -> GeneralFlag -> DynFlags -- | Set a Extension xopt_set :: DynFlags -> Extension -> DynFlags -- | Sets the DynFlags to be appropriate to the optimisation level updOptLevel :: Int -> DynFlags -> DynFlags tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type]) tcSplitMethodTy :: Type -> ([TyVar], PredType, Type) instanceDFunId :: ClsInst -> DFunId instanceSig :: ClsInst -> ([TyVar], [Type], Class, [Type]) instEnvElts :: InstEnv -> [ClsInst] -- | Show a SDoc as a String with the default user style showSDoc :: DynFlags -> SDoc -> String showPpr :: Outputable a => DynFlags -> a -> String failM :: IOEnv env a mkHsApp :: forall (id :: Pass). LHsExpr (GhcPass id) -> LHsExpr (GhcPass id) -> LHsExpr (GhcPass id) mkHsLam :: forall (p :: Pass). (IsPass p, XMG (GhcPass p) (LHsExpr (GhcPass p)) ~ Origin) => [LPat (GhcPass p)] -> LHsExpr (GhcPass p) -> LHsExpr (GhcPass p) mkHsIntegral :: IntegralLit -> HsOverLit GhcPs mkHsFractional :: FractionalLit -> HsOverLit GhcPs nlHsVar :: forall (p :: Pass) a. IsSrcSpanAnn p a => IdP (GhcPass p) -> LHsExpr (GhcPass p) nlVarPat :: forall (p :: Pass) a. IsSrcSpanAnn p a => IdP (GhcPass p) -> LPat (GhcPass p) nlHsIf :: LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs nlList :: [LHsExpr GhcPs] -> LHsExpr GhcPs nlHsAppTy :: forall (p :: Pass). LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p) nlHsTyVar :: forall (p :: Pass) a. IsSrcSpanAnn p a => PromotionFlag -> IdP (GhcPass p) -> LHsType (GhcPass p) nlHsFunTy :: forall (p :: Pass). LHsType (GhcPass p) -> LHsType (GhcPass p) -> LHsType (GhcPass p) nlHsTyConApp :: forall (p :: Pass) a. IsSrcSpanAnn p a => PromotionFlag -> LexicalFixity -> IdP (GhcPass p) -> [LHsTypeArg (GhcPass p)] -> LHsType (GhcPass p) -- | Convert an LHsType to an LHsSigType. hsTypeToHsSigType :: LHsType GhcPs -> LHsSigType GhcPs -- | Convert an LHsType to an LHsSigWcType. hsTypeToHsSigWcType :: LHsType GhcPs -> LHsSigWcType GhcPs mkHsDictLet :: TcEvBinds -> LHsExpr GhcTc -> LHsExpr GhcTc -- | Extract a suitable CtOrigin from a HsExpr lexprCtOrigin :: LHsExpr GhcRn -> CtOrigin lookupHpt :: HomePackageTable -> ModuleName -> Maybe HomeModInfo ue_hpt :: HasDebugCallStack => UnitEnv -> HomePackageTable ms_mod_name :: ModSummary -> ModuleName mkTcRnUnknownMessage :: (Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) => a -> TcRnMessage srcErrorMessages :: SourceError -> Messages GhcMessage printMessages :: Diagnostic a => Logger -> DiagnosticOpts a -> DiagOpts -> Messages a -> IO () -- | Initialise the general configuration for printing diagnostic messages -- For example, this configuration controls things like whether warnings -- are treated like errors. initDiagOpts :: DynFlags -> DiagOpts initDsMessageOpts :: DynFlags -> DiagnosticOpts DsMessage getSession :: GhcMonad m => m HscEnv -- | Call the argument with the current session. withSession :: GhcMonad m => (HscEnv -> m a) -> m a purePlugin :: [CommandLineOption] -> IO PluginRecompile -- | Default plugin: does nothing at all, except for marking that safe -- inference has failed unless -fplugin-trustworthy is passed. -- For compatibility reason you should base all your plugin definitions -- on this default value. defaultPlugin :: Plugin -- | Locate a module that was imported by the user. We have the module's -- name, and possibly a package name. Without a package name, this -- function will use the search path and the known exposed packages to -- find the module, if a package is specified then only that package is -- searched for the module. findImportedModule :: HscEnv -> ModuleName -> PkgQual -> IO FindResult findExposedPackageModule :: FinderCache -> FinderOpts -> UnitState -> ModuleName -> PkgQual -> IO FindResult isNumericClass :: Class -> Bool cannotFindModule :: HscEnv -> ModuleName -> FindResult -> SDoc rnLExpr :: LHsExpr GhcPs -> RnM (LHsExpr GhcRn, FreeVars) tcInferRho :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType) addErrAt :: SrcSpan -> TcRnMessage -> TcRn () addErrs :: [(SrcSpan, TcRnMessage)] -> TcRn () reportDiagnostics :: [MsgEnvelope TcRnMessage] -> TcM () reportDiagnostic :: MsgEnvelope TcRnMessage -> TcRn () failIfErrsM :: TcRn () captureConstraints :: TcM a -> TcM (a, WantedConstraints) failWithTc :: TcRnMessage -> TcM a -- | Throw out any constraints emitted by the thing_inside discardConstraints :: TcM a -> TcM a pushTcLevelM :: TcM a -> TcM (TcLevel, a) -- | Run an IfG (top-level interface monad) computation inside an -- existing TcRn (typecheck-renaming monad) computation by -- initializing an IfGblEnv based on TcGblEnv. initIfaceTcRn :: IfG a -> TcRn a loadInterface :: SDoc -> Module -> WhereFrom -> IfM lcl (MaybeErr SDoc ModIface) -- | Run a DsM action inside the TcM monad. initDsTc :: DsM a -> TcM (Messages DsMessage, Maybe a) -- | Run a DsM action in the context of an existing ModGuts initDsWithModGuts :: HscEnv -> ModGuts -> DsM a -> IO (Messages DsMessage, Maybe a) -- | Replace the body of the function with this block to test the -- hsExprType function in GHC.Tc.Utils.Zonk: putSrcSpanDs loc $ do { -- core_expr <- dsExpr e ; massertPpr (exprType core_expr -- eqType hsExprType e) (ppr e + dcolon + ppr -- (hsExprType e) $$ ppr core_expr + dcolon + ppr (exprType -- core_expr)) ; return core_expr } dsLExpr :: LHsExpr GhcTc -> DsM CoreExpr zonkTopLExpr :: LHsExpr GhcTc -> TcM (LHsExpr GhcTc) captureTopConstraints :: TcM a -> TcM (a, WantedConstraints) simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind) -- | Rename raw package imports renamePkgQual :: UnitEnv -> ModuleName -> Maybe FastString -> PkgQual tcValBinds :: TopLevelFlag -> [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn] -> TcM thing -> TcM ([(RecFlag, LHsBinds GhcTc)], thing) tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType -- | ASSUMES that the module is either in the HomePackageTable or -- is a package module with an interface on disk. If neither of these is -- true, then the result will be an error indicating the interface could -- not be found. getModuleInterface :: HscEnv -> Module -> IO (Messages TcRnMessage, Maybe ModIface) hscTcRcLookupName :: HscEnv -> Name -> IO (Maybe TyThing) -- | Convert a typechecked module to Core hscDesugar :: HscEnv -> ModSummary -> TcGblEnv -> IO ModGuts compileFile :: HscEnv -> StopPhase -> (FilePath, Maybe Phase) -> IO (Maybe FilePath) modInfoTopLevelScope :: ModuleInfo -> Maybe [Name] isDictonaryId :: Id -> Bool -- | Put a Typeable value that we are able to actually turn into bytes into -- a Serialized value ready for deserialization later toSerialized :: Typeable a => (a -> [Word8]) -> a -> Serialized -- | If the Serialized value contains something of the given type, -- then use the specified deserializer to return Just that. -- Otherwise return Nothing. fromSerialized :: Typeable a => ([Word8] -> a) -> Serialized -> Maybe a -- | Use a Data instance to implement a deserialization scheme dual -- to that of serializeWithData deserializeWithData :: Data a => [Word8] -> a -- | Extract top-level comments from a module. apiComments :: ParsedModule -> [Located ApiComment] apiCommentsParsedSource :: Located (HsModule GhcPs) -> [Located ApiComment] dataConSig :: DataCon -> ([TyCoVar], ThetaType, [Type], Type) -- | Desugar a typechecked module. desugarModuleIO :: HscEnv -> ModSummary -> TypecheckedModuleLH -> IO ModGuts fsToUnitId :: FastString -> UnitId -- | Tells if a case alternative calls to patError isPatErrorAlt :: CoreAlt -> Bool lookupModSummary :: HscEnv -> ModuleName -> Maybe ModSummary modInfoLookupNameIO :: HscEnv -> ModuleInfoLH -> Name -> IO (Maybe TyThing) moduleInfoTc :: HscEnv -> TcGblEnv -> IO ModuleInfoLH parseModuleIO :: HscEnv -> ModSummary -> IO ParsedModule qualifiedNameFS :: Name -> FastString -- | The collection of dependencies and usages modules which are relevant -- for liquidHaskell relevantModules :: ModuleGraph -> ModGuts -> Set Module renderWithStyle :: DynFlags -> SDoc -> PprStyle -> String showPprQualified :: Outputable a => a -> String showSDocQualified :: SDoc -> String strictNothing :: Maybe a thisPackage :: DynFlags -> UnitId tyConRealArity :: TyCon -> Int typecheckModuleIO :: HscEnv -> ParsedModule -> IO TypecheckedModuleLH -- | Creates a new StableModule out of a ModuleName and a -- UnitId. mkStableModule :: UnitId -> ModuleName -> StableModule -- | Converts a Module into a StableModule. toStableModule :: Module -> StableModule renderModule :: Module -> String module Language.Haskell.Liquid.GHC.Types -- | A StableName is virtually isomorphic to a GHC's Name but -- crucially we don't use the Eq instance defined on a Name -- because it's Unique-based. In particular, GHC doesn't -- guarantee that if we load an interface multiple times we would get the -- same Unique for the same Name, and this is a problem -- when we rely on Names to be the same when we call -- isExportedVar, which used to use a NameSet derived -- from the '[AvailInfo]'. As the name implies, a NameSet uses a -- Names Unique for duplicate detection and indexing, and -- this would lead to Vars being resolved to a Name which -- is basically the same, but it has a different Unique, -- and that would cause the lookup inside the NameSet to fail. newtype StableName MkStableName :: Name -> StableName [unStableName] :: StableName -> Name -- | Creates a new StableName out of a Name. mkStableName :: Name -> StableName -- | Converts a list of AvailInfo into a "StableNameSet", similarly -- to what availsToNameSet would do. availsToStableNameSet :: [AvailInfo] -> HashSet StableName -- | Datatype For Holding GHC ModGuts -- ------------------------------------------ data MGIModGuts MI :: !CoreProgram -> !Module -> ![TyCon] -> !HashSet StableName -> !Maybe [ClsInst] -> MGIModGuts [mgi_binds] :: MGIModGuts -> !CoreProgram [mgi_module] :: MGIModGuts -> !Module [mgi_tcs] :: MGIModGuts -> ![TyCon] [mgi_exports] :: MGIModGuts -> !HashSet StableName [mgi_cls_inst] :: MGIModGuts -> !Maybe [ClsInst] miModGuts :: Maybe [ClsInst] -> ModGuts -> MGIModGuts mgiNamestring :: MGIModGuts -> String instance GHC.Generics.Generic Language.Haskell.Liquid.GHC.Types.StableName instance GHC.Show.Show Language.Haskell.Liquid.GHC.Types.StableName instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.GHC.Types.StableName instance GHC.Classes.Eq Language.Haskell.Liquid.GHC.Types.StableName module Paths_liquidhaskell_boot version :: Version getBinDir :: IO FilePath getLibDir :: IO FilePath getDynLibDir :: IO FilePath getDataDir :: IO FilePath getLibexecDir :: IO FilePath getDataFileName :: FilePath -> IO FilePath getSysconfDir :: IO FilePath module Language.Haskell.Liquid.Misc type Nat = Int (.&&.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool (.||.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool up :: (b -> c -> d) -> (a -> b) -> (a -> c) -> a -> d timedAction :: Show msg => Maybe msg -> IO a -> IO a (!?) :: [a] -> Int -> Maybe a safeFromJust :: String -> Maybe t -> t safeFromLeft :: String -> Either a b -> a takeLast :: Int -> [a] -> [a] getNth :: Int -> [a] -> Maybe a fst4 :: (t, t1, t2, t3) -> t snd4 :: (t, t1, t2, t3) -> t1 thd4 :: (t1, t2, t3, t4) -> t3 thrd3 :: (t1, t2, t3) -> t3 mapFifth5 :: (t -> t4) -> (t0, t1, t2, t3, t) -> (t0, t1, t2, t3, t4) mapFourth4 :: (t -> t4) -> (t1, t2, t3, t) -> (t1, t2, t3, t4) addFst3 :: t -> (t1, t2) -> (t, t1, t2) addThd3 :: t2 -> (t, t1) -> (t, t1, t2) dropFst3 :: (t, t1, t2) -> (t1, t2) dropThd3 :: (t1, t2, t) -> (t1, t2) replaceN :: (Enum a, Eq a, Num a) => a -> t -> [t] -> [t] thd5 :: (t0, t1, t2, t3, t4) -> t2 snd5 :: (t0, t1, t2, t3, t4) -> t1 fst5 :: (t0, t1, t2, t3, t4) -> t0 fourth4 :: (t, t1, t2, t3) -> t3 third4 :: (t, t1, t2, t3) -> t2 mapSndM :: Applicative m => (b -> m c) -> (a, b) -> m (a, c) firstM :: Functor f => (t -> f a) -> (t, t1) -> f (a, t1) secondM :: Functor f => (t -> f a) -> (t1, t) -> f (t1, a) first3M :: Functor f => (t -> f a) -> (t, t1, t2) -> f (a, t1, t2) second3M :: Functor f => (t -> f a) -> (t1, t, t2) -> f (t1, a, t2) third3M :: Functor f => (t -> f a) -> (t1, t2, t) -> f (t1, t2, a) third3 :: (t -> t3) -> (t1, t2, t) -> (t1, t2, t3) zip4 :: [t] -> [t1] -> [t2] -> [t3] -> [(t, t1, t2, t3)] zip5 :: [t] -> [t1] -> [t2] -> [t3] -> [t4] -> [(t, t1, t2, t3, t4)] unzip4 :: [(t, t1, t2, t3)] -> ([t], [t1], [t2], [t3]) getCssPath :: IO FilePath getCoreToLogicPath :: IO FilePath zipMaybe :: [a] -> [b] -> Maybe [(a, b)] safeZipWithError :: String -> [t] -> [t1] -> [(t, t1)] safeZip3WithError :: String -> [t] -> [t1] -> [t2] -> [(t, t1, t2)] safeZip4WithError :: String -> [t1] -> [t2] -> [t3] -> [t4] -> [(t1, t2, t3, t4)] mapNs :: (Eq a, Num a, Foldable t) => t a -> (a1 -> a1) -> [a1] -> [a1] mapN :: (Eq a, Num a) => a -> (a1 -> a1) -> [a1] -> [a1] zipWithDefM :: Monad m => (a -> a -> m a) -> [a] -> [a] -> m [a] zipWithDef :: (a -> a -> a) -> [a] -> [a] -> [a] single :: t -> [t] mapFst3 :: (t -> t1) -> (t, t2, t3) -> (t1, t2, t3) mapSnd3 :: (t -> t2) -> (t1, t, t3) -> (t1, t2, t3) mapThd3 :: (t -> t3) -> (t1, t2, t) -> (t1, t2, t3) hashMapMapWithKey :: (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2 hashMapMapKeys :: (Eq k2, Hashable k2) => (k1 -> k2) -> HashMap k1 v -> HashMap k2 v concatMapM :: (Monad m, Traversable t) => (a -> m [b]) -> t a -> m [b] replaceSubset :: (Eq k, Hashable k) => [(k, a)] -> [(k, a)] -> [(k, a)] replaceWith :: (Eq a, Hashable a) => (b -> a) -> [b] -> [b] -> [b] firstElems :: [(ByteString, ByteString)] -> ByteString -> Maybe (Int, ByteString, (ByteString, ByteString)) splitters :: [(ByteString, t)] -> ByteString -> [(Int, t, (ByteString, ByteString))] bchopAlts :: [(ByteString, ByteString)] -> ByteString -> [ByteString] chopAlts :: [(String, String)] -> String -> [String] sortDiff :: Ord a => [a] -> [a] -> [a] (<->) :: Doc -> Doc -> Doc angleBrackets :: Doc -> Doc mkGraph :: (Eq a, Eq b, Hashable a, Hashable b) => [(a, b)] -> HashMap a (HashSet b) tryIgnore :: String -> IO () -> IO () condNull :: Monoid m => Bool -> m -> m firstJust :: (a -> Maybe b) -> [a] -> Maybe b intToString :: Int -> String mapAccumM :: (Monad m, Traversable t) => (a -> b -> m (a, c)) -> a -> t b -> m (a, t c) ifM :: Monad m => m Bool -> m b -> m b -> m b nubHashOn :: (Eq k, Hashable k) => (a -> k) -> [a] -> [a] nubHashLast :: (Eq k, Hashable k) => (a -> k) -> [a] -> [a] nubHashLastM :: (Eq k, Hashable k, Monad m) => (a -> m k) -> [a] -> m [a] uniqueByKey :: (Eq k, Hashable k) => [(k, v)] -> Either (k, [v]) [v] uniqueByKey' :: (Eq k, Hashable k) => ((k, [v]) -> Either e v) -> [(k, v)] -> Either e [v] join :: (Eq b, Hashable b) => [(a, b)] -> [(b, c)] -> [(a, c)] fstByRank :: (Ord r, Hashable k, Eq k) => [(r, k, v)] -> [(r, k, v)] sortOn :: Ord b => (a -> b) -> [a] -> [a] firstGroup :: (Eq k, Ord k, Hashable k) => [(k, a)] -> [a] mapErr :: (a -> Either e b) -> [a] -> Either [e] [b] catEithers :: [Either a b] -> Either [a] [b] keyDiff :: (Eq k, Hashable k) => (a -> k) -> [a] -> [a] -> [a] concatUnzip :: [([a], [b])] -> ([a], [b]) sayReadFile :: FilePath -> IO String lastModified :: FilePath -> IO (Maybe UTCTime) data Validate e a Err :: e -> Validate e a Val :: a -> Validate e a instance GHC.Base.Functor (Language.Haskell.Liquid.Misc.Validate e) instance GHC.Base.Monoid e => GHC.Base.Applicative (Language.Haskell.Liquid.Misc.Validate e) -- | This module contains the *types* related creating Errors. It depends -- only on Fixpoint and basic haskell libraries, and hence, should be -- importable everywhere. module Language.Haskell.Liquid.Types.Errors -- | Generic Type for Error Messages -- ------------------------------------------- -- -- INVARIANT : all Error constructors should have a pos field data TError t -- | liquid type error ErrSubType :: !SrcSpan -> !Doc -> Maybe SubcId -> !HashMap Symbol t -> !t -> !t -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [msg] :: TError t -> !Doc [cid] :: TError t -> Maybe SubcId [ctx] :: TError t -> !HashMap Symbol t [tact] :: TError t -> !t [texp] :: TError t -> !t -- | liquid type error with a counter-example ErrSubTypeModel :: !SrcSpan -> !Doc -> Maybe SubcId -> !HashMap Symbol (WithModel t) -> !WithModel t -> !t -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [msg] :: TError t -> !Doc [cid] :: TError t -> Maybe SubcId [ctxM] :: TError t -> !HashMap Symbol (WithModel t) [tactM] :: TError t -> !WithModel t [texp] :: TError t -> !t -- | liquid type error ErrFCrash :: !SrcSpan -> !Doc -> !HashMap Symbol t -> !t -> !t -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [msg] :: TError t -> !Doc [ctx] :: TError t -> !HashMap Symbol t [tact] :: TError t -> !t [texp] :: TError t -> !t -- | hole type ErrHole :: !SrcSpan -> !Doc -> !HashMap Symbol t -> !Symbol -> !t -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [msg] :: TError t -> !Doc [ctx] :: TError t -> !HashMap Symbol t [svar] :: TError t -> !Symbol [thl] :: TError t -> !t -- | hole dependencies form a cycle error ErrHoleCycle :: !SrcSpan -> [Symbol] -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [holesCycle] :: TError t -> [Symbol] -- | condition failure error ErrAssType :: !SrcSpan -> !Oblig -> !Doc -> !HashMap Symbol t -> t -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [obl] :: TError t -> !Oblig [msg] :: TError t -> !Doc [ctx] :: TError t -> !HashMap Symbol t [cond] :: TError t -> t -- | specification parse error ErrParse :: !SrcSpan -> !Doc -> !ParseError -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [msg] :: TError t -> !Doc [pErr] :: TError t -> !ParseError -- | sort error in specification ErrTySpec :: !SrcSpan -> !Maybe Doc -> !Doc -> !t -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [knd] :: TError t -> !Maybe Doc [var] :: TError t -> !Doc [typ] :: TError t -> !t [msg] :: TError t -> !Doc -- | sort error in specification ErrTermSpec :: !SrcSpan -> !Doc -> !Doc -> !Expr -> !t -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [msg] :: TError t -> !Doc [exp] :: TError t -> !Expr [typ] :: TError t -> !t [msg'] :: TError t -> !Doc -- | multiple alias with same name error ErrDupAlias :: !SrcSpan -> !Doc -> !Doc -> ![SrcSpan] -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [kind] :: TError t -> !Doc [locs] :: TError t -> ![SrcSpan] -- | multiple specs for same binder error ErrDupSpecs :: !SrcSpan -> !Doc -> ![SrcSpan] -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [locs] :: TError t -> ![SrcSpan] -- | multiple definitions of the same instance measure ErrDupIMeas :: !SrcSpan -> !Doc -> !Doc -> ![SrcSpan] -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [tycon] :: TError t -> !Doc [locs] :: TError t -> ![SrcSpan] -- | multiple definitions of the same measure ErrDupMeas :: !SrcSpan -> !Doc -> ![SrcSpan] -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [locs] :: TError t -> ![SrcSpan] -- | duplicate fields in same datacon ErrDupField :: !SrcSpan -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [dcon] :: TError t -> !Doc [field] :: TError t -> !Doc -- | name resolves to multiple possible GHC vars ErrDupNames :: !SrcSpan -> !Doc -> ![Doc] -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [names] :: TError t -> ![Doc] -- | bad data type specification (?) ErrBadData :: !SrcSpan -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [msg] :: TError t -> !Doc -- | refined datacon mismatches haskell datacon ErrDataCon :: !SrcSpan -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [msg] :: TError t -> !Doc -- | constructors in refinement do not match original datatype ErrDataConMismatch :: !SrcSpan -> !Doc -> [Doc] -> [Doc] -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [dcs] :: TError t -> [Doc] [rdcs] :: TError t -> [Doc] -- | Invariant sort error ErrInvt :: !SrcSpan -> !t -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [inv] :: TError t -> !t [msg] :: TError t -> !Doc -- | Using sort error ErrIAl :: !SrcSpan -> !t -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [inv] :: TError t -> !t [msg] :: TError t -> !Doc -- | Incompatible using error ErrIAlMis :: !SrcSpan -> !t -> !t -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [tAs] :: TError t -> !t [tUs] :: TError t -> !t [msg] :: TError t -> !Doc -- | Measure sort error ErrMeas :: !SrcSpan -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [ms] :: TError t -> !Doc [msg] :: TError t -> !Doc -- | Haskell bad Measure error ErrHMeas :: !SrcSpan -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [ms] :: TError t -> !Doc [msg] :: TError t -> !Doc -- | Unbound symbol in specification ErrUnbound :: !SrcSpan -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc -- | Unbound predicate being applied ErrUnbPred :: !SrcSpan -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc -- | GHC error: parsing or type checking ErrGhc :: !SrcSpan -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [msg] :: TError t -> !Doc -- | Name resolution error ErrResolve :: !SrcSpan -> !Doc -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [kind] :: TError t -> !Doc [var] :: TError t -> !Doc [msg] :: TError t -> !Doc ErrMismatch :: !SrcSpan -> !Doc -> !Doc -> !Doc -> !Doc -> !Maybe (Doc, Doc) -> !SrcSpan -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [msg] :: TError t -> !Doc [hs] :: TError t -> !Doc [lqTy] :: TError t -> !Doc -- | specific pair of things that mismatch [diff] :: TError t -> !Maybe (Doc, Doc) -- | lq type location [lqPos] :: TError t -> !SrcSpan -- | Mismatch in expected/actual args of abstract refinement ErrPartPred :: !SrcSpan -> !Doc -> !Doc -> !Int -> !Int -> !Int -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [ectr] :: TError t -> !Doc [var] :: TError t -> !Doc [argN] :: TError t -> !Int [expN] :: TError t -> !Int [actN] :: TError t -> !Int -- | Cyclic Refined Type Alias Definitions ErrAliasCycle :: !SrcSpan -> ![(SrcSpan, Doc)] -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [acycle] :: TError t -> ![(SrcSpan, Doc)] -- | Illegal RTAlias application (from BSort, eg. in PVar) ErrIllegalAliasApp :: !SrcSpan -> !Doc -> !SrcSpan -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [dname] :: TError t -> !Doc [dpos] :: TError t -> !SrcSpan ErrAliasApp :: !SrcSpan -> !Doc -> !SrcSpan -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [dname] :: TError t -> !Doc [dpos] :: TError t -> !SrcSpan [msg] :: TError t -> !Doc -- | Termination Error ErrTermin :: !SrcSpan -> ![Doc] -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [bind] :: TError t -> ![Doc] [msg] :: TError t -> !Doc -- | Termination Error ErrStTerm :: !SrcSpan -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [dname] :: TError t -> !Doc [msg] :: TError t -> !Doc -- | Instance Law Error ErrILaw :: !SrcSpan -> !Doc -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [cname] :: TError t -> !Doc [iname] :: TError t -> !Doc [msg] :: TError t -> !Doc -- | Refined Class/Interfaces Conflict ErrRClass :: !SrcSpan -> !Doc -> ![(SrcSpan, Doc)] -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [cls] :: TError t -> !Doc [insts] :: TError t -> ![(SrcSpan, Doc)] -- | Standalone class method refinements ErrMClass :: !SrcSpan -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc -- | Non well sorted Qualifier ErrBadQual :: !SrcSpan -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [qname] :: TError t -> !Doc [msg] :: TError t -> !Doc -- | Previously saved error, that carries over after DiffCheck ErrSaved :: !SrcSpan -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [nam] :: TError t -> !Doc [msg] :: TError t -> !Doc ErrFilePragma :: !SrcSpan -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan ErrTyCon :: !SrcSpan -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [msg] :: TError t -> !Doc [tcname] :: TError t -> !Doc ErrLiftExp :: !SrcSpan -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [msg] :: TError t -> !Doc ErrParseAnn :: !SrcSpan -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [msg] :: TError t -> !Doc ErrNoSpec :: !SrcSpan -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [srcF] :: TError t -> !Doc [bspF] :: TError t -> !Doc ErrFail :: !SrcSpan -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc ErrFailUsed :: !SrcSpan -> !Doc -> ![Doc] -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [var] :: TError t -> !Doc [clients] :: TError t -> ![Doc] ErrRewrite :: !SrcSpan -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> !SrcSpan [msg] :: TError t -> !Doc ErrPosTyCon :: SrcSpan -> !Doc -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> SrcSpan [tc] :: TError t -> !Doc [dc] :: TError t -> !Doc -- | Sigh. Other. ErrOther :: SrcSpan -> !Doc -> TError t -- | haskell type location [pos] :: TError t -> SrcSpan [msg] :: TError t -> !Doc type ParseError = ParseError String Void -- | Context information for Error Messages -- ------------------------------------ data CtxError t CtxError :: TError t -> Doc -> CtxError t [ctErr] :: CtxError t -> TError t [ctCtx] :: CtxError t -> Doc errorsWithContext :: [TError Doc] -> IO [CtxError Doc] -- | Different kinds of Check Obligations -- ------------------------------------ data Oblig -- | Obligation that proves termination OTerm :: Oblig -- | Obligation that proves invariants OInv :: Oblig -- | Obligation that proves subtyping constraints OCons :: Oblig data WithModel t NoModel :: t -> WithModel t WithModel :: !Doc -> t -> WithModel t dropModel :: WithModel t -> t -- | Simple unstructured type for panic -- ---------------------------------------- type UserError = TError Doc -- | Construct and show an Error, then crash panic :: Maybe SrcSpan -> String -> a -- | Construct and show an Error, then crash panicDoc :: SrcSpan -> Doc -> a -- | Construct and show an Error with an optional SrcSpan, then crash This -- function should be used to mark unimplemented functionality todo :: Maybe SrcSpan -> String -> a -- | Construct and show an Error with an optional SrcSpan, then crash This -- function should be used to mark impossible-to-reach codepaths impossible :: Maybe SrcSpan -> String -> a -- | Construct and show an Error, then crash uError :: UserError -> a -- | Convert a GHC error into a list of our errors. sourceErrors :: String -> SourceError -> [TError t] errDupSpecs :: Doc -> ListNE SrcSpan -> TError t ppError :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc ppTicks :: PPrint a => a -> Doc packRealSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int) srcSpanFileMb :: SrcSpan -> Maybe FilePath instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Errors.Oblig instance Data.Data.Data Language.Haskell.Liquid.Types.Errors.Oblig instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Errors.Oblig instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Errors.Oblig instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Errors.WithModel t) instance GHC.Classes.Eq t => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Errors.WithModel t) instance GHC.Show.Show t => GHC.Show.Show (Language.Haskell.Liquid.Types.Errors.WithModel t) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Errors.WithModel instance GHC.Base.Functor Language.Haskell.Liquid.Types.Errors.TError instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Errors.TError t) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Errors.CtxError instance GHC.Classes.Eq (Language.Haskell.Liquid.Types.Errors.CtxError t) instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Errors.UserError instance GHC.Show.Show Language.Haskell.Liquid.Types.Errors.UserError instance GHC.Exception.Type.Exception Language.Haskell.Liquid.Types.Errors.UserError instance GHC.Classes.Eq (Language.Haskell.Liquid.Types.Errors.TError a) instance (Language.Fixpoint.Types.PrettyPrint.PPrint a, GHC.Show.Show a) => Data.Aeson.Types.ToJSON.ToJSON (Language.Haskell.Liquid.Types.Errors.TError a) instance Data.Aeson.Types.FromJSON.FromJSON (Language.Haskell.Liquid.Types.Errors.TError a) instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Errors.WithModel t) instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Errors.Oblig instance GHC.Show.Show Language.Haskell.Liquid.Types.Errors.Oblig instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Errors.Oblig instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Errors.Oblig instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Errors.ParseError instance Language.Fixpoint.Types.PrettyPrint.PPrint GHC.Types.SrcLoc.SrcSpan instance Data.Aeson.Types.ToJSON.ToJSON GHC.Types.SrcLoc.RealSrcSpan instance Data.Aeson.Types.FromJSON.FromJSON GHC.Types.SrcLoc.RealSrcSpan instance Data.Aeson.Types.ToJSON.ToJSON GHC.Types.SrcLoc.SrcSpan instance Data.Aeson.Types.FromJSON.FromJSON GHC.Types.SrcLoc.SrcSpan instance Data.Aeson.Types.ToJSON.ToJSONKey GHC.Types.SrcLoc.SrcSpan instance Data.Aeson.Types.FromJSON.FromJSONKey GHC.Types.SrcLoc.SrcSpan -- | This module exposes variations over the standard GHC's logging -- functions to work with the Doc type from the "pretty" -- package. We would like LiquidHaskell to emit diagnostic messages using -- the very same GHC machinery, so that IDE-like programs (e.g. "ghcid", -- "ghcide" etc) would be able to correctly show errors and warnings to -- the users, in ther editors. -- -- Unfortunately, this is not possible to do out of the box because -- LiquidHaskell uses the Doc type from the "pretty" package but -- GHC uses (for historical reasons) its own version. Due to the fact -- none of the constructors are exported, we simply cannot convert -- between the two types effortlessly, but we have to pay the price of a -- pretty-printing "roundtrip". module Language.Haskell.Liquid.GHC.Logging addTcRnUnknownMessage :: SrcSpan -> Doc -> TcRn () addTcRnUnknownMessages :: [(SrcSpan, Doc)] -> TcRn () fromPJDoc :: Doc -> SDoc putWarnMsg :: Logger -> SrcSpan -> Doc -> IO () -- | This module contains a wrappers and utility functions for accessing -- GHC module information. It should NEVER depend on ANY module inside -- the Language.Haskell.Liquid.* tree. module Language.Haskell.Liquid.GHC.Misc isAnonBinder :: TyConBinder -> Bool mkAlive :: Var -> Id -- | Encoding and Decoding Location -- -------------------------------------------- tickSrcSpan :: CoreTickish -> SrcSpan -- | Generic Helpers for Accessing GHC Innards -- --------------------------------- stringTyVar :: String -> TyVar stringVar :: String -> Type -> Var maybeAuxVar :: Symbol -> Maybe Var stringTyCon :: Char -> Int -> String -> TyCon stringTyConWithKind :: Kind -> Char -> Int -> String -> TyCon hasBaseTypeVar :: Var -> Bool isBaseType :: Type -> Bool isTmpVar :: Var -> Bool isTmpSymbol :: Symbol -> Bool validTyVar :: String -> Bool tvId :: TyVar -> String tidyCBs :: [CoreBind] -> [CoreBind] unTick :: CoreBind -> CoreBind unTickExpr :: CoreExpr -> CoreExpr isFractionalClass :: Class -> Bool isOrdClass :: Class -> Bool -- | Pretty Printers -- ----------------------------------------------------------- notracePpr :: Outputable a => String -> a -> a tracePpr :: Outputable a => String -> a -> a pprShow :: Show a => a -> SDoc toFixSDoc :: Fixpoint a => a -> Doc sDocDoc :: SDoc -> Doc pprDoc :: Outputable a => a -> Doc showPpr :: Outputable a => a -> String showSDoc :: SDoc -> String myQualify :: NamePprCtx showSDocDump :: SDoc -> String typeUniqueString :: Outputable a => a -> String -- | Manipulating Source Spans -- ------------------------------------------------- newtype Loc L :: (Int, Int) -> Loc fSrcSpan :: Loc a => a -> SrcSpan fSourcePos :: Loc a => a -> SourcePos fSrcSpanSrcSpan :: SrcSpan -> SrcSpan srcSpanFSrcSpan :: SrcSpan -> SrcSpan sourcePos2SrcSpan :: SourcePos -> SourcePos -> SrcSpan sourcePosSrcSpan :: SourcePos -> SrcSpan sourcePosSrcLoc :: SourcePos -> SrcLoc srcSpanSourcePos :: SrcSpan -> SourcePos srcSpanSourcePosE :: SrcSpan -> SourcePos srcSpanFilename :: SrcSpan -> String srcSpanStartLoc :: RealSrcSpan -> Loc srcSpanEndLoc :: RealSrcSpan -> Loc oneLine :: RealSrcSpan -> Bool lineCol :: RealSrcSpan -> (Int, Int) realSrcSpanSourcePos :: RealSrcSpan -> SourcePos realSrcLocSourcePos :: RealSrcLoc -> SourcePos realSrcSpanSourcePosE :: RealSrcSpan -> SourcePos getSourcePos :: NamedThing a => a -> SourcePos getSourcePosE :: NamedThing a => a -> SourcePos locNamedThing :: NamedThing a => a -> Located a namedLocSymbol :: (Symbolic a, NamedThing a) => a -> Located Symbol varLocInfo :: (Type -> a) -> Var -> Located a namedPanic :: NamedThing a => a -> String -> b -- | Predicates on CoreExpr and DataCons -- --------------------------------------- isExternalId :: Id -> Bool isTupleId :: Id -> Bool idDataConM :: Id -> Maybe DataCon isDataConId :: Id -> Bool getDataConVarUnique :: Var -> Unique isDictionaryExpression :: Expr Id -> Maybe Id realTcArity :: TyCon -> Arity kindTCArity :: TyCon -> Arity kindArity :: Kind -> Arity uniqueHash :: Uniquable a => Int -> a -> Int lookupRdrName :: HscEnv -> ModuleName -> RdrName -> IO (Maybe Name) ignoreInline :: ParsedModule -> ParsedModule -- | Symbol Conversions -- -------------------------------------------------------- symbolTyVar :: Symbol -> TyVar localVarSymbol :: Var -> Symbol exportedVarSymbol :: Var -> Symbol qualifiedNameSymbol :: Name -> Symbol fastStringText :: FastString -> Text tyConTyVarsDef :: TyCon -> [TyVar] noTyVars :: TyCon -> Bool -- | Manipulating Symbols -- ------------------------------------------------------ takeModuleUnique :: Symbol -> Symbol splitModuleUnique :: Symbol -> (Symbol, Int) base62ToI :: Symbol -> Int splitModuleName :: Symbol -> (Symbol, Symbol) dropModuleNamesAndUnique :: Symbol -> Symbol dropModuleNames :: Symbol -> Symbol dropModuleNamesCorrect :: Symbol -> Symbol takeModuleNames :: Symbol -> Symbol dropModuleUnique :: Symbol -> Symbol cmpSymbol :: Symbol -> Symbol -> Bool sepModNames :: Text sepUnique :: Text mungeNames :: (String -> [Text] -> Symbol) -> Text -> String -> Symbol -> Symbol qualifySymbol :: Symbol -> Symbol -> Symbol isQualifiedSym :: Symbol -> Bool isQualified :: Text -> Bool wrapParens :: (IsString a, Monoid a) => a -> a isParened :: Text -> Bool isDictionary :: Symbolic a => a -> Bool isMethod :: Symbolic a => a -> Bool isInternal :: Symbolic a => a -> Bool isWorker :: Symbolic a => a -> Bool isSCSel :: Symbolic a => a -> Bool stripParens :: Text -> Text stripParensSym :: Symbol -> Symbol desugarModule :: TypecheckedModule -> Ghc DesugaredModule -- | GHC Compatibility Layer -- --------------------------------------------------- gHC_VERSION :: String symbolFastString :: Symbol -> FastString synTyConRhs_maybe :: TyCon -> Maybe Type showCBs :: Bool -> [CoreBind] -> String ignoreCoreBinds :: HashSet Var -> [CoreBind] -> [CoreBind] findVarDef :: Symbol -> [CoreBind] -> Maybe (Var, CoreExpr) findVarDefMethod :: Symbol -> [CoreBind] -> Maybe (Var, CoreExpr) dictionarySymbols :: CoreBind -> [Symbol] methodSymbols :: CoreBind -> [Symbol] coreBindSymbols :: CoreBind -> [Symbol] simplesymbol :: NamedThing t => t -> Symbol binders :: Bind a -> [a] expandVarType :: Var -> Type -- | The following functions test if a CoreExpr or CoreVar -- can be embedded in logic. With type-class support, we can no longer -- erase such expressions arbitrarily. isEmbeddedDictExpr :: CoreExpr -> Bool isEmbeddedDictVar :: Var -> Bool isEmbeddedDictType :: Type -> Bool isPrelEqPred :: Type -> Bool isPrelEqTyCon :: TyCon -> Bool isOrdPred :: Type -> Bool isNumericPred :: Type -> Bool -- | The following functions test if a CoreExpr or CoreVar -- are just types in disguise, e.g. have PredType (in the GHC -- sense of the word), and so shouldn't appear in refinements. isPredExpr :: CoreExpr -> Bool isPredVar :: Var -> Bool isPredType :: Type -> Bool anyF :: [a -> Bool] -> a -> Bool -- | 'defaultDataCons t ds' returns the list of '(dc, types)' pairs, -- corresponding to the _missing_ cases, i.e. _other_ than those in -- ds, that are being handled by DEFAULT. defaultDataCons :: Type -> [AltCon] -> Maybe [(DataCon, [TyVar], [Type])] isEvVar :: Id -> Bool -- | Elaboration elabRnExpr :: LHsExpr GhcPs -> TcRn CoreExpr newtype HashableType HashableType :: Type -> HashableType [getHType] :: HashableType -> Type -- | Superclass coherence canonSelectorChains :: PredType -> Map HashableType [Id] buildCoherenceOblig :: Class -> [[([Id], [Id])]] coherenceObligToRef :: Symbolic s => s -> [Id] -> [Id] -> Reft coherenceObligToRefE :: Expr -> [Id] -> [Id] -> Reft data TcWiredIn TcWiredIn :: Name -> Maybe (Int, FixityDirection) -> LHsType GhcRn -> TcWiredIn [tcWiredInName] :: TcWiredIn -> Name [tcWiredInFixity] :: TcWiredIn -> Maybe (Int, FixityDirection) [tcWiredInType] :: TcWiredIn -> LHsType GhcRn -- | Run a computation in GHC's typechecking monad with wired in values -- locally bound in the typechecking environment. withWiredIn :: TcM a -> TcM a prependGHCRealQual :: FastString -> RdrName isFromGHCReal :: NamedThing a => a -> Bool instance GHC.Show.Show Language.Haskell.Liquid.GHC.Misc.Loc instance GHC.Classes.Ord Language.Haskell.Liquid.GHC.Misc.Loc instance GHC.Classes.Eq Language.Haskell.Liquid.GHC.Misc.Loc instance GHC.Classes.Eq Language.Haskell.Liquid.GHC.Misc.HashableType instance GHC.Classes.Ord Language.Haskell.Liquid.GHC.Misc.HashableType instance GHC.Utils.Outputable.Outputable Language.Haskell.Liquid.GHC.Misc.HashableType instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.GHC.Misc.Loc instance GHC.Utils.Outputable.Outputable a => GHC.Utils.Outputable.Outputable (Data.HashSet.Internal.HashSet a) instance Data.Hashable.Class.Hashable GHC.Types.SrcLoc.SrcSpan instance Language.Fixpoint.Types.Spans.Loc GHC.Types.Var.Var instance Language.Fixpoint.Types.Names.Symbolic GHC.Data.FastString.FastString instance Language.Fixpoint.Types.Names.Symbolic GHC.Core.TyCon.TyCon instance Language.Fixpoint.Types.Names.Symbolic GHC.Core.Class.Class instance Language.Fixpoint.Types.Names.Symbolic GHC.Types.Name.Name instance Language.Fixpoint.Types.Names.Symbolic GHC.Types.Var.Var instance Data.Hashable.Class.Hashable GHC.Types.Var.Var instance Data.Hashable.Class.Hashable GHC.Core.TyCon.TyCon instance Data.Hashable.Class.Hashable GHC.Core.Class.Class instance Data.Hashable.Class.Hashable GHC.Core.DataCon.DataCon instance Language.Fixpoint.Types.PrettyPrint.Fixpoint GHC.Types.Var.Var instance Language.Fixpoint.Types.PrettyPrint.Fixpoint GHC.Types.Name.Name instance Language.Fixpoint.Types.PrettyPrint.Fixpoint GHC.Core.TyCo.Rep.Type instance GHC.Show.Show GHC.Types.Name.Name instance GHC.Show.Show GHC.Types.Var.Var instance GHC.Show.Show GHC.Core.Class.Class instance GHC.Show.Show GHC.Core.TyCon.TyCon instance Control.DeepSeq.NFData GHC.Core.Class.Class instance Control.DeepSeq.NFData GHC.Core.TyCon.TyCon instance Control.DeepSeq.NFData GHC.Core.TyCo.Rep.Type instance Control.DeepSeq.NFData GHC.Types.Var.Var -- | Formats Haskell source code as HTML with CSS and Mouseover Type -- Annotations module Language.Haskell.Liquid.UX.ACSS -- | Formats Haskell source code using HTML and mouse-over annotations hscolour :: Bool -> Bool -> String -> String -- | Formats Haskell source code using HTML and mouse-over annotations hsannot :: Bool -> CommentTransform -> Bool -> (String, AnnMap) -> String data AnnMap Ann :: HashMap Loc (String, String) -> [(Loc, Loc, String)] -> !Status -> ![(RealSrcSpan, (String, String))] -> AnnMap -- | Loc -> (Var, Type) [types] :: AnnMap -> HashMap Loc (String, String) -- | List of error intervals [errors] :: AnnMap -> [(Loc, Loc, String)] [status] :: AnnMap -> !Status -- | Type information with spans [sptypes] :: AnnMap -> ![(RealSrcSpan, (String, String))] breakS :: [Char] srcModuleName :: String -> String data Status Safe :: Status Unsafe :: Status Error :: Status Crash :: Status tokeniseWithLoc :: CommentTransform -> String -> [(TokenType, String, Loc)] instance GHC.Show.Show Language.Haskell.Liquid.UX.ACSS.Status instance GHC.Classes.Ord Language.Haskell.Liquid.UX.ACSS.Status instance GHC.Classes.Eq Language.Haskell.Liquid.UX.ACSS.Status instance GHC.Show.Show Language.Haskell.Liquid.UX.ACSS.Annotation instance GHC.Show.Show Language.Haskell.Liquid.UX.ACSS.Lit instance GHC.Show.Show Language.Haskell.Liquid.UX.ACSS.AnnMap module Language.Haskell.Liquid.Types.Visitors class CBVisitable a freeVars :: CBVisitable a => HashSet Var -> a -> [Var] readVars :: CBVisitable a => a -> [Var] letVars :: CBVisitable a => a -> [Var] literals :: CBVisitable a => a -> [Literal] coreVisitor :: CoreVisitor env acc -> env -> acc -> [CoreBind] -> acc -- | BindVisitor allows for generic, context sensitive traversals -- over the CoreBinds data CoreVisitor env acc CoreVisitor :: (env -> Var -> env) -> (env -> acc -> Var -> acc) -> (env -> acc -> CoreExpr -> acc) -> CoreVisitor env acc [envF] :: CoreVisitor env acc -> env -> Var -> env [bindF] :: CoreVisitor env acc -> env -> acc -> Var -> acc [exprF] :: CoreVisitor env acc -> env -> acc -> CoreExpr -> acc instance Language.Haskell.Liquid.Types.Visitors.CBVisitable [GHC.Core.CoreBind] instance Language.Haskell.Liquid.Types.Visitors.CBVisitable GHC.Core.CoreBind instance Language.Haskell.Liquid.Types.Visitors.CBVisitable (GHC.Core.Expr GHC.Types.Var.Var) instance Language.Haskell.Liquid.Types.Visitors.CBVisitable (GHC.Core.Alt GHC.Types.Var.Var) instance Language.Haskell.Liquid.Types.Visitors.CBVisitable GHC.Core.AltCon module Language.Haskell.Liquid.Types.Variance data Variance Invariant :: Variance Bivariant :: Variance Contravariant :: Variance Covariant :: Variance type VarianceInfo = [Variance] makeTyConVariance :: TyCon -> VarianceInfo flipVariance :: Variance -> Variance instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Variance.Variance instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Variance.Variance instance GHC.Show.Show Language.Haskell.Liquid.Types.Variance.Variance instance Data.Data.Data Language.Haskell.Liquid.Types.Variance.Variance instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Variance.Variance instance GHC.Base.Semigroup Language.Haskell.Liquid.Types.Variance.Variance instance GHC.Base.Monoid Language.Haskell.Liquid.Types.Variance.Variance instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Variance.Variance instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Variance.Variance instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Variance.Variance -- | This module should contain all the global type definitions and basic -- instances. module Language.Haskell.Liquid.Types.Types -- | Which Top-Level Binders Should be Verified data TargetVars AllVars :: TargetVars Only :: ![Var] -> TargetVars -- | Information about Type Constructors data TyConMap TyConMap :: HashMap TyCon RTyCon -> HashMap (TyCon, [Sort]) RTyCon -> HashMap TyCon Int -> TyConMap -- | Map from GHC TyCon to RTyCon [tcmTyRTy] :: TyConMap -> HashMap TyCon RTyCon -- | Map from GHC Family-Instances to RTyCon [tcmFIRTy] :: TyConMap -> HashMap (TyCon, [Sort]) RTyCon -- | Arity of each Family-Tycon [tcmFtcArity] :: TyConMap -> HashMap TyCon Int data () => Located a Loc :: !SourcePos -> !SourcePos -> !a -> Located a -- | Start Position [loc] :: Located a -> !SourcePos -- | End Position [locE] :: Located a -> !SourcePos [val] :: Located a -> !a dummyLoc :: a -> Located a -- | Located Symbols ----------------------------------------------------- type LocSymbol = Located Symbol type LocText = Located Text dummyName :: Symbol isDummy :: Symbolic a => a -> Bool data BTyCon BTyCon :: !LocSymbol -> !Bool -> !Bool -> BTyCon -- | TyCon name with location information [btc_tc] :: BTyCon -> !LocSymbol -- | Is this a class type constructor? [btc_class] :: BTyCon -> !Bool -- | Is Promoted Data Con? [btc_prom] :: BTyCon -> !Bool mkBTyCon :: LocSymbol -> BTyCon isClassBTyCon :: BTyCon -> Bool newtype BTyVar BTV :: Symbol -> BTyVar data RTyCon RTyCon :: TyCon -> ![RPVar] -> !TyConInfo -> RTyCon -- | Co- and Contra-variance for TyCon -------------------------------- -- -- Indexes start from 0 and type or predicate arguments can be both -- covariant and contravaariant e.g., for the below Foo dataType -- -- data Foo a b c d :: b - Prop, q :: Int -> Prop, r :: a -> -- Prop> = F (ar -> bp) | Q (c -> a) | G -- (Intq -> ar) -- -- there will be: -- -- varianceTyArgs = [Bivariant , Covariant, Contravatiant, Invariant] -- variancePsArgs = [Covariant, Contravatiant, Bivariant] data TyConInfo TyConInfo :: !VarianceInfo -> !VarianceInfo -> !Maybe SizeFun -> TyConInfo -- | variance info for type variables [varianceTyArgs] :: TyConInfo -> !VarianceInfo -- | variance info for predicate variables [variancePsArgs] :: TyConInfo -> !VarianceInfo -- | logical UNARY function that computes the size of the structure [sizeFunction] :: TyConInfo -> !Maybe SizeFun defaultTyConInfo :: TyConInfo rTyConPVs :: RTyCon -> [RPVar] rTyConPropVs :: RTyCon -> [PVar RSort] isClassType :: TyConable c => RType c t t1 -> Bool isEqType :: TyConable c => RType c t t1 -> Bool isRVar :: RType c tv r -> Bool -- | Accessors for RTyCon isBool :: RType RTyCon t t1 -> Bool isEmbeddedClass :: TyConable c => RType c t t1 -> Bool data RType c tv r RVar :: !tv -> !r -> RType c tv r [rt_var] :: RType c tv r -> !tv [rt_reft] :: RType c tv r -> !r RFun :: !Symbol -> !RFInfo -> !RType c tv r -> !RType c tv r -> !r -> RType c tv r [rt_bind] :: RType c tv r -> !Symbol [rt_rinfo] :: RType c tv r -> !RFInfo [rt_in] :: RType c tv r -> !RType c tv r [rt_out] :: RType c tv r -> !RType c tv r [rt_reft] :: RType c tv r -> !r RAllT :: !RTVU c tv -> !RType c tv r -> !r -> RType c tv r [rt_tvbind] :: RType c tv r -> !RTVU c tv [rt_ty] :: RType c tv r -> !RType c tv r [rt_ref] :: RType c tv r -> !r -- | "forall x y :: Nat, w :: Int . TYPE" ^^^^^^^^^^^^^^^^^^^ -- (rt_pvbind) RAllP :: !PVU c tv -> !RType c tv r -> RType c tv r [rt_pvbind] :: RType c tv r -> !PVU c tv [rt_ty] :: RType c tv r -> !RType c tv r -- | For example, in [a]- v > h}>, we apply (via RApp) -- * the RProp denoted by `{h -> v > h}` to * the -- RTyCon denoted by `[]`. RApp :: !c -> ![RType c tv r] -> ![RTProp c tv r] -> !r -> RType c tv r [rt_tycon] :: RType c tv r -> !c [rt_args] :: RType c tv r -> ![RType c tv r] [rt_pargs] :: RType c tv r -> ![RTProp c tv r] [rt_reft] :: RType c tv r -> !r RAllE :: !Symbol -> !RType c tv r -> !RType c tv r -> RType c tv r [rt_bind] :: RType c tv r -> !Symbol [rt_allarg] :: RType c tv r -> !RType c tv r [rt_ty] :: RType c tv r -> !RType c tv r REx :: !Symbol -> !RType c tv r -> !RType c tv r -> RType c tv r [rt_bind] :: RType c tv r -> !Symbol [rt_exarg] :: RType c tv r -> !RType c tv r [rt_ty] :: RType c tv r -> !RType c tv r -- | For expression arguments to type aliases see testsposvector2.hs RExprArg :: Located Expr -> RType c tv r RAppTy :: !RType c tv r -> !RType c tv r -> !r -> RType c tv r [rt_arg] :: RType c tv r -> !RType c tv r [rt_res] :: RType c tv r -> !RType c tv r [rt_reft] :: RType c tv r -> !r RRTy :: ![(Symbol, RType c tv r)] -> !r -> !Oblig -> !RType c tv r -> RType c tv r [rt_env] :: RType c tv r -> ![(Symbol, RType c tv r)] [rt_ref] :: RType c tv r -> !r [rt_obl] :: RType c tv r -> !Oblig [rt_ty] :: RType c tv r -> !RType c tv r -- | let LH match against the Haskell type and add k-vars, e.g. `x:_` see -- testsposHoles.hs RHole :: r -> RType c tv r -- | Ref describes `Prop τ` and HProp arguments applied -- to type constructors. For example, in [a]- v > h}>, we -- apply (via RApp) * the RProp denoted by `{h -> v > -- h}` to * the RTyCon denoted by `[]`. Thus, Ref is used -- for abstract-predicate (arguments) that are associated with _type -- constructors_ i.e. whose semantics are _dependent upon_ the data-type. -- In contrast, the Predicate argument in ur_pred in the -- UReft applies directly to any type and has semantics -- _independent of_ the data-type. data Ref τ t RProp :: [(Symbol, τ)] -> t -> Ref τ t -- | arguments. e.g. h in the above example [rf_args] :: Ref τ t -> [(Symbol, τ)] -- | Abstract refinement associated with RTyCon. e.g. v > -- h in the above example [rf_body] :: Ref τ t -> t -- | RTProp is a convenient alias for Ref that will save -- a bunch of typing. In general, perhaps we need not expose Ref -- directly at all. type RTProp c tv r = Ref (RType c tv ()) (RType c tv r) rPropP :: [(Symbol, τ)] -> r -> Ref τ (RType c tv r) newtype RTyVar RTV :: TyVar -> RTyVar -- | Refinement Type Aliases data RTAlias x a RTA :: Symbol -> [x] -> [Symbol] -> a -> RTAlias x a -- | name of the alias [rtName] :: RTAlias x a -> Symbol -- | type parameters [rtTArgs] :: RTAlias x a -> [x] -- | value parameters [rtVArgs] :: RTAlias x a -> [Symbol] -- | what the alias expands to , rtMod :: !ModName -- ^ module where alias -- was defined [rtBody] :: RTAlias x a -> a type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, Reftable r, Reftable (RTProp c tv ()), Reftable (RTProp c tv r), Eq c, Eq tv, Hashable tv) lmapEAlias :: LMap -> Located (RTAlias Symbol Expr) data HSeg t HBind :: !Symbol -> t -> HSeg t [hs_addr] :: HSeg t -> !Symbol [hs_val] :: HSeg t -> t HVar :: UsedPVar -> HSeg t -- | A World is a Separation Logic predicate that is essentially a -- sequence of binders that satisfies two invariants (TODO:LIQUID): 1. -- Each `hs_addr :: Symbol` appears at most once, 2. There is at most one -- HVar in a list. newtype World t World :: [HSeg t] -> World t class (Eq c) => TyConable c isFun :: TyConable c => c -> Bool isList :: TyConable c => c -> Bool isTuple :: TyConable c => c -> Bool ppTycon :: TyConable c => c -> Doc isClass :: TyConable c => c -> Bool isEmbeddedDict :: TyConable c => c -> Bool isEqual :: TyConable c => c -> Bool isOrdCls :: TyConable c => c -> Bool isEqCls :: TyConable c => c -> Bool isNumCls :: TyConable c => c -> Bool isFracCls :: TyConable c => c -> Bool class SubsTy tv ty a subt :: SubsTy tv ty a => (tv, ty) -> a -> a data RTVar tv s RTVar :: tv -> RTVInfo s -> RTVar tv s [ty_var_value] :: RTVar tv s -> tv [ty_var_info] :: RTVar tv s -> RTVInfo s data RTVInfo s RTVNoInfo :: Bool -> RTVInfo s [rtv_is_pol] :: RTVInfo s -> Bool RTVInfo :: Symbol -> s -> Bool -> Bool -> RTVInfo s [rtv_name] :: RTVInfo s -> Symbol [rtv_kind] :: RTVInfo s -> s [rtv_is_val] :: RTVInfo s -> Bool [rtv_is_pol] :: RTVInfo s -> Bool makeRTVar :: tv -> RTVar tv s mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s dropTyVarInfo :: RTVar tv s1 -> RTVar tv s2 rTVarToBind :: RTVar RTyVar s -> Maybe (Symbol, s) setRtvPol :: RTVar tv a -> Bool -> RTVar tv a -- | Abstract Predicate Variables ---------------------------------- data PVar t PV :: !Symbol -> !PVKind t -> !Symbol -> ![(t, Symbol, Expr)] -> PVar t [pname] :: PVar t -> !Symbol [ptype] :: PVar t -> !PVKind t [parg] :: PVar t -> !Symbol [pargs] :: PVar t -> ![(t, Symbol, Expr)] isPropPV :: PVar t -> Bool pvType :: PVar t -> t data PVKind t PVProp :: t -> PVKind t PVHProp :: PVKind t newtype Predicate Pr :: [UsedPVar] -> Predicate data UReft r MkUReft :: !r -> !Predicate -> UReft r [ur_reft] :: UReft r -> !r [ur_pred] :: UReft r -> !Predicate data RelExpr ERBasic :: Expr -> RelExpr ERChecked :: Expr -> RelExpr -> RelExpr ERUnChecked :: Expr -> RelExpr -> RelExpr -- | Termination expressions data SizeFun -- | x -> F.EVar x IdSizeFun :: SizeFun -- | x -> f x SymSizeFun :: LocSymbol -> SizeFun szFun :: SizeFun -> Symbol -> Expr -- | Data type refinements data DataDecl DataDecl :: DataName -> [Symbol] -> [PVar BSort] -> Maybe [DataCtor] -> !SourcePos -> Maybe SizeFun -> Maybe BareType -> !DataDeclKind -> DataDecl -- | Type Constructor Name [tycName] :: DataDecl -> DataName -- | Tyvar Parameters [tycTyVars] :: DataDecl -> [Symbol] -- | PVar Parameters [tycPVars] :: DataDecl -> [PVar BSort] -- | Data Constructors (Nothing is reserved for non-GADT style empty data -- declarations) [tycDCons] :: DataDecl -> Maybe [DataCtor] -- | Source Position [tycSrcPos] :: DataDecl -> !SourcePos -- | Default termination measure [tycSFun] :: DataDecl -> Maybe SizeFun -- | Type of Ind-Prop [tycPropTy] :: DataDecl -> Maybe BareType -- | User-defined or Auto-lifted [tycKind] :: DataDecl -> !DataDeclKind -- | The name of the TyCon corresponding to a DataDecl data DataName -- | for isVanillyAlgTyCon we can directly use the TyCon -- name DnName :: !LocSymbol -> DataName -- | for FamInst TyCon we save some DataCon name DnCon :: !LocSymbol -> DataName dataNameSymbol :: DataName -> LocSymbol -- | Data Constructor data DataCtor DataCtor :: LocSymbol -> [Symbol] -> [BareType] -> [(Symbol, BareType)] -> Maybe BareType -> DataCtor -- | DataCon name [dcName] :: DataCtor -> LocSymbol -- | Type parameters [dcTyVars] :: DataCtor -> [Symbol] -- | The GHC ThetaType corresponding to DataCon.dataConSig [dcTheta] :: DataCtor -> [BareType] -- | field-name and field-Type pairs [dcFields] :: DataCtor -> [(Symbol, BareType)] -- | Possible output (if in GADT form) [dcResult] :: DataCtor -> Maybe BareType data DataConP DataConP :: !SourcePos -> !DataCon -> ![RTyVar] -> ![PVar RSort] -> ![SpecType] -> ![(Symbol, SpecType)] -> !SpecType -> !Bool -> !Symbol -> !SourcePos -> DataConP [dcpLoc] :: DataConP -> !SourcePos -- | Corresponding GHC DataCon [dcpCon] :: DataConP -> !DataCon -- | Type parameters [dcpFreeTyVars] :: DataConP -> ![RTyVar] -- | Abstract Refinement parameters [dcpFreePred] :: DataConP -> ![PVar RSort] -- | ? Class constraints (via dataConStupidTheta) [dcpTyConstrs] :: DataConP -> ![SpecType] -- | Value parameters [dcpTyArgs] :: DataConP -> ![(Symbol, SpecType)] -- | Result type [dcpTyRes] :: DataConP -> !SpecType -- | Was this specified in GADT style (if so, DONT use function names as -- fields) [dcpIsGadt] :: DataConP -> !Bool -- | Which module was this defined in [dcpModule] :: DataConP -> !Symbol [dcpLocE] :: DataConP -> !SourcePos data HasDataDecl NoDecl :: Maybe SizeFun -> HasDataDecl HasDecl :: HasDataDecl hasDecl :: DataDecl -> HasDataDecl -- | What kind of DataDecl is it? data DataDeclKind -- | User defined data-definitions (should have refined fields) DataUser :: DataDeclKind -- | Automatically lifted data-definitions (do not have refined fields) DataReflected :: DataDeclKind data TyConP TyConP :: !SourcePos -> !TyCon -> ![RTyVar] -> ![PVar RSort] -> !VarianceInfo -> !VarianceInfo -> !Maybe SizeFun -> TyConP [tcpLoc] :: TyConP -> !SourcePos [tcpCon] :: TyConP -> !TyCon [tcpFreeTyVarsTy] :: TyConP -> ![RTyVar] [tcpFreePredTy] :: TyConP -> ![PVar RSort] [tcpVarianceTs] :: TyConP -> !VarianceInfo [tcpVariancePs] :: TyConP -> !VarianceInfo [tcpSizeFun] :: TyConP -> !Maybe SizeFun type RRType = -- | "Resolved" version RType RTyCon RTyVar type RRProp r = Ref RSort (RRType r) type BRType = -- | "Bare" parsed version RType BTyCon BTyVar type BRProp r = Ref BSort (BRType r) type BSort = BRType () type BPVar = PVar BSort -- | Unified Representation of Refinement Types -- -------------------------------- type RTVU c tv = RTVar tv (RType c tv ()) type PVU c tv = PVar (RType c tv ()) type BareType = BRType RReft type PrType = RRType Predicate type SpecType = RRType RReft type SpecProp = RRProp RReft type SpecRTVar = RTVar RTyVar RSort type SpecRep = RRep RReft type LocBareType = Located BareType type LocSpecType = Located SpecType type RSort = RRType () -- | Predicates -- ---------------------------------------------------------------- type UsedPVar = PVar () type RPVar = PVar RSort type RReft = UReft Reft -- | The type used during constraint generation, used also to define -- contexts for errors, hence in this file, and NOT in elsewhere. **DO -- NOT ATTEMPT TO MOVE** Am splitting into + global : many bindings, -- shared across all constraints + local : few bindings, relevant to -- particular constraints type REnv = AREnv SpecType data AREnv t REnv :: HashMap Symbol t -> HashMap Symbol t -> AREnv t -- | the "global" names for module [reGlobal] :: AREnv t -> HashMap Symbol t -- | the "local" names for sub-exprs [reLocal] :: AREnv t -> HashMap Symbol t -- | Constructor and Destructors for RTypes -- ------------------------------------ data RTypeRep c tv r RTypeRep :: [(RTVar tv (RType c tv ()), r)] -> [PVar (RType c tv ())] -> [Symbol] -> [RFInfo] -> [r] -> [RType c tv r] -> RType c tv r -> RTypeRep c tv r [ty_vars] :: RTypeRep c tv r -> [(RTVar tv (RType c tv ()), r)] [ty_preds] :: RTypeRep c tv r -> [PVar (RType c tv ())] [ty_binds] :: RTypeRep c tv r -> [Symbol] [ty_info] :: RTypeRep c tv r -> [RFInfo] [ty_refts] :: RTypeRep c tv r -> [r] [ty_args] :: RTypeRep c tv r -> [RType c tv r] [ty_res] :: RTypeRep c tv r -> RType c tv r fromRTypeRep :: RTypeRep c tv r -> RType c tv r toRTypeRep :: RType c tv r -> RTypeRep c tv r mkArrow :: [(RTVar tv (RType c tv ()), r)] -> [PVar (RType c tv ())] -> [(Symbol, RFInfo, RType c tv r, r)] -> RType c tv r -> RType c tv r bkArrowDeep :: RType t t1 a -> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a) bkArrow :: RType t t1 a -> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a) safeBkArrow :: PPrint (RType t t1 a) => RType t t1 a -> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a) mkUnivs :: (Foldable t, Foldable t1) => t (RTVar tv (RType c tv ()), r) -> t1 (PVar (RType c tv ())) -> RType c tv r -> RType c tv r bkUniv :: RType tv c r -> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())], RType tv c r) bkClass :: (PPrint c, TyConable c) => RType c tv r -> ([(c, [RType c tv r])], RType c tv r) bkUnivClass :: SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], [(RTyCon, [SpecType])], SpecType) bkUnivClass' :: SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], [(Symbol, SpecType, RReft)], SpecType) rFun :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r rFun' :: Monoid r => RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r rCls :: Monoid r => TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r rRCls :: Monoid r => c -> [RType c tv r] -> RType c tv r rFunDebug :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r pvars :: Predicate -> [UsedPVar] pappSym :: Show a => a -> Symbol pApp :: Symbol -> [Expr] -> Expr isBase :: RType t t1 t2 -> Bool isFunTy :: RType t t1 t2 -> Bool isTrivial :: (Reftable r, TyConable c) => RType c tv r -> Bool hasHole :: Reftable r => r -> Bool efoldReft :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (c -> [RType c tv r] -> [(Symbol, a)]) -> (RTVar tv (RType c tv ()) -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> b -> RType c tv r -> b foldReft :: (Reftable r, TyConable c) => BScope -> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a foldReft' :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> BScope -> (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a emapReft :: ([Symbol] -> r1 -> r2) -> [Symbol] -> RType c tv r1 -> RType c tv r2 mapReft :: (r1 -> r2) -> RType c tv r1 -> RType c tv r2 mapReftM :: Monad m => (r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2) mapPropM :: Monad m => (RTProp c tv r -> m (RTProp c tv r)) -> RType c tv r -> m (RType c tv r) -- | Visitors -- ------------------------------------------------------------------ mapExprReft :: (Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft mapBot :: (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r mapBind :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r mapRFInfo :: (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r foldRType :: (acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc -- | Different kinds of Check Obligations -- ------------------------------------ data Oblig -- | Obligation that proves termination OTerm :: Oblig -- | Obligation that proves invariants OInv :: Oblig -- | Obligation that proves subtyping constraints OCons :: Oblig ignoreOblig :: RType t t1 t2 -> RType t t1 t2 addInvCond :: SpecType -> RReft -> SpecType -- | Annotations ------------------------------------------------------- newtype AnnInfo a AI :: HashMap SrcSpan [(Maybe Text, a)] -> AnnInfo a data Annot t AnnUse :: t -> Annot t AnnDef :: t -> Annot t AnnRDf :: t -> Annot t AnnLoc :: SrcSpan -> Annot t -- | Var Hole Info ----------------------------------------------------- data HoleInfo i t HoleInfo :: t -> SrcSpan -> AREnv t -> i -> HoleInfo i t [htype] :: HoleInfo i t -> t [hloc] :: HoleInfo i t -> SrcSpan [henv] :: HoleInfo i t -> AREnv t [info] :: HoleInfo i t -> i -- | Output -- -------------------------------------------------------------------- data Output a O :: Maybe [String] -> !AnnInfo a -> !AnnInfo a -> ![SrcSpan] -> ErrorResult -> Output a [o_vars] :: Output a -> Maybe [String] [o_types] :: Output a -> !AnnInfo a [o_templs] :: Output a -> !AnnInfo a [o_bots] :: Output a -> ![SrcSpan] [o_result] :: Output a -> ErrorResult hole :: Expr isHole :: Expr -> Bool hasHoleTy :: RType t t1 t2 -> Bool ofRSort :: Reftable r => RType c tv () -> RType c tv r toRSort :: RType c tv r -> RType c tv () rTypeValueVar :: Reftable r => RType c tv r -> Symbol rTypeReft :: Reftable r => RType c tv r -> Reft stripRTypeBase :: RType c tv r -> Maybe r topRTypeBase :: Reftable r => RType c tv r -> RType c tv r -- | Implement either pprintTidy or pprintPrec class () => PPrint a pprintTidy :: PPrint a => Tidy -> a -> Doc pprintPrec :: PPrint a => Int -> Tidy -> a -> Doc -- | Top-level pretty printer pprint :: PPrint a => a -> Doc showpp :: PPrint a => a -> String -- | Printer -- ---------------------------------------------------------------- data PPEnv PP :: Bool -> Bool -> Bool -> Bool -> PPEnv -- | print abstract-predicates [ppPs] :: PPEnv -> Bool -- | print the unique suffix for each tyvar [ppTyVar] :: PPEnv -> Bool -- | print the tycons without qualification [ppShort] :: PPEnv -> Bool -- | gross with full info [ppDebug] :: PPEnv -> Bool ppEnv :: PPEnv ppEnvShort :: PPEnv -> PPEnv -- | Module Names -- -------------------------------------------------------------- data ModName ModName :: !ModType -> !ModuleName -> ModName data ModType Target :: ModType SrcImport :: ModType SpecImport :: ModType isSrcImport :: ModName -> Bool isSpecImport :: ModName -> Bool isTarget :: ModName -> Bool getModName :: ModName -> ModuleName getModString :: ModName -> String qualifyModName :: ModName -> Symbol -> Symbol -- | Refinement Type Aliases -- --------------------------------------------------- data RTEnv tv t RTE :: HashMap Symbol (Located (RTAlias tv t)) -> HashMap Symbol (Located (RTAlias Symbol Expr)) -> RTEnv tv t [typeAliases] :: RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t)) [exprAliases] :: RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr)) type BareRTEnv = RTEnv Symbol BareType type SpecRTEnv = RTEnv RTyVar SpecType type BareRTAlias = RTAlias Symbol BareType type SpecRTAlias = RTAlias RTyVar SpecType type Error = TError SpecType -- | Error Data Type -- ----------------------------------------------------------- type ErrorResult = FixResult UserError -- | Diagnostic info -- ----------------------------------------------------------- data Warning mkWarning :: SrcSpan -> Doc -> Warning data Diagnostics mkDiagnostics :: [Warning] -> [Error] -> Diagnostics emptyDiagnostics :: Diagnostics noErrors :: Diagnostics -> Bool allWarnings :: Diagnostics -> [Warning] allErrors :: Diagnostics -> [Error] -- | Printing Warnings -- --------------------------------------------------------- printWarning :: Logger -> Warning -> IO () -- | Source Information Associated With Constraints -- ---------------------------- data Cinfo Ci :: !SrcSpan -> !Maybe Error -> !Maybe Var -> Cinfo [ci_loc] :: Cinfo -> !SrcSpan [ci_err] :: Cinfo -> !Maybe Error [ci_var] :: Cinfo -> !Maybe Var data Measure ty ctor M :: LocSymbol -> ty -> [Def ty ctor] -> !MeasureKind -> !UnSortedExprs -> Measure ty ctor [msName] :: Measure ty ctor -> LocSymbol [msSort] :: Measure ty ctor -> ty [msEqns] :: Measure ty ctor -> [Def ty ctor] [msKind] :: Measure ty ctor -> !MeasureKind [msUnSorted] :: Measure ty ctor -> !UnSortedExprs type UnSortedExprs = [UnSortedExpr] type UnSortedExpr = ([Symbol], Expr) data MeasureKind -- | due to `reflect foo` MsReflect :: MeasureKind -- | due to `measure foo` with old-style (non-haskell) equations MsMeasure :: MeasureKind -- | due to `measure foo` with new-style haskell equations MsLifted :: MeasureKind -- | due to `class measure` definition MsClass :: MeasureKind -- | due to `measure foo` without equations c.f. testsposT1223.hs MsAbsMeasure :: MeasureKind -- | due to selector-fields e.g. `data Foo = Foo { fld :: Int }` MsSelector :: MeasureKind -- | due to checkers e.g. `is-F` for `data Foo = F ... | G ...` MsChecker :: MeasureKind data CMeasure ty CM :: LocSymbol -> ty -> CMeasure ty [cName] :: CMeasure ty -> LocSymbol [cSort] :: CMeasure ty -> ty data Def ty ctor Def :: LocSymbol -> ctor -> Maybe ty -> [(Symbol, Maybe ty)] -> Body -> Def ty ctor [measure] :: Def ty ctor -> LocSymbol [ctor] :: Def ty ctor -> ctor [dsort] :: Def ty ctor -> Maybe ty [binds] :: Def ty ctor -> [(Symbol, Maybe ty)] [body] :: Def ty ctor -> Body -- | Measures data Body -- | Measure Refinement: {v | v = e } E :: Expr -> Body -- | Measure Refinement: {v | (? v) = p } P :: Expr -> Body -- | Measure Refinement: {v | p} R :: Symbol -> Expr -> Body data MSpec ty ctor MSpec :: HashMap Symbol [Def ty ctor] -> HashMap LocSymbol (Measure ty ctor) -> HashMap LocSymbol (Measure ty ()) -> ![Measure ty ctor] -> MSpec ty ctor [ctorMap] :: MSpec ty ctor -> HashMap Symbol [Def ty ctor] [measMap] :: MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor) [cmeasMap] :: MSpec ty ctor -> HashMap LocSymbol (Measure ty ()) [imeas] :: MSpec ty ctor -> ![Measure ty ctor] -- | Information about scope Binders Scope in type BScope = Bool data RClass ty RClass :: BTyCon -> [ty] -> [BTyVar] -> [(LocSymbol, ty)] -> RClass ty [rcName] :: RClass ty -> BTyCon [rcSupers] :: RClass ty -> [ty] [rcTyVars] :: RClass ty -> [BTyVar] [rcMethods] :: RClass ty -> [(LocSymbol, ty)] -- | KVar Profile -- -------------------------------------------------------------- data KVKind -- | Recursive binder letrec x = ... RecBindE :: Var -> KVKind -- | Non recursive binder let x = ... NonRecBindE :: Var -> KVKind TypeInstE :: KVKind PredInstE :: KVKind LamE :: KVKind -- | Int is the number of cases CaseE :: Int -> KVKind LetE :: KVKind -- | Projecting out field of ProjectE :: KVKind data KVProf emptyKVProf :: KVProf updKVProf :: KVKind -> Kuts -> KVProf -> KVProf mapRTAVars :: (a -> b) -> RTAlias a ty -> RTAlias b ty insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a data LogicMap LM :: HashMap Symbol LMap -> HashMap Var (Maybe Symbol) -> LogicMap -- | Map from symbols to equations they define [lmSymDefs] :: LogicMap -> HashMap Symbol LMap -- | Map from (lifted) Vars to Symbol; see: NOTE:LIFTED-VAR-SYMBOLS -- and NOTE:REFLECT-IMPORTs [lmVarSyms] :: LogicMap -> HashMap Var (Maybe Symbol) toLogicMap :: [(LocSymbol, [Symbol], Expr)] -> LogicMap eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr data LMap LMap :: LocSymbol -> [Symbol] -> Expr -> LMap [lmVar] :: LMap -> LocSymbol [lmArgs] :: LMap -> [Symbol] [lmExpr] :: LMap -> Expr type RDEnv = DEnv Var SpecType newtype DEnv x ty DEnv :: HashMap x (HashMap Symbol (RISig ty)) -> DEnv x ty -- | Refined Instances -- --------------------------------------------------------- data RInstance t RI :: BTyCon -> [t] -> [(LocSymbol, RISig t)] -> RInstance t [riclass] :: RInstance t -> BTyCon [ritype] :: RInstance t -> [t] [risigs] :: RInstance t -> [(LocSymbol, RISig t)] data RISig t RIAssumed :: t -> RISig t RISig :: t -> RISig t data RILaws ty RIL :: BTyCon -> [ty] -> [ty] -> [(LocSymbol, LocSymbol)] -> Located () -> RILaws ty [rilName] :: RILaws ty -> BTyCon [rilSupers] :: RILaws ty -> [ty] [rilTyArgs] :: RILaws ty -> [ty] [rilEqus] :: RILaws ty -> [(LocSymbol, LocSymbol)] [rilPos] :: RILaws ty -> Located () data MethodType t MT :: !Maybe t -> !Maybe t -> MethodType t [tyInstance] :: MethodType t -> !Maybe t [tyClass] :: MethodType t -> !Maybe t getMethodType :: MethodType t -> Maybe t class Reftable r => UReftable r ofUReft :: UReftable r => UReft Reft -> r liquidBegin :: String liquidEnd :: String -- | Values Related to Specifications ------------------------------------ data Axiom b s e Axiom :: (Var, Maybe DataCon) -> Maybe b -> [b] -> [s] -> e -> e -> Axiom b s e [aname] :: Axiom b s e -> (Var, Maybe DataCon) [rname] :: Axiom b s e -> Maybe b [abinds] :: Axiom b s e -> [b] [atypes] :: Axiom b s e -> [s] [alhs] :: Axiom b s e -> e [arhs] :: Axiom b s e -> e type HAxiom = Axiom Var Type CoreExpr rtyVarType :: RTyVar -> Type tyVarVar :: RTVar RTyVar c -> Var newtype RFInfo RFInfo :: Maybe Bool -> RFInfo [permitTC] :: RFInfo -> Maybe Bool defRFInfo :: RFInfo mkRFInfo :: Config -> RFInfo classRFInfo :: Bool -> RFInfo classRFInfoType :: Bool -> RType c tv r -> RType c tv r ordSrcSpan :: SrcSpan -> SrcSpan -> Ordering instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.RFInfo instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.RFInfo instance Data.Data.Data Language.Haskell.Liquid.Types.Types.RFInfo instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.RFInfo instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.PPEnv instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.LogicMap instance GHC.Show.Show t => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.PVKind t) instance Data.Traversable.Traversable Language.Haskell.Liquid.Types.Types.PVKind instance Data.Foldable.Foldable Language.Haskell.Liquid.Types.Types.PVKind instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.PVKind instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.Types.PVKind t) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.PVKind t) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.PVar instance GHC.Show.Show t => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.PVar t) instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.Types.PVar t) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.PVar t) instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.Predicate instance Data.Data.Data Language.Haskell.Liquid.Types.Types.Predicate instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.Predicate instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.RelExpr instance Data.Data.Data Language.Haskell.Liquid.Types.Types.RelExpr instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.RelExpr instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.RelExpr instance Data.Data.Data Language.Haskell.Liquid.Types.Types.BTyVar instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.BTyVar instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.BTyVar instance Data.Data.Data Language.Haskell.Liquid.Types.Types.RTyVar instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.RTyVar instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.BTyCon instance Data.Data.Data Language.Haskell.Liquid.Types.Types.BTyCon instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.BTyCon instance Data.Hashable.Class.Hashable s => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.RTVInfo s) instance GHC.Classes.Eq s => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.RTVInfo s) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.RTVInfo instance Data.Data.Data s => Data.Data.Data (Language.Haskell.Liquid.Types.Types.RTVInfo s) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.RTVInfo s) instance (Data.Hashable.Class.Hashable tv, Data.Hashable.Class.Hashable s) => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.RTVar tv s) instance (Data.Data.Data s, Data.Data.Data tv) => Data.Data.Data (Language.Haskell.Liquid.Types.Types.RTVar tv s) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.RTVar tv s) instance (Data.Hashable.Class.Hashable τ, Data.Hashable.Class.Hashable t) => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.Ref τ t) instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Types.Ref τ) instance (Data.Data.Data τ, Data.Data.Data t) => Data.Data.Data (Language.Haskell.Liquid.Types.Types.Ref τ t) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.Ref τ t) instance (GHC.Classes.Eq τ, GHC.Classes.Eq t) => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.Ref τ t) instance (Data.Hashable.Class.Hashable tv, Data.Hashable.Class.Hashable r, Data.Hashable.Class.Hashable c) => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.RType c tv r) instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Types.RType c tv) instance (Data.Data.Data tv, Data.Data.Data c, Data.Data.Data r) => Data.Data.Data (Language.Haskell.Liquid.Types.Types.RType c tv r) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.RType c tv r) instance (GHC.Classes.Eq tv, GHC.Classes.Eq c, GHC.Classes.Eq r) => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.RType c tv r) instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.Types.HSeg t) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.HSeg t) instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.Types.World t) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.World t) instance Data.Hashable.Class.Hashable r => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.UReft r) instance Data.Traversable.Traversable Language.Haskell.Liquid.Types.Types.UReft instance Data.Foldable.Foldable Language.Haskell.Liquid.Types.Types.UReft instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.UReft instance Data.Data.Data r => Data.Data.Data (Language.Haskell.Liquid.Types.Types.UReft r) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.UReft r) instance GHC.Classes.Eq r => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.UReft r) instance Data.Hashable.Class.Hashable ty => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.RILaws ty) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.RILaws ty) instance Data.Data.Data ty => Data.Data.Data (Language.Haskell.Liquid.Types.Types.RILaws ty) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.RILaws instance GHC.Show.Show ty => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.RILaws ty) instance GHC.Classes.Eq ty => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.RILaws ty) instance Data.Hashable.Class.Hashable t => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.RISig t) instance GHC.Show.Show t => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.RISig t) instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.Types.RISig t) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.RISig instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.RISig t) instance GHC.Classes.Eq t => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.RISig t) instance Data.Hashable.Class.Hashable t => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.RInstance t) instance GHC.Show.Show t => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.RInstance t) instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.Types.RInstance t) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.RInstance instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.RInstance t) instance GHC.Classes.Eq t => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.RInstance t) instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Types.DEnv x) instance (GHC.Show.Show x, GHC.Show.Show ty) => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.DEnv x ty) instance Data.Hashable.Class.Hashable x => GHC.Base.Monoid (Language.Haskell.Liquid.Types.Types.DEnv x ty) instance Data.Hashable.Class.Hashable x => GHC.Base.Semigroup (Language.Haskell.Liquid.Types.Types.DEnv x ty) instance GHC.Show.Show t => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.MethodType t) instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.DataName instance Data.Data.Data Language.Haskell.Liquid.Types.Types.DataName instance GHC.Classes.Ord Language.Haskell.Liquid.Types.Types.DataName instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.DataName instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.DataCtor instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.DataCtor instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.DataCtor instance Data.Data.Data Language.Haskell.Liquid.Types.Types.DataCtor instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.SizeFun instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.SizeFun instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.SizeFun instance Data.Data.Data Language.Haskell.Liquid.Types.Types.SizeFun instance Data.Data.Data Language.Haskell.Liquid.Types.Types.TyConInfo instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.TyConInfo instance Data.Data.Data Language.Haskell.Liquid.Types.Types.RTyCon instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.RTyCon instance Data.Data.Data Language.Haskell.Liquid.Types.Types.DataConP instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.DataConP instance Data.Data.Data Language.Haskell.Liquid.Types.Types.TyConP instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.TyConP instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.DataDeclKind instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.DataDeclKind instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.DataDeclKind instance Data.Data.Data Language.Haskell.Liquid.Types.Types.DataDeclKind instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.DataDeclKind instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.DataDecl instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.DataDecl instance Data.Data.Data Language.Haskell.Liquid.Types.Types.DataDecl instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.HasDataDecl instance (Data.Hashable.Class.Hashable x, Data.Hashable.Class.Hashable a) => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.RTAlias x a) instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Types.RTAlias x) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.RTAlias x a) instance (Data.Data.Data x, Data.Data.Data a) => Data.Data.Data (Language.Haskell.Liquid.Types.Types.RTAlias x a) instance (GHC.Classes.Eq x, GHC.Classes.Eq a) => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.RTAlias x a) instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.Warning instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.Warning instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.Diagnostics instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.Cinfo instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.Cinfo instance Data.Data.Data Language.Haskell.Liquid.Types.Types.ModType instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.ModType instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.ModType instance GHC.Classes.Ord Language.Haskell.Liquid.Types.Types.ModType instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.ModType instance Data.Data.Data Language.Haskell.Liquid.Types.Types.ModName instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.ModName instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.ModName instance GHC.Classes.Ord Language.Haskell.Liquid.Types.Types.ModName instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.ModName instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.Body instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.Body instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.Body instance Data.Data.Data Language.Haskell.Liquid.Types.Types.Body instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.Body instance (Data.Hashable.Class.Hashable ctor, Data.Hashable.Class.Hashable ty) => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.Def ty ctor) instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Types.Def ty) instance (GHC.Classes.Eq ctor, GHC.Classes.Eq ty) => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.Def ty ctor) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.Def ty ctor) instance (Data.Data.Data ty, Data.Data.Data ctor) => Data.Data.Data (Language.Haskell.Liquid.Types.Types.Def ty ctor) instance (GHC.Show.Show ctor, GHC.Show.Show ty) => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.Def ty ctor) instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.MeasureKind instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.MeasureKind instance Data.Data.Data Language.Haskell.Liquid.Types.Types.MeasureKind instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.MeasureKind instance GHC.Classes.Ord Language.Haskell.Liquid.Types.Types.MeasureKind instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.MeasureKind instance (Data.Hashable.Class.Hashable ty, Data.Hashable.Class.Hashable ctor) => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.Measure ty ctor) instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Types.Measure ty) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.Measure ty ctor) instance (Data.Data.Data ctor, Data.Data.Data ty) => Data.Data.Data (Language.Haskell.Liquid.Types.Types.Measure ty ctor) instance (GHC.Classes.Eq ty, GHC.Classes.Eq ctor) => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.Measure ty ctor) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.CMeasure instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.CMeasure ty) instance Data.Data.Data ty => Data.Data.Data (Language.Haskell.Liquid.Types.Types.CMeasure ty) instance Data.Hashable.Class.Hashable ty => Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.RClass ty) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.RClass ty) instance Data.Data.Data ty => Data.Data.Data (Language.Haskell.Liquid.Types.Types.RClass ty) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.RClass instance GHC.Show.Show ty => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.RClass ty) instance GHC.Classes.Eq ty => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.RClass ty) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.AnnInfo instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.AnnInfo a) instance Data.Data.Data a => Data.Data.Data (Language.Haskell.Liquid.Types.Types.AnnInfo a) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.Annot instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.Annot t) instance Data.Data.Data t => Data.Data.Data (Language.Haskell.Liquid.Types.Types.Annot t) instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.Output instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.Output a) instance Data.Data.Data Language.Haskell.Liquid.Types.Types.KVKind instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.KVKind instance GHC.Classes.Ord Language.Haskell.Liquid.Types.Types.KVKind instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.KVKind instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.KVKind instance GHC.Generics.Generic Language.Haskell.Liquid.Types.Types.KVProf instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Types.MSpec ty) instance GHC.Generics.Generic (Language.Haskell.Liquid.Types.Types.MSpec ty ctor) instance (Data.Data.Data ty, Data.Data.Data ctor) => Data.Data.Data (Language.Haskell.Liquid.Types.Types.MSpec ty ctor) instance Data.Bifunctor.Bifunctor Language.Haskell.Liquid.Types.Types.MSpec instance (Language.Fixpoint.Types.PrettyPrint.PPrint t, Language.Fixpoint.Types.PrettyPrint.PPrint a) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.MSpec t a) instance (GHC.Show.Show ty, GHC.Show.Show ctor, Language.Fixpoint.Types.PrettyPrint.PPrint ctor, Language.Fixpoint.Types.PrettyPrint.PPrint ty) => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.MSpec ty ctor) instance GHC.Classes.Eq ctor => GHC.Base.Semigroup (Language.Haskell.Liquid.Types.Types.MSpec ty ctor) instance GHC.Classes.Eq ctor => GHC.Base.Monoid (Language.Haskell.Liquid.Types.Types.MSpec ty ctor) instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.KVProf instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.KVProf instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.KVKind instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.KVKind instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.KVKind instance Language.Fixpoint.Types.PrettyPrint.PPrint a => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.Output a) instance GHC.Base.Monoid (Language.Haskell.Liquid.Types.Types.Output a) instance GHC.Base.Semigroup (Language.Haskell.Liquid.Types.Types.Output a) instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Types.Annot a) instance GHC.Base.Monoid (Language.Haskell.Liquid.Types.Types.AnnInfo a) instance GHC.Base.Semigroup (Language.Haskell.Liquid.Types.Types.AnnInfo a) instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Types.AnnInfo a) instance GHC.Base.Functor (Language.Haskell.Liquid.Types.Types.HoleInfo i) instance Language.Fixpoint.Types.PrettyPrint.PPrint t => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.HoleInfo i t) instance Language.Fixpoint.Types.PrettyPrint.PPrint t => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.RClass t) instance Data.Binary.Class.Binary ty => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.RClass ty) instance Language.Fixpoint.Types.PrettyPrint.PPrint t => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.CMeasure t) instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.CMeasure t) => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.CMeasure t) instance Language.Fixpoint.Types.Spans.Loc (Language.Haskell.Liquid.Types.Types.Measure a b) instance Data.Bifunctor.Bifunctor Language.Haskell.Liquid.Types.Types.Measure instance (Data.Binary.Class.Binary t, Data.Binary.Class.Binary c) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.Measure t c) instance (Language.Fixpoint.Types.PrettyPrint.PPrint t, Language.Fixpoint.Types.PrettyPrint.PPrint a) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.Measure t a) instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.Measure t a) => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.Measure t a) instance Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.Types.Measure ty ctor) instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.MeasureKind instance Data.Bifunctor.Bifunctor Language.Haskell.Liquid.Types.Types.Def instance (Data.Binary.Class.Binary t, Data.Binary.Class.Binary c) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.Def t c) instance Language.Fixpoint.Types.PrettyPrint.PPrint a => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.Def t a) instance Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.Types.Def ty ctor) instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.Body instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.Body instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.Types.Body instance GHC.Base.Monoid (Language.Haskell.Liquid.Types.Types.RTEnv tv t) instance GHC.Base.Semigroup (Language.Haskell.Liquid.Types.Types.RTEnv tv t) instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.ModName instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.ModName instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.Types.ModName instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.ModType instance Language.Fixpoint.Types.PrettyPrint.Fixpoint Language.Haskell.Liquid.Types.Types.Cinfo instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.Cinfo instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.Types.Cinfo instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.Cinfo instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.Cinfo instance GHC.Base.Semigroup Language.Haskell.Liquid.Types.Types.Diagnostics instance GHC.Base.Monoid Language.Haskell.Liquid.Types.Types.Diagnostics instance GHC.Base.Semigroup Language.Haskell.Liquid.Types.Types.REnv instance GHC.Base.Monoid Language.Haskell.Liquid.Types.Types.REnv instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.REnv instance GHC.Base.Functor Language.Haskell.Liquid.Types.Types.AREnv instance Language.Fixpoint.Types.PrettyPrint.PPrint t => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.AREnv t) instance Language.Haskell.Liquid.Types.Types.UReftable (Language.Haskell.Liquid.Types.Types.UReft Language.Fixpoint.Types.Refinements.Reft) instance Language.Haskell.Liquid.Types.Types.UReftable () instance (Data.Binary.Class.Binary x, Data.Binary.Class.Binary a) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.RTAlias x a) instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.HasDataDecl instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.DataDecl instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.DataDecl instance GHC.Classes.Ord Language.Haskell.Liquid.Types.Types.DataDecl instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.Types.DataDecl instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.DataDecl instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.Types.DataDecl instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.DataDeclKind instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.DataDeclKind instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.Types.TyConP instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.Types.DataConP instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.Types.RTyCon instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.RTyCon instance Language.Haskell.Liquid.Types.Types.TyConable Language.Haskell.Liquid.Types.Types.RTyCon instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.RTyCon instance Language.Fixpoint.Types.PrettyPrint.Fixpoint Language.Haskell.Liquid.Types.Types.RTyCon instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.RTyCon instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.RTyCon instance Data.Default.Class.Default Language.Haskell.Liquid.Types.Types.TyConInfo instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.TyConInfo instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.TyConInfo instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.SizeFun instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.SizeFun instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.SizeFun instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.SizeFun instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.DataCtor instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.Types.DataCtor instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.DataName instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.DataName instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.Types.DataName instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.DataName instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.Types.DataName instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.DataName instance GHC.Show.Show (Language.Haskell.Liquid.Types.Types.Axiom GHC.Types.Var.Var GHC.Core.TyCo.Rep.Type GHC.Core.CoreExpr) instance Language.Fixpoint.Types.PrettyPrint.PPrint t => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.RInstance t) instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.RInstance t) instance Language.Fixpoint.Types.PrettyPrint.PPrint t => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.RISig t) instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.RISig t) instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.RILaws t) instance Language.Fixpoint.Types.PrettyPrint.PPrint t => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.RILaws t) instance Language.Haskell.Liquid.Types.Types.TyConable GHC.Core.TyCon.TyCon instance Language.Haskell.Liquid.Types.Types.TyConable Language.Haskell.Liquid.Types.Types.Symbol instance Language.Haskell.Liquid.Types.Types.TyConable Language.Fixpoint.Types.Names.LocSymbol instance Language.Haskell.Liquid.Types.Types.TyConable Language.Haskell.Liquid.Types.Types.BTyCon instance (Language.Fixpoint.Types.Refinements.Reftable r, Language.Haskell.Liquid.Types.Types.TyConable c) => Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.Types.RTProp c tv r) instance (Language.Fixpoint.Types.Refinements.Subable r, Language.Fixpoint.Types.Refinements.Reftable r, Language.Haskell.Liquid.Types.Types.TyConable c) => Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.Types.RType c tv r) instance GHC.Base.Semigroup a => GHC.Base.Semigroup (Language.Haskell.Liquid.Types.Types.UReft a) instance GHC.Base.Monoid a => GHC.Base.Monoid (Language.Haskell.Liquid.Types.Types.UReft a) instance Control.DeepSeq.NFData r => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Types.UReft r) instance Data.Binary.Class.Binary r => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.UReft r) instance (Language.Fixpoint.Types.PrettyPrint.PPrint r, Language.Fixpoint.Types.Refinements.Reftable r) => Language.Fixpoint.Types.Refinements.Reftable (Language.Haskell.Liquid.Types.Types.UReft r) instance Language.Fixpoint.Types.Refinements.Expression (Language.Haskell.Liquid.Types.Types.UReft ()) instance Language.Fixpoint.Types.Refinements.Subable r => Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.Types.UReft r) instance GHC.Show.Show tv => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.RTVU c tv) instance (Data.Binary.Class.Binary c, Data.Binary.Class.Binary tv, Data.Binary.Class.Binary r) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.RType c tv r) instance (Control.DeepSeq.NFData c, Control.DeepSeq.NFData tv, Control.DeepSeq.NFData r) => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Types.RType c tv r) instance (Language.Fixpoint.Types.PrettyPrint.PPrint r, Language.Fixpoint.Types.Refinements.Reftable r, Language.Fixpoint.Types.PrettyPrint.PPrint t, Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.RType c tv r)) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.Ref t (Language.Haskell.Liquid.Types.Types.RType c tv r)) instance (Data.Binary.Class.Binary τ, Data.Binary.Class.Binary t) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.Ref τ t) instance (Control.DeepSeq.NFData τ, Control.DeepSeq.NFData t) => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Types.Ref τ t) instance GHC.Classes.Eq tv => GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.RTVar tv s) instance (Data.Binary.Class.Binary tv, Data.Binary.Class.Binary s) => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.RTVar tv s) instance (Control.DeepSeq.NFData tv, Control.DeepSeq.NFData s) => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Types.RTVar tv s) instance Language.Fixpoint.Types.PrettyPrint.PPrint v => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.RTVar v s) instance Control.DeepSeq.NFData s => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Types.RTVInfo s) instance Data.Binary.Class.Binary s => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.RTVInfo s) instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.BTyCon instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.Types.BTyCon instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.BTyCon instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.BTyCon instance GHC.Classes.Ord Language.Haskell.Liquid.Types.Types.BTyCon instance Language.Fixpoint.Types.PrettyPrint.Fixpoint Language.Haskell.Liquid.Types.Types.BTyCon instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.BTyCon instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.BTyCon instance Language.Fixpoint.Types.Spans.Loc Language.Haskell.Liquid.Types.Types.BTyCon instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.RTyVar instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.Types.RTyVar instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.RTyVar instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.BTyVar instance GHC.Classes.Ord Language.Haskell.Liquid.Types.Types.BTyVar instance Data.String.IsString Language.Haskell.Liquid.Types.Types.BTyVar instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.BTyVar instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.BTyVar instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.BTyVar instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Liquid.Types.Types.BTyVar instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.BTyVar instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.RelExpr instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.RelExpr instance GHC.Classes.Eq Language.Haskell.Liquid.Types.Types.Predicate instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.Predicate instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.Predicate instance GHC.Base.Monoid Language.Haskell.Liquid.Types.Types.Predicate instance GHC.Base.Semigroup Language.Haskell.Liquid.Types.Types.Predicate instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.Types.Predicate instance Language.Fixpoint.Types.Refinements.Reftable Language.Haskell.Liquid.Types.Types.Predicate instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.Predicate instance Language.Fixpoint.Types.Refinements.Subable Language.Haskell.Liquid.Types.Types.UsedPVar instance GHC.Classes.Eq (Language.Haskell.Liquid.Types.Types.PVar t) instance GHC.Classes.Ord (Language.Haskell.Liquid.Types.Types.PVar t) instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.PVar t) instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Types.PVar t) instance Data.Hashable.Class.Hashable (Language.Haskell.Liquid.Types.Types.PVar a) instance Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.PVar a) instance Data.Binary.Class.Binary a => Data.Binary.Class.Binary (Language.Haskell.Liquid.Types.Types.PVKind a) instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Types.PVKind a) instance GHC.Base.Monoid Language.Haskell.Liquid.Types.Types.LogicMap instance GHC.Base.Semigroup Language.Haskell.Liquid.Types.Types.LogicMap instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.LMap instance Data.Hashable.Class.Hashable Language.Haskell.Liquid.Types.Types.RFInfo instance Control.DeepSeq.NFData Language.Haskell.Liquid.Types.Types.RFInfo instance Data.Binary.Class.Binary Language.Haskell.Liquid.Types.Types.RFInfo instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Language.Haskell.Liquid.Types.Errors.TError a) instance Language.Fixpoint.Types.Names.Symbolic Language.Haskell.Syntax.Module.Name.ModuleName instance Language.Fixpoint.Types.Refinements.Subable t => Language.Fixpoint.Types.Refinements.Subable (Language.Haskell.Liquid.Types.Errors.WithModel t) instance Language.Fixpoint.Types.Names.Symbolic GHC.Core.DataCon.DataCon instance Language.Fixpoint.Types.PrettyPrint.PPrint GHC.Core.DataCon.DataCon instance GHC.Classes.Ord GHC.Core.TyCon.TyCon instance GHC.Classes.Ord GHC.Core.DataCon.DataCon instance Language.Fixpoint.Types.PrettyPrint.PPrint GHC.Types.TyThing.TyThing instance GHC.Show.Show GHC.Core.DataCon.DataCon -- | This module contains a single function that converts a RType -> Doc -- without using *any* simplifications. module Language.Haskell.Liquid.Types.PrettyPrint type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, Reftable r, Reftable (RTProp c tv ()), Reftable (RTProp c tv r), Eq c, Eq tv, Hashable tv) rtypeDoc :: OkRT c tv r => Tidy -> RType c tv r -> Doc pprManyOrdered :: (PPrint a, Ord a) => Tidy -> String -> [a] -> [Doc] pprintLongList :: PPrint a => Tidy -> [a] -> Doc pprintSymbol :: Symbol -> Doc -- | Printing Warnings -- --------------------------------------------------------- printWarning :: Logger -> Warning -> IO () -- | Filters match errors. They are used to ignore classes of errors -- they match. AnyFilter matches all errors. StringFilter -- matches any error whose "representation" contains the given -- String. A "representation" is pretty-printed String of the -- error. data Filter StringFilter :: String -> Filter AnyFilter :: Filter -- | Retrieve the Filters from the Config. getFilters :: Config -> [Filter] -- | Return the list of filters that matched the err , -- given a renderer for the err and some -- filters reduceFilters :: (e -> String) -> [Filter] -> e -> [Filter] -- | Report errors via GHC's API stating the given Filters did not -- get matched. Does nothing if the list of filters is empty. defaultFilterReporter :: FilePath -> [Filter] -> TcRn () -- | Used in filterReportErrorsWith' data FilterReportErrorsArgs m filter msg e a FilterReportErrorsArgs :: ([e] -> m ()) -> ([filter] -> m ()) -> m a -> m a -> (e -> [filter]) -> [filter] -> FilterReportErrorsArgs m filter msg e a -- | Report the msgs to the monad (usually IO) [errorReporter] :: FilterReportErrorsArgs m filter msg e a -> [e] -> m () -- | Report unmatched filters to the monad [filterReporter] :: FilterReportErrorsArgs m filter msg e a -> [filter] -> m () -- | Continuation for when there are unmatched filters or unmatched errors [failure] :: FilterReportErrorsArgs m filter msg e a -> m a -- | Continuation for when there are no unmatched errors or filters [continue] :: FilterReportErrorsArgs m filter msg e a -> m a -- | Yields the filters that map a given error. Must only yield filters in -- the filters field. [matchingFilters] :: FilterReportErrorsArgs m filter msg e a -> e -> [filter] -- | List of filters which could have been matched [filters] :: FilterReportErrorsArgs m filter msg e a -> [filter] -- | Calls the continuations in FilterReportErrorsArgs depending on -- whethere there are unmatched errors, unmatched filters or none. filterReportErrorsWith :: (Monad m, Ord filter) => FilterReportErrorsArgs m filter msg e a -> [e] -> m a -- | Pretty-printing errors -- ---------------------------------------------------- -- -- Similar in spirit to reportErrors from the GHC API, but it -- uses our pretty-printer and shim functions under the hood. Also -- filters the errors according to the given Filter list. -- -- filterReportErrors failure continue filters k will call -- failure if there are unexpected errors, or will call -- continue otherwise. -- -- An error is expected if there is any filter that matches it. filterReportErrors :: forall e' a. (Show e', PPrint e') => FilePath -> TcRn a -> TcRn a -> [Filter] -> Tidy -> [TError e'] -> TcRn a instance GHC.Show.Show Language.Haskell.Liquid.Types.PrettyPrint.Filter instance GHC.Classes.Ord Language.Haskell.Liquid.Types.PrettyPrint.Filter instance GHC.Classes.Eq Language.Haskell.Liquid.Types.PrettyPrint.Filter instance Language.Fixpoint.Types.PrettyPrint.PPrint GHC.Types.SourceError.SourceError instance Language.Fixpoint.Types.PrettyPrint.PPrint GHC.Types.Var.Var instance Language.Fixpoint.Types.PrettyPrint.PPrint (GHC.Core.Expr GHC.Types.Var.Var) instance Language.Fixpoint.Types.PrettyPrint.PPrint (GHC.Core.Bind GHC.Types.Var.Var) instance Language.Fixpoint.Types.PrettyPrint.PPrint GHC.Types.Name.Name instance Language.Fixpoint.Types.PrettyPrint.PPrint GHC.Core.TyCon.TyCon instance Language.Fixpoint.Types.PrettyPrint.PPrint GHC.Core.TyCo.Rep.Type instance Language.Fixpoint.Types.PrettyPrint.PPrint GHC.Core.Class.Class instance GHC.Show.Show Language.Haskell.Liquid.Types.Types.Predicate instance Language.Fixpoint.Types.PrettyPrint.PPrint t => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.Annot t) instance Language.Fixpoint.Types.PrettyPrint.PPrint a => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.AnnInfo a) instance Language.Fixpoint.Types.PrettyPrint.PPrint a => GHC.Show.Show (Language.Haskell.Liquid.Types.Types.AnnInfo a) instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.LMap instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Haskell.Liquid.Types.Types.LogicMap instance Language.Haskell.Liquid.Types.Types.OkRT c tv r => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.RType c tv r) instance (Language.Fixpoint.Types.PrettyPrint.PPrint tv, Language.Fixpoint.Types.PrettyPrint.PPrint ty) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.RTAlias tv ty) instance (Language.Fixpoint.Types.PrettyPrint.PPrint tv, Language.Fixpoint.Types.PrettyPrint.PPrint t) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.RTEnv tv t) instance Language.Fixpoint.Types.PrettyPrint.PPrint Language.Fixpoint.Types.PrettyPrint.Tidy instance (Language.Fixpoint.Types.PrettyPrint.PPrint r, Language.Fixpoint.Types.Refinements.Reftable r) => Language.Fixpoint.Types.PrettyPrint.PPrint (Language.Haskell.Liquid.Types.Types.UReft r) -- | This module contains the code for generating "tags" for constraints -- based on their source, i.e. the top-level binders under which the -- constraint was generated. These tags are used by fixpoint to -- prioritize constraints by the "source-level" function. module Language.Haskell.Liquid.UX.CTags -- | The TagKey is the top-level binder, and Tag is a -- singleton Int list type TagKey = Var type TagEnv = HashMap TagKey Tag defaultTag :: Tag makeTagEnv :: [CoreBind] -> TagEnv getTag :: TagKey -> TagEnv -> Tag memTagEnv :: TagKey -> TagEnv -> Bool module Language.Haskell.Liquid.Transforms.InlineAux inlineAux :: Config -> Module -> CoreProgram -> CoreProgram module Language.Haskell.Liquid.GHC.TypeRep mkTyArg :: TyVar -> TyVarBinder showTy :: Type -> String instance (GHC.Classes.Eq tyvar, GHC.Classes.Eq argf) => GHC.Classes.Eq (GHC.Types.Var.VarBndr tyvar argf) instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy GHC.Core.TyCo.Rep.Type instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy GHC.Core.TyCo.Rep.Coercion instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy Language.Haskell.Syntax.Basic.Role instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy (GHC.Core.Coercion.Axiom.CoAxiom GHC.Core.Coercion.Axiom.Branched) instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy GHC.Core.TyCo.Rep.UnivCoProvenance instance Language.Haskell.Liquid.GHC.TypeRep.SubstTy GHC.Core.Coercion.Axiom.CoAxiomRule instance (Language.Haskell.Liquid.GHC.TypeRep.SubstTy a, GHC.Base.Functor m) => Language.Haskell.Liquid.GHC.TypeRep.SubstTy (m a) instance GHC.Classes.Eq GHC.Core.TyCo.Rep.Type instance GHC.Classes.Eq GHC.Core.TyCo.Rep.Coercion module Language.Haskell.Liquid.GHC.SpanStack -- | A single span data Span -- | binder for whom we are generating constraint Var :: !Var -> Span -- | nearest known Source Span Tick :: !CoreTickish -> Span Span :: SrcSpan -> Span -- | Opaque type for a stack of spans data SpanStack empty :: SpanStack push :: Span -> SpanStack -> SpanStack srcSpan :: SpanStack -> SrcSpan showSpan :: Show a => a -> SrcSpan instance GHC.Show.Show Language.Haskell.Liquid.GHC.SpanStack.Span -- | This module contains functions for "resugaring" low-level GHC -- CoreExpr into high-level patterns, that can receive special -- case handling in different phases (e.g. ANF, Constraint Generation, -- etc.) module Language.Haskell.Liquid.GHC.Resugar -- | Data type for high-level patterns -- ----------------------------------------- data Pattern -- | e1 >>= x -> e2 PatBind :: !CoreExpr -> !Var -> !CoreExpr -> !Type -> !CoreExpr -> !Type -> !Type -> !Var -> Pattern [patE1] :: Pattern -> !CoreExpr -- | x [patX] :: Pattern -> !Var [patE2] :: Pattern -> !CoreExpr -- | m [patM] :: Pattern -> !Type -- | $dT [patDct] :: Pattern -> !CoreExpr [patTyA] :: Pattern -> !Type [patTyB] :: Pattern -> !Type [patFF] :: Pattern -> !Var PatReturn :: !CoreExpr -> !Type -> !CoreExpr -> !Type -> !Var -> Pattern -- | e [patE] :: Pattern -> !CoreExpr -- | m [patM] :: Pattern -> !Type -- | $dT [patDct] :: Pattern -> !CoreExpr -- | t [patTy] :: Pattern -> !Type -- | "return" [patRet] :: Pattern -> !Var PatProject :: !Var -> !Var -> !Type -> !DataCon -> ![Var] -> !Int -> Pattern -- | xe [patXE] :: Pattern -> !Var -- | x [patX] :: Pattern -> !Var -- | t [patTy] :: Pattern -> !Type -- | C [patCtor] :: Pattern -> !DataCon -- |