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

Cryptol.TypeCheck.Instantiate

Description

Synopsis

instantiateWith :: Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Type)
data TypeArg = TypeArg {
- tyArgName :: Maybe (Located Ident)
- tyArgType :: MaybeCheckedType
}
uncheckedTypeArg :: TypeInst Name -> TypeArg
data MaybeCheckedType
- = Checked Type
- | Unchecked (Type Name)
instantiatePCon :: Name -> InferM ([Type], Int, [Type], Type)

Documentation

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

data TypeArg Source #

Constructors

TypeArg
Fields tyArgName :: Maybe (Located Ident) tyArgType :: MaybeCheckedType

uncheckedTypeArg :: TypeInst Name -> TypeArg Source #

data MaybeCheckedType Source #

Constructors

Checked Type
Unchecked (Type Name)

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

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)