{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.DeadCode (eliminateDeadCode) where

import qualified Control.Exception as E
import Control.Monad.Trans

import Data.Maybe
import Data.Monoid (All(..))
import qualified Data.Map.Strict as MapS
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap

import Agda.Interaction.Options

import qualified Agda.Syntax.Abstract as A

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Names
import Agda.Syntax.Scope.Base

import qualified Agda.Benchmarking as Bench
import qualified Agda.TypeChecking.Monad.Benchmark as Bench

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce

import Agda.Utils.Impossible
import Agda.Utils.Lens

-- | Run before serialisation to remove any definitions and
-- meta-variables that are not reachable from the module's public
-- interface.
--
-- Things that are reachable only from warnings are removed.

eliminateDeadCode ::
  BuiltinThings PrimFun -> DisplayForms -> Signature ->
  LocalMetaStore ->
  TCM (DisplayForms, Signature, RemoteMetaStore)
eliminateDeadCode :: BuiltinThings PrimFun
-> HashMap QName [LocalDisplayForm]
-> Signature
-> LocalMetaStore
-> TCM
     (HashMap QName [LocalDisplayForm], Signature, RemoteMetaStore)
eliminateDeadCode BuiltinThings PrimFun
bs HashMap QName [LocalDisplayForm]
disp Signature
sig LocalMetaStore
ms = Account (BenchPhase (TCMT IO))
-> TCM
     (HashMap QName [LocalDisplayForm], Signature, RemoteMetaStore)
-> TCM
     (HashMap QName [LocalDisplayForm], Signature, RemoteMetaStore)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.DeadCode] (TCM (HashMap QName [LocalDisplayForm], Signature, RemoteMetaStore)
 -> TCM
      (HashMap QName [LocalDisplayForm], Signature, RemoteMetaStore))
-> TCM
     (HashMap QName [LocalDisplayForm], Signature, RemoteMetaStore)
-> TCM
     (HashMap QName [LocalDisplayForm], Signature, RemoteMetaStore)
forall a b. (a -> b) -> a -> b
$ do
  PatternSynDefns
patsyn <- TCMT IO PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns
  Set QName
