:: a typeCtrl KGHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05
ModuleAgda-2.7.0.1Haskell2010
checkArguments cmp exph r args t0 t k tries checkArgumentsE exph 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 := ((_ : t0) args) : t.
checkArguments_ :: ComparisonComparison for target
-> ExpandHiddenEagerly insert trailing hidden arguments?
-> RangeRange of application.
-> [NamedArg Expr]Arguments to check.
-> TelescopeTelescope 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 hd args e t checks an application.
Precondition: Application hs args = appView e
checkApplication disambiguates constructors
(and continues to checkConstructorApplication)
and resolves pattern synonyms.
Precondition: Application hd args = appView e.
Checking the type of an overloaded projection application.
See inferOrCheckProjAppToKnownPrincipalArg.