HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Internal.Blockers

  • 4 types
  • 30 values
  • PackageAgda-2.7.0.1
  • Exports34
  • LanguageHaskell2010
  • LicenceMIT
  • SourceBlockers.hs

Blocked Terms

19 declarations
datadata NotBlocked' t
#

Even if we are not stuck on a meta during reduction we can fail to reduce a definition by pattern matching for another reason.

Constructors

  • StuckOn (Elim' t)

    The Elim is neutral and blocks a pattern match.

  • Underapplied

    Not enough arguments were supplied to complete the matching.

  • AbsurdMatch

    We matched an absurd clause, results in a neutral Def.

  • MissingClauses QName

    We ran out of clauses for QName, all considered clauses produced an actual mismatch. This can happen when try to reduce a function application but we are still missing some function clauses. See Agda.TypeChecking.Patterns.Match.

  • ReallyNotBlocked

    Reduction was not blocked, we reached a whnf which can be anything but a stuck Def.

Instances9Eq, EmbPrj, Show, Generic, Semigroup, Monoid, …
datadata Blocker
#

What is causing the blocking? Or in other words which metas or problems need to be solved to unblock the blocked computation/constraint.

Constructors

Instances13Eq, Ord, Show, Generic, NFData, Pretty, …
datadata Blocked' t a
#

Something where a meta variable may block reduction. Notably a top-level meta is considered blocking. This did not use to be the case (pre Aug 2020).

Constructors

Instances22EmbPrj, MonadError, Eq, Functor, Applicative, Foldable, …
valuestuckOn :: Elim' t -> NotBlocked' t -> NotBlocked' t
#

When trying to reduce f es, on match failed on one elimination e ∈ es that came with info r :: NotBlocked. stuckOn e r produces the new NotBlocked info.

MissingClauses must be propagated, as this is blockage that can be lifted in the future (as more clauses are added).

StuckOn e0 is also propagated, since it provides more precise information as StuckOn e (as e0 is the original reason why reduction got stuck and usually a subterm of e). An information like StuckOn (Apply (Arg info (Var i []))) (stuck on a variable) could be used by the lhs/coverage checker to trigger a split on that (pattern) variable.

In the remaining cases for r, we are terminally stuck due to StuckOn e. Propagating AbsurdMatch does not seem useful.

Underapplied must not be propagated, as this would mean that f es is underapplied, which is not the case (it is stuck). Note that Underapplied can only arise when projection patterns were missing to complete the original match (in e). (Missing ordinary pattern would mean the e is of function type, but we cannot match against something of function type.)

Handling blocked terms.

6 declarations

Waking up logic

9 declarations
datadata WakeUp
#

Should a constraint wake up or not? If not, we might refine the unblocker.

Constructors

Instances2Eq, Show
  • Eq WakeUpDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Blockers
  • Show WakeUpDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Blockers