cryptol-2.4.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
Language | Haskell98

Cryptol.TypeCheck.InferTypes

Description

This module contains types used during type inference.

Synopsis

- data SolverConfig = SolverConfig {
  - solverPath :: FilePath
  - solverArgs :: [String]
  - solverVerbose :: Int
  }
- data VarType
  - = ExtVar Schema
  - | CurSCC Expr Type
- newtype Goals = Goals (TypeMap Goal)
- emptyGoals :: Goals
- nullGoals :: Goals -> Bool
- fromGoals :: Goals -> [Goal]
- insertGoal :: Goal -> Goals -> Goals
- data Goal = Goal {
  - goalSource :: ConstraintSource
  - goalRange :: Range
  - goal :: Prop
  }
- data HasGoal = HasGoal {
  - hasName :: !Int
  - hasGoal :: Goal
  }
- data DelayedCt = DelayedCt {
  - dctSource :: Name
  - dctForall :: [TParam]
  - dctAsmps :: [Prop]
  - dctGoals :: [Goal]
  }
- data Solved
  - = Solved (Maybe Subst) [Goal]
  - | Unsolved
  - | Unsolvable
- data Warning
  - = DefaultingKind (TParam Name) Kind
  - | DefaultingWildType Kind
  - | DefaultingTo Doc Type
- data Error
  - = ErrorMsg Doc
  - | KindMismatch Kind Kind
  - | TooManyTypeParams Int Kind
  - | TooManyTySynParams Name Int
  - | TooFewTySynParams Name Int
  - | RepeatedTyParams [TParam Name]
  - | RepeatedDefinitions Name [Range]
  - | RecursiveTypeDecls [Name]
  - | UndefinedTypeSynonym Name
  - | UndefinedVariable Name
  - | UndefinedTypeParam (Located Ident)
  - | MultipleTypeParamDefs Ident [Range]
  - | TypeMismatch Type Type
  - | RecursiveType Type Type
  - | UnsolvedGoal Bool Goal
  - | UnsolvedDelayedCt DelayedCt
  - | UnexpectedTypeWildCard
  - | TypeVariableEscaped Type [TVar]
  - | NotForAll TVar Type
  - | UnusableFunction Name [Prop]
  - | TooManyPositionalTypeParams
  - | CannotMixPositionalAndNamedTypeParams
  - | AmbiguousType [Name]
- data ConstraintSource
  - = CtComprehension
  - | CtSplitPat
  - | CtTypeSig
  - | CtInst Expr
  - | CtSelector
  - | CtExactType
  - | CtEnumeration
  - | CtDefaulting
  - | CtPartialTypeFun TyFunName
  - | CtImprovement
  - | CtPattern Doc
- data TyFunName
  - = UserTyFun Name
  - | BuiltInTyFun TFun
- cppKind :: Kind -> Doc
- addTVarsDescs :: FVS t => NameMap -> t -> Doc -> Doc
- ppUse :: Expr -> Doc

# Documentation

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

Instances

Show SolverConfig Source # |
Methods showsPrec :: Int -> SolverConfig -> ShowS # show :: SolverConfig -> String # showList :: [SolverConfig] -> ShowS #
Generic SolverConfig Source # |
Associated Types type Rep SolverConfig :: * -> * # Methods from :: SolverConfig -> Rep SolverConfig x # to :: Rep SolverConfig x -> SolverConfig #
NFData SolverConfig Source # |
Methods rnf :: SolverConfig -> () #
type Rep SolverConfig Source # |

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

data VarType Source #

The types of variables in the environment.

Constructors

ExtVar Schema | Known type
CurSCC Expr Type | Part of current SCC

newtype Goals Source #

Constructors

Goals (TypeMap Goal) |

Instances

Show Goals Source # |
Methods showsPrec :: Int -> Goals -> ShowS # show :: Goals -> String # showList :: [Goals] -> ShowS #
TVars Goals Source # |
Methods apSubst :: Subst -> Goals -> Goals Source #

