liquidhaskell-boot-0.9.2.5.0: Liquid Types for Haskell
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Haskell.Liquid.Types.Specs

Description

This module contains the top-level structures that hold information about specifications.

Synopsis

Different types of specifications

There are different types or "flavours" for a specification, depending on its lifecycle. The main goal is always the same, i.e. refining the Haskell types and produce a final statement (i.e. safe or unsafe) about the input program. In order to do so, a specification is transformed in the way described by this picture:

    +---------------+                                +-------------------+
    |   BareSpec    |                                |                   |  checked by liquid/liquidOne
    |               |                    ------------|    TargetSpec     |----------------------------- ..
    |(input module) |                   /            |                   |
    +---------------+  makeTargetSpec  /             +-------------------+
           +         -----------------/
    +---------------+                 \              +-------------------+
    | {LiftedSpec}  |                  \             |                   |    serialised on disk
    |               |                   -------------|    LiftedSpec     |----------------------------- ..
    |(dependencies) |                                |                   |
    +---------------+                                +-------------------+
          ^                                                    |
          |                   used-as                          |
          +----------------------------------------------------+

More specifically, we distinguish:

  • BareSpec - is the specification obtained by parsing the Liquid annotations of the input Haskell file. It typically contains information about the associated input Haskell module, with the exceptions of assumptions that can refer to functions defined in other modules.
  • LiftedSpec - is the specification we obtain by "lifting" the BareSpec. Most importantly, a LiftedSpec gets serialised on disk and becomes a dependency for the verification of other BareSpecs.

Lifting in this context consist of:

  1. Perform name-resolution (e.g. make all the relevant GHC's Vars qualified, resolve GHC's Names, etc);
  2. Strip the final LiftedSpec with information which are relevant (read: local) to just the input BareSpec. An example would be local signatures, used to annotate internal, auxiliary functions within a Module;
  3. Strip termination checks, which are required (if specified) for a BareSpec but not for the LiftedSpec.
  • TargetSpec - is the specification we actually use for refinement, and is conceptually an "augmented" BareSpec. You can create a TargetSpec by calling makeTargetSpec.

In order to produce these spec types we have to gather information about the module being compiled by using the GHC API and retain enough context of the compiled Module in order to be able to construct the types introduced aboves. The rest of this module introduced also these intermediate structures.

The following is the overall type for specifications obtained from parsing the target source and dependent libraries. IMPORTANT: A TargetInfo is what is checked by LH itself and it NEVER contains the LiftedSpec, because the checking happens only on the BareSpec of the target module.

data TargetInfo Source #

Constructors

TargetInfo 

Fields

Gathering information about a module

data TargetSrc Source #

The TargetSrc type is a collection of all the things we know about a module being currently checked. It include things like the name of the module, the list of CoreBinds, the TyCons declared in this module (that includes TyCons for classes), typeclass instances and so and so forth. It might be consider a sort of ModGuts embellished with LH-specific information (for example, giDefVars are populated with datacons from the module plus the let vars derived from the A-normalisation).

Constructors

TargetSrc 

Fields

TargetSpec

 

data TargetSpec Source #

A TargetSpec is what we actually check via LiquidHaskell. It is created as part of mkTargetSpec alongside the LiftedSpec. It shares a similar structure with a BareSpec, but manipulates and transforms the data in preparation to the checking process.

Instances

Instances details
PPrint TargetSpec Source #

Pretty Printing -----------------------------------------------------------

Instance details

Defined in Language.Haskell.Liquid.GHC.Interface

HasConfig TargetSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

BareSpec

 

newtype BareSpec Source #

A BareSpec is the spec we derive by parsing the Liquid Haskell annotations of a single file. As such, it contains things which are relevant for validation and lifting; it contains things like the pragmas the user defined, the termination condition (if termination-checking is enabled) and so on and so forth. Crucially, as a BareSpec is still subject to "preflight checks", it may contain duplicates (e.g. duplicate measures, duplicate type declarations etc.) and therefore most of the fields for a BareSpec are lists, so that we can report these errors to the end user: it would be an error to silently ignore the duplication and leave the duplicate resolution to whichever Eq instance is implemented for the relevant field.

