{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE RecordWildCards #-}

module Mikan.TypeChecking.Rules.Decl where

import Prelude hiding ( null )

import Control.Monad.Writer (tell)

import Data.Either (partitionEithers)
import Data.Foldable qualified as Fold
import Data.Map.Strict qualified as MapS
import Data.Maybe
import Data.Set qualified as Set
import Data.Set (Set)

import Mikan.Interaction.Highlighting.Generate

import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Scope.Errors
import Mikan.Syntax.Abstract.Views (deepUnscopeDecl, deepUnscopeDecls)
import Mikan.Syntax.Internal
import Mikan.Syntax.Info qualified as Info
import Mikan.Syntax.Position
import Mikan.Syntax.Common
import Mikan.Syntax.Common.Pretty (prettyShow)
import Mikan.Syntax.Literal

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Monad.Benchmark (MonadBench, Phase)
import Mikan.TypeChecking.Monad.Benchmark qualified as Bench

import Mikan.TypeChecking.Constraints
import Mikan.TypeChecking.Conversion
import Mikan.TypeChecking.IApplyConfluence
import Mikan.TypeChecking.Generalize
import Mikan.TypeChecking.Injectivity
import Mikan.TypeChecking.InstanceArguments
import Mikan.TypeChecking.Positivity
import Mikan.TypeChecking.Positivity.Occurrence
import Mikan.TypeChecking.Polarity
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Primitive
import Mikan.TypeChecking.ProjectionLike
import Mikan.TypeChecking.Unquote
import Mikan.TypeChecking.Records
import Mikan.TypeChecking.RecordPatterns
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Warnings

import Mikan.TypeChecking.Rules.Application
import Mikan.TypeChecking.Rules.Term
import Mikan.TypeChecking.Rules.Data    ( checkDataDef )
import Mikan.TypeChecking.Rules.Record  ( checkRecDef )
import Mikan.TypeChecking.Rules.Def     ( checkFunDef, newSection, useTerPragma )
import Mikan.TypeChecking.Rules.Builtin
import Mikan.TypeChecking.Rules.Display ( checkDisplayPragma )

import Mikan.Termination.TermCheck

import Mikan.Utils.Function ( applyUnless )
import Mikan.Utils.Functor
import Mikan.Utils.List
import Mikan.Utils.List1 ( List1, pattern (:|), (<|) )
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Utils.Size
import Mikan.Utils.Update
import Mikan.Syntax.Common.Pretty qualified as P
import Mikan.Utils.SmallSet qualified as SmallSet

import Mikan.Utils.Impossible

-- | Cached checkDecl
checkDeclCached :: A.Declaration -> TCM ()
checkDeclCached :: Declaration -> TCM ()
checkDeclCached d :: Declaration
d@A.ScopedDecl{} = Declaration -> TCM ()
checkDecl Declaration
d
checkDeclCached
  d :: Declaration
d@(A.Section Range
_ ModuleName
mname (A.GeneralizeTel Map QName Name
_ Telescope
tbinds) [Declaration]
_) = do
  e <- TCMT IO (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog  -- Can ignore the set of generalizable vars (they occur in the telescope)
  reportSLn "cache.decl" 10 $ "checkDeclCached: " ++! show (isJust e)
  case e of
    Just (EnterSection ModuleName
mname' Telescope
tbinds', PostScopeState
_)
      | ModuleName
mname ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
mname' Bool -> Bool -> Bool
&& Telescope
tbinds Telescope -> Telescope -> Bool
forall a. Eq a => a -> a -> Bool
== Telescope
tbinds' ->
        () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe (TypeCheckAction, PostScopeState)
_ -> TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
  writeToCurrentLog $ EnterSection mname tbinds
  checkDecl d
  readFromCachedLog >>= \case
    Just (LeaveSection ModuleName
mname', PostScopeState
_) | ModuleName
mname ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
mname' -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Maybe (TypeCheckAction, PostScopeState)
_ -> TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
  writeToCurrentLog $ LeaveSection mname

checkDeclCached Declaration
d = do
  e <- TCMT IO (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog

  case e of
    Just (Decl Declaration
d', PostScopeState
s) | Declaration -> Declaration -> Bool
compareDecl Declaration
d Declaration
d' -> do
      PostScopeState -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCState m) =>
PostScopeState -> m ()
restorePostScopeState PostScopeState
s
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"cache.decl" Int
50 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"range: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d)
      Range -> TCM ()
printSyntaxInfo (Declaration -> Range
forall a. HasRange a => a -> Range
getRange Declaration
d)
    Maybe (TypeCheckAction, PostScopeState)
_ -> do
      TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
      Declaration -> TCM ()
checkDeclWrap Declaration
d

  writeToCurrentLog $ Decl d
 where
   compareDecl :: Declaration -> Declaration -> Bool
compareDecl A.Section{} A.Section{} = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
   compareDecl A.ScopedDecl{} A.ScopedDecl{} = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
   -- Andreas, 2025-12-12:
   -- We could consider all A.UnfoldingDecl as equal for the sake of caching
   -- because it is supposed to be there only for highlighting purposes.
   -- However, I fixed the caching problem for opaque blocks
   -- by emitting A.UnfoldingDecl after the declaration in the opaque block,
   -- so changes in an opaque block do not invalidate the whole block.
   -- (See ConcreteToAbstract, case NiceOpaque.)
   -- Thus, the following line should not offer an improvement:
   -- compareDecl A.UnfoldingDecl{} A.UnfoldingDecl{} = True
     -- A.UnfoldingDecl exists only for highlighting purposes,
     -- so it should not affect the caching
   compareDecl Declaration
x Declaration
y = Declaration
x Declaration -> Declaration -> Bool
forall a. Eq a => a -> a -> Bool
== Declaration
y
   -- changes to CS inside a RecDef or Mutual ought not happen,
   -- but they do happen, so we discard them.
   ignoreChanges :: m a -> m a
ignoreChanges m a
m = m a -> m a
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
localCache (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
     m ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
     m a
m
   checkDeclWrap :: Declaration -> TCM ()
checkDeclWrap d :: Declaration
d@A.RecDef{} = TCM () -> TCM ()
forall {m :: * -> *} {a}.
(MonadTCState m, ReadTCState m, MonadDebug m) =>
m a -> m a
ignoreChanges (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Declaration -> TCM ()
checkDecl Declaration
d
   checkDeclWrap d :: Declaration
d@A.Mutual{} = TCM () -> TCM ()
forall {m :: * -> *} {a}.
(MonadTCState m, ReadTCState m, MonadDebug m) =>
m a -> m a
ignoreChanges (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Declaration -> TCM ()
checkDecl Declaration
d
   checkDeclWrap Declaration
d            = Declaration -> TCM ()
checkDecl Declaration
d

-- | Type check a sequence of declarations.
checkDecls :: [A.Declaration] -> TCM ()
checkDecls :: [Declaration] -> TCM ()
checkDecls [Declaration]
ds = do
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
45 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Checking " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Int -> [Char]
forall a. Show a => a -> [Char]
show ([Declaration] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Declaration]
ds) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
" declarations..."
  (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Declaration -> TCM ()
checkDecl [Declaration]
ds

-- | Type check a single declaration.

checkDecl :: A.Declaration -> TCM ()
checkDecl :: Declaration -> TCM ()
checkDecl Declaration
d = Declaration -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Declaration
d (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking declaration"
    Declaration -> TCM ()
debugPrintDecl Declaration
d
    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
90 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (List1 Declaration -> [Char])
-> List1 Declaration
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 Declaration -> [Char]
forall a. Show a => a -> [Char]
show) (Declaration -> List1 Declaration
deepUnscopeDecl Declaration
d)
    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Declaration -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Declaration
d  -- Might loop, see e.g. Issue 1597

    let -- What kind of final checks/computations should be performed
        -- if we're not inside a mutual block?
        none :: f a -> f (Maybe a)
none        f a
m = f a
m f a -> Maybe a -> f (Maybe a)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>  Maybe a
forall a. Maybe a
Nothing           -- skip all checks
        meta :: f a -> f (Maybe (m ()))
meta        f a
m = f a
m f a -> Maybe (m ()) -> f (Maybe (m ()))
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>  m () -> Maybe (m ())
forall a. a -> Maybe a
Just (() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ())  -- do the usual checks
        mutual :: MutualInfo
-> TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ()))
mutual MutualInfo
i    TCMT IO (MutualId, Set QName)
m = TCMT IO (MutualId, Set QName)
m TCMT IO (MutualId, Set QName)
-> ((MutualId, Set QName) -> Maybe (TCM ()))
-> TCMT IO (Maybe (TCM ()))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> TCM () -> Maybe (TCM ())
forall a. a -> Maybe a
Just (TCM () -> Maybe (TCM ()))
-> ((MutualId, Set QName) -> TCM ())
-> (MutualId, Set QName)
-> Maybe (TCM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MutualId -> Set QName -> TCM ())
-> (MutualId, Set QName) -> TCM ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (MutualInfo -> Declaration -> MutualId -> Set QName -> TCM ()
mutualChecks MutualInfo
i Declaration
d)
        impossible :: f a -> f b
impossible  f a
m = f a
m f a -> b -> f b
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>  b
forall a. HasCallStack => a
__IMPOSSIBLE__
                        -- We're definitely inside a mutual block.

    (finalChecks, metas) <- TCMT IO (Maybe (TCM ()))
-> TCMT IO (Maybe (TCM ()), LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy (TCMT IO (Maybe (TCM ()))
 -> TCMT IO (Maybe (TCM ()), LocalMetaStores))
-> TCMT IO (Maybe (TCM ()))
-> TCMT IO (Maybe (TCM ()), LocalMetaStores)
forall a b. (a -> b) -> a -> b
$ case Declaration
d of
      A.Axiom{}                -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {m :: * -> *} {f :: * -> *} {a}.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ Declaration -> TCM ()
checkTypeSignature Declaration
d
      A.Generalize Set QName
s DefInfo
i ArgInfo
info QName
x Expr
e -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {m :: * -> *} {f :: * -> *} {a}.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> TCM ()
checkGeneralize Set QName
s DefInfo
i ArgInfo
info QName
x Expr
e
      A.Field{}                -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ IgnoredRecordDeclaration -> TCM ()
forall (m :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
e -> m ()
warning IgnoredRecordDeclaration
FieldOutsideRecord
      A.Primitive DefInfo
i QName
x Expr
e        -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {m :: * -> *} {f :: * -> *} {a}.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ DefInfo -> QName -> Expr -> TCM ()
checkPrimitive DefInfo
i QName
x Expr
e
      A.Mutual MutualInfo
i List1 Declaration
ds            -> MutualInfo
-> TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ()))
mutual MutualInfo
i (TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ())))
-> TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ MutualInfo -> List1 Declaration -> TCMT IO (MutualId, Set QName)
checkMutual MutualInfo
i List1 Declaration
ds
      A.Section Range
_r ModuleName
x GeneralizeTelescope
tel [Declaration]
ds    -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {m :: * -> *} {f :: * -> *} {a}.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ ModuleName -> GeneralizeTelescope -> [Declaration] -> TCM ()
checkSection ModuleName
x GeneralizeTelescope
tel [Declaration]
ds
      A.Apply ModuleInfo
i ModuleName
x ModuleApplication
mapp ScopeCopyInfo
ci ImportDirective
d    -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {m :: * -> *} {f :: * -> *} {a}.
(Monad m, Functor f) =>
f a -> f (Maybe (m ()))
meta (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ ModuleInfo
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> TCM ()
checkSectionApplication ModuleInfo
i ModuleName
x ModuleApplication
mapp ScopeCopyInfo
ci ImportDirective
d
      A.Import ModuleInfo
_ ModuleName
_ ImportDirective
dir         -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      A.Pragma Range
i Pragma
p             -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ Range -> Pragma -> TCM ()
checkPragma Range
i Pragma
p
      A.ScopedDecl ScopeInfo
scope List1 Declaration
ds    -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> TCM ()
setScope ScopeInfo
scope TCM () -> TCM () -> TCM ()
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Declaration -> TCM ()) -> List1 Declaration -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Declaration -> TCM ()
checkDeclCached List1 Declaration
ds
      A.FunDef DefInfo
i QName
x List1 Clause
cs          -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
impossible (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ QName -> DefInfo -> TCM () -> TCM ()
forall (m :: * -> *) i a.
(MonadTCEnv m, MonadDebug m, MonadBench m, BenchPhase m ~ Phase,
 AnyIsAbstract i, AllAreOpaque i) =>
QName -> i -> m a -> m a
check QName
x DefInfo
i (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ DefInfo -> QName -> [Clause] -> TCM ()
checkFunDef DefInfo
i QName
x ([Clause] -> TCM ()) -> [Clause] -> TCM ()
forall a b. (a -> b) -> a -> b
$ List1 Clause -> [Item (List1 Clause)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Clause
cs
      A.DataDef DefInfo
i QName
x PositivityCheck
pc UniverseCheck
uc DataDefParams
ps [Declaration]
cs -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
impossible (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ QName -> DefInfo -> TCM () -> TCM ()
forall (m :: * -> *) i a.
(MonadTCEnv m, MonadDebug m, MonadBench m, BenchPhase m ~ Phase,
 AnyIsAbstract i, AllAreOpaque i) =>
QName -> i -> m a -> m a
check QName
x DefInfo
i (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ DefInfo
-> QName
-> PositivityCheck
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> TCM ()
checkDataDef DefInfo
i QName
x PositivityCheck
pc UniverseCheck
uc DataDefParams
ps [Declaration]
cs
      A.RecDef DefInfo
i QName
x PositivityCheck
pc UniverseCheck
uc RecordDirectives
dir DataDefParams
ps Expr
tel [Declaration]
cs -> TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
impossible (TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ())))
-> TCMT IO (MutualId, Set QName) -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ QName
-> DefInfo
-> TCMT IO (MutualId, Set QName)
-> TCMT IO (MutualId, Set QName)
forall (m :: * -> *) i a.
(MonadTCEnv m, MonadDebug m, MonadBench m, BenchPhase m ~ Phase,
 AnyIsAbstract i, AllAreOpaque i) =>
QName -> i -> m a -> m a
check QName
x DefInfo
i (TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName))
-> TCMT IO (MutualId, Set QName) -> TCMT IO (MutualId, Set QName)
forall a b. (a -> b) -> a -> b
$ do
                                    DefInfo
-> QName
-> PositivityCheck
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> TCM ()
checkRecDef DefInfo
i QName
x PositivityCheck
pc UniverseCheck
uc RecordDirectives
dir DataDefParams
ps Expr
tel [Declaration]
cs
                                    blockId <- Definition -> MutualId
defMutual (Definition -> MutualId) -> TCMT IO Definition -> TCMT IO MutualId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
x

                                    -- Andreas, 2016-10-01 testing whether
                                    -- envMutualBlock is set correctly.
                                    -- Apparently not.
                                    verboseS "tc.decl.mutual" 70 $ do
                                      current <- viewTC eMutualBlock
                                      unless (Just blockId == current) $ do
                                        reportS "" 0
                                          [ "mutual block id discrepancy for " ++! prettyShow x
                                          , "  current    mut. bl. = " ++! show current
                                          , "  calculated mut. bl. = " ++! show blockId
                                          ]

                                    return (blockId, Set.singleton x)
      A.DataSig DefInfo
i QName
x GeneralizeTelescope
ps Expr
t       -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
impossible (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ KindOfName
-> DefInfo -> QName -> GeneralizeTelescope -> Expr -> TCM ()
checkSig KindOfName
DataName DefInfo
i QName
x GeneralizeTelescope
ps Expr
t
      A.RecSig DefInfo
i QName
x GeneralizeTelescope
ps Expr
t        -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ KindOfName
-> DefInfo -> QName -> GeneralizeTelescope -> Expr -> TCM ()
checkSig KindOfName
RecName DefInfo
i QName
x GeneralizeTelescope
ps Expr
t
                                  -- A record signature is always followed by a
                                  -- record definition. Metas should not be
                                  -- frozen until after the definition has been
                                  -- checked. NOTE: Metas are not frozen
                                  -- immediately after the last field. Perhaps
                                  -- they should be (unless we're in a mutual
                                  -- block).
      A.Open ModuleInfo
_ ModuleName
_ ImportDirective
dir           -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      A.UnfoldingDecl{}        -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      A.PatternSynDef{}        -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {a}. Functor f => f a -> f (Maybe a)
none (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                  -- Open and PatternSynDef are just artifacts
                                  -- from the concrete syntax, retained for
                                  -- highlighting purposes.
      -- Andreas, 2019-08-19, issue #4010, observe @abstract@ also for unquoting.
      -- TODO: is it possible that some of the unquoted declarations/definitions
      -- are abstract and some are not?  Then allowing all to look into abstract things,
      -- as we do here, will leak information about the implementation of abstract things.
      -- TODO: Benchmarking for unquote.
      A.UnquoteDecl MutualInfo
mi [DefInfo]
is [QName]
xs Expr
e -> [DefInfo] -> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()))
forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i) =>
i -> m a -> m a
checkMaybeAbstractly [DefInfo]
is (TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ())))
-> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ MutualInfo
-> [DefInfo] -> [QName] -> Expr -> TCMT IO (Maybe (TCM ()))
checkUnquoteDecl MutualInfo
mi [DefInfo]
is [QName]
xs Expr
e
      A.UnquoteDef [DefInfo]