emptyGoals :: Goals Source #

nullGoals :: Goals -> Bool Source #

fromGoals :: Goals -> [Goal] Source #

insertGoal :: Goal -> Goals -> Goals Source #

data Goal Source #

Something that we need to find evidence for.

Constructors

Goal |

Fields

- goalSource :: ConstraintSource

  What it is about

- goalRange :: Range

  Part of source code that caused goal

- goal :: Prop

  What needs to be proved

Instances

Show Goal Source # |
Methods showsPrec :: Int -> Goal -> ShowS # show :: Goal -> String # showList :: [Goal] -> ShowS #
Generic Goal Source # |
Associated Types type Rep Goal :: * -> * # Methods from :: Goal -> Rep Goal x # to :: Rep Goal x -> Goal #
NFData Goal Source # |
Methods rnf :: Goal -> () #
TVars Goal Source # |
Methods apSubst :: Subst -> Goal -> Goal Source #
FVS Goal Source # |
Methods fvs :: Goal -> Set TVar Source #
DebugLog Goal Source # |
Methods debugLog :: Solver -> Goal -> IO () Source # debugLogList :: Solver -> [Goal] -> IO () Source #
PP (WithNames Goal) Source # |
Methods ppPrec :: Int -> WithNames Goal -> Doc Source #
type Rep Goal Source # |

type Rep Goal = D1 (MetaData "Goal" "Cryptol.TypeCheck.InferTypes" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "Goal" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "goalSource") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ConstraintSource)) ((:*:) (S1 (MetaSel (Just Symbol "goalRange") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range)) (S1 (MetaSel (Just Symbol "goal") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Prop)))))

data HasGoal Source #

Constructors

HasGoal |

Fields

- hasName :: !Int
- hasGoal :: Goal

Instances

Show HasGoal Source # |
Methods showsPrec :: Int -> HasGoal -> ShowS # show :: HasGoal -> String # showList :: [HasGoal] -> ShowS #
TVars HasGoal Source # |
Methods apSubst :: Subst -> HasGoal -> HasGoal Source #

data DelayedCt Source #

Delayed implication constraints, arising from user-specified type sigs.

Constructors

DelayedCt |

Fields

- dctSource :: Name

  Signature that gave rise to this constraint

- dctForall :: [TParam]
- dctAsmps :: [Prop]
- dctGoals :: [Goal]

Instances

Show DelayedCt Source # |
Methods showsPrec :: Int -> DelayedCt -> ShowS # show :: DelayedCt -> String # showList :: [DelayedCt] -> ShowS #
Generic DelayedCt Source # |
Associated Types type Rep DelayedCt :: * -> * # Methods from :: DelayedCt -> Rep DelayedCt x # to :: Rep DelayedCt x -> DelayedCt #
NFData DelayedCt Source # |
Methods rnf :: DelayedCt -> () #
TVars DelayedCt Source # |
Methods apSubst :: Subst -> DelayedCt -> DelayedCt Source #
FVS DelayedCt Source # |
Methods fvs :: DelayedCt -> Set TVar Source #
PP (WithNames DelayedCt) Source # |
Methods ppPrec :: Int -> WithNames DelayedCt -> Doc Source #
type Rep DelayedCt Source # |

type Rep DelayedCt = D1 (MetaData "DelayedCt" "Cryptol.TypeCheck.InferTypes" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "DelayedCt" PrefixI True) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "dctSource") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Just Symbol "dctForall") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TParam]))) ((:*:) (S1 (MetaSel (Just Symbol "dctAsmps") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop])) (S1 (MetaSel (Just Symbol "dctGoals") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Goal])))))

data Solved Source #

Constructors

Solved (Maybe Subst) [Goal] | Solved, assuming the sub-goals.
Unsolved | We could not solve the goal.
Unsolvable | The goal can never be solved.

