[ re #3289 ] Postfix projections shouldn't have hiding information

src/full/Agda/Syntax/Abstract.hs

@@ -496,21 +496,24 @@ instance IsProjP Expr where
   isProjP (ScopedExpr _ e) = isProjP e
   isProjP _ = Nothing
 
-class MaybePostfixProjP a where
-  maybePostfixProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)
+class MaybeProjP a where
+  maybeProjP :: a -> Maybe (ProjOrigin, AmbiguousQName)
 
-instance IsProjP e => MaybePostfixProjP (Pattern' e) where
+instance IsProjP e => MaybeProjP (Pattern' e) where
   -- Andreas, 2018-06-19, issue #3130
   -- Do not interpret things like .(p) as projection pattern any more.
   -- maybePostfixProjP (DotP _ e)    = isProjP e <&> \ (_o, d) -> (ProjPostfix, d)
-  maybePostfixProjP (ProjP _ o d) = Just (o, d)
-  maybePostfixProjP _ = Nothing
+  maybeProjP (ProjP _ o d) = Just (o, d)
+  maybeProjP _ = Nothing
 
-instance MaybePostfixProjP a => MaybePostfixProjP (Arg a) where
-  maybePostfixProjP = maybePostfixProjP . unArg
+instance MaybeProjP a => MaybeProjP (Arg a) where
+  maybeProjP p = case maybeProjP $ unArg p of
+    Just (ProjPostfix , f)
+     | getHiding p /= NotHidden -> Nothing
+    x -> x
 
-instance MaybePostfixProjP a => MaybePostfixProjP (Named n a) where
-  maybePostfixProjP = maybePostfixProjP . namedThing
+instance MaybeProjP a => MaybeProjP (Named n a) where
+  maybeProjP = maybeProjP . namedThing
 
 {--------------------------------------------------------------------------
     Things we parse but are not part of the Agda file syntax

src/full/Agda/Syntax/Abstract/Views.hs

@@ -41,6 +41,7 @@ appView' e =
     App i e1 e2
       | Dot _ e2' <- unScope $ namedArg e2
       , Just f <- maybeProjTurnPostfix e2'
+      , getHiding e2 == NotHidden -- Jesper, 2018-12-13: postfix projections shouldn't be hidden
                    -> Application f [defaultNamedArg (i, e1)]
     App i e1 arg
       | Application hd es <- appView' e1

src/full/Agda/TypeChecking/Rules/LHS.hs

@@ -535,7 +535,7 @@ transferOrigins ps qs = do
     matchingArgs p q
       -- The arguments match if
       -- 1. they are both projections,
-      | isJust (A.maybePostfixProjP p) = isJust (isProjP q)
+      | isJust (A.maybeProjP p) = isJust (isProjP q)
       -- 2. or they are both visible,
       | visible p && visible q = True
       -- 3. or they have the same hiding and the argument is not named,
@@ -965,7 +965,7 @@ checkLHS mf = updateRelevance checkLHS_ where
         ]
 
       -- @p@ should be a projection pattern projection from @target@
-      (orig, ambProjName) <- ifJust (A.maybePostfixProjP p) return $
+      (orig, ambProjName) <- ifJust (A.maybeProjP p) return $
         addContext tel $ softTypeError $ CannotEliminateWithPattern p (unArg target)
 
       (projName, projType) <- suspendErrors $ do

src/full/Agda/TypeChecking/Rules/LHS/Implicit.hs

@@ -80,7 +80,7 @@ insertImplicitPatternsT exh            ps a = do
       -- Andreas, 2015-05-11.
       -- If p is a projection pattern, make it visible for the purpose of
       -- calling insImp / insertImplicit, to get correct behavior.
-      let p' = applyWhen (isJust $ A.maybePostfixProjP p) (setHiding NotHidden) p
+      let p' = applyWhen (isJust $ A.maybeProjP p) (setHiding NotHidden) p
       hs <- insImp p' tel
       case hs of
         [] -> do

src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs

@@ -110,7 +110,7 @@ updateProblemRest st@(LHSState tel0 qs0 p@(Problem oldEqs ps ret) a psplit) = do
   reportSDoc "tc.lhs.imp" 20 $
     "insertImplicitPatternsT returned" <+> fsep (map prettyA ps)
   -- (Issue 734: Do only the necessary telView to preserve clause types as much as possible.)
-  let m = length $ takeWhile (isNothing . A.maybePostfixProjP) ps
+  let m = length $ takeWhile (isNothing . A.maybeProjP) ps
   (TelV gamma b, boundary) <- telViewUpToPathBoundaryP m $ unArg a
   forM_ (zip ps (telToList gamma)) $ \(p, a) ->
     unless (sameHiding p a) $ typeError WrongHidingInLHS

src/full/Agda/TypeChecking/With.hs

@@ -420,7 +420,7 @@ stripWithClausePatterns cxtNames parent f t delta qs npars perm ps = do
         , nest 2 $ "t   =" <+> prettyTCM t
         ]
       case namedArg q of
-        ProjP o d -> case A.maybePostfixProjP p of
+        ProjP o d -> case A.maybeProjP p of
           Just (o', AmbQ ds) -> do
             -- Andreas, 2016-12-28, issue #2360:
             -- We disambiguate the projection in the with clause

test/Fail/Issue3289-rhs.agda

@@ -0,0 +1,16 @@
+open import Agda.Builtin.Nat
+
+record R : Set where
+  field
+    x : Nat
+
+open R {{...}}
+
+f₁ : R
+
+-- This is fine.
+x ⦃ f₁ ⦄ = 0
+
+-- THIS WORKS BUT MAKES NO SENSE!!!
+_ : Nat
+_ = f₁ {{ .x }}

test/Fail/Issue3289-rhs.err

@@ -0,0 +1,4 @@
+Issue3289-rhs.agda:16,5-7
+R should be a function type, but it isn't
+when checking that ⦃ .x ⦄ is a valid argument to a function of type
+R

test/Fail/Issue3289.agda

@@ -0,0 +1,15 @@
+open import Agda.Builtin.Nat
+
+record R : Set where
+  field
+    x : Nat
+
+open R {{...}}
+
+f₁ f₂ : R
+
+-- This is fine.
+x ⦃ f₁ ⦄ = 0
+
+-- THIS WORKS BUT MAKES NO SENSE!!!
+f₂ ⦃ .x ⦄ = 0

test/Fail/Issue3289.err

@@ -0,0 +1,3 @@
+Issue3289.agda:15,6-8
+Cannot eliminate type R with projection pattern ⦃ .x ⦄
+when checking that the clause f₂ ⦃ .x ⦄ = 0 has type R