{-# LANGUAGE NondecreasingIndentation #-}
module Mikan.TypeChecking.Opacity
  ( saturateOpaqueBlocks

  , isAccessibleDef
  , hasAccessibleDef

  , canSolveMetaOpaquely
  )
  where

import Control.Monad.State
import Control.Exception
import Control.DeepSeq
import Control.Monad

import Data.HashMap.Strict qualified as HashMap
import Data.Map.Strict qualified as Map
import Data.HashSet qualified as HashSet
import Data.List qualified as List
import Data.HashMap.Strict (HashMap)
import Data.HashSet (HashSet)
import Data.Map.Strict (Map)
import Data.Foldable
import Data.Monoid
import Data.Maybe

import Mikan.Syntax.Internal.Names
import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Internal
import Mikan.Syntax.Position
import Mikan.Syntax.Common

import Mikan.TypeChecking.Warnings
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Monad

import Mikan.Utils.Impossible
import Mikan.Utils.Lens
import Mikan.Utils.List
import Mikan.Utils.Monad

-- | Ensure that opaque blocks defined in the current module have
-- saturated unfolding sets.
saturateOpaqueBlocks
  :: forall m. (MonadTCState m, MonadFresh OpaqueId m, MonadTrace m, MonadWarning m, MonadIO m)
  => m ()
saturateOpaqueBlocks :: forall (m :: * -> *).
(MonadTCState m, MonadFresh OpaqueId m, MonadTrace m,
 MonadWarning m, MonadIO m) =>
m ()
saturateOpaqueBlocks = m ()
entry where
  entry :: m ()
entry = do
    known   <- Getter TCState (Map OpaqueId OpaqueBlock)
-> m (Map OpaqueId OpaqueBlock)
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (Map OpaqueId OpaqueBlock -> f (Map OpaqueId OpaqueBlock))
-> TCState -> f TCState
Lens' TCState (Map OpaqueId OpaqueBlock)
Getter TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks
    inverse <- useTC stOpaqueIds
    OpaqueId _ ourmod <- fresh

    canonical  <- useTC stCopiedNames
    backcopies <- useTC stNameCopies

    reportSDoc "tc.opaque.copy" 45 $ "Canonical names of copied definitions:" $+$ pretty (HashMap.toList canonical <&> fmap snd)
    reportSDoc "tc.opaque.copy" 45 $ "Backcopies:" $+$ pretty (HashMap.toList (toList <$> backcopies))

    let
      isOurs (OpaqueId Word64
_ ModuleNameHash
mod, OpaqueBlock
_) = ModuleNameHash
mod ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleNameHash
ourmod
      canonise QName
name = QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
name (QName
-> HashMap QName (ScopeCopyRef, QName)
-> Maybe (ScopeCopyRef, QName)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup QName
name HashMap QName (ScopeCopyRef, QName)
canonical Maybe (ScopeCopyRef, QName)
-> ((ScopeCopyRef, QName) -> QName) -> Maybe QName
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (ScopeCopyRef, QName) -> QName
forall a b. (a, b) -> b
snd)
      ours = (OpaqueId, OpaqueBlock) -> OpaqueBlock
forall a b. (a, b) -> b
snd ((OpaqueId, OpaqueBlock) -> OpaqueBlock)
-> [(OpaqueId, OpaqueBlock)] -> [OpaqueBlock]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((OpaqueId, OpaqueBlock) -> Bool)
-> [(OpaqueId, OpaqueBlock)] -> [(OpaqueId, OpaqueBlock)]
forall a. (a -> Bool) -> [a] -> [a]
filter (OpaqueId, OpaqueBlock) -> Bool
isOurs (Map OpaqueId OpaqueBlock -> [(OpaqueId, OpaqueBlock)]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map OpaqueId OpaqueBlock
known)

    () <- liftIO $ evaluate (rnf (canonical, backcopies))

    reportSDoc "tc.opaque" 30 $ vcat $
      text "Opaque blocks defined in this module:":map pretty ours

    -- Only compute transitive closure for opaque blocks declared in
    -- the current top-level module. Deserialised blocks are always
    -- closed, so this work would be redundant.
    (blocks, names) <- computeClosure canonise known inverse ours

    -- Associate copies with the opaque blocks of their originals. Since
    -- modules importing this one won't know how to canonicalise names
    -- we have defined, we make the work easier for them by associating
    -- copies with their original's opaque blocks.
    let names' = ((QName, HashSet QName)
 -> Map QName OpaqueId -> Map QName OpaqueId)
