| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Types.Errors
Description
This module contains the *types* related creating Errors. It depends only on Fixpoint and basic haskell libraries, and hence, should be importable everywhere.
Synopsis
- data TError t
- = ErrSubType { }
- | ErrSubTypeModel { }
- | ErrFCrash { }
- | ErrHole { }
- | ErrHoleCycle {
- pos :: !SrcSpan
- holesCycle :: [Symbol]
- | ErrAssType { }
- | ErrParse { }
- | ErrTySpec { }
- | ErrTermSpec { }
- | ErrDupAlias { }
- | ErrDupSpecs { }
- | ErrDupIMeas { }
- | ErrDupMeas { }
- | ErrDupField { }
- | ErrDupNames { }
- | ErrBadData { }
- | ErrBadGADT { }
- | ErrDataCon { }
- | ErrInvt { }
- | ErrIAl { }
- | ErrIAlMis { }
- | ErrMeas { }
- | ErrHMeas { }
- | ErrUnbound { }
- | ErrUnbPred { }
- | ErrGhc { }
- | ErrResolve { }
- | ErrMismatch { }
- | ErrPartPred { }
- | ErrAliasCycle { }
- | ErrIllegalAliasApp { }
- | ErrAliasApp { }
- | ErrTermin { }
- | ErrStTerm { }
- | ErrILaw { }
- | ErrRClass { }
- | ErrMClass { }
- | ErrBadQual { }
- | ErrSaved { }
- | ErrFilePragma { }
- | ErrTyCon { }
- | ErrLiftExp { }
- | ErrParseAnn { }
- | ErrNoSpec { }
- | ErrFail { }
- | ErrFailUsed { }
- | ErrRewrite { }
- | ErrOther { }
- data CtxError t = CtxError {}
- errorsWithContext :: [TError Doc] -> IO [CtxError Doc]
- data Oblig
- data WithModel t
- dropModel :: WithModel t -> t
- type UserError = TError Doc
- panic :: Maybe SrcSpan -> String -> a
- panicDoc :: SrcSpan -> Doc -> a
- todo :: Maybe SrcSpan -> String -> a
- impossible :: Maybe SrcSpan -> String -> a
- uError :: UserError -> a
- 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
- realSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan
- unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int)
- srcSpanFileMb :: SrcSpan -> Maybe FilePath
Generic Error Type
Generic Type for Error Messages -------------------------------------------
INVARIANT : all Error constructors should have a pos field
Constructors
| ErrSubType | liquid type error |
| ErrSubTypeModel | liquid type error with a counter-example |
| ErrFCrash | liquid type error |
| ErrHole | hole type |
| ErrHoleCycle | hole dependencies form a cycle error |
Fields
| |
| ErrAssType | condition failure error |
| ErrParse | specification parse error |
| ErrTySpec | sort error in specification |
| ErrTermSpec | sort error in specification |
| ErrDupAlias | multiple alias with same name error |
| ErrDupSpecs | multiple specs for same binder error |
| ErrDupIMeas | multiple definitions of the same instance measure |
| ErrDupMeas | multiple definitions of the same measure |
| ErrDupField | duplicate fields in same datacon |
| ErrDupNames | name resolves to multiple possible GHC vars |
| ErrBadData | bad data type specification (?) |
| ErrBadGADT | bad data type specification (?) |
| ErrDataCon | refined datacon mismatches haskell datacon |
| ErrInvt | Invariant sort error |
| ErrIAl | Using sort error |
| ErrIAlMis | Incompatible using error |
| ErrMeas | Measure sort error |
| ErrHMeas | Haskell bad Measure error |
| ErrUnbound | Unbound symbol in specification |
| ErrUnbPred | Unbound predicate being applied |
| ErrGhc | GHC error: parsing or type checking |
| ErrResolve | Name resolution error |
| ErrMismatch | Mismatch between Liquid and Haskell types |
| ErrPartPred | Mismatch in expected/actual args of abstract refinement |
| ErrAliasCycle | Cyclic Refined Type Alias Definitions |
| ErrIllegalAliasApp | Illegal RTAlias application (from BSort, eg. in PVar) |
| ErrAliasApp | |
| ErrTermin | Termination Error |
| ErrStTerm | Termination Error |
| ErrILaw | Instance Law Error |
| ErrRClass | Refined Class/Interfaces Conflict |
| ErrMClass | Standalone class method refinements |
| ErrBadQual | Non well sorted Qualifier |
| ErrSaved | Previously saved error, that carries over after DiffCheck |
| ErrFilePragma | |
| ErrTyCon | |
| ErrLiftExp | |
| ErrParseAnn | |
| ErrNoSpec | |
| ErrFail | |
| ErrFailUsed | |
| ErrRewrite | |
| ErrOther | Sigh. Other. |
Instances
Error with Source Context
Context information for Error Messages ------------------------------------
Instances
| Functor CtxError Source # | |
| Eq (CtxError t) Source # | |
| Ord (CtxError t) Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| Show (CtxError Doc) Source # | |
| PPrint (CtxError Doc) Source # | Pretty Printing Error Messages -------------------------------------------- Need to put |
Defined in Language.Haskell.Liquid.UX.Tidy | |
| PPrint (CtxError SpecType) Source # | |
Defined in Language.Haskell.Liquid.UX.Tidy | |
Subtyping Obligation Type
Different kinds of Check Obligations ------------------------------------
Constructors
| OTerm | Obligation that proves termination |
| OInv | Obligation that proves invariants |
| OCons | Obligation that proves subtyping constraints |
Instances
| Eq Oblig Source # | |
| Data Oblig Source # | |
Defined in Language.Haskell.Liquid.Types.Errors Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Oblig -> c Oblig # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Oblig # dataTypeOf :: Oblig -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Oblig) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Oblig) # gmapT :: (forall b. Data b => b -> b) -> Oblig -> Oblig # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r # gmapQ :: (forall d. Data d => d -> u) -> Oblig -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Oblig -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Oblig -> m Oblig # | |
| Show Oblig Source # | |
| Generic Oblig Source # | |
| NFData Oblig Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| Binary Oblig Source # | |
| Hashable Oblig Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| PPrint Oblig Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| type Rep Oblig Source # | |
Defined in Language.Haskell.Liquid.Types.Errors type Rep Oblig = D1 ('MetaData "Oblig" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" 'False) (C1 ('MetaCons "OTerm" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OInv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OCons" 'PrefixI 'False) (U1 :: Type -> Type))) | |
Adding a Model of the context
Instances
| Functor WithModel Source # | |
| Eq t => Eq (WithModel t) Source # | |
| Show t => Show (WithModel t) Source # | |
| Generic (WithModel t) Source # | |
| NFData t => NFData (WithModel t) Source # | |
Defined in Language.Haskell.Liquid.Types.Errors | |
| Subable t => Subable (WithModel t) Source # | |
Defined in Language.Haskell.Liquid.Types.Types | |
| type Rep (WithModel t) Source # | |
Defined in Language.Haskell.Liquid.Types.Errors type Rep (WithModel t) = D1 ('MetaData "WithModel" "Language.Haskell.Liquid.Types.Errors" "liquidhaskell-0.8.10.2-L92dB1QZcuO9sqg2FFZRKf" 'False) (C1 ('MetaCons "NoModel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "WithModel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Doc) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))) | |
Panic (unexpected failures)
type UserError = TError Doc Source #
Simple unstructured type for panic ----------------------------------------
todo :: Maybe SrcSpan -> String -> a Source #
Construct and show an Error with an optional SrcSpan, then crash This function should be used to mark unimplemented functionality
impossible :: Maybe SrcSpan -> String -> a Source #
Construct and show an Error with an optional SrcSpan, then crash This function should be used to mark impossible-to-reach codepaths
sourceErrors :: String -> SourceError -> [TError t] Source #
Convert a GHC error into a list of our errors.
Printing Errors
SrcSpan Helpers
realSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan Source #
unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int) Source #
Orphan instances
| NFData ParseError Source # | |
Methods rnf :: ParseError -> () # | |
| ToJSON RealSrcSpan Source # | |
Methods toJSON :: RealSrcSpan -> Value # toEncoding :: RealSrcSpan -> Encoding # toJSONList :: [RealSrcSpan] -> Value # toEncodingList :: [RealSrcSpan] -> Encoding # | |
| ToJSON SrcSpan Source # | |
| ToJSONKey SrcSpan Source # | |
| FromJSON RealSrcSpan Source # | |
| FromJSON SrcSpan Source # | |
| FromJSONKey SrcSpan Source # | |
Methods | |
| PPrint SrcSpan Source # | |
| PPrint ParseError Source # | |