HORIZON HASKELLDocslts/ghc-10.0.x8174fa42026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 8174fa4 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Rules.Application

  • 8 values
  • PackageAgda-2.8.0.2
  • Exports8
  • LanguageHaskell2010
  • LicenceMIT
  • SourceApplication.hs
valuecheckArguments
  1. :: Comparison

    How the inferred type should be compared to the expected result type.

  2. -> ExpandHidden

    Insert trailing hidden arguments?

  3. -> Expr

    The function (a head).

  4. -> [NamedArg Expr]

    The arguments to check.

  5. -> Type

    Type of the function.

  6. -> Type

    Expected result type (type of the whole application).

  7. -> (ArgsCheckState CheckedTarget -> TCM Term)

    Continuation receiving the check arguments.

  8. -> 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.

valuecheckArguments_
  1. :: Comparison

    Comparison for target

  2. -> ExpandHidden

    Eagerly insert trailing hidden arguments?

  3. -> Expr

    Function.

  4. -> [NamedArg Expr]

    Arguments to check.

  5. -> Telescope

    Telescope to check arguments against.

  6. -> 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.

valuecheckApplication :: Comparison -> Expr -> Args -> Expr -> Type -> TCM Term
#

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.