Instances

Show Solved Source # |
Methods showsPrec :: Int -> Solved -> ShowS # show :: Solved -> String # showList :: [Solved] -> ShowS #
PP Solved Source # |
Methods ppPrec :: Int -> Solved -> Doc Source #

data Warning Source #

Constructors

DefaultingKind (TParam Name) Kind |
DefaultingWildType Kind |
DefaultingTo Doc Type |

Instances

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

type Rep Warning = D1 (MetaData "Warning" "Cryptol.TypeCheck.InferTypes" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "DefaultingKind" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TParam Name))) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)))) ((:+:) (C1 (MetaCons "DefaultingWildType" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind))) (C1 (MetaCons "DefaultingTo" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Doc)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type))))))

data Error Source #

Various errors that might happen during type checking/inference

Constructors

ErrorMsg Doc | Just say this
KindMismatch Kind Kind | Expected kind, inferred kind
TooManyTypeParams Int Kind | Number of extra parameters, kind of result (which should not be of the form `_ -> _`)
TooManyTySynParams Name Int | Type-synonym, number of extra params
TooFewTySynParams Name Int | Type-synonym, number of missing params
RepeatedTyParams [TParam Name] | Type parameters with the same name (in definition)
RepeatedDefinitions Name [Range] | Multiple definitions for the same name
RecursiveTypeDecls [Name] | The type synonym declarations are recursive
UndefinedTypeSynonym Name | Use of a type synonym that was not defined
UndefinedVariable Name | Use of a variable that was not defined
UndefinedTypeParam (Located Ident) | Attempt to explicitly instantiate a non-existent param.
MultipleTypeParamDefs Ident [Range] | Multiple definitions for the same type parameter
TypeMismatch Type Type | Expected type, inferred type
RecursiveType Type Type | Unification results in a recursive type
UnsolvedGoal Bool Goal | A constraint that we could not solve The boolean indicates if we know that this constraint is impossible.
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 Type [TVar] | Unification variable depends on quantified variables that are not in scope.
NotForAll TVar Type | Quantified type variables (of kind *) need to match the given type, so it does not work for all types.
UnusableFunction Name [Prop] | The given constraints causes the signature of the function to be not-satisfiable.
TooManyPositionalTypeParams | Too many positional type arguments, in an explicit type instantiation
CannotMixPositionalAndNamedTypeParams |
AmbiguousType [Name] |

Instances

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

