summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rules/Decl.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/Decl.hs')
-rw-r--r--src/full/Agda/TypeChecking/Rules/Decl.hs254
1 files changed, 163 insertions, 91 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/Decl.hs b/src/full/Agda/TypeChecking/Rules/Decl.hs
index 86a5335..db68dd9 100644
--- a/src/full/Agda/TypeChecking/Rules/Decl.hs
+++ b/src/full/Agda/TypeChecking/Rules/Decl.hs
@@ -1,21 +1,21 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TupleSections #-}
-
-#if __GLASGOW_HASKELL__ >= 710
-{-# LANGUAGE FlexibleContexts #-}
-#endif
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Decl where
+import Prelude hiding (null)
+
import Control.Monad
import Control.Monad.Reader
-import Control.Monad.State (modify, gets)
+import Control.Monad.State (modify, gets, get)
import Control.Monad.Writer (tell)
+import Data.Either (partitionEithers)
import qualified Data.Foldable as Fold
+import Data.List (genericLength)
import Data.Maybe
import Data.Map (Map)
+import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import Data.Set (Set)
@@ -45,6 +45,7 @@ import Agda.TypeChecking.Errors
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Positivity
+import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
@@ -52,6 +53,7 @@ import Agda.TypeChecking.ProjectionLike
import Agda.TypeChecking.Quote
import Agda.TypeChecking.Unquote
import Agda.TypeChecking.Records
+import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rewriting
import Agda.TypeChecking.SizedTypes.Solve
@@ -62,18 +64,21 @@ import Agda.TypeChecking.Unquote
import Agda.TypeChecking.Rules.Term
import Agda.TypeChecking.Rules.Data ( checkDataDef )
import Agda.TypeChecking.Rules.Record ( checkRecDef )
-import Agda.TypeChecking.Rules.Def ( checkFunDef, useTerPragma )
+import Agda.TypeChecking.Rules.Def ( checkFunDef, newSection, useTerPragma )
import Agda.TypeChecking.Rules.Builtin
import Agda.TypeChecking.Rules.Display ( checkDisplayPragma )
import Agda.Termination.TermCheck
-import qualified Agda.Utils.HashMap as HMap
+import Agda.Utils.Except
+import Agda.Utils.Functor
+import Agda.Utils.Function
+import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
+import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Size
-import Agda.Utils.Except
#include "undefined.h"
import Agda.Utils.Impossible
@@ -147,17 +152,16 @@ checkDecl d = setCurrentRange d $ do
reportSDoc "tc.decl" 10 $ prettyA d -- Might loop, see e.g. Issue 1597
-- Issue 418 fix: freeze metas before checking an abstract thing
- when_ isAbstract freezeMetas
+ -- when_ isAbstract freezeMetas -- WAS IN PLACE 2012-2016, but too crude
+ -- applyWhen isAbstract withFreezeMetas $ do -- WRONG
let -- What kind of final checks/computations should be performed
-- if we're not inside a mutual block?
- none m = m >> return Nothing
- meta m = m >> return (Just (return ()))
- mutual i ds m = m >>= return . Just . uncurry (mutualChecks i d ds)
- impossible m = m >> return __IMPOSSIBLE__
- -- We're definitely inside a mutual block.
-
- let mi = Info.MutualInfo TerminationCheck True noRange
+ none m = m $> Nothing -- skip all checks
+ meta m = m $> Just (return ()) -- do the usual checks
+ mutual i ds m = m <&> Just . uncurry (mutualChecks i d ds)
+ impossible m = m $> __IMPOSSIBLE__
+ -- We're definitely inside a mutual block.
finalChecks <- case d of
A.Axiom{} -> meta $ checkTypeSignature d
@@ -165,15 +169,28 @@ checkDecl d = setCurrentRange d $ do
A.Primitive i x e -> meta $ checkPrimitive i x e
A.Mutual i ds -> mutual i ds $ checkMutual i ds
A.Section i x tel ds -> meta $ checkSection i x tel ds
- A.Apply i x modapp rd rm _adir -> meta $ checkSectionApplication i x modapp rd rm
+ A.Apply i x modapp ci _adir -> meta $ checkSectionApplication i x modapp ci
A.Import i x _adir -> none $ checkImport i x
A.Pragma i p -> none $ checkPragma i p
A.ScopedDecl scope ds -> none $ setScope scope >> mapM_ checkDeclCached ds
A.FunDef i x delayed cs -> impossible $ check x i $ checkFunDef delayed i x cs
A.DataDef i x ps cs -> impossible $ check x i $ checkDataDef i x ps cs
- A.RecDef i x ind eta c ps tel cs -> mutual mi [d] $ check x i $ do
+ A.RecDef i x ind eta c ps tel cs -> mutual empty [d] $ check x i $ do
checkRecDef i x ind eta c ps tel cs
blockId <- mutualBlockOf x
+
+ -- Andreas, 2016-10-01 testing whether
+ -- envMutualBlock is set correctly.
+ -- Apparently not.
+ verboseS "tc.decl.mutual" 70 $ do
+ current <- asks envMutualBlock
+ unless (Just blockId == current) $ do
+ reportSLn "" 0 $ unlines
+ [ "mutual block id discrepancy for " ++ show x
+ , " current mut. bl. = " ++ show current
+ , " calculated mut. bl. = " ++ show blockId
+ ]
+
return (blockId, Set.singleton x)
A.DataSig i x ps t -> impossible $ checkSig i x ps t
A.RecSig i x ps t -> none $ checkSig i x ps t
@@ -209,7 +226,8 @@ checkDecl d = setCurrentRange d $ do
-- check record or data type signature
checkSig i x ps t = checkTypeSignature $
- A.Axiom A.NoFunSig i defaultArgInfo x (A.Pi (Info.ExprRange (fuseRange ps t)) ps t)
+ A.Axiom A.NoFunSig i defaultArgInfo Nothing x
+ (A.Pi (Info.ExprRange (fuseRange ps t)) ps t)
check x i m = do
reportSDoc "tc.decl" 5 $ text "Checking" <+> prettyTCM x <> text "."
@@ -230,11 +248,13 @@ checkDecl d = setCurrentRange d $ do
mutualChecks :: Info.MutualInfo -> A.Declaration -> [A.Declaration] -> MutualId -> Set QName -> TCM ()
mutualChecks mi d ds mid names = do
-- Andreas, 2014-04-11: instantiate metas in definition types
- mapM_ instantiateDefinitionType $ Set.toList names
+ let nameList = Set.toList names
+ mapM_ instantiateDefinitionType nameList
-- Andreas, 2013-02-27: check termination before injectivity,
-- to avoid making the injectivity checker loop.
- checkTermination_ mid d
+ local (\ e -> e { envMutualBlock = Just mid }) $ checkTermination_ d
checkPositivity_ mi names
+ revisitRecordPatternTranslation nameList -- Andreas, 2016-11-19 issue #2308
-- Andreas, 2015-03-26 Issue 1470:
-- Restricting coinduction to recursive does not solve the
-- actual problem, and prevents interesting sound applications
@@ -251,6 +271,30 @@ mutualChecks mi d ds mid names = do
checkInjectivity_ names
checkProjectionLikeness_ 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 qs = do
+ -- rs: inferred eta record types of this mutual block
+ -- qccs: compiled clauses of definitions
+ (rs, qccs) <- partitionEithers . catMaybes <$> mapM classify qs
+ unless (null rs) $ forM_ qccs $ \(q,cc) -> do
+ cc <- translateCompiledClauses cc
+ modifySignature $ updateDefinition q $ updateTheDef $
+ updateCompiledClauses $ const $ Just cc
+ 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 q = inConcreteOrAbstractMode q $ \ def -> do
+ case theDef def of
+ Record{ recEtaEquality' = Inferred True } -> return $ Just $ Left q
+ Function{ funCompiled = Just cc } -> return $ Just $ Right (q, cc)
+ _ -> return Nothing
+
type FinalChecks = Maybe (TCM ())
checkUnquoteDecl :: Info.MutualInfo -> [Info.DefInfo] -> [QName] -> A.Expr -> TCM FinalChecks
@@ -353,17 +397,19 @@ highlight_ d = do
"do not highlight construct(ed/or) type"
-- | Termination check a declaration.
-checkTermination_ :: MutualId -> A.Declaration -> TCM ()
-checkTermination_ mid d = Bench.billTo [Bench.Termination] $ do
+checkTermination_ :: A.Declaration -> TCM ()
+checkTermination_ d = Bench.billTo [Bench.Termination] $ do
reportSLn "tc.decl" 20 $ "checkDecl: checking termination..."
- whenM (optTerminationCheck <$> pragmaOptions) $ do
- case d of
+ case d of
-- Record module definitions should not be termination-checked twice.
A.RecDef {} -> return ()
_ -> disableDestructiveUpdate $ do
- termErrs <- termDecl mid d
- unless (null termErrs) $
- typeError $ TerminationCheckFailed termErrs
+ termErrs <- termDecl d
+ -- If there are some termination errors, we collect them in
+ -- the state.
+ -- The termination checker already marked non-terminating functions as such.
+ unless (null termErrs) $ do
+ warning $ TerminationIssue termErrs
-- | Check a set of mutual names for positivity.
checkPositivity_ :: Info.MutualInfo -> Set QName -> TCM ()
@@ -381,7 +427,7 @@ checkPositivity_ mi names = Bench.billTo [Bench.Positivity] $ do
-- (Otherwise, one can implement invalid recursion schemes just like
-- for the old coinduction.)
checkCoinductiveRecords :: [A.Declaration] -> TCM ()
-checkCoinductiveRecords ds = forM_ ds $ \ d -> case d of
+checkCoinductiveRecords ds = forM_ ds $ \case
A.RecDef _ q (Just (Ranged r CoInductive)) _ _ _ _ _ -> setCurrentRange r $ do
unlessM (isRecursiveRecord q) $ typeError $ GenericError $
"Only recursive records can be coinductive"
@@ -394,7 +440,7 @@ checkInjectivity_ names = Bench.billTo [Bench.Injectivity] $ do
-- 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
- Fold.forM_ names $ \ q -> inConcreteOrAbstractMode q $ do
+ Fold.forM_ names $ \ q -> inConcreteOrAbstractMode q $ \ def -> do
-- For abstract q, we should be inAbstractMode,
-- otherwise getConstInfo returns Axiom.
--
@@ -406,7 +452,6 @@ checkInjectivity_ names = Bench.billTo [Bench.Injectivity] $ do
-- or super modules inAbstractMode.
-- I changed that in Monad.Signature.treatAbstractly', so we can see
-- our own local definitions.
- def <- getConstInfo q
case theDef def of
d@Function{ funClauses = cs, funTerminates = term } -> do
case term of
@@ -447,9 +492,27 @@ checkProjectionLikeness_ names = Bench.billTo [Bench.ProjectionLikeness] $ do
_ -> reportSLn "tc.proj.like" 25 $
"mutual definitions are not considered for projection-likeness"
+-- | Freeze metas created by given computation if in abstract mode.
+whenAbstractFreezeMetasAfter :: Info.DefInfo -> TCM a -> TCM a
+whenAbstractFreezeMetasAfter Info.DefInfo{ defAccess, defAbstract} m = do
+ let pubAbs = defAccess == PublicAccess && defAbstract == AbstractDef
+ if not pubAbs then m else do
+ (a, ms) <- metasCreatedBy m
+ xs <- freezeMetas' $ (`Set.member` ms)
+ reportSDoc "tc.decl.ax" 20 $ vcat
+ [ text "Abstract type signature produced new metas: " <+> sep (map prettyTCM $ Set.toList ms)
+ , text "We froze the following ones of these: " <+> sep (map prettyTCM xs)
+ ]
+ return a
+
-- | Type check an axiom.
-checkAxiom :: A.Axiom -> Info.DefInfo -> ArgInfo -> QName -> A.Expr -> TCM ()
-checkAxiom funSig i info0 x e = do
+checkAxiom :: A.Axiom -> Info.DefInfo -> ArgInfo ->
+ Maybe [Occurrence] -> QName -> A.Expr -> TCM ()
+checkAxiom funSig i info0 mp x e = whenAbstractFreezeMetasAfter i $ do
+ -- Andreas, 2016-07-19 issues #418 #2102:
+ -- We freeze metas in type signatures of abstract definitions, to prevent
+ -- leakage of implementation details.
+
-- Andreas, 2012-04-18 if we are in irrelevant context, axioms is irrelevant
-- even if not declared as such (Issue 610).
rel <- max (getRelevance info0) <$> asks envRelevance
@@ -462,37 +525,48 @@ checkAxiom funSig i info0 x e = do
, nest 2 $ text "of sort " <+> prettyTCM (getSort t)
]
- -- check macro type if necessary
- when (Info.defMacro i == MacroDef) $ do
- t' <- normalise t
- TelV tel tr <- telView t'
-
- let telList = telToList tel
- resType = abstract (telFromList (drop (length telList - 1) telList)) tr
- expectedType <- el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit)
- equalType resType expectedType
- `catchError` \ _ -> typeError . GenericDocError =<< sep [ text "Result type of a macro must be"
- , nest 2 $ prettyTCM expectedType ]
-
-- Andreas, 2015-03-17 Issue 1428: Do not postulate sizes in parametrized
-- modules!
when (funSig == A.NoFunSig) $ do
whenM ((== SizeUniv) <$> do reduce $ getSort t) $ do
whenM ((> 0) <$> getContextSize) $ do
typeError $ GenericError $ "We don't like postulated sizes in parametrized modules."
+
+ -- Ensure that polarity pragmas do not contain too many occurrences.
+ (occs, pols) <- case mp of
+ Nothing -> return ([], [])
+ Just occs -> do
+ TelV tel _ <- telView t
+ let n = genericLength (telToList tel)
+ when (n < genericLength occs) $
+ typeError $ TooManyPolarities x n
+ let pols = map polFromOcc occs
+ reportSLn "tc.polarity.pragma" 10 $
+ "Setting occurrences and polarity for " ++ show x ++ ":\n " ++
+ show occs ++ "\n " ++ show pols
+ return (occs, pols)
+
-- Not safe. See Issue 330
-- t <- addForcingAnnotations t
addConstant x =<< do
- useTerPragma $ defaultDefn info x t $
- case funSig of
- A.FunSig -> emptyFunction
- A.NoFunSig -> Axiom -- NB: used also for data and record type sigs
+ useTerPragma $
+ (defaultDefn info x t $
+ case funSig of
+ A.FunSig -> set funMacro (Info.defMacro i == MacroDef) emptyFunction
+ A.NoFunSig -> Axiom) -- NB: used also for data and record type sigs
+ { defArgOccurrences = occs
+ , defPolarity = pols
+ }
-- Add the definition to the instance table, if needed
when (Info.defInstance i == InstanceDef) $ do
addTypedInstance x t
- traceCall (IsType_ e) $ solveSizeConstraints DefaultToInfty -- need Range for error message
+ traceCall (IsType_ e) $ do -- need Range for error message
+ -- Andreas, 2016-06-21, issue #2054
+ -- Do not default size metas to ∞ in local type signatures
+ checkingWhere <- asks envCheckingWhere
+ solveSizeConstraints $ if checkingWhere then DontDefaultToInfty else DefaultToInfty
-- Andreas, 2011-05-31, that freezing below is probably wrong:
-- when_ (Info.defAbstract i == AbstractDef) $ freezeMetas
@@ -662,11 +736,6 @@ checkPragma r p =
addCoreType x dt'
sequence_ $ zipWith addCoreConstr cs cons'
_ -> typeError $ GenericError "COMPILED_DATA_UHC on non datatype"
- A.NoSmashingPragma x -> do
- def <- getConstInfo x
- case theDef def of
- Function{} -> markNoSmashing x
- _ -> typeError $ GenericError "NO_SMASHING directive only works on functions"
A.StaticPragma x -> do
def <- getConstInfo x
case theDef def of
@@ -685,43 +754,42 @@ checkPragma r p =
-- All definitions which have so far been assigned to the given mutual
-- block are returned.
checkMutual :: Info.MutualInfo -> [A.Declaration] -> TCM (MutualId, Set QName)
-checkMutual i ds = inMutualBlock $ do
+checkMutual i ds = inMutualBlock $ \ blockId -> do
- blockId <- currentOrFreshMutualBlock
verboseS "tc.decl.mutual" 20 $ do
reportSDoc "tc.decl.mutual" 20 $ vcat $
(text "Checking mutual block" <+> text (show blockId) <> text ":") :
map (nest 2 . prettyA) ds
+ insertMutualBlockInfo blockId i
local (\e -> e { envTerminationCheck = () <$ Info.mutualTermCheck i }) $
mapM_ checkDecl ds
- (blockId, ) <$> lookupMutualBlock blockId
+ (blockId, ) . mutualNames <$> lookupMutualBlock blockId
-- | Type check the type signature of an inductive or recursive definition.
checkTypeSignature :: A.TypeSignature -> TCM ()
checkTypeSignature (A.ScopedDecl scope ds) = do
setScope scope
mapM_ checkTypeSignature ds
-checkTypeSignature (A.Axiom funSig i info x e) =
- case Info.defAccess i of
- PublicAccess -> inConcreteMode $ checkAxiom funSig i info x e
- PrivateAccess -> inAbstractMode $ checkAxiom funSig i info x e
- OnlyQualified -> __IMPOSSIBLE__
+checkTypeSignature (A.Axiom funSig i info mp x e) =
+ Bench.billTo [Bench.Typing, Bench.TypeSig] $
+ let abstr = case Info.defAccess i of
+ PrivateAccess{}
+ | Info.defAbstract i == AbstractDef -> inAbstractMode
+ -- Issue #2321, only go to AbstractMode for abstract definitions
+ | otherwise -> inConcreteMode
+ PublicAccess -> inConcreteMode
+ OnlyQualified -> __IMPOSSIBLE__
+ in abstr $ checkAxiom funSig i info mp x e
checkTypeSignature _ = __IMPOSSIBLE__ -- type signatures are always axioms
+
-- | Type check a module.
+
checkSection :: Info.ModuleInfo -> ModuleName -> A.Telescope -> [A.Declaration] -> TCM ()
-checkSection i x tel ds =
- checkTelescope tel $ \ tel' -> do
- addSection x
- verboseS "tc.mod.check" 10 $ do
- dx <- prettyTCM x
- dtel <- mapM prettyAs tel
- dtel' <- prettyTCM =<< lookupSection x
- reportSLn "tc.mod.check" 10 $ "checking section " ++ show dx ++ " " ++ show dtel
- reportSLn "tc.mod.check" 10 $ " actual tele: " ++ show dtel'
- withCurrentModule x $ mapM_ checkDeclCached ds
+checkSection _ x tel ds = newSection x tel $ mapM_ checkDeclCached ds
+
-- | Helper for 'checkSectionApplication'.
--
@@ -768,22 +836,20 @@ checkSectionApplication
:: Info.ModuleInfo
-> ModuleName -- ^ Name @m1@ of module defined by the module macro.
-> A.ModuleApplication -- ^ The module macro @λ tel → m2 args@.
- -> A.Ren QName -- ^ Imported names (given as renaming).
- -> A.Ren ModuleName -- ^ Imported modules (given as renaming).
+ -> A.ScopeCopyInfo -- ^ Imported names and modules
-> TCM ()
-checkSectionApplication i m1 modapp rd rm =
+checkSectionApplication i m1 modapp copyInfo =
traceCall (CheckSectionApplication (getRange i) m1 modapp) $
- checkSectionApplication' i m1 modapp rd rm
+ checkSectionApplication' i m1 modapp copyInfo
-- | 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.Ren QName -- ^ Imported names (given as renaming).
- -> A.Ren ModuleName -- ^ Imported modules (given as renaming).
+ -> A.ScopeCopyInfo -- ^ Imported names and modules
-> TCM ()
-checkSectionApplication' i m1 (A.SectionApp ptel m2 args) rd rm = do
+checkSectionApplication' i m1 (A.SectionApp ptel m2 args) copyInfo = do
-- Module applications can appear in lets, in which case we treat
-- lambda-bound variables as additional parameters to the module.
extraParams <- do
@@ -825,17 +891,22 @@ checkSectionApplication' i m1 (A.SectionApp ptel m2 args) rd rm = do
]
-- Andreas, 2014-04-06, Issue 1094:
-- Add the section with well-formed telescope.
- addCtxTel aTel $ addSection m1
+ addContext aTel $ do
+ reportSDoc "tc.mod.apply" 80 $
+ text "addSection" <+> prettyTCM m1 <+> (getContextTelescope >>= \ tel -> inTopContext (prettyTCM tel))
+ addSection m1
reportSDoc "tc.mod.apply" 20 $ vcat
[ sep [ text "applySection", prettyTCM m1, text "=", prettyTCM m2, fsep $ map prettyTCM (vs ++ ts) ]
- , nest 2 $ text " defs:" <+> text (show rd)
- , nest 2 $ text " mods:" <+> text (show rm)
+ , nest 2 $ pretty copyInfo
]
args <- instantiateFull $ vs ++ ts
- applySection m1 ptel m2 args rd rm
+ let n = size aTel
+ etaArgs <- inTopContext $ addContext aTel getContextArgs
+ addContext' aTel $
+ applySection m1 (ptel `abstract` aTel) m2 (raise n args ++ etaArgs) copyInfo
-checkSectionApplication' i m1 (A.RecordModuleIFS x) rd rm = do
+checkSectionApplication' i m1 (A.RecordModuleIFS x) copyInfo = do
let name = mnameToQName x
tel' <- lookupSection x
vs <- freeVarsToApply name
@@ -853,7 +924,7 @@ checkSectionApplication' i m1 (A.RecordModuleIFS x) rd rm = do
instFinal (ExtendTel (Dom info t) (Abs n EmptyTel)) =
ExtendTel (Dom ifo' t) (Abs n EmptyTel)
where ifo' = setHiding Instance info
- -- Otherwise, keep searchinf for last parameter:
+ -- Otherwise, keep searching for last parameter:
instFinal (ExtendTel arg (Abs n tel)) =
ExtendTel arg (Abs n (instFinal tel))
-- Before instFinal is invoked, we have checked that the @tel@ is not empty.
@@ -875,7 +946,7 @@ checkSectionApplication' i m1 (A.RecordModuleIFS x) rd rm = do
when (tel == EmptyTel) $
typeError $ GenericError $ show (qnameToConcrete name) ++ " is not a parameterised section"
- addCtxTel telInst $ do
+ addContext' telInst $ do
vs <- freeVarsToApply name
reportSDoc "tc.mod.apply" 20 $ vcat
[ nest 2 $ text "vs =" <+> sep (map prettyTCM vs)
@@ -885,7 +956,8 @@ checkSectionApplication' i m1 (A.RecordModuleIFS x) rd rm = do
[ nest 2 $ text "vs =" <+> text (show vs)
, nest 2 $ text "args =" <+> text (show args)
]
- applySection m1 telInst x (vs ++ args) rd rm
+ addSection m1
+ applySection m1 telInst x (vs ++ args) copyInfo
-- | Type check an import declaration. Actually doesn't do anything, since all
-- the work is done when scope checking.