cryptol-3.0.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe-Inferred
Language | Haskell2010

Cryptol.TypeCheck

Description

Synopsis

- tcModule :: Module Name -> InferInput -> IO (InferOutput TCTopEntity)
- tcExpr :: Expr Name -> InferInput -> IO (InferOutput (Expr, Schema))
- tcDecls :: [TopDecl Name] -> InferInput -> IO (InferOutput ([DeclGroup], Map Name TySyn))
- data InferInput = InferInput {
  - inpRange :: Range
  - inpVars :: Map Name Schema
  - inpTSyns :: Map Name TySyn
  - inpNewtypes :: Map Name Newtype
  - inpAbstractTypes :: Map Name AbstractType
  - inpSignatures :: !(Map Name ModParamNames)
  - inpTopModules :: ModName -> Maybe (ModuleG (), IfaceG ())
  - inpTopSignatures :: ModName -> Maybe ModParamNames
  - inpParams :: !ModParamNames
  - inpNameSeeds :: NameSeeds
  - inpMonoBinds :: Bool
  - inpCallStacks :: Bool
  - inpSearchPath :: [FilePath]
  - inpPrimNames :: !PrimMap
  - inpSupply :: !Supply
  - inpSolver :: Solver
  }
- data InferOutput a
  - = InferFailed NameMap [(Range, Warning)] [(Range, Error)]
  - | InferOK NameMap [(Range, Warning)] NameSeeds Supply a
- data SolverConfig = SolverConfig {
  - solverPath :: FilePath
  - solverArgs :: [String]
  - solverVerbose :: Int
  - solverPreludePath :: [FilePath]
  }
- defaultSolverConfig :: [FilePath] -> SolverConfig
- data NameSeeds
- nameSeeds :: NameSeeds
- data Error
  - = KindMismatch (Maybe TypeSource) Kind Kind
  - | TooManyTypeParams Int Kind
  - | TyVarWithParams
  - | TooManyTySynParams Name Int
  - | TooFewTyParams Name Int
  - | RecursiveTypeDecls [Name]
  - | TypeMismatch TypeSource Path Type Type
  - | SchemaMismatch Ident Schema Schema
  - | RecursiveType TypeSource Path Type Type
  - | UnsolvedGoals [Goal]
  - | UnsolvableGoals [Goal]
  - | UnsolvedDelayedCt DelayedCt
  - | UnexpectedTypeWildCard
  - | TypeVariableEscaped TypeSource Path Type [TParam]
  - | NotForAll TypeSource Path TVar Type
  - | TooManyPositionalTypeParams
  - | BadParameterKind TParam Kind
  - | CannotMixPositionalAndNamedTypeParams
  - | UndefinedTypeParameter (Located Ident)
  - | RepeatedTypeParameter Ident [Range]
  - | AmbiguousSize TVarInfo (Maybe Type)
  - | BareTypeApp
  - | UndefinedExistVar Name
  - | TypeShadowing String Name String
  - | MissingModTParam (Located Ident)
  - | MissingModVParam (Located Ident)
  - | MissingModParam Ident
  - | FunctorInstanceMissingArgument Ident
  - | FunctorInstanceBadArgument Ident
  - | FunctorInstanceMissingName Namespace Ident
  - | FunctorInstanceBadBacktick BadBacktickInstance
  - | UnsupportedFFIKind TypeSource TParam Kind
  - | UnsupportedFFIType TypeSource FFITypeError
  - | NestedConstraintGuard Ident
  - | DeclarationRequiresSignatureCtrGrd Ident
  - | InvalidConstraintGuard Prop
  - | TemporaryError Doc
- data Warning
  - = DefaultingKind (TParam Name) Kind
  - | DefaultingWildType Kind
  - | DefaultingTo !TVarInfo Type
  - | NonExhaustivePropGuards Name
- ppWarning :: (Range, Warning) -> Doc
- ppError :: (Range, Error) -> Doc
- data WithNames a = WithNames a NameMap
- type NameMap = IntMap String
- ppNamedWarning :: NameMap -> (Range, Warning) -> Doc
- ppNamedError :: NameMap -> (Range, Error) -> Doc

# Documentation

tcModule :: Module Name -> InferInput -> IO (InferOutput TCTopEntity) Source #

tcExpr :: Expr Name -> InferInput -> IO (InferOutput (Expr, Schema)) Source #

tcDecls :: [TopDecl Name] -> InferInput -> IO (InferOutput ([DeclGroup], Map Name TySyn)) Source #

data InferInput Source #

Information needed for type inference.

Constructors

InferInput |

Fields

- inpRange :: Range

  Location of program source

- inpVars :: Map Name Schema

  Variables that are in scope

- inpTSyns :: Map Name TySyn

  Type synonyms that are in scope

