| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.TypeChecking.Rules.Application
Synopsis
- data AppHead
- type ArgsCheck = ArgRanges -> Elims -> Type -> TCM Elims
- type ArgRanges = [Range]
- checkArguments :: Comparison -> ExpandHidden -> Expr -> [NamedArg Expr] -> Type -> Type -> (ArgsCheckState CheckedTarget -> TCM Term) -> TCM Term
- checkArguments_ :: Comparison -> ExpandHidden -> Expr -> [NamedArg Expr] -> Telescope -> TCM (Elims, Telescope)
- checkApplication :: Comparison -> Expr -> Args -> Expr -> Type -> TCM Term
- inferApplication :: ExpandHidden -> Expr -> Args -> Expr -> TCM (Term, Type)
- checkProjAppToKnownPrincipalArg :: Comparison -> Expr -> ProjOrigin -> AmbiguousQName -> Expr -> Args -> Type -> Int -> Term -> Type -> PrincipalArgTypeMetas -> TCM Term
- disambiguateConstructor' :: ConstructorDisambiguationData -> (ConHead -> TCM Term) -> TCM Term
- univChecks :: Univ -> TCM ()
- suffixToLevel :: Suffix -> Integer
- coerce' :: Comparison -> CheckedTarget -> Term -> Type -> Type -> TCM Term
Documentation
Something that can appear as the head of an elimination spine in abstract syntax.
Constructors
| TermAppHd Term | A head term that has already been elaborated, and does not impose any constraints on the shape of its arguments. Used for metavariables, which are already applied to their context, but may be of function type; and for the known-good argument that was used to disambiguate an overloaded projection, which may receive further arguments. |
| ConAppHd !ConHead !Int | A constructor with the given number of parameters. |
| PrimAppHd !QName !ArgsCheck | A bound primitive which imposes extra checks on its argument
spine. In this case, the eliminations given must all be |
Arguments
| :: Comparison | How the inferred type should be compared to the expected result type. |
| -> ExpandHidden | Insert trailing hidden arguments? |
| -> Expr | The function (a head). |
| -> [NamedArg Expr] | The arguments to check. |
| -> Type | Type of the function. |
| -> Type | Expected result type (type of the whole application). |
| -> (ArgsCheckState CheckedTarget -> TCM Term) | Continuation receiving the check arguments. |
| -> TCM Term |
checkArguments cmp exph hd args t0 t k tries checkArgumentsE cmp exph hd args t0 t.
If it succeeds, it continues k with the returned results. If it fails,
it registers a postponed typechecking problem and returns the resulting new
meta variable.
Checks e := ((hd : t0) args) : t.
Arguments
| :: Comparison | Comparison for target |
| -> ExpandHidden | Eagerly insert trailing hidden arguments? |
| -> Expr | Function. |
| -> [NamedArg Expr] | Arguments to check. |
| -> Telescope | Telescope to check arguments against. |
| -> TCM (Elims, Telescope) | Checked arguments and remaining telescope if successful. |
Check that a list of arguments fits a telescope. Inserts hidden arguments as necessary. Returns the type-checked arguments and the remaining telescope.
checkApplication :: Comparison -> Expr -> Args -> Expr -> Type -> TCM Term Source #
checkApplication hd args e t checks an application.
Precondition: Application hs args = appView e
checkApplication disambiguates constructors
(and continues to checkConstructorApplication)
and resolves pattern synonyms.
inferApplication :: ExpandHidden -> Expr -> Args -> Expr -> TCM (Term, Type) Source #
Precondition: Application hd args = appView e.
checkProjAppToKnownPrincipalArg :: Comparison -> Expr -> ProjOrigin -> AmbiguousQName -> Expr -> Args -> Type -> Int -> Term -> Type -> PrincipalArgTypeMetas -> TCM Term Source #
Checking the type of an overloaded projection application.
See inferOrCheckProjAppToKnownPrincipalArg.
disambiguateConstructor' :: ConstructorDisambiguationData -> (ConHead -> TCM Term) -> TCM Term Source #
Retry a constructor disambiguation.
univChecks :: Univ -> TCM () Source #
suffixToLevel :: Suffix -> Integer Source #
coerce' :: Comparison -> CheckedTarget -> Term -> Type -> Type -> TCM Term Source #
If we've already checked the target type we don't have to call coerce.