-> Map QName OpaqueId
-> [(QName, HashSet QName)]
-> Map QName OpaqueId
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (QName, HashSet QName) -> Map QName OpaqueId -> Map QName OpaqueId
addBackcopy Map QName OpaqueId
names (HashMap QName (HashSet QName) -> [(QName, HashSet QName)]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap QName (HashSet QName)
backcopies)

    reportSDoc "tc.opaque.sat" 30 $ vcat $
      text "Saturated local opaque blocks":[ pretty block | b@(_,block) <- Map.toList blocks, isOurs b ]

    reportSDoc "tc.opaque.sat.full" 50 $ text "Saturated opaque blocks:" $+$ pretty blocks

    modifyTC (set stOpaqueBlocks blocks . set stOpaqueIds names')

  -- Actually compute the closure.
  computeClosure
    :: (QName -> QName)
    -> Map OpaqueId OpaqueBlock
      -- Accumulates the satured opaque blocks; also contains the
      -- opaque blocks of imported modules.
    -> Map QName OpaqueId
      -- Accumulates a mapping from names to opaque blocks; also
      -- contains imported opaque names.
    -> [OpaqueBlock]
      -- List of our opaque blocks, in dependency order.
    -> m ( Map OpaqueId OpaqueBlock
         , Map QName OpaqueId
         )
  computeClosure :: (QName -> QName)
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> [OpaqueBlock]
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
computeClosure QName -> QName
canonise !Map OpaqueId OpaqueBlock
blocks !Map QName OpaqueId
names [] = (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map OpaqueId OpaqueBlock
blocks, Map QName OpaqueId
names)
  computeClosure QName -> QName
canonise Map OpaqueId OpaqueBlock
blocks Map QName OpaqueId
names (OpaqueBlock
block:[OpaqueBlock]
xs) = Range
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (OpaqueBlock -> Range
opaqueRange OpaqueBlock
block) (m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
 -> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId))
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
forall a b. (a -> b) -> a -> b
$ do
    let
      yell :: QName -> a -> m a
yell QName
nm a
accum = Range -> m a -> m a
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
nm) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
        Warning -> m ()
forall (m :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
e -> m ()
warning (QName -> Warning
UnfoldTransparentName QName
nm)
        a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
accum

      -- Add the unfolding-set of the given name to the accumulator
      -- value.
      transitive :: QName -> HashSet QName -> m (HashSet QName)
transitive QName
prenom HashSet QName
accum = m (HashSet QName) -> Maybe (m (HashSet QName)) -> m (HashSet QName)
forall a. a -> Maybe a -> a
fromMaybe (QName -> HashSet QName -> m (HashSet QName)
forall {m :: * -> *} {a}.
(MonadTrace m, MonadWarning m) =>
QName -> a -> m a
yell QName
prenom HashSet QName
accum) (Maybe (m (HashSet QName)) -> m (HashSet QName))
-> Maybe (m (HashSet QName)) -> m (HashSet QName)
forall a b. (a -> b) -> a -> b
$ do
        -- NB: If the name is a local copy, we won't yet have added the
        -- copy name to an opaque block, but we will have added the
        -- reduced name (provided it is opaque)
        let nm :: QName
nm = QName -> QName
canonise QName
prenom
        id    <- QName -> Map QName OpaqueId -> Maybe OpaqueId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
nm Map QName OpaqueId
names
        block <- Map.lookup id blocks
        pure . pure $ HashSet.union (opaqueUnfolding block) accum

    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque.copy" VerboseLevel
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"Stated unfolding clause:  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (HashSet QName -> [QName]
forall a. HashSet a -> [a]
HashSet.toList (OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block))
           , TCMT IO Doc