- inpNewtypes :: Map Name Newtype

  Newtypes in scope

- inpAbstractTypes :: Map Name AbstractType

  Abstract types in scope

- inpSignatures :: !(Map Name ModParamNames)

  Signatures in scope

- inpTopModules :: ModName -> Maybe (ModuleG (), IfaceG ())
- inpTopSignatures :: ModName -> Maybe ModParamNames
- inpParams :: !ModParamNames
- inpNameSeeds :: NameSeeds

  Private state of type-checker

- inpMonoBinds :: Bool

  Should local bindings without signatures be monomorphized?

- inpCallStacks :: Bool

  Are we tracking call stacks?

- inpSearchPath :: [FilePath]

  Where to look for Cryptol theory file.

- inpPrimNames :: !PrimMap

  This is used when the type-checker needs to refer to a predefined identifier (e.g., `number`).

- inpSupply :: !Supply

  The supply for fresh name generation

- inpSolver :: Solver

  Solver connection for typechecking

data InferOutput a Source #

The results of type inference.

Constructors

InferFailed NameMap [(Range, Warning)] [(Range, Error)] | We found some errors
InferOK NameMap [(Range, Warning)] NameSeeds Supply a | Type inference was successful.

#### Instances

Instances details

Show a => Show (InferOutput a) Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods showsPrec :: Int -> InferOutput a -> ShowS Source # show :: InferOutput a -> String Source # showList :: [InferOutput a] -> ShowS Source #

data SolverConfig Source #

Constructors

SolverConfig |

Fields

- solverPath :: FilePath

  The SMT solver to invoke

- solverArgs :: [String]

  Additional arguments to pass to the solver

- solverVerbose :: Int

  How verbose to be when type-checking

- solverPreludePath :: [FilePath]

  Look for the solver prelude in these locations.

#### Instances

Instances details

Generic SolverConfig Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Associated Types type Rep SolverConfig :: Type -> Type Source # Methods from :: SolverConfig -> Rep SolverConfig x Source # to :: Rep SolverConfig x -> SolverConfig Source #
Show SolverConfig Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> SolverConfig -> ShowS Source # show :: SolverConfig -> String Source # showList :: [SolverConfig] -> ShowS Source #
NFData SolverConfig Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: SolverConfig -> () Source #
type Rep SolverConfig Source # |

Instance details

Defined in Cryptol.TypeCheck.InferTypes