Also, a BareSpec has not yet been subject to name resolution, so it may refer to undefined or out-of-scope entities.

Instances

Instances details
Monoid BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Semigroup BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Generic BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Associated Types

type Rep BareSpec :: Type -> Type #

Methods

from :: BareSpec -> Rep BareSpec x #

to :: Rep BareSpec x -> BareSpec #

Show BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Binary BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

put :: BareSpec -> Put #

get :: Get BareSpec #

putList :: [BareSpec] -> Put #

type Rep BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

type Rep BareSpec = D1 ('MetaData "BareSpec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'True) (C1 ('MetaCons "MkBareSpec" 'PrefixI 'True) (S1 ('MetaSel ('Just "getBareSpec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Spec LocBareType LocSymbol))))

LiftedSpec

 

data LiftedSpec Source #

A LiftedSpec is derived from an input BareSpec and a set of its dependencies. The general motivations for lifting a spec are (a) name resolution, (b) the fact that some info is only relevant for checking the body of functions but does not need to be exported, e.g. termination measures, or the fact that a type signature was assumed. A LiftedSpec is what we serialise on disk and what the clients should will be using.

What we do not have compared to a BareSpec:

  • The localSigs, as it's not necessary/visible to clients;
  • The includes, as they are probably not reachable for clients anyway;
  • The reflSigs, they are now just "normal" signatures;
  • The lazy, we don't do termination checking in lifted specs;
  • The reflects, the reflection has already happened at this point;
  • The hmeas, we have already turned these into measures at this point;
  • The hbounds, ditto as hmeas;
  • The inlines, ditto as hmeas;
  • The ignores, ditto as hmeas;
  • The pragmas, we can't make any use of this information for lifted specs;
  • The termexprs, we don't do termination checking in lifted specs;

Apart from less fields, a LiftedSpec replaces all instances of lists with sets, to enforce duplicate detection and removal on what we serialise on disk.

Constructors

LiftedSpec 

Fields

Instances

Instances details
Generic LiftedSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Associated Types

type Rep LiftedSpec :: Type -> Type #

Show LiftedSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Binary LiftedSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Eq LiftedSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Hashable LiftedSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

type Rep LiftedSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

type Rep LiftedSpec = D1 ('MetaData "LiftedSpec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "LiftedSpec" 'PrefixI 'True) ((((S1 ('MetaSel ('Just "liftedMeasures") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Measure LocBareType LocSymbol))) :*: (S1 ('MetaSel ('Just "liftedImpSigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Symbol, Sort))) :*: S1 ('MetaSel ('Just "liftedExpSigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Symbol, Sort))))) :*: ((S1 ('MetaSel ('Just "liftedAsmSigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (LocSymbol, LocBareType))) :*: S1 ('MetaSel ('Just "liftedSigs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (LocSymbol, LocBareType)))) :*: (S1 ('MetaSel ('Just "liftedInvariants") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Maybe LocSymbol, LocBareType))) :*: S1 ('MetaSel ('Just "liftedIaliases") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (LocBareType, LocBareType)))))) :*: ((S1 ('MetaSel ('Just "liftedImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet Symbol)) :*: (S1 ('MetaSel ('Just "liftedDataDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet DataDecl)) :*: S1 ('MetaSel ('Just "liftedNewtyDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet DataDecl)))) :*: ((S1 ('MetaSel ('Just "liftedAliases") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Located (RTAlias Symbol BareType)))) :*: S1 ('MetaSel ('Just "liftedEaliases") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Located (RTAlias Symbol Expr))))) :*: (S1 ('MetaSel ('Just "liftedEmbeds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TCEmb LocSymbol)) :*: S1 ('MetaSel ('Just "liftedQualifiers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet Qualifier)))))) :*: (((S1 ('MetaSel ('Just "liftedLvars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet LocSymbol)) :*: (S1 ('MetaSel ('Just "liftedAutois") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap LocSymbol (Maybe Int))) :*: S1 ('MetaSel ('Just "liftedAutosize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet LocSymbol)))) :*: ((S1 ('MetaSel ('Just "liftedCmeasures") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Measure LocBareType ()))) :*: S1 ('MetaSel ('Just "liftedImeasures") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (Measure LocBareType LocSymbol)))) :*: (S1 ('MetaSel ('Just "liftedClasses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (RClass LocBareType))) :*: S1 ('MetaSel ('Just "liftedClaws") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (RClass LocBareType)))))) :*: ((S1 ('MetaSel ('Just "liftedRinstance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (RInstance LocBareType))) :*: (S1 ('MetaSel ('Just "liftedIlaws") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (RILaws LocBareType))) :*: S1 ('MetaSel ('Just "liftedDsize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [([LocBareType], LocSymbol)]))) :*: ((S1 ('MetaSel ('Just "liftedDvariance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet (LocSymbol, [Variance]))) :*: S1 ('MetaSel ('Just "liftedBounds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RRBEnv LocBareType))) :*: (S1 ('MetaSel ('Just "liftedDefs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap LocSymbol Symbol)) :*: S1 ('MetaSel ('Just "liftedAxeqs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashSet Equation))))))))

Tracking dependencies

 

newtype TargetDependencies Source #

The target dependencies that concur to the creation of a TargetSpec and a LiftedSpec.

Instances

Instances details
Monoid TargetDependencies Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Semigroup TargetDependencies Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Generic TargetDependencies Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Associated Types

type Rep TargetDependencies :: Type -> Type #

Show TargetDependencies Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Binary TargetDependencies Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Eq TargetDependencies Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

type Rep TargetDependencies Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

type Rep TargetDependencies = D1 ('MetaData "TargetDependencies" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'True) (C1 ('MetaCons "TargetDependencies" 'PrefixI 'True) (S1 ('MetaSel ('Just "getDependencies") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HashMap StableModule LiftedSpec))))

Predicates on spec types

 

isPLEVar :: TargetSpec -> Var -> Bool Source #

Returns True if the input Var is a PLE one.

isExportedVar :: TargetSrc -> Var -> Bool Source #

Returns True if the input Var was exported in the module the input TargetSrc represents.

Other types

data QImports Source #

QImports is a map of qualified imports.

Constructors

QImports 

Fields

Instances

Instances details
Show QImports Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

data Spec ty bndr Source #

A generic Spec type, polymorphic over the inner choice of type and binder.

Constructors

Spec 

Fields

Instances

Instances details
Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Monoid (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

mempty :: Spec ty bndr #

mappend :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr #

mconcat :: [Spec ty bndr] -> Spec ty bndr #

Semigroup (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

(<>) :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr #

sconcat :: NonEmpty (Spec ty bndr) -> Spec ty bndr #

stimes :: Integral b => b -> Spec ty bndr -> Spec ty bndr #

Generic (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Associated Types

type Rep (Spec ty bndr) :: Type -> Type #

Methods

from :: Spec ty bndr -> Rep (Spec ty bndr) x #

to :: Rep (Spec ty bndr) x -> Spec ty bndr #

(PPrint ty, PPrint bndr, Show ty) => Show (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

showsPrec :: Int -> Spec ty bndr -> ShowS #

show :: Spec ty bndr -> String #

showList :: [Spec ty bndr] -> ShowS #

Binary (Spec LocBareType LocSymbol) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

(Show ty, Show bndr, PPrint ty, PPrint bndr) => PPrint (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

pprintTidy :: Tidy -> Spec ty bndr -> Doc #

pprintPrec :: Int -> Tidy -> Spec ty bndr -> Doc #

type Rep (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

type Rep (Spec ty bndr) = D1 ('MetaData "Spec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "Spec" 'PrefixI 'True) (((((S1 ('MetaSel ('Just "measures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty bndr]) :*: S1 ('MetaSel ('Just "impSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)])) :*: (S1 ('MetaSel ('Just "expSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)]) :*: (S1 ('MetaSel ('Just "asmSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)]) :*: S1 ('MetaSel ('Just "sigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)])))) :*: ((S1 ('MetaSel ('Just "localSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)]) :*: (S1 ('MetaSel ('Just "reflSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)]) :*: S1 ('MetaSel ('Just "invariants") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Maybe LocSymbol, ty)]))) :*: (S1 ('MetaSel ('Just "ialiases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(ty, ty)]) :*: (S1 ('MetaSel ('Just "imports") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "dataDecls") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataDecl]))))) :*: (((S1 ('MetaSel ('Just "newtyDecls") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataDecl]) :*: S1 ('MetaSel ('Just "includes") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [FilePath])) :*: (S1 ('MetaSel ('Just "aliases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located (RTAlias Symbol BareType)]) :*: (S1 ('MetaSel ('Just "ealiases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located (RTAlias Symbol Expr)]) :*: S1 ('MetaSel ('Just "embeds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (TCEmb LocSymbol))))) :*: ((S1 ('MetaSel ('Just "qualifiers") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Qualifier]) :*: (S1 ('MetaSel ('Just "lvars") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: S1 ('MetaSel ('Just "lazy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)))) :*: (S1 ('MetaSel ('Just "rewrites") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: (S1 ('MetaSel ('Just "rewriteWith") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol [LocSymbol])) :*: S1 ('MetaSel ('Just "fails") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol))))))) :*: ((((S1 ('MetaSel ('Just "reflects") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: S1 ('MetaSel ('Just "autois") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol (Maybe Int)))) :*: (S1 ('MetaSel ('Just "hmeas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: (S1 ('MetaSel ('Just "hbounds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: S1 ('MetaSel ('Just "inlines") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol))))) :*: ((S1 ('MetaSel ('Just "ignores") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: (S1 ('MetaSel ('Just "autosize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: S1 ('MetaSel ('Just "pragmas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located String]))) :*: (S1 ('MetaSel ('Just "cmeasures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty ()]) :*: (S1 ('MetaSel ('Just "imeasures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty bndr]) :*: S1 ('MetaSel ('Just "classes") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RClass ty]))))) :*: (((S1 ('MetaSel ('Just "claws") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RClass ty]) :*: S1 ('MetaSel ('Just "relational") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)])) :*: (S1 ('MetaSel ('Just "asmRel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]) :*: (S1 ('MetaSel ('Just "termexprs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, [Located Expr])]) :*: S1 ('MetaSel ('Just "rinstance") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RInstance ty])))) :*: ((S1 ('MetaSel ('Just "ilaws") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RILaws ty]) :*: (S1 ('MetaSel ('Just "dvariance") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, [Variance])]) :*: S1 ('MetaSel ('Just "dsize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [([ty], LocSymbol)]))) :*: (S1 ('MetaSel ('Just "bounds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (RRBEnv ty)) :*: (S1 ('MetaSel ('Just "defs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol Symbol)) :*: S1 ('MetaSel ('Just "axeqs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Equation]))))))))

data GhcSpecVars Source #

The collection of GHC Vars that a TargetSpec needs to verify (or skip).

Constructors

SpVar 

Fields

data GhcSpecSig Source #

Constructors

SpSig 

Fields

data GhcSpecNames Source #

Constructors

SpNames 

Fields

data GhcSpecTerm Source #

Constructors

SpTerm 

Fields

data GhcSpecRefl Source #

Constructors

SpRefl 

Fields

data GhcSpecLaws Source #

Constructors

SpLaws 

Fields

data GhcSpecData Source #

Constructors

SpData 

Fields

data GhcSpecQual Source #

Constructors

SpQual 

Fields

Legacy data structures

 

data GhcSrc Source #

Constructors

Src 

Fields

data GhcSpec Source #

Constructors

SP 

Fields

Instances

Instances details
HasConfig GhcSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Provisional compatibility exports & optics

Orphan instances

Binary Equation Source # 
Instance details

Methods

put :: Equation -> Put #

get :: Get Equation #

putList :: [Equation] -> Put #