Cryptol.TypeCheck.Instantiate

Documentation

instantiateWith :: Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Type)

data TypeArg

Constructors

TypeArg

Fields

• tyArgName :: Maybe (Located Ident)
• tyArgType :: MaybeCheckedType

uncheckedTypeArg :: TypeInst Name -> TypeArg

data MaybeCheckedType

Constructors

Checked Type

Unchecked (Type Name)

instantiatePCon :: Name -> InferM ([Type], Int, [Type], Type)

Instantiate a pattern constructor. Returns (A,B,C,D) where: A) are the instantiations of the type parameters of the constructor B) is how many proofs we would have if we had dictionaries C) are the types of the fields of the constructor D) is the type of the result of the constructor (i.e., what we are mathcing)