type Rep SolverConfig = D1 ('MetaData "SolverConfig" "Cryptol.TypeCheck.InferTypes" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "SolverConfig" 'PrefixI 'True) ((S1 ('MetaSel ('Just "solverPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "solverArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :*: (S1 ('MetaSel ('Just "solverVerbose") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "solverPreludePath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]))))

defaultSolverConfig :: [FilePath] -> SolverConfig Source #

A default configuration for using Z3, where the solver prelude is expected to be found in the given search path.

data NameSeeds Source #

This is used for generating various names.

#### Instances

Instances details

Generic NameSeeds Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Associated Types type Rep NameSeeds :: Type -> Type Source # Methods from :: NameSeeds -> Rep NameSeeds x Source # to :: Rep NameSeeds x -> NameSeeds Source #
Show NameSeeds Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods showsPrec :: Int -> NameSeeds -> ShowS Source # show :: NameSeeds -> String Source # showList :: [NameSeeds] -> ShowS Source #
NFData NameSeeds Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods rnf :: NameSeeds -> () Source #
type Rep NameSeeds Source # |

Instance details

Defined in Cryptol.TypeCheck.Monad

type Rep NameSeeds = D1 ('MetaData "NameSeeds" "Cryptol.TypeCheck.Monad" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "NameSeeds" 'PrefixI 'True) (S1 ('MetaSel ('Just "seedTVar") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "seedGoal") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

nameSeeds :: NameSeeds Source #

The initial seeds, used when checking a fresh program. XXX: why does this start at 10?

data Error Source #

Various errors that might happen during type checking/inference

Constructors

KindMismatch (Maybe TypeSource) Kind Kind | Expected kind, inferred kind
TooManyTypeParams Int Kind | Number of extra parameters, kind of result (which should not be of the form `_ -> _`)
TyVarWithParams | A type variable was applied to some arguments.
TooManyTySynParams Name Int | Type-synonym, number of extra params
TooFewTyParams Name Int | Who is missing params, number of missing params
RecursiveTypeDecls [Name] | The type synonym declarations are recursive
TypeMismatch TypeSource Path Type Type | Expected type, inferred type
SchemaMismatch Ident Schema Schema | Name of module parameter, expected scehema, actual schema. This may happen when instantiating modules.
RecursiveType TypeSource Path Type Type | Unification results in a recursive type
UnsolvedGoals [Goal] | A constraint that we could not solve, usually because there are some left-over variables that we could not infer.
UnsolvableGoals [Goal] | A constraint that we could not solve and we know it is impossible to do it.
UnsolvedDelayedCt DelayedCt | A constraint (with context) that we could not solve
UnexpectedTypeWildCard | Type wild cards are not allowed in this context (e.g., definitions of type synonyms).
TypeVariableEscaped TypeSource Path Type [TParam] | Unification variable depends on quantified variables that are not in scope.
NotForAll TypeSource Path TVar Type | Quantified type variables (of kind *) need to match the given type, so it does not work for all types.
TooManyPositionalTypeParams | Too many positional type arguments, in an explicit type instantiation
BadParameterKind TParam Kind | Kind other than `*` or `#` given to parameter of type synonym, newtype, function signature, etc.
CannotMixPositionalAndNamedTypeParams |
UndefinedTypeParameter (Located Ident) |
RepeatedTypeParameter Ident [Range] |
AmbiguousSize TVarInfo (Maybe Type) | Could not determine the value of a numeric type variable, but we know it must be at least as large as the given type (or unconstrained, if Nothing).
BareTypeApp | Bare expression of the form `{_}
UndefinedExistVar Name |
TypeShadowing String Name String |
MissingModTParam (Located Ident) |
MissingModVParam (Located Ident) |
MissingModParam Ident |
FunctorInstanceMissingArgument Ident |
FunctorInstanceBadArgument Ident |
FunctorInstanceMissingName Namespace Ident |
FunctorInstanceBadBacktick BadBacktickInstance |
UnsupportedFFIKind TypeSource TParam Kind | Kind is not supported for FFI
UnsupportedFFIType TypeSource FFITypeError | Type is not supported for FFI
NestedConstraintGuard Ident | Constraint guards may only apper at the top-level
DeclarationRequiresSignatureCtrGrd Ident | All declarataions in a recursive group involving constraint guards should have signatures
InvalidConstraintGuard Prop | The given constraint may not be used as a constraint guard
TemporaryError Doc | This is for errors that don't fit other cateogories. We should not use it much, and is generally to be used for transient errors, which are due to incomplete implementation.

#### Instances

Instances details

Generic Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Associated Types type Rep Error :: Type -> Type Source # Methods from :: Error -> Rep Error x Source # to :: Rep Error x -> Error Source #
Show Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods showsPrec :: Int -> Error -> ShowS Source # show :: Error -> String Source # showList :: [Error] -> ShowS Source #
TVars Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods apSubst :: Subst -> Error -> Error Source #
FVS Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Error -> Set TVar Source #
PP Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods ppPrec :: Int -> Error -> Doc Source #
NFData Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods rnf :: Error -> () Source #
PP (WithNames Error) Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods ppPrec :: Int -> WithNames Error -> Doc Source #
type Rep Error Source # |

Instance details

Defined in Cryptol.TypeCheck.Error

type Rep Error = D1 ('MetaData "Error" "Cryptol.TypeCheck.Error" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (((((C1 ('MetaCons "KindMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe TypeSource)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind))) :+: C1 ('MetaCons "TooManyTypeParams" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind))) :+: (C1 ('MetaCons "TyVarWithParams" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TooManyTySynParams" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))) :+: ((C1 ('MetaCons "TooFewTyParams" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "RecursiveTypeDecls" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))) :+: (C1 ('MetaCons "TypeMismatch" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSource) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Path)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: (C1 ('MetaCons "SchemaMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Schema) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Schema))) :+: C1 ('MetaCons "RecursiveType" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSource) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Path)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))))) :+: (((C1 ('MetaCons "UnsolvedGoals" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Goal])) :+: C1 ('MetaCons "UnsolvableGoals" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Goal]))) :+: (C1 ('MetaCons "UnsolvedDelayedCt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DelayedCt)) :+: C1 ('MetaCons "UnexpectedTypeWildCard" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TypeVariableEscaped" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSource) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Path)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam]))) :+: C1 ('MetaCons "NotForAll" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSource) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Path)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVar) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) :+: (C1 ('MetaCons "TooManyPositionalTypeParams" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BadParameterKind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TParam) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :+: C1 ('MetaCons "CannotMixPositionalAndNamedTypeParams" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "UndefinedTypeParameter" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Ident))) :+: C1 ('MetaCons "RepeatedTypeParameter" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Range]))) :+: (C1 ('MetaCons "AmbiguousSize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVarInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Type))) :+: C1 ('MetaCons "BareTypeApp" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UndefinedExistVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "TypeShadowing" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))) :+: (C1 ('MetaCons "MissingModTParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Ident))) :+: (C1 ('MetaCons "MissingModVParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Ident))) :+: C1 ('MetaCons "MissingModParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)))))) :+: (((C1 ('MetaCons "FunctorInstanceMissingArgument" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)) :+: C1 ('MetaCons "FunctorInstanceBadArgument" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident))) :+: (C1 ('MetaCons "FunctorInstanceMissingName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Namespace) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)) :+: (C1 ('MetaCons "FunctorInstanceBadBacktick" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BadBacktickInstance)) :+: C1 ('MetaCons "UnsupportedFFIKind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSource) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TParam) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)))))) :+: ((C1 ('MetaCons "UnsupportedFFIType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSource) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFITypeError)) :+: C1 ('MetaCons "NestedConstraintGuard" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident))) :+: (C1 ('MetaCons "DeclarationRequiresSignatureCtrGrd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)) :+: (C1 ('MetaCons "InvalidConstraintGuard" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Prop)) :+: C1 ('MetaCons "TemporaryError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Doc))))))))

data Warning Source #

Constructors

DefaultingKind (TParam Name) Kind |
DefaultingWildType Kind |
DefaultingTo !TVarInfo Type |
NonExhaustivePropGuards Name |

#### Instances

Instances details

Generic Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Associated Types type Rep Warning :: Type -> Type Source # Methods from :: Warning -> Rep Warning x Source # to :: Rep Warning x -> Warning Source #
Show Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods showsPrec :: Int -> Warning -> ShowS Source # show :: Warning -> String Source # showList :: [Warning] -> ShowS Source #
TVars Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods apSubst :: Subst -> Warning -> Warning Source #
FVS Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Warning -> Set TVar Source #
PP Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods ppPrec :: Int -> Warning -> Doc Source #
NFData Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods rnf :: Warning -> () Source #
PP (WithNames Warning) Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods ppPrec :: Int -> WithNames Warning -> Doc Source #
type Rep Warning Source # |

Instance details

Defined in Cryptol.TypeCheck.Error

type Rep Warning = D1 ('MetaData "Warning" "Cryptol.TypeCheck.Error" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) ((C1 ('MetaCons "DefaultingKind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TParam Name)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :+: C1 ('MetaCons "DefaultingWildType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind))) :+: (C1 ('MetaCons "DefaultingTo" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TVarInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "NonExhaustivePropGuards" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))))

ppWarning :: (Range, Warning) -> Doc Source #

ppError :: (Range, Error) -> Doc Source #

data WithNames a Source #

This packages together a type with some names to be used to display the variables. It is used for pretty printing types.

Constructors

WithNames a NameMap |

#### Instances

Instances details

PP (WithNames Decl) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames Decl -> Doc Source #
PP (WithNames DeclDef) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames DeclDef -> Doc Source #
PP (WithNames DeclGroup) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames DeclGroup -> Doc Source #
PP (WithNames Expr) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames Expr -> Doc Source #
PP (WithNames Match) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames Match -> Doc Source #
PP n => PP (WithNames (ModuleG n)) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames (ModuleG n) -> Doc Source #
PP (WithNames TCTopEntity) Source # |
Instance details Defined in Cryptol.TypeCheck.AST Methods ppPrec :: Int -> WithNames TCTopEntity -> Doc Source #
PP (WithNames Error) Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods ppPrec :: Int -> WithNames Error -> Doc Source #
PP (WithNames Warning) Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods ppPrec :: Int -> WithNames Warning -> Doc Source #
PP (WithNames FFITypeError) Source # |
Instance details Defined in Cryptol.TypeCheck.FFI.Error Methods ppPrec :: Int -> WithNames FFITypeError -> Doc Source #
PP (WithNames FFITypeErrorReason) Source # |
Instance details Defined in Cryptol.TypeCheck.FFI.Error Methods ppPrec :: Int -> WithNames FFITypeErrorReason -> Doc Source #
PP (WithNames DelayedCt) Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods ppPrec :: Int -> WithNames DelayedCt -> Doc Source #
PP (WithNames Goal) Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods ppPrec :: Int -> WithNames Goal -> Doc Source #
PP (WithNames Subst) Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods ppPrec :: Int -> WithNames Subst -> Doc Source #
PP (WithNames Newtype) Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames Newtype -> Doc Source #
PP (WithNames Schema) Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames Schema -> Doc Source #
PP (WithNames TParam) Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TParam -> Doc Source #
PP (WithNames TVar) Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TVar -> Doc Source #
PP (WithNames TySyn) Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TySyn -> Doc Source #

PP (WithNames Type) Source #

The precedence levels used by this pretty-printing instance correspond with parser non-terminals as follows:

- 0-1: `type`
- 2: `infix_type`
- 3: `app_type`
- 4: `dimensions atype`
- 5: `atype`

Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames Type -> Doc Source #

type NameMap = IntMap String Source #

ppNamedWarning :: NameMap -> (Range, Warning) -> Doc Source #

ppNamedError :: NameMap -> (Range, Error) -> Doc Source #