Merge branch 'maint-2.4.2'

HACKING

@@ -126,8 +126,9 @@ Working with Git (from 2013-06-15)
 
   The script:
 
+    ## Remove cpphs upper bound
     sed -ri -e 's/cpphs >=.*/cpphs/' Agda.cabal
-
+    ## Run the test
     if cabal install --force-reinstalls \
                      --disable-library-profiling \
                      --disable-documentation
@@ -138,9 +139,8 @@ Working with Git (from 2013-06-15)
     else
         status=125
     fi
-
+    ## Clean up and exit
     git reset --hard
-
     exit $status
 
 Standard library submodule

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

@@ -851,7 +851,9 @@ scopeCheckNiceModule r p name tel checkDs
       (name, p, open) <- do
         if isNoName name then do
           (i :: NameId) <- fresh
-          return (C.NoName (getRange name) i, PrivateAccess, True)
+          -- Issue 1701: PublicAccess is necessary for being copied
+          -- during module aliasing and subsequent query with getSection.
+          return (C.NoName (getRange name) i, p, True) -- Before Issue 1701, p was PrivateAccess
          else return (name, p, False)
 
       -- Check and bind the module, using the supplied check for its contents.

src/full/Agda/TypeChecking/Monad/Signature.hs

@@ -307,10 +307,10 @@ applySection' new ptel old ts rd rm = do
     argsToUse new = do
       let m = mnameFromList $ commonPrefix (mnameToList old) (mnameToList new)
       reportSLn "tc.mod.apply" 80 $ "Common prefix: " ++ show m
-      let ms = tail . map mnameFromList . inits . mnameToList $ m
-      ps <- mapM (maybe 0 secFreeVars <.> getSection) ms
+      let ms = map mnameFromList . tail . inits . mnameToList $ m  -- NB: tail . inits computes the non-empty prefixes
+      ps <- mapM (fmap secFreeVars <.> getSection) ms
       reportSLn "tc.mod.apply" 80 $ "  params: " ++ show (zip ms ps)
-      return $ sum ps
+      return $ sum $ map (fromMaybe 0) ps
 
     copyDef :: Args -> (QName, QName) -> TCM ()
     copyDef ts (x, y) = do

test/succeed/Issue1701.agda

@@ -0,0 +1,38 @@
+-- Andreas, 2015-10-26, issue reported by Wolfram Kahl
+-- {-# OPTIONS -v scope.mod.inst:30 -v tc.mod.check:10 -v tc.mod.apply:80 #-}
+
+module _ where
+
+  module ModParamsRecord (A : Set) where
+    record R (B : Set) : Set where
+      field F : A → B
+
+  module ModParamsToLoose (A : Set) where
+    open ModParamsRecord
+
+    -- WORKS:
+    -- module M (B : Set) (G : A → B) where
+    --   r : R A B
+    --   r = record { F = G }
+    --
+    --   module r = R A r
+    -- open M public
+
+    -- SHOULD WORK:
+    module _ (B : Set) (G : A → B) where
+      r : R A B
+      r = record { F = G }
+
+      module r = R A r
+
+  module ModParamsLost (A : Set) where
+    open ModParamsRecord
+    open ModParamsToLoose A
+
+    f : (A → A) → A → A
+    f G = S.F
+      where
+        module S = r A G           -- expected |S.F : A → A|,
+                                   -- WAS: but obtained |S.F : (B : Set) (G₁ : A → B) → A → B|
+        -- module S = r            -- as expected: |S.F : (B : Set) (G₁ : A → B) → A → B|
+        -- module S = R A (r A G)  -- as expected: |S.F : A → A|