type Rep Error = D1 (MetaData "Error" "Cryptol.TypeCheck.InferTypes" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "ErrorMsg" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Doc))) (C1 (MetaCons "KindMismatch" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind))))) ((:+:) (C1 (MetaCons "TooManyTypeParams" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)))) ((:+:) (C1 (MetaCons "TooManyTySynParams" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)))) (C1 (MetaCons "TooFewTySynParams" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))))))) ((:+:) ((:+:) (C1 (MetaCons "RepeatedTyParams" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TParam Name]))) ((:+:) (C1 (MetaCons "RepeatedDefinitions" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Range])))) (C1 (MetaCons "RecursiveTypeDecls" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]))))) ((:+:) (C1 (MetaCons "UndefinedTypeSynonym" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) ((:+:) (C1 (MetaCons "UndefinedVariable" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) (C1 (MetaCons "UndefinedTypeParam" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Located Ident)))))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "MultipleTypeParamDefs" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Ident)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Range])))) ((:+:) (C1 (MetaCons "TypeMismatch" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))) (C1 (MetaCons "RecursiveType" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))))) ((:+:) (C1 (MetaCons "UnsolvedGoal" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Goal)))) ((:+:) (C1 (MetaCons "UnsolvedDelayedCt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 DelayedCt))) (C1 (MetaCons "UnexpectedTypeWildCard" PrefixI False) U1)))) ((:+:) ((:+:) (C1 (MetaCons "TypeVariableEscaped" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TVar])))) ((:+:) (C1 (MetaCons "NotForAll" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TVar)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))) (C1 (MetaCons "UnusableFunction" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop])))))) ((:+:) (C1 (MetaCons "TooManyPositionalTypeParams" PrefixI False) U1) ((:+:) (C1 (MetaCons "CannotMixPositionalAndNamedTypeParams" PrefixI False) U1) (C1 (MetaCons "AmbiguousType" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]))))))))

data ConstraintSource Source #

Information about how a constraint came to be, used in error reporting.

Constructors

CtComprehension | Computing shape of list comprehension
CtSplitPat | Use of a split pattern
CtTypeSig | A type signature in a pattern or expression
CtInst Expr | Instantiation of this expression
CtSelector |
CtExactType |
CtEnumeration |
CtDefaulting | Just defaulting on the command line
CtPartialTypeFun TyFunName | Use of a partial type function.
CtImprovement |
CtPattern Doc | Constraints arising from type-checking patterns

Instances

Show ConstraintSource Source # |
Methods showsPrec :: Int -> ConstraintSource -> ShowS # show :: ConstraintSource -> String # showList :: [ConstraintSource] -> ShowS #
Generic ConstraintSource Source # |
Associated Types type Rep ConstraintSource :: * -> * # Methods from :: ConstraintSource -> Rep ConstraintSource x # to :: Rep ConstraintSource x -> ConstraintSource #
NFData ConstraintSource Source # |
Methods rnf :: ConstraintSource -> () #
PP ConstraintSource Source # |
Methods ppPrec :: Int -> ConstraintSource -> Doc Source #
TVars ConstraintSource Source # |
Methods apSubst :: Subst -> ConstraintSource -> ConstraintSource Source #
type Rep ConstraintSource Source # |

type Rep ConstraintSource = D1 (MetaData "ConstraintSource" "Cryptol.TypeCheck.InferTypes" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "CtComprehension" PrefixI False) U1) (C1 (MetaCons "CtSplitPat" PrefixI False) U1)) ((:+:) (C1 (MetaCons "CtTypeSig" PrefixI False) U1) ((:+:) (C1 (MetaCons "CtInst" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Expr))) (C1 (MetaCons "CtSelector" PrefixI False) U1)))) ((:+:) ((:+:) (C1 (MetaCons "CtExactType" PrefixI False) U1) ((:+:) (C1 (MetaCons "CtEnumeration" PrefixI False) U1) (C1 (MetaCons "CtDefaulting" PrefixI False) U1))) ((:+:) (C1 (MetaCons "CtPartialTypeFun" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TyFunName))) ((:+:) (C1 (MetaCons "CtImprovement" PrefixI False) U1) (C1 (MetaCons "CtPattern" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Doc)))))))

data TyFunName Source #

Constructors

UserTyFun Name |
BuiltInTyFun TFun |

Instances

Show TyFunName Source # |
Methods showsPrec :: Int -> TyFunName -> ShowS # show :: TyFunName -> String # showList :: [TyFunName] -> ShowS #
Generic TyFunName Source # |
Associated Types type Rep TyFunName :: * -> * # Methods from :: TyFunName -> Rep TyFunName x # to :: Rep TyFunName x -> TyFunName #
NFData TyFunName Source # |
Methods rnf :: TyFunName -> () #
PP TyFunName Source # |
Methods ppPrec :: Int -> TyFunName -> Doc Source #
type Rep TyFunName Source # |

type Rep TyFunName = D1 (MetaData "TyFunName" "Cryptol.TypeCheck.InferTypes" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "UserTyFun" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) (C1 (MetaCons "BuiltInTyFun" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TFun))))

cppKind :: Kind -> Doc Source #

For use in error messages

addTVarsDescs :: FVS t => NameMap -> t -> Doc -> Doc Source #

ppUse :: Expr -> Doc Source #