diff --git a/src/full/Agda/Syntax/Abstract.hs b/src/full/Agda/Syntax/Abstract.hs index 539b09f0bf0..63870027417 100644 --- a/src/full/Agda/Syntax/Abstract.hs +++ b/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 diff --git a/src/full/Agda/Syntax/Abstract/Views.hs b/src/full/Agda/Syntax/Abstract/Views.hs index d433a197dcc..2c7e45abb4a 100644 --- a/src/full/Agda/Syntax/Abstract/Views.hs +++ b/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 diff --git a/src/full/Agda/TypeChecking/Rules/LHS.hs b/src/full/Agda/TypeChecking/Rules/LHS.hs index b197961904d..8f648a8c98e 100644 --- a/src/full/Agda/TypeChecking/Rules/LHS.hs +++ b/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 diff --git a/src/full/Agda/TypeChecking/Rules/LHS/Implicit.hs b/src/full/Agda/TypeChecking/Rules/LHS/Implicit.hs index 69aacb90113..aa16851f997 100644 --- a/src/full/Agda/TypeChecking/Rules/LHS/Implicit.hs +++ b/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 diff --git a/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs b/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs index 987a6a86bf8..231920a511d 100644 --- a/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs +++ b/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 diff --git a/src/full/Agda/TypeChecking/With.hs b/src/full/Agda/TypeChecking/With.hs index b5cd4ee16c8..039c7edabfd 100644 --- a/src/full/Agda/TypeChecking/With.hs +++ b/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 diff --git a/test/Fail/Issue3289-rhs.agda b/test/Fail/Issue3289-rhs.agda new file mode 100644 index 00000000000..7d476c9a3bc --- /dev/null +++ b/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 }} diff --git a/test/Fail/Issue3289-rhs.err b/test/Fail/Issue3289-rhs.err new file mode 100644 index 00000000000..87c99095254 --- /dev/null +++ b/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 diff --git a/test/Fail/Issue3289.agda b/test/Fail/Issue3289.agda new file mode 100644 index 00000000000..227b9eca4a1 --- /dev/null +++ b/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 diff --git a/test/Fail/Issue3289.err b/test/Fail/Issue3289.err new file mode 100644 index 00000000000..368648f8d1d --- /dev/null +++ b/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