is [QName]
xs Expr
e     -> TCM () -> TCMT IO (Maybe (TCM ()))
forall {f :: * -> *} {a} {b}. Functor f => f a -> f b
impossible (TCM () -> TCMT IO (Maybe (TCM ())))
-> TCM () -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ [DefInfo] -> TCM () -> TCM ()
forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i) =>
i -> m a -> m a
checkMaybeAbstractly [DefInfo]
is (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ [DefInfo] -> [QName] -> Expr -> TCM ()
checkUnquoteDef [DefInfo]
is [QName]
xs Expr
e
      A.UnquoteData [DefInfo]
is QName
x UniverseCheck
uc [DefInfo]
js [QName]
cs Expr
e -> [DefInfo] -> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()))
forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i) =>
i -> m a -> m a
checkMaybeAbstractly ([DefInfo]
is [DefInfo] -> [DefInfo] -> [DefInfo]
forall a. [a] -> [a] -> [a]
++! [DefInfo]
js) (TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ())))
-> TCMT IO (Maybe (TCM ())) -> TCMT IO (Maybe (TCM ()))
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.unquote.data" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking unquoteDecl data" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x
        Maybe (TCM ())
forall a. Maybe a
Nothing Maybe (TCM ()) -> TCMT IO [QName] -> TCMT IO (Maybe (TCM ()))
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [QName] -> Expr -> TCMT IO [QName]
unquoteTop (QName
xQName -> [QName] -> [QName]
forall a. a -> [a] -> [a]
:[QName]
cs) Expr
e

    whenNothingM (viewTC eMutualBlock) $ do

      -- Syntax highlighting.
      highlight_ DontHightlightModuleContents d

      -- Post-typing checks.
      whenJust finalChecks \TCM ()
