| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
UntypedPlutusCore.Check.Scope
Synopsis
- checkScope ∷ ∀ e m name uni fun a. (HasIndex name, MonadError e m, AsFreeVariableError e) ⇒ Term name uni fun a → m ()
Documentation
checkScope ∷ ∀ e m name uni fun a. (HasIndex name, MonadError e m, AsFreeVariableError e) ⇒ Term name uni fun a → m () Source #
A pass to check that the input term: 1) does not contain free variables and 2) that all binders are set to debruijn index 0.
Feeding the result of the debruijnification to this function is expected to pass.
On the other hand, because of (2), this pass is stricter than the undebruijnification's (indirect) scope-checking, see Note [DeBruijn indices of Binders].
Inlining this function makes a big difference, since it will usually be called in a context where all the type variables are known. That then means that GHC can optimize go locally in a completely monomorphic setting, which helps a lot.