"with (sub)canonical names:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (QName -> QName
canonise (QName -> QName) -> [QName] -> [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet QName -> [QName]
forall a. HashSet a -> [a]
HashSet.toList (OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block))
           ]

    -- Compute the transitive closure: bring in names
    --
    --   ... that are defined as immediate children of the opaque block
    --   ... that are unfolded by the parent opaque block
    --   ... that are implied by each name in the unfolding clause.
    closed <- (QName -> HashSet QName -> m (HashSet QName))
-> HashSet QName -> HashSet QName -> m (HashSet QName)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM QName -> HashSet QName -> m (HashSet QName)
transitive
      (  OpaqueBlock -> HashSet QName
opaqueDecls OpaqueBlock
block
      HashSet QName -> HashSet QName -> HashSet QName
forall a. Semigroup a => a -> a -> a
<> (OpaqueBlock -> HashSet QName)
-> Maybe OpaqueBlock -> HashSet QName
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap OpaqueBlock -> HashSet QName
opaqueUnfolding (OpaqueBlock -> Maybe OpaqueId
opaqueParent OpaqueBlock
block Maybe OpaqueId
-> (OpaqueId -> Maybe OpaqueBlock) -> Maybe OpaqueBlock
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (OpaqueId -> Map OpaqueId OpaqueBlock -> Maybe OpaqueBlock)
-> Map OpaqueId OpaqueBlock -> OpaqueId -> Maybe OpaqueBlock
forall a b c. (a -> b -> c) -> b -> a -> c
flip OpaqueId -> Map OpaqueId OpaqueBlock -> Maybe OpaqueBlock
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Map OpaqueId OpaqueBlock
blocks)
      )
      (OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block)

    let
      block' = OpaqueBlock
block { opaqueUnfolding = closed }

      -- Update the mapping from names to blocks, so that future
      -- references to names defined in our opaque block will know the
      -- right unfolding set.
      names' = (QName -> Map QName OpaqueId -> Map QName OpaqueId)