theMutualChecks -> do
        [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Attempting to solve constraints before freezing."
        Lens' TCState Bool -> (Bool -> Bool) -> TCM () -> TCM ()
forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stInstanceHack (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TCM ()
wakeupConstraints_   -- solve emptiness and instance constraints

        checkingWhere <- Lens' TCEnv WhereClause_ -> TCMT IO WhereClause_
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (WhereClause_ -> f WhereClause_) -> TCEnv -> f TCEnv
Lens' TCEnv WhereClause_
eCheckingWhere
        wakeupConstraints_   -- Size solver might have unblocked some constraints

        case d of
          A.Generalize{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Declaration
_ -> do
            [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Freezing all open metas."
            TCMT IO (Set MetaId) -> TCM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TCMT IO (Set MetaId) -> TCM ()) -> TCMT IO (Set MetaId) -> TCM ()
forall a b. (a -> b) -> a -> b
$ [MetaId] -> TCMT IO (Set MetaId)
forall (m :: * -> *) (t :: * -> *).
(MonadTCState m, ReadTCState m, Traversable t) =>
t MetaId -> m (Set MetaId)
freezeMetas ([MetaId] -> TCMT IO (Set MetaId))
-> [MetaId] -> TCMT IO (Set MetaId)
forall a b. (a -> b) -> a -> b
$ Map MetaId MetaVariable -> [MetaId]
forall k a. Map k a -> [k]
MapS.keys (Map MetaId MetaVariable -> [MetaId])
-> Map MetaId MetaVariable -> [MetaId]
forall a b. (a -> b) -> a -> b
$ LocalMetaStores -> Map MetaId MetaVariable
openMetas LocalMetaStores
metas

        theMutualChecks

    where

    -- Switch maybe to abstract mode, benchmark, and debug print bracket.
    check :: forall m i a
          . ( MonadTCEnv m, MonadDebug m
            , MonadBench m, Bench.BenchPhase m ~ Phase
            , AnyIsAbstract i
            , AllAreOpaque i
            )
          => QName -> i -> m a -> m a
    check :: forall (m :: * -> *) i a.
(MonadTCEnv m, MonadDebug m, MonadBench m, BenchPhase m ~ Phase,
 AnyIsAbstract i, AllAreOpaque i) =>
QName -> i -> m a -> m a
check QName
x i
i m a
m = Account (BenchPhase m) -> m a -> m a
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [QName -> Phase
Bench.Definition QName
x] (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
      [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
5 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc
"Checking" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"."
      [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl.abstract" Int
25 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ IsAbstract -> [Char]
forall a. Show a => a -> [Char]
show (IsAbstract -> [Char]) -> IsAbstract -> [Char]
forall a b. (a -> b) -> a -> b
$ i -> IsAbstract
forall a. AnyIsAbstract a => a -> IsAbstract
anyIsAbstract i
i
      r <- i -> m a -> m a
forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i) =>
i -> m a -> m a
checkMaybeAbstractly i
i m a
m
      reportSDoc "tc.decl" 5 $ ("Checked" <+> prettyTCM x) <> "."
      return r

    -- Switch to AbstractMode if any of the i is AbstractDef.
    checkMaybeAbstractly :: forall m i a . ( MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i )
                         => i -> m a -> m a
    checkMaybeAbstractly :: forall (m :: * -> *) i a.
(MonadTCEnv m, AnyIsAbstract i, AllAreOpaque i) =>
i -> m a -> m a
checkMaybeAbstractly i
abs m a
cont = do
      let
        k1 :: m a -> m a
k1 = (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (ASetter TCEnv TCEnv IsAbstract IsAbstract
-> IsAbstract -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv IsAbstract IsAbstract
forall a. LensIsAbstract a => Lens' a IsAbstract
Lens' TCEnv IsAbstract
lensIsAbstract (i -> IsAbstract
forall a. AnyIsAbstract a => a -> IsAbstract
anyIsAbstract i
abs))
      k2 <- case i -> JointOpacity
forall a. AllAreOpaque a => a -> JointOpacity
jointOpacity i
abs of
        UniqueOpaque OpaqueId
i     -> (m a -> m a) -> m (m a -> m a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((m a -> m a) -> m (m a -> m a)) -> (m a -> m a) -> m (m a -> m a)
forall a b. (a -> b) -> a -> b
$ (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (ASetter TCEnv TCEnv (Maybe OpaqueId) (Maybe OpaqueId)
-> Maybe OpaqueId -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv (Maybe OpaqueId) (Maybe OpaqueId)
Lens' TCEnv (Maybe OpaqueId)
eCurrentOpaqueId (OpaqueId -> Maybe OpaqueId
forall a. a -> Maybe a
Just OpaqueId
i))
        JointOpacity
NoOpaque           -> (m a -> m a) -> m (m a -> m a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure m a -> m a
forall a. a -> a
id
        DifferentOpaque HashSet OpaqueId
hs -> m (m a -> m a)
forall a. HasCallStack => a
__IMPOSSIBLE__
      k1 (k2 cont)

-- Some checks that should be run at the end of a mutual block. The
-- set names contains the names defined in the mutual block.
mutualChecks :: Info.MutualInfo -> A.Declaration -> MutualId -> Set QName -> TCM ()
mutualChecks :: MutualInfo -> Declaration -> MutualId -> Set QName -> TCM ()
mutualChecks MutualInfo
mi Declaration
d MutualId
mid Set QName
names = do
  -- Andreas, 2014-04-11: instantiate metas in definition types
  let nameList :: [QName]
nameList = Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
names
  (QName -> TCM ()) -> [QName] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> TCM ()
instantiateDefinitionType [QName]
nameList
  -- Andreas, 2017-03-23: check positivity before termination.
  -- This allows us to reuse the information about SCCs
  -- to skip termination of non-recursive functions.
  (AllowedReductions -> AllowedReductions) -> TCM () -> TCM ()
forall (m :: * -> *) a.
MonadTCEnv m =>
(AllowedReductions -> AllowedReductions) -> m a -> m a
modifyAllowedReductions (AllowedReduction -> AllowedReductions -> AllowedReductions
forall a. SmallSetElement a => a -> SmallSet a -> SmallSet a
SmallSet.delete AllowedReduction
UnconfirmedReductions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    MutualInfo -> Set QName -> TCM ()
checkPositivity_ MutualInfo
mi Set QName
names
  -- Andreas, 2013-02-27: check termination before injectivity,
  -- to avoid making the injectivity checker loop.
  (TCEnv -> TCEnv) -> TCM () -> TCM ()
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (ASetter TCEnv TCEnv (Maybe MutualId) (Maybe MutualId)
-> Maybe MutualId -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv (Maybe MutualId) (Maybe MutualId)
Lens' TCEnv (Maybe MutualId)
eMutualBlock (MutualId -> Maybe MutualId
forall a. a -> Maybe a
Just MutualId
mid)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    Declaration -> TCM ()
checkTermination_ Declaration
d
  [QName] -> TCM ()
revisitRecordPatternTranslation [QName]
nameList -- Andreas, 2016-11-19 issue #2308

  (QName -> TCM ()) -> [QName] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> TCM ()
checkIApplyConfluence_ [QName]
nameList

  -- Andreas, 2019-07-11: The following remarks about injectivity
  -- and polarity seem outdated, since the UnusedArg Relevance has
  -- been removed.
  -- -- Andreas, 2012-09-11:  Injectivity check stores clauses
  -- -- whose 'Relevance' is affected by polarity computation,
  -- -- so do it here (again).
  -- -- Andreas, 2015-07-01:  In particular, 'UnusedArg's of local functions
  -- -- are only recognized after the polarity computation.
  -- -- See Issue 1366 for an example where injectivity of a local function
  -- -- is used to solve metas.  It fails if we do injectivity analysis
  -- -- before polarity only.
  -- However, we need to repeat injectivity checking after termination checking,
  -- since more reductions are available after termination checking, thus,
  -- more instances of injectivity can be recognized.
  Set QName -> TCM ()
checkInjectivity_        Set QName
names
  Set QName -> TCM ()
checkProjectionLikeness_ Set QName
names

-- | Check if there is a inferred eta record type in the mutual block.
--   If yes, repeat the record pattern translation for all function definitions
--   in the block.
--   This is necessary since the original record pattern translation will
--   have skipped record patterns of the new record types (as eta was off for them).
--   See issue #2308 (and #2197).
revisitRecordPatternTranslation :: [QName] -> TCM ()
revisitRecordPatternTranslation :: [QName] -> TCM ()
revisitRecordPatternTranslation [QName]
qs = do
  -- rs: inferred eta record types of this mutual block
  -- qccs: compiled clauses of definitions
  (rs, qccs) <- [Either QName (QName, CompiledClauses)]
-> ([QName], [(QName, CompiledClauses)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either QName (QName, CompiledClauses)]
 -> ([QName], [(QName, CompiledClauses)]))
-> ([Maybe (Either QName (QName, CompiledClauses))]
    -> [Either QName (QName, CompiledClauses)])
-> [Maybe (Either QName (QName, CompiledClauses))]
-> ([QName], [(QName, CompiledClauses)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (Either QName (QName, CompiledClauses))]
-> [Either QName (QName, CompiledClauses)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Either QName (QName, CompiledClauses))]
 -> ([QName], [(QName, CompiledClauses)]))
-> TCMT IO [Maybe (Either QName (QName, CompiledClauses))]
-> TCMT IO ([QName], [(QName, CompiledClauses)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCMT IO (Maybe (Either QName (QName, CompiledClauses))))
-> [QName]
-> TCMT IO [Maybe (Either QName (QName, CompiledClauses))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM QName -> TCMT IO (Maybe (Either QName (QName, CompiledClauses)))
forall {m :: * -> *}.
HasConstInfo m =>
QName -> m (Maybe (Either QName (QName, CompiledClauses)))
classify [QName]
qs
  unless (null rs) $ forM_ qccs $ \(QName
q,CompiledClauses
cc) -> do
    (cc, recordExpressionBecameCopatternLHS) <- ChangeT (TCMT IO) CompiledClauses
-> TCMT IO (CompiledClauses, Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT (TCMT IO) CompiledClauses
 -> TCMT IO (CompiledClauses, Bool))
-> ChangeT (TCMT IO) CompiledClauses
-> TCMT IO (CompiledClauses, Bool)
forall a b. (a -> b) -> a -> b
$ QName -> CompiledClauses -> ChangeT (TCMT IO) CompiledClauses
forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
QName -> CompiledClauses -> m CompiledClauses
translateCompiledClauses QName
q CompiledClauses
cc
    modifyingTC (stSignature . ix q) \Definition
def -> Definition
def
      Definition -> (Definition -> Definition) -> Definition
forall a b. a -> (a -> b) -> b
& (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ((Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
updateCompiledClauses ((Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn)
-> (Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
forall a b. (a -> b) -> a -> b
$ Maybe CompiledClauses
-> Maybe CompiledClauses -> Maybe CompiledClauses
forall a b. a -> b -> a
const (Maybe CompiledClauses
 -> Maybe CompiledClauses -> Maybe CompiledClauses)
-> Maybe CompiledClauses
-> Maybe CompiledClauses
-> Maybe CompiledClauses
forall a b. (a -> b) -> a -> b
$ CompiledClauses -> Maybe CompiledClauses
forall a. a -> Maybe a
Just CompiledClauses
cc)
      Definition -> (Definition -> Definition) -> Definition
forall a b. a -> (a -> b) -> b
& (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS (Bool -> Bool -> Bool
|| Bool
recordExpressionBecameCopatternLHS)
  where
  -- Walk through the definitions and return the set of inferred eta record types
  -- and the set of function definitions in the mutual block
  classify :: QName -> m (Maybe (Either QName (QName, CompiledClauses)))
classify QName
q = QName
-> (Definition
    -> m (Maybe (Either QName (QName, CompiledClauses))))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall (m :: * -> *) a.
HasConstInfo m =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q ((Definition -> m (Maybe (Either QName (QName, CompiledClauses))))
 -> m (Maybe (Either QName (QName, CompiledClauses))))
-> (Definition
    -> m (Maybe (Either QName (QName, CompiledClauses))))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> do
    case Definition -> Defn
theDef Definition
def of
      Record{ recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' = Inferred HasEta' PatternOrCopattern
YesEta } -> Maybe (Either QName (QName, CompiledClauses))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Either QName (QName, CompiledClauses))
 -> m (Maybe (Either QName (QName, CompiledClauses))))
-> Maybe (Either QName (QName, CompiledClauses))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall a b. (a -> b) -> a -> b
$ Either QName (QName, CompiledClauses)
-> Maybe (Either QName (QName, CompiledClauses))
forall a. a -> Maybe a
Just (Either QName (QName, CompiledClauses)
 -> Maybe (Either QName (QName, CompiledClauses)))
-> Either QName (QName, CompiledClauses)
-> Maybe (Either QName (QName, CompiledClauses))
forall a b. (a -> b) -> a -> b
$ QName -> Either QName (QName, CompiledClauses)
forall a b. a -> Either a b
Left QName
q
      Function
        { funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Left ProjectionLikenessMissing
MaybeProjection
            -- Andreas, 2017-08-10, issue #2664:
            -- Do not record pattern translate record projection definitions!
        , funCompiled :: Defn -> Maybe CompiledClauses
funCompiled   = Just CompiledClauses
cc
        } -> Maybe (Either QName (QName, CompiledClauses))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Either QName (QName, CompiledClauses))
 -> m (Maybe (Either QName (QName, CompiledClauses))))
-> Maybe (Either QName (QName, CompiledClauses))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall a b. (a -> b) -> a -> b
$ Either QName (QName, CompiledClauses)
-> Maybe (Either QName (QName, CompiledClauses))
forall a. a -> Maybe a
Just (Either QName (QName, CompiledClauses)
 -> Maybe (Either QName (QName, CompiledClauses)))
-> Either QName (QName, CompiledClauses)
-> Maybe (Either QName (QName, CompiledClauses))
forall a b. (a -> b) -> a -> b
$ (QName, CompiledClauses) -> Either QName (QName, CompiledClauses)
forall a b. b -> Either a b
Right (QName
q, CompiledClauses
cc)
      Defn
_ -> Maybe (Either QName (QName, CompiledClauses))
-> m (Maybe (Either QName (QName, CompiledClauses)))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Either QName (QName, CompiledClauses))
forall a. Maybe a
Nothing

type FinalChecks = Maybe (TCM ())

checkUnquoteDecl :: Info.MutualInfo -> [A.DefInfo] -> [QName] -> A.Expr -> TCM FinalChecks
checkUnquoteDecl :: MutualInfo
-> [DefInfo] -> [QName] -> Expr -> TCMT IO (Maybe (TCM ()))
checkUnquoteDecl MutualInfo
mi [DefInfo]
is [QName]
xs Expr
e = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.unquote.decl" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking unquoteDecl" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((QName -> TCMT IO Doc) -> [QName] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM [QName]
xs)
  Maybe (TCM ())
forall a. Maybe a
Nothing Maybe (TCM ()) -> TCMT IO [QName] -> TCMT IO (Maybe (TCM ()))
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [QName] -> Expr -> TCMT IO [QName]
unquoteTop [QName]
xs Expr
e

checkUnquoteDef :: [A.DefInfo] -> [QName] -> A.Expr -> TCM ()
checkUnquoteDef :: [DefInfo] -> [QName] -> Expr -> TCM ()
checkUnquoteDef [DefInfo]
_ [QName]
xs Expr
e = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.unquote.decl" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking unquoteDef" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((QName -> TCMT IO Doc) -> [QName] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM [QName]
xs)
  () () -> TCMT IO [QName] -> TCM ()
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [QName] -> Expr -> TCMT IO [QName]
unquoteTop [QName]
xs Expr
e

-- | Run a reflected TCM computatation expected to define a given list of
--   names.
unquoteTop :: [QName] -> A.Expr -> TCM [QName]
unquoteTop :: [QName] -> Expr -> TCMT IO [QName]
unquoteTop [QName]
xs Expr
e = do
  tcm   <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM
  unit  <- primUnit
  lzero <- primLevelZero
  let vArg = a -> Arg a
forall a. a -> Arg a
defaultArg
      hArg = Hiding -> Arg a -> Arg a
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden (Arg a -> Arg a) -> (a -> Arg a) -> a -> Arg a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Arg a
forall a. a -> Arg a
vArg
  m    <- checkExpr e $ El (mkType 0) $ apply tcm [hArg lzero, vArg unit]
  res  <- runUnquoteM $ tell xs >> evalTCM m
  case res of
    Left UnquoteError
err      -> UnquoteError -> TCMT IO [QName]
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError UnquoteError
err
    Right (Term
_, [QName]
xs) -> [QName] -> TCMT IO [QName]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [QName]
xs

-- | Instantiate all metas in 'Definition' associated to 'QName'.
--   Makes sense after freezing metas. Some checks, like free variable
--   analysis, are not in 'TCM', so they will be more precise (see issue 1099)
--   after meta instantiation.
--   Precondition: name has been added to signature already.
instantiateDefinitionType :: QName -> TCM ()
instantiateDefinitionType :: QName -> TCM ()
instantiateDefinitionType QName
q = do
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl.inst" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"instantiating type of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q
  t  <- Definition -> Type
defType (Definition -> Type)
-> (Maybe Definition -> Definition) -> Maybe Definition -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Maybe Definition -> Definition
forall a. a -> Maybe a -> a
fromMaybe Definition
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Definition -> Type)
-> TCMT IO (Maybe Definition) -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getter TCState (Maybe Definition) -> TCMT IO (Maybe Definition)
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC ((Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((Maybe Definition -> f (Maybe Definition))
    -> Signature -> f Signature)
-> (Maybe Definition -> f (Maybe Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Lens' Signature (Maybe (IxValue Signature))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index Signature
QName
q)
  t' <- instantiateFull t
  modifyingTC (stSignature . ix q) $ updateDefType $ const t'
  reportSDoc "tc.decl.inst" 30 $ vcat
    [ "  t  = " <+> prettyTCM t
    , "  t' = " <+> prettyTCM t'
    ]

data HighlightModuleContents = DontHightlightModuleContents | DoHighlightModuleContents
  deriving (HighlightModuleContents -> HighlightModuleContents -> Bool
(HighlightModuleContents -> HighlightModuleContents -> Bool)
-> (HighlightModuleContents -> HighlightModuleContents -> Bool)
-> Eq HighlightModuleContents
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HighlightModuleContents -> HighlightModuleContents -> Bool
== :: HighlightModuleContents -> HighlightModuleContents -> Bool
$c/= :: HighlightModuleContents -> HighlightModuleContents -> Bool
/= :: HighlightModuleContents -> HighlightModuleContents -> Bool
Eq)

-- | Highlight a declaration. Called after checking a mutual block (to ensure
--   we have the right definitions for all names). For modules inside mutual
--   blocks we haven't highlighted their contents, but for modules not in a
--   mutual block we have. Hence the flag.
highlight_ :: HighlightModuleContents -> A.Declaration -> TCM ()
highlight_ :: HighlightModuleContents -> Declaration -> TCM ()
highlight_ HighlightModuleContents
hlmod Declaration
d = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Highlighting a declaration with the following spine:"
      TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
    [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (DeclarationSpine -> [Char]
forall a. Show a => a -> [Char]
show (DeclarationSpine -> [Char]) -> DeclarationSpine -> [Char]
forall a b. (a -> b) -> a -> b
$ Declaration -> DeclarationSpine
A.declarationSpine Declaration
d)
  let highlight :: Declaration -> TCM ()
highlight Declaration
d = Declaration -> Level -> Bool -> TCM ()
generateAndPrintSyntaxInfo Declaration
d Level
Full Bool
True
  Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Highlighting] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ case Declaration
d of
    A.Axiom{}                -> Declaration -> TCM ()
highlight Declaration
d
    A.Field{}                -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    A.Primitive{}            -> Declaration -> TCM ()
highlight Declaration
d
    A.Mutual MutualInfo
i List1 Declaration
ds            -> (Declaration -> TCM ()) -> List1 Declaration -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HighlightModuleContents -> Declaration -> TCM ()
highlight_ HighlightModuleContents
DoHighlightModuleContents) (List1 Declaration -> TCM ()) -> List1 Declaration -> TCM ()
forall a b. (a -> b) -> a -> b
$ List1 Declaration -> List1 Declaration
forall (t :: * -> *).
DeepUnscopeDecls t =>
t Declaration -> t Declaration
deepUnscopeDecls List1 Declaration
ds
    A.Apply{}                -> Declaration -> TCM ()
highlight Declaration
d
    A.Import{}               -> Declaration -> TCM ()
highlight Declaration
d
    A.Pragma{}               -> Declaration -> TCM ()
highlight Declaration
d
    A.ScopedDecl{}           -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    A.FunDef{}               -> Declaration -> TCM ()
highlight Declaration
d
    A.DataDef{}              -> Declaration -> TCM ()
highlight Declaration
d
    A.DataSig{}              -> Declaration -> TCM ()
highlight Declaration
d
    A.Open{}                 -> Declaration -> TCM ()
highlight Declaration
d
    A.PatternSynDef{}        -> Declaration -> TCM ()
highlight Declaration
d
    A.UnfoldingDecl{}        -> Declaration -> TCM ()
highlight Declaration
d
    A.Generalize{}           -> Declaration -> TCM ()
highlight Declaration
d
    A.UnquoteDecl{}          -> Declaration -> TCM ()
highlight Declaration
d
    A.UnquoteDef{}           -> Declaration -> TCM ()
highlight Declaration
d
    A.UnquoteData{}          -> Declaration -> TCM ()
highlight Declaration
d
    A.Section Range
i ModuleName
x GeneralizeTelescope
tel [Declaration]
ds  -> do
      Declaration -> TCM ()
highlight (Range
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
A.Section Range
i ModuleName
x GeneralizeTelescope
tel [])
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (HighlightModuleContents
hlmod HighlightModuleContents -> HighlightModuleContents -> Bool
forall a. Eq a => a -> a -> Bool
== HighlightModuleContents
DoHighlightModuleContents) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HighlightModuleContents -> Declaration -> TCM ()
highlight_ HighlightModuleContents
hlmod) ([Declaration] -> [Declaration]
forall (t :: * -> *).
DeepUnscopeDecls t =>
t Declaration -> t Declaration
deepUnscopeDecls [Declaration]
ds)
    A.RecSig{}               -> Declaration -> TCM ()
highlight Declaration
d
    A.RecDef DefInfo
i QName
x PositivityCheck
pc UniverseCheck
uc RecordDirectives
dir DataDefParams
ps Expr
tel [Declaration]
cs ->
      Declaration -> TCM ()
highlight (DefInfo
-> QName
-> PositivityCheck
-> UniverseCheck
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> Declaration
A.RecDef DefInfo
i QName
x PositivityCheck
pc UniverseCheck
uc RecordDirectives
dir DataDefParams
ps Expr
dummy [Declaration]
cs)
      -- The telescope has already been highlighted.
      where
      -- Andreas, 2016-01-22, issue 1790
      -- The expression denoting the record constructor type
      -- is replace by a dummy expression in order to /not/
      -- generate highlighting from it.
      -- Simply because all the highlighting info is wrong
      -- in the record constructor type:
      -- i) fields become bound variables,
      -- ii) declarations become let-bound variables.
      -- We do not need that crap.
      dummy :: Expr
dummy = ExprInfo -> Literal -> Expr
A.Lit ExprInfo
forall a. Null a => a
empty (Literal -> Expr) -> Literal -> Expr
forall a b. (a -> b) -> a -> b
$ ArgName -> Literal
LitString (ArgName -> Literal) -> ArgName -> Literal
forall a b. (a -> b) -> a -> b
$
        ArgName
"do not highlight construct(ed/or) type"

-- | Termination check a declaration.
checkTermination_ :: A.Declaration -> TCM ()
checkTermination_ :: Declaration -> TCM ()
checkTermination_ Declaration
d = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Termination] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"checkDecl: checking termination..."
  -- If there are some termination errors, we throw a warning.
  -- The termination checker already marked non-terminating functions as such.
  TCMT IO [TerminationError]
-> (List1 TerminationError -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
Monad m =>
m [a] -> (List1 a -> m ()) -> m ()
List1.unlessNullM (Declaration -> TCMT IO [TerminationError]
termDecl Declaration
d) \ List1 TerminationError
termErrs -> do
    Warning -> TCM ()
forall (m :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
e -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ List1 TerminationError -> Warning
TerminationIssue List1 TerminationError
termErrs

-- | Check a set of mutual names for positivity.
checkPositivity_ :: Info.MutualInfo -> Set QName -> TCM ()
checkPositivity_ :: MutualInfo -> Set QName -> TCM ()
checkPositivity_ MutualInfo
mi Set QName
names = do
  -- Positivity checking.
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"checkDecl: checking positivity..."
  MutualInfo -> Set QName -> TCM ()
checkStrictlyPositive MutualInfo
mi Set QName
names

  -- Andreas, 2012-02-13: Polarity computation uses information from the
  -- positivity check, so it needs happen after the positivity check.
  [QName] -> TCM ()
computePolarity ([QName] -> TCM ()) -> [QName] -> TCM ()
forall a b. (a -> b) -> a -> b
$ Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
names

-- | Check a set of mutual names for constructor-headedness.
checkInjectivity_ :: Set QName -> TCM ()
checkInjectivity_ :: Set QName -> TCM ()
checkInjectivity_ Set QName
names = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Injectivity] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"checkDecl: checking injectivity..."
  -- Andreas, 2015-07-01, see Issue1366b:
  -- Injectivity check needs also to be run for abstract definitions.
  -- Fold.forM_ names $ \ q -> ignoreAbstractMode $ do -- NOT NECESSARY after all
  Set QName -> (QName -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Fold.forM_ Set QName
names ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
q -> QName -> (Definition -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
HasConstInfo m =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
q ((Definition -> TCM ()) -> TCM ())
-> (Definition -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Definition
def -> do
    -- For abstract q, we should be inAbstractMode,
    -- otherwise getConstInfo returns Axiom.
    --
    -- Andreas, 2015-07-01:
    -- Quite surprisingly, inAbstractMode does not allow us to look
    -- at a local definition (@where@ block) of an abstract definition.
    -- This is because the local definition is defined in a strict submodule.
    -- We can only see through abstract definitions in the current module
    -- or super modules inAbstractMode.
    -- I changed that in Monad.Signature.treatAbstractly', so we can see
    -- our own local definitions.
    case Definition -> Defn
theDef Definition
def of
      d :: Defn
d@Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funTerminates :: Defn -> Maybe Bool
funTerminates = Maybe Bool
term, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Either ProjectionLikenessMissing Projection
mproj }
        | Maybe Bool
term Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True -> do
            -- Not terminating, thus, running the injectivity check could get us into a loop.
            [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.inj.check" Int
35 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
              QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
" is not verified as terminating, thus, not considered for injectivity"
        | Defn -> Bool
isProperProjection Defn
d -> do
            [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.inj.check" Int
40 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
              QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
" is a projection, thus, not considered for injectivity"
        | Bool
otherwise -> do
            inv <- QName -> [Clause] -> TCM FunctionInverse
checkInjectivity QName
q [Clause]
cs
            setTCLens (stSignature . ix q . lensTheDef) $ d { funInv = inv }

      Defn
_ -> do
        abstr <- Lens' TCEnv AbstractMode -> TCMT IO AbstractMode
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (AbstractMode -> f AbstractMode) -> TCEnv -> f TCEnv
Lens' TCEnv AbstractMode
eAbstractMode
        reportSLn "tc.inj.check" 40 $
          "we are in " ++! show abstr ++! " and " ++
             prettyShow q ++! " is abstract or not a function, thus, not considered for injectivity"

-- | Check a set of mutual names for projection likeness.
--
--   Only a single, non-abstract function can be projection-like.
--   Making an abstract function projection-like would break the
--   invariant that the type of the principle argument of a projection-like
--   function is always inferable.

checkProjectionLikeness_ :: Set QName -> TCM ()
checkProjectionLikeness_ :: Set QName -> TCM ()
checkProjectionLikeness_ Set QName
names = Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.ProjectionLikeness] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      -- Non-mutual definitions can be considered for
      -- projection likeness
      let ds :: [QName]
ds = Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
names
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"checkDecl: checking projection-likeness of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [QName] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [QName]
ds
      case [QName]
ds of
        [QName
d] -> do
          def <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
          -- For abstract identifiers, getConstInfo returns Axiom.
          -- Thus, abstract definitions are not considered for projection-likeness.
          case theDef def of
            Function{} -> QName -> TCM ()
makeProjection (Definition -> QName
defName Definition
def)
            Defn
_          -> [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
25 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
              QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
d [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
" is abstract or not a function, thus, not considered for projection-likeness"
        [QName]
_ -> [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.proj.like" Int
25 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
               [Char]
"mutual definitions are not considered for projection-likeness"

-- | Freeze metas created by given computation if in abstract mode.
whenAbstractFreezeMetasAfter :: A.DefInfo -> TCM a -> TCM a
whenAbstractFreezeMetasAfter :: forall a. DefInfo -> TCM a -> TCM a
whenAbstractFreezeMetasAfter Info.DefInfo{Access
defAccess :: Access
defAccess :: forall t. DefInfo' t -> Access
defAccess, IsAbstract
defAbstract :: IsAbstract
defAbstract :: forall t. DefInfo' t -> IsAbstract
defAbstract, IsOpaque
defOpaque :: IsOpaque
defOpaque :: forall t. DefInfo' t -> IsOpaque
defOpaque} TCM a
m = do
  if (IsAbstract
defAbstract IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
ConcreteDef Bool -> Bool -> Bool
&& IsOpaque
defOpaque IsOpaque -> IsOpaque -> Bool
forall a. Eq a => a -> a -> Bool
== IsOpaque
TransparentDef) then TCM a
m else do
    (a, ms) <- TCM a -> TCMT IO (a, LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy TCM a
m

    reportSLn "tc.decl" 20 $ "Attempting to solve constraints before freezing."
    locallyTCState stInstanceHack (const True) $
      wakeupConstraints_   -- solve emptiness and instance constraints
    let oms = Map MetaId MetaVariable -> [MetaId]
forall k a. Map k a -> [k]
MapS.keys (Map MetaId MetaVariable -> [MetaId])
-> Map MetaId MetaVariable -> [MetaId]
forall a b. (a -> b) -> a -> b
$ LocalMetaStores -> Map MetaId MetaVariable
openMetas LocalMetaStores
ms
    xs <- freezeMetas oms

    reportSDoc "tc.decl.ax" 20 $ vcat
      [ "Abstract type signature produced new open metas: " <+>
        sep (map' prettyTCM oms)
      , "We froze the following ones of these:            " <+>
        sep (map' prettyTCM $ Set.toList xs)
      ]
    return a

checkGeneralize :: Set QName -> A.DefInfo -> ArgInfo -> QName -> A.Expr -> TCM ()
checkGeneralize :: Set QName -> DefInfo -> ArgInfo -> QName -> Expr -> TCM ()
checkGeneralize Set QName
s DefInfo
i ArgInfo
info QName
x Expr
e = do

    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl.gen" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
sep
      [ TCMT IO Doc
"checking type signature of generalizable variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e
      ]

    -- Check the signature and collect the created metas.
    (telNames, tGen) <-
      Set QName -> TCMT IO Type -> TCM ([Maybe QName], Type)
generalizeType Set QName
s (TCMT IO Type -> TCM ([Maybe QName], Type))
-> TCMT IO Type -> TCM ([Maybe QName], Type)
forall a b. (a -> b) -> a -> b
$ Lens' TCEnv DoGeneralize
-> (DoGeneralize -> DoGeneralize) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (DoGeneralize -> f DoGeneralize) -> TCEnv -> f TCEnv
Lens' TCEnv DoGeneralize
eGeneralizeMetas (DoGeneralize -> DoGeneralize -> DoGeneralize
forall a b. a -> b -> a
const DoGeneralize
YesGeneralize) (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$
        TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a. (MonadTCEnv m, MonadDebug m) => m a -> m a
workOnTypes (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO Type
isType_ Expr
e
    let n = [Maybe QName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Maybe QName]
telNames

    reportSDoc "tc.decl.gen" 10 $ sep
      [ "checked type signature of generalizable variable" <+> prettyTCM x <+> ":"
      , nest 2 $ prettyTCM tGen
      ]

    addConstant x $ defaultDefn info x tGen $
      GeneralizableVar $ SomeGeneralizableArgs n

-- | Type check an axiom.
checkAxiom :: KindOfName -> A.DefInfo -> ArgInfo ->
              Maybe PragmaPolarities -> QName -> A.Expr -> TCM ()
checkAxiom :: KindOfName
-> DefInfo
-> ArgInfo
-> Maybe PragmaPolarities
-> QName
-> Expr
-> TCM ()
checkAxiom = Maybe GeneralizeTelescope
-> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe PragmaPolarities
-> QName
-> Expr
-> TCM ()
checkAxiom' Maybe GeneralizeTelescope
forall a. Maybe a
Nothing

-- | Data and record type signatures need to remember the generalized
--   parameters for when checking the corresponding definition, so for these we
--   pass in the parameter telescope separately.
checkAxiom' :: Maybe A.GeneralizeTelescope -> KindOfName -> A.DefInfo -> ArgInfo ->
               Maybe PragmaPolarities -> QName -> A.Expr -> TCM ()
checkAxiom' :: Maybe GeneralizeTelescope
-> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe PragmaPolarities
-> QName
-> Expr
-> TCM ()
checkAxiom' Maybe GeneralizeTelescope
gentel KindOfName
kind DefInfo
i ArgInfo
info Maybe PragmaPolarities
mp QName
x Expr
e = DefInfo -> TCM () -> TCM ()
forall a. DefInfo -> TCM a -> TCM a
whenAbstractFreezeMetasAfter DefInfo
i (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  -- Andreas, 2016-07-19 issues #418 #2102:
  -- We freeze metas in type signatures of abstract definitions, to prevent
  -- leakage of implementation details.

  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl.ax" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
sep
    [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"checking type signature"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Maybe GeneralizeTelescope
-> TCMT IO Doc
-> (GeneralizeTelescope -> TCMT IO Doc)
-> TCMT IO Doc
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe GeneralizeTelescope
gentel TCMT IO Doc
"(no gentel)" ((GeneralizeTelescope -> TCMT IO Doc) -> TCMT IO Doc)
-> (GeneralizeTelescope -> TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ \ GeneralizeTelescope
_ -> TCMT IO Doc
"(has gentel)"
    ]

  let fromData :: ModTelOrigin
fromData = case KindOfName
kind of
        KindOfName
DataName -> ModTelOrigin
ModTelData
        KindOfName
_        -> ModTelOrigin
ModTelNotData

  (genParams, npars, t) <- TCMT IO ([Maybe Name], Int, Type)
-> TCMT IO ([Maybe Name], Int, Type)
forall (m :: * -> *) a. (MonadTCEnv m, MonadDebug m) => m a -> m a
workOnTypes (TCMT IO ([Maybe Name], Int, Type)
 -> TCMT IO ([Maybe Name], Int, Type))
-> TCMT IO ([Maybe Name], Int, Type)
-> TCMT IO ([Maybe Name], Int, Type)
forall a b. (a -> b) -> a -> b
$ case Maybe GeneralizeTelescope
gentel of
        Maybe GeneralizeTelescope
Nothing     -> ([], Int
0,) (Type -> ([Maybe Name], Int, Type))
-> TCMT IO Type -> TCMT IO ([Maybe Name], Int, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCMT IO Type
isType_ Expr
e
        Just GeneralizeTelescope
gentel ->
          ModTelOrigin
-> Maybe ModuleName
-> GeneralizeTelescope
-> ([Maybe Name]
    -> Tele (Dom' Term Type) -> TCMT IO ([Maybe Name], Int, Type))
-> TCMT IO ([Maybe Name], Int, Type)
forall a.
ModTelOrigin
-> Maybe ModuleName
-> GeneralizeTelescope
-> ([Maybe Name] -> Tele (Dom' Term Type) -> TCM a)
-> TCM a
checkGeneralizeTelescope ModTelOrigin
fromData Maybe ModuleName
forall a. Maybe a
Nothing GeneralizeTelescope
gentel (([Maybe Name]
  -> Tele (Dom' Term Type) -> TCMT IO ([Maybe Name], Int, Type))
 -> TCMT IO ([Maybe Name], Int, Type))
-> ([Maybe Name]
    -> Tele (Dom' Term Type) -> TCMT IO ([Maybe Name], Int, Type))
-> TCMT IO ([Maybe Name], Int, Type)
forall a b. (a -> b) -> a -> b
$
            \[Maybe Name]
genParams Tele (Dom' Term Type)
ptel -> do
              t <- TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a. (MonadTCEnv m, MonadDebug m) => m a -> m a
workOnTypes (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO Type
isType_ Expr
e
              return (genParams, size ptel, abstract ptel t)

  reportSDoc "tc.decl.ax" 10 $ sep
    [ text $ "checked type signature"
    , nest 2 $ prettyTCM x <+> ":" <+> prettyTCM t
    , nest 2 $ "of sort " <+> prettyTCM (getSort t)
    ]

  unless (null genParams) $
    reportSLn "tc.decl.ax" 40 $ "  generalized params: " ++! show genParams

  -- Jesper, 2018-06-05: should be done AFTER generalizing
  --whenM (optDoubleCheck <$> pragmaOptions) $ workOnTypes $ do
  --  checkInternal (unEl t) (sort $ getSort t)

  occs <- case mp of
    Maybe PragmaPolarities
Nothing -> [Occurrence] -> TCMT IO [Occurrence]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Just PragmaPolarities
occs1 -> do
      -- Ensure that polarity pragmas do not contain too many occurrences.
      let occs :: [Item PragmaPolarities]
occs = PragmaPolarities -> [Item PragmaPolarities]
forall l. IsList l => l -> [Item l]
List1.toList PragmaPolarities
occs1
      let m :: Int
m = [Ranged Occurrence] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Item PragmaPolarities]
[Ranged Occurrence]
occs
      TelV tel _core <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo Int
m Type
t
      let n = Tele (Dom' Term Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term Type)
tel
      when (n < m) do
        -- Andreas, 2025-05-03, #7851
        -- ifBlocked _core  then the warning might be spurious.
        -- However, postponing this check seems like an overkill.
        warning $ TooManyPolarities x $
          List1.fromListSafe __IMPOSSIBLE__ $ drop n occs

      return $ map' rangedThing occs

  -- Set blocking tag to MissingClauses if we still expect clauses
  let blk = case KindOfName
kind of
        KindOfName
FunName   -> NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (QName -> NotBlocked' Term
forall t. QName -> NotBlocked' t
MissingClauses QName
x) ()
        KindOfName
MacroName -> NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (QName -> NotBlocked' Term
forall t. QName -> NotBlocked' t
MissingClauses QName
x) ()
        KindOfName
_         -> NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
forall t. NotBlocked' t
ReallyNotBlocked ()

  -- Not safe. See Issue 330
  -- t <- addForcingAnnotations t

  let funD = FunctionData
emptyFunctionData

  let defn = ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
info QName
x Type
t (Defn -> Definition) -> Defn -> Definition
forall a b. (a -> b) -> a -> b
$
        case KindOfName
kind of   -- #4833: set abstract already here so it can be inherited by with functions
          KindOfName
FunName   -> Defn
fun
          KindOfName
MacroName -> ASetter Defn Defn Bool Bool -> Bool -> Defn -> Defn
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter Defn Defn Bool Bool
Lens' Defn Bool
funMacro Bool
True Defn
fun
          KindOfName
DataName  -> Int -> Defn
DataOrRecSig Int
npars
          KindOfName
RecName   -> Int -> Defn
DataOrRecSig Int
npars
          KindOfName
AxiomName -> Defn
defaultAxiom     -- Old comment: NB: used also for data and record type sigs
          KindOfName
_         -> Defn
forall a. HasCallStack => a
__IMPOSSIBLE__
        where
          fun :: Defn
fun = FunctionData -> Defn
FunctionDefn (FunctionData -> Defn) -> FunctionData -> Defn
forall a b. (a -> b) -> a -> b
$ ASetter FunctionData FunctionData IsAbstract IsAbstract
-> IsAbstract -> FunctionData -> FunctionData
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter FunctionData FunctionData IsAbstract IsAbstract
Lens' FunctionData IsAbstract
funAbstr_ (DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i) FunctionData
funD{ _funOpaque = Info.defOpaque i }

  let pols = (Occurrence -> Polarity) -> [Occurrence] -> [Polarity]
forall a b. (a -> b) -> [a] -> [b]
map' Occurrence -> Polarity
polFromOcc [Occurrence]
occs

  addConstant x =<< do
    useTerPragma $ defn
        { defArgOccurrences    = occs
        , defPolarity          = pols
        , defGeneralizedParams = genParams
        , defBlocked           = blk
        }

  reportSLn "tc.polarity" 10 $
    "Setting occurrences and polarity for " ++! prettyShow x ++! ":\n  " ++
    prettyShow occs ++! "\n  " ++! prettyShow pols

  -- Add the definition to the instance table, if needed
  case Info.defInstance i of
    InstanceDef KwRange
kwr -> QName -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
x (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ KwRange -> QName -> Type -> TCM ()
addTypedInstance KwRange
kwr QName
x Type
t
      -- Put highlighting on name only; including the instance keyword,
      -- like @(getRange (r,x))@, does not produce good results.
    IsInstance
NotInstanceDef -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Type check a primitive function declaration.
checkPrimitive :: A.DefInfo -> QName -> A.Expr -> TCM ()
checkPrimitive :: DefInfo -> QName -> Expr -> TCM ()
checkPrimitive DefInfo
i QName
x Expr
e =
    Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> Expr -> Call
CheckPrimitive (DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i) QName
x Expr
e) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    (name, PrimImpl t' pf) <- QName -> TCM (PrimitiveId, PrimitiveImpl)
lookupPrimitiveFunctionQ QName
x

    when (name `elem` builtinPrimitives) $ do
      reportSDoc "tc.prim" 20 $ pretty name <+> "is a BUILTIN, not a primitive!"
      typeError $ NoSuchPrimitiveFunction (getBuiltinId name)

    t <- isType_ e

    -- The reduction (and type-checking, for the constrainedPrims) rules
    -- of primitive functions assume that their arguments are actually
    -- as their type specifies, and can't handle extra quantification.
    --
    -- Instead of forbidding the definition of these primitives in
    -- parametrised modules, we can just check that the *full* type is
    -- correct.
    tel <- getContextTelescope
    inTopContext $ noConstraints $ equalType (abstract tel t) t'

    let s  = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> [Char]) -> Name -> [Char]
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
    -- Checking the ArgInfo. Currently all primitive definitions require default
    -- ArgInfos, and likely very few will have different ArgInfos in the
    -- future. Thus, rather than, the arguably nicer solution of adding an
    -- ArgInfo to PrimImpl we simply check the few special primitives here.
    bindPrimitive name pf
    addConstant x
      (defaultDefn defaultArgInfo x t Primitive
        { primAbstr    = Info.defAbstract i
        , primOpaque   = TransparentDef
        , primName     = name
        , primClauses  = []
        , primInv      = NotInjective
        , primCompiled = Nothing })
      { defArgOccurrences = primFunArgOccurrences pf }

-- | Check a pragma.
checkPragma :: Range -> A.Pragma -> TCM ()
checkPragma :: Range -> Pragma -> TCM ()
checkPragma Range
r Pragma
p = do
    let uselessPragma :: Doc -> TCM ()
uselessPragma = Warning -> TCM ()
forall (m :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
e -> m ()
warning (Warning -> TCM ()) -> (Doc -> Warning) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Doc -> Warning
UselessPragma Range
r
    Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> Pragma -> Call
CheckPragma Range
r Pragma
p) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ case Pragma
p of
        A.BuiltinPragma RString
rb ResolvedName
x
          | (BuiltinId -> Bool) -> Maybe BuiltinId -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any BuiltinId -> Bool
isUntypedBuiltin Maybe BuiltinId
b -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          | Just BuiltinId
b' <- Maybe BuiltinId
b -> BuiltinId -> ResolvedName -> TCM ()
bindBuiltin BuiltinId
b' ResolvedName
x
          | Bool
otherwise -> TypeError -> TCM ()
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
NoSuchBuiltinName ArgName
ident
          where
            ident :: ArgName
ident = RString -> ArgName
forall a. Ranged a -> a
rangedThing RString
rb
            b :: Maybe BuiltinId
b = ArgName -> Maybe BuiltinId
builtinById ArgName
ident
        A.BuiltinNoDefPragma RString
rb KindOfName
_kind QName
x
          | Just BuiltinId
b' <- ArgName -> Maybe BuiltinId
builtinById ArgName
b -> BuiltinId -> QName -> TCM ()
bindBuiltinNoDef BuiltinId
b' QName
x
          | Bool
otherwise -> TypeError -> TCM ()
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
NoSuchBuiltinName ArgName
b
          where b :: ArgName
b = RString -> ArgName
forall a. Ranged a -> a
rangedThing RString
rb
        A.CompilePragma RString
b QName
x [Char]
s -> do
          -- Check that x resides in the same module (or a child) as the pragma.
          x' <- Definition -> QName
defName (Definition -> QName) -> TCMT IO Definition -> TCMT IO QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
x  -- Get the canonical name of x.
          ifM ((x' `isInModule`) <$> currentModule)
            {- then -} (addPragma (rangedThing b) x s)
            {- else -} $ uselessPragma
              "COMPILE pragmas must appear in the same module as their corresponding definitions,"
        A.InjectivePragma QName
x -> TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> TCMT IO Bool
forall (m :: * -> *). ReadTCState m => QName -> m Bool
isLocal QName
x)
          {-then-} (QName -> TCM ()
markInjective QName
x)
          {-else-} (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM ()
uselessPragma
            Doc
"INJECTIVE pragmas must appear in the same file as their corresponding definitions"
        A.InjectiveForInferencePragma QName
x -> do
          def <- TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (TCMT IO Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
x
          unlessM (isLocal x) $ uselessPragma
            "INJECTIVE_FOR_INFERENCE directives must appear in the same file as their corresponding definitions"
          case theDef def of
            Function{} -> QName -> TCM ()
markFirstOrder QName
x
            Defn
_ -> Doc -> TCM ()
uselessPragma Doc
"INJECTIVE_FOR_INFERENCE directive only applies to functions"
        A.NotProjectionLikePragma QName
qn -> do
          def <- TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (TCMT IO Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
qn
          case theDef def of
            it :: Defn
it@Function{} ->
              TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> TCMT IO Bool
forall (m :: * -> *). ReadTCState m => QName -> m Bool
isLocal QName
qn)
                {-then-} (ASetter' TCState Defn -> Defn -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> a -> m ()
setTCLens ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Defn -> Identity Defn) -> Signature -> Identity Signature)
-> ASetter' TCState Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
qn ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Identity Defn)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef ) Defn
it{ funProjection = Left NeverProjection })
                {-else-} (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM ()
uselessPragma
                  Doc
"NOT_PROJECTION_LIKE pragmas must appear in the same file as their corresponding definitions"
            Defn
_ -> Doc -> TCM ()
uselessPragma Doc
"NOT_PROJECTION_LIKE directive only applies to functions"
        A.InlinePragma Bool
b QName
x -> do
          def <- TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (TCMT IO Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
x
          case theDef def of
            Function{} ->
              TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> TCMT IO Bool
forall (m :: * -> *). ReadTCState m => QName -> m Bool
isLocal QName
x)
                {-then-} (Bool -> QName -> TCM ()
markInline Bool
b QName
x)
                {-else-} (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM ()
uselessPragma
                  Doc
"INLINE pragmas must appear in the same file as their corresponding definitions"
            d :: Defn
d@Constructor{ ConHead
conSrcCon :: ConHead
conSrcCon :: Defn -> ConHead
conSrcCon } | ConHead -> Bool
forall a. CopatternMatchingAllowed a => a -> Bool
copatternMatchingAllowed ConHead
conSrcCon
              -> TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> TCMT IO Bool
forall (m :: * -> *). ReadTCState m => QName -> m Bool
isLocal QName
x)
                {-then-} (ASetter' TCState Defn -> Defn -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> a -> m ()
setTCLens ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Defn -> Identity Defn) -> Signature -> Identity Signature)
-> ASetter' TCState Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
x ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Identity Defn)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef) Defn
d{ conInline = b })
                {-else-} (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM ()
uselessPragma
                  Doc
"INLINE pragmas must appear in the same file as their corresponding definitions"
            Defn
_ -> Doc -> TCM ()
uselessPragma (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
forall a. [Char] -> Doc a
P.text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless Bool
b ([Char]
"NO" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) [Char]
"INLINE directive only works on functions or constructors of records that allow copattern matching"
        A.OptionsPragma{} -> Doc -> TCM ()
uselessPragma (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc
"OPTIONS pragma only allowed at beginning of file, before top module declaration"
        A.DisplayPragma QName
f [NamedArg Pattern]
ps Expr
e -> QName -> [NamedArg Pattern] -> Expr -> TCM ()
checkDisplayPragma QName
f [NamedArg Pattern]
ps Expr
e

        A.OverlapPragma QName
q OverlapMode
new -> do
          TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM ((QName
q QName -> ModuleName -> Bool
`isInModule`) (ModuleName -> Bool) -> TCMT IO ModuleName -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
            (Doc -> TCM ()
uselessPragma (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
              [Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"This" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++! [OverlapMode -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty OverlapMode
new] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
              [Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"pragma must appear in the same module as the definition of" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
              [QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q]))

            {- else -} do

          def <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
q
          case defInstance def of
            Just i :: InstanceInfo
i@InstanceInfo{ instanceOverlap :: InstanceInfo -> OverlapMode
instanceOverlap = OverlapMode
DefaultOverlap } ->
              ASetter' TCState Definition -> (Definition -> Definition) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Definition -> Identity Definition)
    -> Signature -> Identity Signature)
-> ASetter' TCState Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
q) \Definition
x -> Definition
x { defInstance = Just i{ instanceOverlap = new } }
            Just InstanceInfo{ instanceOverlap :: InstanceInfo -> OverlapMode
instanceOverlap = OverlapMode
old } -> TypeError -> TCM ()
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> OverlapMode -> OverlapMode -> TypeError
DuplicateOverlapPragma QName
q OverlapMode
old OverlapMode
new
            Maybe InstanceInfo
Nothing -> Doc -> TCM ()
uselessPragma (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< OverlapMode -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty OverlapMode
new TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"pragma can only be applied to instances"

        A.EtaPragma QName
q -> QName -> TCMT IO (Maybe RecordData)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe RecordData)
isRecord QName
q TCMT IO (Maybe RecordData)
-> (Maybe RecordData -> TCM ()) -> TCM ()
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Maybe RecordData
Nothing -> TCM ()
noRecord
            Just RecordData{ _recInduction :: RecordData -> Maybe Induction
_recInduction = Maybe Induction
ind, _recEtaEquality' :: RecordData -> EtaEquality
_recEtaEquality' = EtaEquality
eta }
              | Maybe Induction
ind Maybe Induction -> Maybe Induction -> Bool
forall a. Eq a => a -> a -> Bool
/= Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
CoInductive  -> TCM ()
noRecord
              | Specified NoEta{} <- EtaEquality
eta -> Doc -> TCM ()
uselessPragma Doc
"ETA pragma conflicts with no-eta-equality declaration"
              | Bool
otherwise -> QName -> (EtaEquality -> EtaEquality) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
QName -> (EtaEquality -> EtaEquality) -> m ()
modifyRecEta QName
q ((EtaEquality -> EtaEquality) -> TCM ())
-> (EtaEquality -> EtaEquality) -> TCM ()
forall a b. (a -> b) -> a -> b
$ EtaEquality -> EtaEquality -> EtaEquality
forall a b. a -> b -> a
const (EtaEquality -> EtaEquality -> EtaEquality)
-> EtaEquality -> EtaEquality -> EtaEquality
forall a b. (a -> b) -> a -> b
$ HasEta' PatternOrCopattern -> EtaEquality
Specified HasEta' PatternOrCopattern
forall a. HasEta' a
YesEta
          where
            noRecord :: TCM ()
noRecord = Doc -> TCM ()
uselessPragma Doc
"ETA pragma is only applicable to coinductive records"

-- | Type check a bunch of mutual inductive recursive definitions.
--
-- All definitions which have so far been assigned to the given mutual
-- block are returned.
checkMutual :: Info.MutualInfo -> List1 A.Declaration -> TCM (MutualId, Set QName)
checkMutual :: MutualInfo -> List1 Declaration -> TCMT IO (MutualId, Set QName)
checkMutual MutualInfo
i List1 Declaration
ds = (MutualId -> TCMT IO (MutualId, Set QName))
-> TCMT IO (MutualId, Set QName)
forall a. (MutualId -> TCM a) -> TCM a
inMutualBlock ((MutualId -> TCMT IO (MutualId, Set QName))
 -> TCMT IO (MutualId, Set QName))
-> (MutualId -> TCMT IO (MutualId, Set QName))
-> TCMT IO (MutualId, Set QName)
forall a b. (a -> b) -> a -> b
$ \ MutualId
blockId -> do

  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl.mutual" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
-> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
      ((TCMT IO Doc
"Checking mutual block" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (MutualId -> [Char]
forall a. Show a => a -> [Char]
show MutualId
blockId)) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
":") TCMT IO Doc -> NonEmpty (TCMT IO Doc) -> NonEmpty (TCMT IO Doc)
forall a. a -> NonEmpty a -> NonEmpty a
<|
      (Declaration -> TCMT IO Doc)
-> List1 Declaration -> NonEmpty (TCMT IO Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc)
-> (Declaration -> TCMT IO Doc) -> Declaration -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Declaration -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA) List1 Declaration
ds

  MutualId -> MutualInfo -> TCM ()
insertMutualBlockInfo MutualId
blockId MutualInfo
i
  (TCEnv -> TCEnv) -> TCM () -> TCM ()
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ( ASetter TCEnv TCEnv TerminationCheck TerminationCheck
-> TerminationCheck -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv TerminationCheck TerminationCheck
Lens' TCEnv TerminationCheck
eTerminationCheck (MutualInfo -> TerminationCheck
Info.mutualTerminationCheck MutualInfo
i)
          (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter TCEnv TCEnv CoverageCheck CoverageCheck
-> CoverageCheck -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv CoverageCheck CoverageCheck
Lens' TCEnv CoverageCheck
eCoverageCheck (MutualInfo -> CoverageCheck
Info.mutualCoverageCheck MutualInfo
i)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    (Declaration -> TCM ()) -> List1 Declaration -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Declaration -> TCM ()
checkDecl List1 Declaration
ds

  (MutualId
blockId, ) (Set QName -> (MutualId, Set QName))
-> (MutualBlock -> Set QName)
-> MutualBlock
-> (MutualId, Set QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MutualBlock -> Set QName
mutualNames (MutualBlock -> (MutualId, Set QName))
-> TCMT IO MutualBlock -> TCMT IO (MutualId, Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MutualId -> TCMT IO MutualBlock
forall (tcm :: * -> *).
ReadTCState tcm =>
MutualId -> tcm MutualBlock
lookupMutualBlock MutualId
blockId

    -- check record or data type signature
checkSig ::
  KindOfName -> A.DefInfo -> QName -> A.GeneralizeTelescope ->
  A.Expr -> TCM ()
checkSig :: KindOfName
-> DefInfo -> QName -> GeneralizeTelescope -> Expr -> TCM ()
checkSig KindOfName
kind DefInfo
i QName
x GeneralizeTelescope
gtel Expr
t =
  Maybe GeneralizeTelescope -> Declaration -> TCM ()
checkTypeSignature' (GeneralizeTelescope -> Maybe GeneralizeTelescope
forall a. a -> Maybe a
Just GeneralizeTelescope
gtel) (Declaration -> TCM ()) -> Declaration -> TCM ()
forall a b. (a -> b) -> a -> b
$
  KindOfName
-> DefInfo
-> Origin
-> Maybe PragmaPolarities
-> QName
-> Expr
-> Declaration
A.Axiom KindOfName
kind DefInfo
i Origin
UserWritten
    Maybe PragmaPolarities
forall a. Maybe a
Nothing QName
x Expr
t

-- | Type check the type signature of an inductive or recursive definition.
checkTypeSignature :: A.TypeSignature -> TCM ()
checkTypeSignature :: Declaration -> TCM ()
checkTypeSignature = Maybe GeneralizeTelescope -> Declaration -> TCM ()
checkTypeSignature' Maybe GeneralizeTelescope
forall a. Maybe a
Nothing

checkTypeSignature' :: Maybe A.GeneralizeTelescope -> A.TypeSignature -> TCM ()
checkTypeSignature' :: Maybe GeneralizeTelescope -> Declaration -> TCM ()
checkTypeSignature' Maybe GeneralizeTelescope
gtel (A.ScopedDecl ScopeInfo
scope List1 Declaration
ds) = do
  ScopeInfo -> TCM ()
setScope ScopeInfo
scope
  (Declaration -> TCM ()) -> List1 Declaration -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Maybe GeneralizeTelescope -> Declaration -> TCM ()
checkTypeSignature' Maybe GeneralizeTelescope
gtel) List1 Declaration
ds
checkTypeSignature' Maybe GeneralizeTelescope
gtel (A.Axiom KindOfName
funSig DefInfo
i Origin
orig Maybe PragmaPolarities
mp QName
x Expr
e) =
  Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [QName -> Phase
Bench.Definition QName
x] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
  Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Typing, BenchPhase (TCMT IO)
Phase
Bench.TypeSig] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    let abstr :: TCM () -> TCM ()
abstr = case DefInfo -> Access
forall t. DefInfo' t -> Access
Info.defAccess DefInfo
i of
          PrivateAccess{}
            | DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
AbstractDef -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
              -- Issue #2321, only go to AbstractMode for abstract definitions
              -- Issue #418, #3744, in fact don't go to AbstractMode at all
            | Bool
otherwise -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
          Access
PublicAccess  -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
    in TCM () -> TCM ()
abstr (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Maybe GeneralizeTelescope
-> KindOfName
-> DefInfo
-> ArgInfo
-> Maybe PragmaPolarities
-> QName
-> Expr
-> TCM ()
checkAxiom' Maybe GeneralizeTelescope
gtel KindOfName
funSig DefInfo
i (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
orig ArgInfo
defaultArgInfo) Maybe PragmaPolarities
mp QName
x Expr
e
checkTypeSignature' Maybe GeneralizeTelescope
_ Declaration
_ =
  TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__   -- type signatures are always axioms


-- | Type check a module.

checkSection ::
  ModuleName -> A.GeneralizeTelescope -> [A.Declaration] ->
  TCM ()
checkSection :: ModuleName -> GeneralizeTelescope -> [Declaration] -> TCM ()
checkSection ModuleName
x GeneralizeTelescope
tel [Declaration]
ds =
  ModuleName -> GeneralizeTelescope -> TCM () -> TCM ()
forall a. ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
newSection ModuleName
x GeneralizeTelescope
tel (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Declaration -> TCM ()
checkDeclCached [Declaration]
ds


-- | Helper for 'checkSectionApplication'.
--
--   Matches the arguments of the module application with the
--   module parameters.
--
--   Returns the remaining module parameters as an open telescope.
--   Warning: the returned telescope is /not/ the final result,
--   an actual instantiation of the parameters does not occur.
checkModuleArity ::
     ModuleName           -- ^ Name of applied module.
  -> Telescope            -- ^ The module parameters.
  -> [NamedArg A.Expr]    -- ^ The arguments this module is applied to.
  -> TCM Telescope        -- ^ The remaining module parameters (has free de Bruijn indices!).
checkModuleArity :: ModuleName
-> Tele (Dom' Term Type)
-> [NamedArg Expr]
-> TCMT IO (Tele (Dom' Term Type))
checkModuleArity ModuleName
m Tele (Dom' Term Type)
tel = \case
  []   -> Tele (Dom' Term Type) -> TCMT IO (Tele (Dom' Term Type))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Tele (Dom' Term Type)
tel
  NamedArg Expr
a:[NamedArg Expr]
as -> Tele (Dom' Term Type)
-> NamedArg Expr
-> [NamedArg Expr]
-> TCMT IO (Tele (Dom' Term Type))
check1 Tele (Dom' Term Type)
tel NamedArg Expr
a [NamedArg Expr]
as
    where
    bad :: TCMT IO (Tele (Dom' Term Type))
bad = TypeError -> TCMT IO (Tele (Dom' Term Type))
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCMT IO (Tele (Dom' Term Type)))
-> TypeError -> TCMT IO (Tele (Dom' Term Type))
forall a b. (a -> b) -> a -> b
$ ModuleName
-> Tele (Dom' Term Type)
-> Either (List1 (NamedArg Expr)) [Arg Term]
-> TypeError
ModuleArityMismatch ModuleName
m Tele (Dom' Term Type)
tel (List1 (NamedArg Expr) -> Either (List1 (NamedArg Expr)) [Arg Term]
forall a b. a -> Either a b
Left (NamedArg Expr
a NamedArg Expr -> [NamedArg Expr] -> List1 (NamedArg Expr)
forall a. a -> [a] -> NonEmpty a
:| [NamedArg Expr]
as))

    check :: Telescope -> [NamedArg A.Expr] -> TCM Telescope
    check :: Tele (Dom' Term Type)
-> [NamedArg Expr] -> TCMT IO (Tele (Dom' Term Type))
check Tele (Dom' Term Type)
tel []             = Tele (Dom' Term Type) -> TCMT IO (Tele (Dom' Term Type))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Tele (Dom' Term Type)
tel
    check Tele (Dom' Term Type)
tel (NamedArg Expr
a : [NamedArg Expr]
as)       = Tele (Dom' Term Type)
-> NamedArg Expr
-> [NamedArg Expr]
-> TCMT IO (Tele (Dom' Term Type))
check1 Tele (Dom' Term Type)
tel NamedArg Expr
a [NamedArg Expr]
as

    check1 :: Telescope -> NamedArg A.Expr -> [NamedArg A.Expr] -> TCM Telescope
    check1 :: Tele (Dom' Term Type)
-> NamedArg Expr
-> [NamedArg Expr]
-> TCMT IO (Tele (Dom' Term Type))
check1 Tele (Dom' Term Type)
EmptyTel NamedArg Expr
_ [NamedArg Expr]
_ = TCMT IO (Tele (Dom' Term Type))
bad
    check1 (ExtendTel dom :: Dom' Term Type
dom@(Getting ArgInfo (Dom' Term Type) ArgInfo
-> Dom' Term Type -> ArgInfo
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo -> ArgInfo
info) Abs (Tele (Dom' Term Type))
btel) arg0 :: NamedArg Expr
arg0@(Arg ArgInfo
info' Named_ Expr
arg) [NamedArg Expr]
args = do
      let name :: Maybe ArgName
name = Named_ Expr -> Maybe ArgName
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameOf Named_ Expr
arg
          my :: Maybe ArgName
my   = Dom' Term Type -> Maybe ArgName
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameOf Dom' Term Type
dom
          tel :: Tele (Dom' Term Type)
tel  = Abs (Tele (Dom' Term Type)) -> Tele (Dom' Term Type)
forall a. Subst a => Abs a -> a
absBody Abs (Tele (Dom' Term Type))
btel
      case (ArgInfo -> Hiding
argInfoHiding ArgInfo
info, ArgInfo -> Hiding
argInfoHiding ArgInfo
info', Maybe ArgName
name) of
        (Instance{}, Hiding
NotHidden, Maybe ArgName
_)        -> Tele (Dom' Term Type)
-> NamedArg Expr
-> [NamedArg Expr]
-> TCMT IO (Tele (Dom' Term Type))
check1 Tele (Dom' Term Type)
tel NamedArg Expr
arg0 [NamedArg Expr]
args
        (Instance{}, Hiding
Hidden, Maybe ArgName
_)           -> Tele (Dom' Term Type)
-> NamedArg Expr
-> [NamedArg Expr]
-> TCMT IO (Tele (Dom' Term Type))
check1 Tele (Dom' Term Type)
tel NamedArg Expr
arg0 [NamedArg Expr]
args
        (Instance{}, Instance{}, Maybe ArgName
Nothing) -> Tele (Dom' Term Type)
-> [NamedArg Expr] -> TCMT IO (Tele (Dom' Term Type))
check  Tele (Dom' Term Type)
tel [NamedArg Expr]
args
        (Instance{}, Instance{}, Just ArgName
x)
          | ArgName -> Maybe ArgName
forall a. a -> Maybe a
Just ArgName
x Maybe ArgName -> Maybe ArgName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe ArgName
my                  -> Tele (Dom' Term Type)
-> [NamedArg Expr] -> TCMT IO (Tele (Dom' Term Type))
check  Tele (Dom' Term Type)
tel [NamedArg Expr]
args
          | Bool
otherwise                     -> Tele (Dom' Term Type)
-> NamedArg Expr
-> [NamedArg Expr]
-> TCMT IO (Tele (Dom' Term Type))
check1 Tele (Dom' Term Type)
tel NamedArg Expr
arg0 [NamedArg Expr]
args
        (Hiding
Hidden, Hiding
NotHidden, Maybe ArgName
_)            -> Tele (Dom' Term Type)
-> NamedArg Expr
-> [NamedArg Expr]
-> TCMT IO (Tele (Dom' Term Type))
check1 Tele (Dom' Term Type)
tel NamedArg Expr
arg0 [NamedArg Expr]
args
        (Hiding
Hidden, Instance{}, Maybe ArgName
_)           -> Tele (Dom' Term Type)
-> NamedArg Expr
-> [NamedArg Expr]
-> TCMT IO (Tele (Dom' Term Type))
check1 Tele (Dom' Term Type)
tel NamedArg Expr
arg0 [NamedArg Expr]
args
        (Hiding
Hidden, Hiding
Hidden, Maybe ArgName
Nothing)         -> Tele (Dom' Term Type)
-> [NamedArg Expr] -> TCMT IO (Tele (Dom' Term Type))
check  Tele (Dom' Term Type)
tel [NamedArg Expr]
args
        (Hiding
Hidden, Hiding
Hidden, Just ArgName
x)
          | ArgName -> Maybe ArgName
forall a. a -> Maybe a
Just ArgName
x Maybe ArgName -> Maybe ArgName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe ArgName
my                  -> Tele (Dom' Term Type)
-> [NamedArg Expr] -> TCMT IO (Tele (Dom' Term Type))
check  Tele (Dom' Term Type)
tel [NamedArg Expr]
args
          | Bool
otherwise                     -> Tele (Dom' Term Type)
-> NamedArg Expr
-> [NamedArg Expr]
-> TCMT IO (Tele (Dom' Term Type))
check1 Tele (Dom' Term Type)
tel NamedArg Expr
arg0 [NamedArg Expr]
args
        (Hiding
NotHidden, Hiding
NotHidden, Maybe ArgName
_)         -> Tele (Dom' Term Type)
-> [NamedArg Expr] -> TCMT IO (Tele (Dom' Term Type))
check  Tele (Dom' Term Type)
tel [NamedArg Expr]
args
        (Hiding
NotHidden, Hiding
Hidden, Maybe ArgName
_)            -> TCMT IO (Tele (Dom' Term Type))
bad
        (Hiding
NotHidden, Instance{}, Maybe ArgName
_)        -> TCMT IO (Tele (Dom' Term Type))
bad

-- | Check an application of a section.
checkSectionApplication
  :: Info.ModuleInfo
  -> ModuleName          -- ^ Name @m1@ of module defined by the module macro.
  -> A.ModuleApplication -- ^ The module macro @λ tel → m2 args@.
  -> A.ScopeCopyInfo     -- ^ Imported names and modules
  -> A.ImportDirective
  -> TCM ()
checkSectionApplication :: ModuleInfo
-> ModuleName
-> ModuleApplication
-> ScopeCopyInfo
-> ImportDirective
-> TCM ()
checkSectionApplication ModuleInfo
i ModuleName
m1 ModuleApplication
modapp ScopeCopyInfo
copyInfo ImportDirective
dir =
  Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> ModuleName -> ModuleApplication -> Call
CheckSectionApplication (ModuleInfo -> Range
forall a. HasRange a => a -> Range
getRange ModuleInfo
i) ModuleName
m1 ModuleApplication
modapp) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  ModuleInfo
-> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
checkSectionApplication' ModuleInfo
i ModuleName
m1 ModuleApplication
modapp ScopeCopyInfo
copyInfo

-- | Check an application of a section. (Do not invoke this procedure
-- directly, use 'checkSectionApplication'.)
checkSectionApplication'
  :: Info.ModuleInfo
  -> ModuleName          -- ^ Name @m1@ of module defined by the module macro.
  -> A.ModuleApplication -- ^ The module macro @λ tel → m2 args@.
  -> A.ScopeCopyInfo     -- ^ Imported names and modules
  -> TCM ()
checkSectionApplication' :: ModuleInfo
-> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
checkSectionApplication'
  ModuleInfo
i ModuleName
m1 (A.SectionApp Telescope
ptel ModuleName
m2 [NamedArg Expr]
args) ScopeCopyInfo
copyInfo =
  Account (BenchPhase (TCMT IO)) -> TCM () -> TCM ()
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Typing, BenchPhase (TCMT IO)
Phase
Bench.ApplySection]
  do
  -- Module applications can appear in lets, in which case we treat
  -- lambda-bound variables as additional parameters to the module.
  extraParams <- do
    mfv <- TCM Int
getCurrentModuleFreeVars
    fv  <- getContextSize
    return (fv - mfv)
  when (extraParams > 0) $ reportSLn "tc.mod.apply" 30 $ "Extra parameters to " ++! prettyShow m1 ++! ": " ++! show extraParams
  -- Type-check the LHS (ptel) of the module macro.
  checkTelescope ModTelNotData ptel $ \ Tele (Dom' Term Type)
ptel -> do
    -- We are now in the context @ptel@.
    -- Get the correct parameter telescope of @m2@. This is the fully lifted
    -- telescope obtained by `lookupSection` instantiated with the module
    -- parameters of `m2` currently in scope. For instance
    -- ```
    --  module _ (A : Type) where
    --    module M (B : Type) where ...
    --    module M' = M B
    -- ```
    -- In the application `M' = M B`, `tel = (A B : Type)` and
    -- `moduleParamsToApply M = [A]`, so the resulting parameter telescope is
    -- `tel' = (B : Type)`.
    tel <- ModuleName -> TCMT IO (Tele (Dom' Term Type))
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Tele (Dom' Term Type))
lookupSection ModuleName
m2
    vs  <- moduleParamsToApply m2
    let tel'  = Tele (Dom' Term Type) -> [Arg Term] -> Tele (Dom' Term Type)
forall t. Apply t => t -> [Arg Term] -> t
apply Tele (Dom' Term Type)
tel [Arg Term]
vs
    -- Compute the remaining parameter telescope after stripping of
    -- the initial parameters that are determined by the @args@.
    -- Warning: @etaTel@ is not well-formed in @ptel@, since
    -- the actual application has not happened.
    etaTel <- checkModuleArity m2 tel' args
    -- Take the module parameters that will be instantiated by @args@.
    let tel'' = ListTel -> Tele (Dom' Term Type)
telFromList (ListTel -> Tele (Dom' Term Type))
-> ListTel -> Tele (Dom' Term Type)
forall a b. (a -> b) -> a -> b
$ Int -> ListTel -> ListTel
forall a. Int -> [a] -> [a]
take (Tele (Dom' Term Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term Type)
tel' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom' Term Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term Type)
etaTel) (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term Type) -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom' Term Type)
tel'
    reportSDoc "tc.mod.apply" 15 $
        "applying section" <+> prettyTCM m2
    reportSDoc "tc.mod.apply" 15 $
        nest 2 $ "args =" <+> sep (map' prettyA args)
    reportSDoc "tc.mod.apply" 15 $
        nest 2 $ "ptel =" <+> escapeContext impossible (size ptel) (prettyTCM ptel)
    reportSDoc "tc.mod.apply" 15 $
        nest 2 $ "tel  =" <+> prettyTCM tel
    reportSDoc "tc.mod.apply" 15 $
        nest 2 $ "tel' =" <+> prettyTCM tel'
    reportSDoc "tc.mod.apply" 15 $
        nest 2 $ "tel''=" <+> prettyTCM tel''
    reportSDoc "tc.mod.apply" 15 $
        nest 2 $ "eta  =" <+> escapeContext impossible (size ptel) (addContext tel'' $ prettyTCM etaTel)

    -- Now, type check arguments.
    -- Andreas, 2024-12-06: We fake a head A.Expr for the application.
    let
      hd = QName -> Expr
A.Def (QName -> Expr) -> QName -> Expr
forall a b. (a -> b) -> a -> b
$ ModuleName -> QName
mnameToQName ModuleName
m2
      -- Amy, 2025-04-16, issue #7799: for parity with checking
      -- declaration right-hand-sides we have to check section
      -- applications with the 'instance hack' enabled.
      k = Lens' TCState Bool -> (Bool -> Bool) -> TCMT IO b -> TCMT IO b
forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stInstanceHack (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (TCMT IO b -> TCMT IO b)
-> (TCMT IO b -> TCMT IO b) -> TCMT IO b -> TCMT IO b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCMT IO b -> TCMT IO b
forall (m :: * -> *) a.
(MonadConstraint m, MonadFresh ProblemId m) =>
m a -> m a
noConstraints

    ts <- k (checkArguments_ CmpEq DontExpandLast hd args tel') >>= \case
      (Elims
ts', Tele (Dom' Term Type)
etaTel') | (Tele (Dom' Term Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term Type)
etaTel Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Tele (Dom' Term Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term Type)
etaTel')
                     , Just [Arg Term]
ts <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
ts' -> [Arg Term] -> TCMT IO [Arg Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Arg Term]
ts
      (Elims, Tele (Dom' Term Type))
_ -> TCMT IO [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__
    -- Perform the application of the module parameters.
    let aTel = Tele (Dom' Term Type)
tel' Tele (Dom' Term Type) -> [Arg Term] -> Tele (Dom' Term Type)
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
ts
    reportSDoc "tc.mod.apply" 15 $ vcat
      [ nest 2 $ "aTel =" <+> prettyTCM aTel
      ]
    -- Andreas, 2014-04-06, Issue 1094:
    -- Add the section with well-formed telescope.
    -- Nathaniel, 2026-02-08:
    ctxTel <- getContextTelescope
    reportSDoc "tc.mod.apply" 80 $
        "addSection" <+> prettyTCM m1 <+>
        (inTopContext $ prettyTCM $ ctxTel `abstract` aTel)
    addSection' m1 $ ctxTel `abstract` aTel

    reportSDoc "tc.mod.apply" 20 $ vcat
      [ sep [ "applySection", prettyTCM m1, "=", prettyTCM m2, fsep $ map' prettyTCM (vs ++! ts) ]
      , nest 2 $ pretty copyInfo
      ]

    args <- instantiateFull $ vs ++! ts

    -- If we want to avoid eta-expanding modules (while supporting the current
    -- 'open public' behaviour) we should also change 'renName'/'renMod'
    -- in Agda.Syntax.Scope.Monad
    -- See #8443
    let n = Tele (Dom' Term Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term Type)
aTel
    etaArgs <- inTopContext $ addContext aTel getContextArgs
    addContext (KeepNames aTel) $
      applySection m1 (ptel `abstract` aTel) m2 (raise n args ++! etaArgs) copyInfo

checkSectionApplication'
  ModuleInfo
i ModuleName
m1 (A.RecordModuleInstance ModuleName
x) ScopeCopyInfo
copyInfo = do
  let name :: QName
name = ModuleName -> QName
mnameToQName ModuleName
x
  tel' <- ModuleName -> TCMT IO (Tele (Dom' Term Type))
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Tele (Dom' Term Type))
lookupSection ModuleName
x
  vs   <- moduleParamsToApply x
  let tel = Tele (Dom' Term Type)
tel' Tele (Dom' Term Type) -> [Arg Term] -> Tele (Dom' Term Type)
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
vs
      args = Tele (Dom' Term Type) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom' Term Type)
tel

      telInst :: Telescope
      telInst = Tele (Dom' Term Type) -> Tele (Dom' Term Type)
instFinal Tele (Dom' Term Type)
tel

      -- Locate last (rightmost) parameter and make it @Instance@.
      -- Issue #3463: also name it so it can be given by name.
      instFinal :: Telescope -> Telescope
      -- Telescopes do not have @NoAbs@.
      instFinal (ExtendTel Dom' Term Type
_ NoAbs{}) = Tele (Dom' Term Type)
forall a. HasCallStack => a
__IMPOSSIBLE__
      -- Found last parameter: switch it to @Instance@.
      instFinal (ExtendTel Dom' Term Type
dom (Abs ArgName
n Tele (Dom' Term Type)
EmptyTel)) =
                 Dom' Term Type
-> Abs (Tele (Dom' Term Type)) -> Tele (Dom' Term Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' Term Type
do' (ArgName -> Tele (Dom' Term Type) -> Abs (Tele (Dom' Term Type))
forall a. ArgName -> a -> Abs a
Abs ArgName
n Tele (Dom' Term Type)
forall a. Tele a
EmptyTel)
        where do' :: Dom' Term Type
do' = Dom' Term Type -> Dom' Term Type
forall a. LensHiding a => a -> a
makeInstance (Dom' Term Type
dom Dom' Term Type
-> (Dom' Term Type -> Dom' Term Type) -> Dom' Term Type
forall a b. a -> (a -> b) -> b
& (Maybe (NameOf (Dom' Term Type))
 -> Identity (Maybe (NameOf (Dom' Term Type))))
-> Dom' Term Type -> Identity (Dom' Term Type)
(Maybe NamedName -> Identity (Maybe NamedName))
-> Dom' Term Type -> Identity (Dom' Term Type)
forall a. LensNamed a => Lens' a (Maybe (NameOf a))
Lens' (Dom' Term Type) (Maybe (NameOf (Dom' Term Type)))
lensNamed ((Maybe NamedName -> Identity (Maybe NamedName))
 -> Dom' Term Type -> Identity (Dom' Term Type))
-> NamedName -> Dom' Term Type -> Dom' Term Type
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ Origin -> RString -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (ArgName -> RString
forall a. a -> Ranged a
unranged ArgName
"r"))
      -- Otherwise, keep searchinf for last parameter:
      instFinal (ExtendTel Dom' Term Type
arg (Abs ArgName
n Tele (Dom' Term Type)
tel)) =
                 Dom' Term Type
-> Abs (Tele (Dom' Term Type)) -> Tele (Dom' Term Type)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' Term Type
arg (ArgName -> Tele (Dom' Term Type) -> Abs (Tele (Dom' Term Type))
forall a. ArgName -> a -> Abs a
Abs ArgName
n (Tele (Dom' Term Type) -> Tele (Dom' Term Type)
instFinal Tele (Dom' Term Type)
tel))
      -- Before instFinal is invoked, we have checked that the @tel@ is not empty.
      instFinal Tele (Dom' Term Type)
EmptyTel = Tele (Dom' Term Type)
forall a. HasCallStack => a
__IMPOSSIBLE__

  reportSDoc "tc.mod.apply" 20 $ vcat
    [ sep [ "applySection", prettyTCM name, "{{...}}" ]
    , nest 2 $ "x       =" <+> prettyTCM x
    , nest 2 $ "name    =" <+> prettyTCM name
    , nest 2 $ "tel     =" <+> prettyTCM tel
    , nest 2 $ "telInst =" <+> prettyTCM telInst
    , nest 2 $ "vs      =" <+> sep (map' prettyTCM vs)
    -- , nest 2 $ "args    =" <+> sep (map' prettyTCM args)
    ]
  reportSDoc "tc.mod.apply" 60 $ vcat
    [ nest 2 $ "vs      =" <+> text (show vs)
    -- , nest 2 $ "args    =" <+> text (show args)
    ]
  when (tel == EmptyTel) $ typeError $ ModuleArityMismatch x EmptyTel (Right vs)

  addContext telInst $ do
    vs <- moduleParamsToApply x
    reportSDoc "tc.mod.apply" 20 $ vcat
      [ nest 2 $ "vs      =" <+> sep (map' prettyTCM vs)
      , nest 2 $ "args    =" <+> sep (map' (parens . prettyTCM) args)
      ]
    reportSDoc "tc.mod.apply" 60 $ vcat
      [ nest 2 $ "vs      =" <+> text (show vs)
      , nest 2 $ "args    =" <+> text (show args)
      ]
    addSection m1
    applySection m1 telInst x (vs ++! args) copyInfo

------------------------------------------------------------------------
-- * Debugging
------------------------------------------------------------------------

class ShowHead a where
  showHead :: a -> String

instance ShowHead A.Declaration where
  showHead :: Declaration -> [Char]
showHead Declaration
d =
    case Declaration
d of
      A.Axiom        {} -> [Char]
"Axiom"
      A.Field        {} -> [Char]
"Field"
      A.Primitive    {} -> [Char]
"Primitive"
      A.Mutual       {} -> [Char]
"Mutual"
      A.Section      {} -> [Char]
"Section"
      A.Apply        {} -> [Char]
"Apply"
      A.Import       {} -> [Char]
"Import"
      A.Pragma       {} -> [Char]
"Pragma"
      A.Open         {} -> [Char]
"Open"
      A.FunDef       {} -> [Char]
"FunDef"
      A.DataSig      {} -> [Char]
"DataSig"
      A.DataDef      {} -> [Char]
"DataDef"
      A.RecSig       {} -> [Char]
"RecSig"
      A.RecDef       {} -> [Char]
"RecDef"
      A.PatternSynDef{} -> [Char]
"PatternSynDef"
      A.Generalize   {} -> [Char]
"Generalize"
      A.UnquoteDecl  {} -> [Char]
"UnquoteDecl"
      A.ScopedDecl   {} -> [Char]
"ScopedDecl"
      A.UnquoteDef   {} -> [Char]
"UnquoteDef"
      A.UnquoteData  {} -> [Char]
"UnquoteDecl data"
      A.UnfoldingDecl{} -> [Char]
"UnfoldingDecl"

debugPrintDecl :: A.Declaration -> TCM ()
debugPrintDecl :: Declaration -> TCM ()
debugPrintDecl Declaration
d = do
    [Char] -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.decl" Int
45 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
45 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"checking a " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Declaration -> [Char]
forall a. ShowHead a => a -> [Char]
showHead Declaration
d
      case Declaration
d of
        A.Section Range
info ModuleName
mname GeneralizeTelescope
tel [Declaration]
ds -> do
          [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl" Int
45 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
            [Char]
"section " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ModuleName
mname [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
" has "
              [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Int -> [Char]
forall a. Show a => a -> [Char]
show (Telescope -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Telescope -> Int) -> Telescope -> Int
forall a b. (a -> b) -> a -> b
$ GeneralizeTelescope -> Telescope
A.generalizeTel GeneralizeTelescope
tel) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
" parameters and "
              [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! Int -> [Char]
forall a. Show a => a -> [Char]
show ([Declaration] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Declaration]
ds) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
" declarations"
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
            Declaration -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Declaration -> TCMT IO Doc) -> Declaration -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Range
-> ModuleName
-> GeneralizeTelescope
-> [Declaration]
-> Declaration
A.Section Range
info ModuleName
mname GeneralizeTelescope
tel []
          [Declaration] -> (Declaration -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Declaration]
ds ((Declaration -> TCM ()) -> TCM ())
-> (Declaration -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Declaration
d -> do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.decl" Int
45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Declaration -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Declaration
d
        Declaration
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()