public <- (AbstractName -> QName) -> Set AbstractName -> Set QName
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic AbstractName -> QName
anameName (Set AbstractName -> Set QName)
-> (ScopeInfo -> Set AbstractName) -> ScopeInfo -> Set QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> Set AbstractName
publicNames (ScopeInfo -> Set QName)
-> TCMT IO ScopeInfo -> TCMT IO (Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  Bool
save   <- PragmaOptions -> Bool
optSaveMetas (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  HashMap QName Definition
defs   <- (if Bool
save then HashMap QName Definition -> TCMT IO (HashMap QName Definition)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return else (Definition -> TCMT IO Definition)
-> HashMap QName Definition -> TCMT IO (HashMap QName Definition)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HashMap QName a -> f (HashMap QName b)
traverse Definition -> TCMT IO Definition
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull)
                 (Signature
sig Signature
-> Lens' Signature (HashMap QName Definition)
-> HashMap QName Definition
forall o i. o -> Lens' o i -> i
^. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions)
  -- #2921: Eliminating definitions with attached COMPILE pragmas results in
  -- the pragmas not being checked. Simple solution: don't eliminate these.
  -- #6022 (Andreas, 2022-09-30): Eliminating cubical primitives can lead to crashes.
   -- Simple solution: retain all primitives (shouldn't be many).
  let hasCompilePragma :: Definition -> Bool
hasCompilePragma = Bool -> Bool
not (Bool -> Bool) -> (Definition -> Bool) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map [Char] [CompilerPragma] -> Bool
forall k a. Map k a -> Bool
MapS.null (Map [Char] [CompilerPragma] -> Bool)
-> (Definition -> Map [Char] [CompilerPragma])
-> Definition
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Map [Char] [CompilerPragma]
defCompiledRep
      isPrimitive :: Defn -> Bool
isPrimitive = \case
        Primitive{}     -> Bool
True
        PrimitiveSort{} -> Bool
True
        Defn
_ -> Bool
False
      extraRootsFilter :: (a, Definition) -> Maybe a
extraRootsFilter (a
name, Definition
def)
        | Definition -> Bool
hasCompilePragma Definition
def Bool -> Bool -> Bool
|| Defn -> Bool
isPrimitive (Definition -> Defn
theDef Definition
def) = a -> Maybe a
forall a. a -> Maybe a
Just a
name
        | Bool
otherwise = Maybe a
forall a. Maybe a
Nothing
      extraRoots :: Set QName
extraRoots =
        [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
forall a b. (a -> b) -> a -> b
$ ((QName, Definition) -> Maybe QName)
-> [(QName, Definition)] -> [QName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (QName, Definition) -> Maybe QName
forall {a}. (a, Definition) -> Maybe a
extraRootsFilter ([(QName, Definition)] -> [QName])
-> [(QName, Definition)] -> [QName]
forall a b. (a -> b) -> a -> b
$ HashMap QName Definition -> [(QName, Definition)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList HashMap QName Definition
defs

      rootNames :: Set QName
rootNames = Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
public Set QName
extraRoots
      rootMetas :: Set MetaId
rootMetas =
        if Bool -> Bool
not Bool
save then Set MetaId
forall a. Set a
Set.empty else (BuiltinThings PrimFun, Sections, RewriteRuleMap,
 HashMap QName [LocalDisplayForm])
-> Set MetaId
forall a m. (NamesIn a, Collection MetaId m) => a -> m
metasIn
          ( BuiltinThings PrimFun
bs
          , Signature
sig Signature -> Lens' Signature Sections -> Sections
forall o i. o -> Lens' o i -> i
^. (Sections -> f Sections) -> Signature -> f Signature
Lens' Signature Sections
sigSections
          , Signature
sig Signature -> Lens' Signature RewriteRuleMap -> RewriteRuleMap
forall o i. o -> Lens' o i -> i
^. (RewriteRuleMap -> f RewriteRuleMap) -> Signature -> f Signature
Lens' Signature RewriteRuleMap
sigRewriteRules
          , (QName -> [LocalDisplayForm] -> Bool)
-> HashMap QName [LocalDisplayForm]
-> HashMap QName [LocalDisplayForm]
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HMap.filterWithKey (\QName
x [LocalDisplayForm]
_ -> QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
rootNames) HashMap QName [LocalDisplayForm]
disp
          )
      (Set QName
rns, Set MetaId
rms) =
        (Set QName, Set MetaId)
-> PatternSynDefns
-> HashMap QName [LocalDisplayForm]
-> HashMap QName Definition
-> LocalMetaStore
-> (Set QName, Set MetaId)
reachableFrom (Set QName
rootNames, Set MetaId
rootMetas) PatternSynDefns
patsyn HashMap QName [LocalDisplayForm]
disp HashMap QName Definition
defs LocalMetaStore
ms
      dead :: Set QName
dead  = [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList (HashMap QName Definition -> [QName]
forall k v. HashMap k v -> [k]
HMap.keys HashMap QName Definition
defs) Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set QName
rns
      valid :: LocalDisplayForm -> Bool
valid = All -> Bool
getAll (All -> Bool)
-> (LocalDisplayForm -> All) -> LocalDisplayForm -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> All) -> LocalDisplayForm -> All
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' (Bool -> All
All (Bool -> All) -> (QName -> Bool) -> QName -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set QName
dead))  -- no used name is dead
      defs' :: HashMap QName Definition
defs' = (Definition -> Definition)
-> HashMap QName Definition -> HashMap QName Definition
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map ( \ Definition
d -> Definition
d { defDisplay = filter valid (defDisplay d) } )
            (HashMap QName Definition -> HashMap QName Definition)
-> HashMap QName Definition -> HashMap QName Definition
forall a b. (a -> b) -> a -> b
$ (QName -> Definition -> Bool)
-> HashMap QName Definition -> HashMap QName Definition
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HMap.filterWithKey (\ QName
x Definition
_ -> QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
rns) HashMap QName Definition
defs
      disp' :: HashMap QName [LocalDisplayForm]
disp' = ([LocalDisplayForm] -> Bool)
-> HashMap QName [LocalDisplayForm]
-> HashMap QName [LocalDisplayForm]
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not (Bool -> Bool)
-> ([LocalDisplayForm] -> Bool) -> [LocalDisplayForm] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LocalDisplayForm] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (HashMap QName [LocalDisplayForm]
 -> HashMap QName [LocalDisplayForm])
-> HashMap QName [LocalDisplayForm]
-> HashMap QName [LocalDisplayForm]
forall a b. (a -> b) -> a -> b
$ ([LocalDisplayForm] -> [LocalDisplayForm])
-> HashMap QName [LocalDisplayForm]
-> HashMap QName [LocalDisplayForm]
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map ((LocalDisplayForm -> Bool)
-> [LocalDisplayForm] -> [LocalDisplayForm]
forall a. (a -> Bool) -> [a] -> [a]
filter LocalDisplayForm -> Bool
valid) HashMap QName [LocalDisplayForm]
disp
      ms' :: RemoteMetaStore
ms'   = [(MetaId, RemoteMetaVariable)] -> RemoteMetaStore
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList ([(MetaId, RemoteMetaVariable)] -> RemoteMetaStore)
-> [(MetaId, RemoteMetaVariable)] -> RemoteMetaStore
forall a b. (a -> b) -> a -> b
$
              ((MetaId, MetaVariable) -> Maybe (MetaId, RemoteMetaVariable))
-> [(MetaId, MetaVariable)] -> [(MetaId, RemoteMetaVariable)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
                (\(MetaId
m, MetaVariable
mv) ->
                  if Bool -> Bool
not (MetaId -> Set MetaId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member MetaId
m Set MetaId
rms)
                  then Maybe (MetaId, RemoteMetaVariable)
forall a. Maybe a
Nothing
                  else (MetaId, RemoteMetaVariable) -> Maybe (MetaId, RemoteMetaVariable)
forall a. a -> Maybe a
Just (MetaId
m, MetaVariable -> RemoteMetaVariable
remoteMetaVariable MetaVariable
mv)) ([(MetaId, MetaVariable)] -> [(MetaId, RemoteMetaVariable)])
-> [(MetaId, MetaVariable)] -> [(MetaId, RemoteMetaVariable)]
forall a b. (a -> b) -> a -> b
$
              LocalMetaStore -> [(MetaId, MetaVariable)]
forall k a. Map k a -> [(k, a)]
MapS.toList LocalMetaStore
ms
  -- The hashmaps are forced to WHNF to ensure that the computations
  -- are billed to the right account.
  HashMap QName [LocalDisplayForm]
disp' <- IO (HashMap QName [LocalDisplayForm])
-> TCMT IO (HashMap QName [LocalDisplayForm])
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (HashMap QName [LocalDisplayForm])
 -> TCMT IO (HashMap QName [LocalDisplayForm]))
-> IO (HashMap QName [LocalDisplayForm])
-> TCMT IO (HashMap QName [LocalDisplayForm])
forall a b. (a -> b) -> a -> b
$ HashMap QName [LocalDisplayForm]
-> IO (HashMap QName [LocalDisplayForm])
forall a. a -> IO a
E.evaluate HashMap QName [LocalDisplayForm]
disp'
  HashMap QName Definition
defs' <- IO (HashMap QName Definition) -> TCMT IO (HashMap QName Definition)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (HashMap QName Definition)
 -> TCMT IO (HashMap QName Definition))
-> IO (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall a b. (a -> b) -> a -> b
$ HashMap QName Definition -> IO (HashMap QName Definition)
forall a. a -> IO a
E.evaluate HashMap QName Definition
defs'
  RemoteMetaStore
ms'   <- IO RemoteMetaStore -> TCMT IO RemoteMetaStore
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO RemoteMetaStore -> TCMT IO RemoteMetaStore)
-> IO RemoteMetaStore -> TCMT IO RemoteMetaStore
forall a b. (a -> b) -> a -> b
$ RemoteMetaStore -> IO RemoteMetaStore
forall a. a -> IO a
E.evaluate RemoteMetaStore
ms'
  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.dead" Int
10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [Char]
"Removed " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (HashMap QName Definition -> Int
forall k v. HashMap k v -> Int
HMap.size HashMap QName Definition
defs Int -> Int -> Int
forall a. Num a => a -> a -> a
- HashMap QName Definition -> Int
forall k v. HashMap k v -> Int
HMap.size HashMap QName Definition
defs') [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
    [Char]
" unused definitions and " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (LocalMetaStore -> Int
forall k a. Map k a -> Int
MapS.size LocalMetaStore
ms Int -> Int -> Int
forall a. Num a => a -> a -> a
- RemoteMetaStore -> Int
forall k v. HashMap k v -> Int
HMap.size RemoteMetaStore
ms') [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
    [Char]
" unused meta-variables."
  (HashMap QName [LocalDisplayForm], Signature, RemoteMetaStore)
-> TCM
     (HashMap QName [LocalDisplayForm], Signature, RemoteMetaStore)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (HashMap QName [LocalDisplayForm]
disp', Lens' Signature (HashMap QName Definition)
-> LensSet Signature (HashMap QName Definition)
forall o i. Lens' o i -> LensSet o i
set (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions HashMap QName Definition
defs' Signature
sig, RemoteMetaStore
ms')

reachableFrom
  :: (Set QName, Set MetaId)  -- ^ Roots.
  -> A.PatternSynDefns -> DisplayForms -> Definitions -> LocalMetaStore
  -> (Set QName, Set MetaId)
reachableFrom :: (Set QName, Set MetaId)
-> PatternSynDefns
-> HashMap QName [LocalDisplayForm]
-> HashMap QName Definition
-> LocalMetaStore
-> (Set QName, Set MetaId)
reachableFrom (Set QName
ids, Set MetaId
ms) PatternSynDefns
psyns HashMap QName [LocalDisplayForm]
disp HashMap QName Definition
defs LocalMetaStore
insts =
  (Set QName, Set MetaId)
-> [Either QName MetaId] -> (Set QName, Set MetaId)
follow (Set QName
ids, Set MetaId
ms)
    ((QName -> Either QName MetaId) -> [QName] -> [Either QName MetaId]
forall a b. (a -> b) -> [a] -> [b]
map QName -> Either QName MetaId
forall a b. a -> Either a b
Left (Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
ids) [Either QName MetaId]
-> [Either QName MetaId] -> [Either QName MetaId]
forall a. [a] -> [a] -> [a]
++ (MetaId -> Either QName MetaId)
-> [MetaId] -> [Either QName MetaId]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> Either QName MetaId
forall a b. b -> Either a b
Right (Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList Set MetaId
ms))
  where
  follow :: (Set QName, Set MetaId)
-> [Either QName MetaId] -> (Set QName, Set MetaId)
follow (Set QName, Set MetaId)
seen        []       = (Set QName, Set MetaId)
seen
  follow (!Set QName
ids, !Set MetaId
ms) (Either QName MetaId
x : [Either QName MetaId]
xs) =
    (Set QName, Set MetaId)
-> [Either QName MetaId] -> (Set QName, Set MetaId)
follow (Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
ids'' Set QName
ids, Set MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set MetaId
ms'' Set MetaId
ms)
      ((QName -> Either QName MetaId) -> [QName] -> [Either QName MetaId]
forall a b. (a -> b) -> [a] -> [b]
map QName -> Either QName MetaId
forall a b. a -> Either a b
Left  (Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
ids'') [Either QName MetaId]
-> [Either QName MetaId] -> [Either QName MetaId]
forall a. [a] -> [a] -> [a]
++
       (MetaId -> Either QName MetaId)
-> [MetaId] -> [Either QName MetaId]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> Either QName MetaId
forall a b. b -> Either a b
Right (Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList Set MetaId
ms'')  [Either QName MetaId]
-> [Either QName MetaId] -> [Either QName MetaId]
forall a. [a] -> [a] -> [a]
++
       [Either QName MetaId]
xs)
    where
    ids'' :: Set QName
ids'' = Set QName
ids' Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set QName
ids
    ms'' :: Set MetaId
ms''  = Set MetaId
ms'  Set MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set MetaId
ms

    (Set QName
ids', Set MetaId
ms') = case Either QName MetaId
x of
      Left QName
x ->
        (Maybe Definition, Maybe PSyn, Maybe [LocalDisplayForm])
-> (Set QName, Set MetaId)
forall a m1 m2.
(NamesIn a, Collection QName m1, Collection MetaId m2) =>
a -> (m1, m2)
namesAndMetasIn
          ( QName -> HashMap QName Definition -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
x HashMap QName Definition
defs
          , PatternSynDefn -> PSyn
PSyn (PatternSynDefn -> PSyn) -> Maybe PatternSynDefn -> Maybe PSyn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> PatternSynDefns -> Maybe PatternSynDefn
forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup QName
x PatternSynDefns
psyns
          , QName
-> HashMap QName [LocalDisplayForm] -> Maybe [LocalDisplayForm]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
x HashMap QName [LocalDisplayForm]
disp
          )
      Right MetaId
m -> case MetaId -> LocalMetaStore -> Maybe MetaVariable
forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup MetaId
m LocalMetaStore
insts of
        Maybe MetaVariable
Nothing -> (Set QName
forall a. Set a
Set.empty, Set MetaId
forall a. Set a
Set.empty)
        Just MetaVariable
mv -> Term -> (Set QName, Set MetaId)
forall a m1 m2.
(NamesIn a, Collection QName m1, Collection MetaId m2) =>
a -> (m1, m2)
namesAndMetasIn (Instantiation -> Term
instBody (MetaVariable -> Instantiation
theInstantiation MetaVariable
mv))

-- | Returns the instantiation.
--
-- Precondition: The instantiation must be of the form @'InstV' inst@.

theInstantiation :: MetaVariable -> Instantiation
theInstantiation :: MetaVariable -> Instantiation
theInstantiation MetaVariable
mv = case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
  InstV Instantiation
inst                     -> Instantiation
inst
  Open{}                         -> Instantiation
forall a. HasCallStack => a
__IMPOSSIBLE__
  OpenInstance{}                 -> Instantiation
forall a. HasCallStack => a
__IMPOSSIBLE__
  BlockedConst{}                 -> Instantiation
forall a. HasCallStack => a
__IMPOSSIBLE__
  PostponedTypeCheckingProblem{} -> Instantiation
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Converts from 'MetaVariable' to 'RemoteMetaVariable'.
--
-- Precondition: The instantiation must be of the form @'InstV' inst@.

remoteMetaVariable :: MetaVariable -> RemoteMetaVariable
remoteMetaVariable :: MetaVariable -> RemoteMetaVariable
remoteMetaVariable MetaVariable
mv = RemoteMetaVariable
  { rmvInstantiation :: Instantiation
rmvInstantiation = MetaVariable -> Instantiation
theInstantiation MetaVariable
mv
  , rmvModality :: Modality
rmvModality      = MetaVariable -> Modality
forall a. LensModality a => a -> Modality
getModality MetaVariable
mv
  , rmvJudgement :: Judgement MetaId
rmvJudgement     = MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv
  }