| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.TypeChecking.Opacity
Synopsis
- saturateOpaqueBlocks :: (MonadTCState m, MonadFresh OpaqueId m, MonadTrace m, MonadWarning m, MonadIO m) => m ()
- isAccessibleDef :: TCEnv -> TCState -> Definition -> Bool
- hasAccessibleDef :: (ReadTCState m, HasConstInfo m) => QName -> m Bool
- canSolveMetaOpaquely :: MetaInfo -> Teletype -> TCM Bool
Documentation
saturateOpaqueBlocks :: (MonadTCState m, MonadFresh OpaqueId m, MonadTrace m, MonadWarning m, MonadIO m) => m () Source #
Ensure that opaque blocks defined in the current module have saturated unfolding sets.
isAccessibleDef :: TCEnv -> TCState -> Definition -> Bool Source #
Decide whether or not a definition is reducible. Returns True if
the definition can step.
hasAccessibleDef :: (ReadTCState m, HasConstInfo m) => QName -> m Bool Source #
Will the given QName have a proper definition, or will it be
wrapped in an AbstractDefn?
canSolveMetaOpaquely :: MetaInfo -> Teletype -> TCM Bool Source #
Check whether a metavariable with the given MetaInfo, and of the
given Teletype, can be solved in the current environment, without
risking "information leakage" from a difference in the abstractness
and/or opacity of the environment vs. that of the metavariable.
This is a conservative check. A True result indicates that both
contexts have sufficiently similar reducibility that nothing untoward
can happen, but a False result only indicates that care must be
taken.