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

GHC 9.14.1 · lts/ghc-9.14.x · 45dd537 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.LevelConstraints

  • 1 value
  • PackageAgda-2.8.0.2
  • Exports1
  • LanguageHaskell2010
  • LicenceMIT
  • SourceLevelConstraints.hs
valuesimplifyLevelConstraint
  1. :: Constraint

    Constraint c to simplify.

  2. -> List1 Constraint

    Other constraints, enable simplification.

  3. -> Maybe [Constraint]

    Just: list of constraints equal to the original c. Nothing: no simplification possible.

#

simplifyLevelConstraint c cs turns an c into an equality constraint if it is an inequality constraint and the reverse inequality is contained in cs.

The constraints don't necessarily have to live in the same context, but they do need to be universally quanitfied over the context. This function takes care of renaming variables when checking for matches.