-> Map QName OpaqueId -> HashSet QName -> Map QName OpaqueId
forall b a. (b -> a -> a) -> a -> HashSet b -> a
HashSet.foldr (\QName
name -> QName -> OpaqueId -> Map QName OpaqueId -> Map QName OpaqueId
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert QName
name (OpaqueBlock -> OpaqueId
opaqueId OpaqueBlock
block)) Map QName OpaqueId
names
        (OpaqueBlock -> HashSet QName
opaqueDecls OpaqueBlock
block)

    computeClosure canonise (Map.insert (opaqueId block) block' blocks) names' xs

  addBackcopy :: (QName, HashSet QName) -> Map QName OpaqueId -> Map QName OpaqueId
  addBackcopy :: (QName, HashSet QName) -> Map QName OpaqueId -> Map QName OpaqueId
addBackcopy (QName
from, HashSet QName
prop) Map QName OpaqueId
map
    | Just OpaqueId
id <- QName -> Map QName OpaqueId -> Maybe OpaqueId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
from Map QName OpaqueId
map = (QName -> Map QName OpaqueId -> Map QName OpaqueId)
-> Map QName OpaqueId -> HashSet QName -> Map QName OpaqueId
forall b a. (b -> a -> a) -> a -> HashSet b -> a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((QName -> OpaqueId -> Map QName OpaqueId -> Map QName OpaqueId)
-> OpaqueId -> QName -> Map QName OpaqueId -> Map QName OpaqueId
forall a b c. (a -> b -> c) -> b -> a -> c
flip QName -> OpaqueId -> Map QName OpaqueId -> Map QName OpaqueId
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert OpaqueId
id) Map QName OpaqueId
map HashSet QName
prop
    | Bool
otherwise = Map QName OpaqueId
map

-- | Decide whether or not a definition is reducible. Returns 'True' if
-- the definition /can/ step.
isAccessibleDef :: TCEnv -> TCState -> Definition -> Bool

-- IgnoreAbstractMode ignores both abstract and opaque. It is used for
-- getting the original definition (for inConcreteOrAbstractMode), and
-- for "normalise ignoring abstract" interactively.
isAccessibleDef :: TCEnv -> TCState -> Definition -> Bool
isAccessibleDef TCEnv
env TCState
state Definition
defn
  | (TCEnv
env TCEnv -> Getting AbstractMode TCEnv AbstractMode -> AbstractMode
forall s a. s -> Getting a s a -> a
^. Getting AbstractMode TCEnv AbstractMode
Lens' TCEnv AbstractMode
eAbstractMode) AbstractMode -> AbstractMode -> Bool
forall a. Eq a => a -> a -> Bool
== AbstractMode
IgnoreAbstractMode = Bool
True

-- Otherwise, actually apply the reducibility rules..
isAccessibleDef TCEnv
env TCState
state Definition
defn =
  let
    -- Reducibility rules for abstract definitions:
    concretise :: IsAbstract -> IsAbstract
concretise IsAbstract
def = case TCEnv
env TCEnv -> Getting AbstractMode TCEnv AbstractMode -> AbstractMode
forall s a. s -> Getting a s a -> a
^. Getting AbstractMode TCEnv AbstractMode
Lens' TCEnv AbstractMode
eAbstractMode of
      -- Being outside an abstract block has no effect on concreteness
      AbstractMode
ConcreteMode       -> IsAbstract
def

      -- This clause is redundant with the preceding guard but GHC can't
      -- figure it out:
      AbstractMode
IgnoreAbstractMode -> IsAbstract
ConcreteDef

      AbstractMode
AbstractMode -> let
        dropLastModule :: ModuleName -> ModuleName
dropLastModule (MName [Name]
ms) = [Name] -> ModuleName
MName ([Name] -> ModuleName) -> [Name] -> ModuleName
forall a b. (a -> b) -> a -> b
$ [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
initWithDefault [Name]
forall a. HasCallStack => a
__IMPOSSIBLE__ [Name]
ms
        dropAnon :: ModuleName -> ModuleName
dropAnon       (MName [Name]
ms) = [Name] -> ModuleName
MName ([Name] -> ModuleName) -> [Name] -> ModuleName
forall a b. (a -> b) -> a -> b
$ (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName [Name]
ms

        current :: ModuleName
current = ModuleName -> ModuleName
dropAnon (ModuleName -> ModuleName) -> ModuleName -> ModuleName
forall a b. (a -> b) -> a -> b
$ TCEnv
env TCEnv -> Getting ModuleName TCEnv ModuleName -> ModuleName
forall s a. s -> Getting a s a -> a
^. Getting ModuleName TCEnv ModuleName
Lens' TCEnv ModuleName
eCurrentModule

        modname :: ModuleName
modname = case Definition -> Defn
theDef Definition
defn of
          -- Hack to make abstract constructors work properly. The constructors
          -- live in a module with the same name as the datatype, but for 'abstract'
          -- purposes they're considered to be in the same module as the datatype.
          Constructor{} -> ModuleName -> ModuleName
dropAnon (ModuleName -> ModuleName) -> ModuleName -> ModuleName
forall a b. (a -> b) -> a -> b
$ ModuleName -> ModuleName
dropLastModule (ModuleName -> ModuleName) -> ModuleName -> ModuleName
forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule (QName -> ModuleName) -> QName -> ModuleName
forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName Definition
defn
          Defn
_             -> ModuleName -> ModuleName
dropAnon (ModuleName -> ModuleName) -> ModuleName -> ModuleName
forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule (QName -> ModuleName) -> QName -> ModuleName
forall a b. (a -> b) -> a -> b
$ Definition -> QName
defName Definition
defn

       in if ModuleName
current ModuleName -> ModuleName -> Bool
`isLeChildModuleOf` ModuleName
modname
        then IsAbstract
ConcreteDef
        else IsAbstract
def

    -- Reducibility rule for opaque definitions: If we are operating
    -- under an unfolding block,
    clarify :: IsOpaque -> IsOpaque
clarify IsOpaque
def = case TCEnv
env TCEnv
-> Getting (Maybe OpaqueId) TCEnv (Maybe OpaqueId)
-> Maybe OpaqueId
forall s a. s -> Getting a s a -> a
^. Getting (Maybe OpaqueId) TCEnv (Maybe OpaqueId)
Lens' TCEnv (Maybe OpaqueId)
eCurrentOpaqueId of
      Just OpaqueId
oid ->
        let
          block :: OpaqueBlock
block = OpaqueBlock -> Maybe OpaqueBlock -> OpaqueBlock
forall a. a -> Maybe a -> a
fromMaybe OpaqueBlock
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe OpaqueBlock -> OpaqueBlock)
-> Maybe OpaqueBlock -> OpaqueBlock
forall a b. (a -> b) -> a -> b
$ OpaqueId -> Map OpaqueId OpaqueBlock -> Maybe OpaqueBlock
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup OpaqueId
oid (Getting
  (Map OpaqueId OpaqueBlock) TCState (Map OpaqueId OpaqueBlock)
-> TCState -> Map OpaqueId OpaqueBlock
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Map OpaqueId OpaqueBlock) TCState (Map OpaqueId OpaqueBlock)
Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks TCState
state)

          -- Then any name which is a member of the unfolding-set
          -- associated to that block will be unfolded.
          okay :: Bool
okay = Definition -> QName
defName Definition
defn QName -> HashSet QName -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HashSet.member` OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block
        in if Bool
okay then IsOpaque
TransparentDef else IsOpaque
def
      Maybe OpaqueId
Nothing -> IsOpaque
def

    -- Short-circuit the map lookup for vanilla definitions
    plainDef :: Bool
plainDef = Definition -> IsAbstract
defAbstract Definition
defn IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
ConcreteDef
            Bool -> Bool -> Bool
&& Definition -> IsOpaque
defOpaque   Definition
defn IsOpaque -> IsOpaque -> Bool
forall a. Eq a => a -> a -> Bool
== IsOpaque
TransparentDef

  in Bool
plainDef
  Bool -> Bool -> Bool
|| ( IsAbstract -> IsAbstract
concretise (Definition -> IsAbstract
defAbstract Definition
defn) IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
ConcreteDef
    Bool -> Bool -> Bool
&& IsOpaque -> IsOpaque
clarify    (Definition -> IsOpaque
defOpaque Definition
defn)   IsOpaque -> IsOpaque -> Bool
forall a. Eq a => a -> a -> Bool
== IsOpaque
TransparentDef)

-- | Will the given 'QName' have a proper definition, or will it be
-- wrapped in an 'AbstractDefn'?
hasAccessibleDef
  :: (ReadTCState m, HasConstInfo m) => QName -> m Bool
hasAccessibleDef :: forall (m :: * -> *).
(ReadTCState m, HasConstInfo m) =>
QName -> m Bool
hasAccessibleDef QName
qn = do
  env <- m TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
  st <- getTCState
  ignoreAbstractMode $ do
    def <- getConstInfo qn
    pure $ isAccessibleDef env st def

-- | 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.
canSolveMetaOpaquely :: MetaInfo -> Teletype -> TCM Bool
canSolveMetaOpaquely :: MetaInfo -> Teletype -> TCM Bool
canSolveMetaOpaquely MetaInfo
mi Teletype
t = TCM Bool
both where
  -- these are the happy cases, where we can cheaply determine just
  -- looking at the flags whether the reducibility settings changed.
  -- if the current environment is concrete, we can solve any
  -- metavariable. concrete environments don't unfold anything extra.
  abs :: IsAbstract -> IsAbstract -> Bool
abs IsAbstract
_           IsAbstract
ConcreteDef = Bool
True
  -- however, if the current environment is abstract, we can only solve
  -- other abstract metas. this is because, if the meta was concrete, it
  -- will not know about reductions that may have been added by going
  -- into abstract mode for this comparison.
  abs IsAbstract
AbstractDef IsAbstract
AbstractDef = Bool
True
  abs IsAbstract
ConcreteDef IsAbstract
AbstractDef = Bool
False

  -- the rules for opacity are a bit more complicated, but again a
  -- transparent environment can solve anything, while a transparent
  -- meta can not be solved under an opaque block.
  opq :: IsOpaque -> IsOpaque -> Bool
opq IsOpaque
_              IsOpaque
TransparentDef = Bool
True
  opq IsOpaque
TransparentDef OpaqueDef{}    = Bool
False
  -- however, if the meta is also opaque, we have to decide whether
  -- everything that can be unfolded *now* (i.e. where we are assigning
  -- the meta) could also be unfolded *then* (i.e. where the meta was
  -- created). this is simple if we are in the same opaque block.
  opq (OpaqueDef OpaqueId
mv) (OpaqueDef OpaqueId
eb) = OpaqueId
mv OpaqueId -> OpaqueId -> Bool
forall a. Eq a => a -> a -> Bool
== OpaqueId
eb

  -- in the sad case, we check that any name that is accessible in the
  -- current environment was already accessible in the meta's
  -- environment.
  sad :: TCM Bool
sad = do
    st      <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
    now_env <- askTC
    let mv_env = MetaInfo -> Closure Range
miClosRange MetaInfo
mi Closure Range -> Getting TCEnv (Closure Range) TCEnv -> TCEnv
forall s a. s -> Getting a s a -> a
^. Getting TCEnv (Closure Range) TCEnv
forall a. LensTCEnv a => Lens' a TCEnv
Lens' (Closure Range) TCEnv
lensTCEnv
    getAll <$> flip namesIn' t \QName
name -> Bool -> All
All (Bool -> All) -> TCM Bool -> TCMT IO All
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      def <- TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
name)
      pure $! isAccessibleDef now_env st def <= isAccessibleDef mv_env st def

  both :: TCM Bool
both = [TCM Bool] -> TCM Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
orM
    [ [TCM Bool] -> TCM Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM
      [ IsAbstract -> IsAbstract -> Bool
abs (MetaInfo
mi MetaInfo -> Getting IsAbstract MetaInfo IsAbstract -> IsAbstract
forall s a. s -> Getting a s a -> a
^. Getting IsAbstract MetaInfo IsAbstract
forall a. LensIsAbstract a => Lens' a IsAbstract
Lens' MetaInfo IsAbstract
lensIsAbstract) (IsAbstract -> Bool) -> TCMT IO IsAbstract -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv IsAbstract -> TCMT IO IsAbstract
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (IsAbstract -> f IsAbstract) -> TCEnv -> f TCEnv
forall a. LensIsAbstract a => Lens' a IsAbstract
Lens' TCEnv IsAbstract
lensIsAbstract
      , IsOpaque -> IsOpaque -> Bool
opq (MetaInfo
mi MetaInfo -> Getting IsOpaque MetaInfo IsOpaque -> IsOpaque
forall s a. s -> Getting a s a -> a
^. Getting IsOpaque MetaInfo IsOpaque
forall a. LensIsOpaque a => Lens' a IsOpaque
Lens' MetaInfo IsOpaque
lensIsOpaque)   (IsOpaque -> Bool) -> TCMT IO IsOpaque -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv IsOpaque -> TCMT IO IsOpaque
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (IsOpaque -> f IsOpaque) -> TCEnv -> f TCEnv
forall a. LensIsOpaque a => Lens' a IsOpaque
Lens' TCEnv IsOpaque
lensIsOpaque
      ]
    , TCM Bool
sad ]