Issue317.agda

module Issue317 (A : Set) where

postulate F : Set → Set

-- Try evaluating F A at the top-level:
--
-- 1,3-4
-- Not in scope:
--   A at 1,3-4
-- when scope checking A
--
-- OK, in that case the inferred type of F should be
-- (A : Set) → Set → Set, right? No, it isn't, it's Set → Set.
--
-- I think the parameters should be in scope when "top-level" commands
-- are executed, because these commands should behave in the same way
-- as commands executed in a top-level goal at the end of the module.
-- It seems as if the implementation of
-- Agda.Interaction.BasicOps.atTopLevel has to be modified.