[ fixed #4560 ] pattern attribute no-eta-equality inductive records

Having both pattern and copattern matching for records without
eta-equality breaks subject reduction.

If you want to pattern match on the constructor for a no-eta record, you
have to declare it 'pattern'.  The default is copattern matching.

The attribute 'pattern' is ignored for 'coinductive' or 'eta-equality'
records.  Recursive records might be declared as no-eta by the
positivity checker; thus, we need to remember the attribute 'pattern'
until the positivity checker has run.  It is stored in the new field

  recPatternMatching :: PatternOrCopattern

of the Record alternative of TCM.Defn.  Ultimately, the choice of
PatternMatching or CopatternMatching is integrated in the field

  recEtaEquality' :: HasEta

This change to Agda affects a dozen test cases and also the standard
library at some places.

src/full/Agda/Interaction/Highlighting/FromAbstract.hs

@@ -204,7 +204,7 @@ instance Hilite A.Declaration where
       A.DataSig _di x tel e                  -> hl x <> hl tel <> hl e
       A.DataDef _di x _uc pars cs            -> hl x <> hl pars <> hl cs
       A.RecSig _di x tel e                   -> hl x <> hl tel <> hl e
-      A.RecDef _di x _uc _ind _eta y bs e ds -> hl x <> hl y <> hl bs <> hl e <> hl ds
+      A.RecDef _di x _uc _ind _eta _pat y bs e ds -> hl x <> hl y <> hl bs <> hl e <> hl ds
       A.PatternSynDef x xs p                 -> hl x <> hl xs <> hl p
       A.UnquoteDecl _mi _di xs e             -> hl xs <> hl e
       A.UnquoteDef _di xs e                  -> hl xs <> hl e

src/full/Agda/Interaction/Highlighting/Generate.hs

@@ -412,6 +412,7 @@ warningHighlighting w = case tcWarning w of
   IllformedAsClause{}        -> deadcodeHighlighting $ getRange w
   UselessPublic{}            -> deadcodeHighlighting $ getRange w
   UselessInline{}            -> mempty
+  UselessPatternDeclarationForRecord{} -> deadcodeHighlighting $ getRange w
   ClashesViaRenaming _ xs    -> foldMap (deadcodeHighlighting . getRange) xs
     -- #4154, TODO: clashing renamings are not dead code, but introduce problems.
     -- Should we have a different color?

src/full/Agda/Interaction/Options/Warnings.hs

@@ -211,6 +211,7 @@ data WarningName
   | UnsolvedInteractionMetas_
   | UnsolvedMetaVariables_
   | UselessInline_
+  | UselessPatternDeclarationForRecord_
   | UselessPublic_
   | UserWarning_
   | WithoutKFlagPrimEraseEquality_
@@ -310,6 +311,7 @@ warningNameDescription = \case
   UselessInstance_                 -> "`instance' blocks where they have no effect."
   UselessPrivate_                  -> "`private' blocks where they have no effect."
   UselessPublic_                   -> "`public' blocks where they have no effect."
+  UselessPatternDeclarationForRecord_ -> "`pattern' attributes where they have no effect."
   -- Scope and Type Checking Warnings
   AbsurdPatternRequiresNoRHS_      -> "A clause with an absurd pattern does not need a Right Hand Side."
   CantGeneralizeOverSorts_         -> "Attempt to generalize over sort metas in 'variable' declaration."

src/full/Agda/Syntax/Abstract.hs

@@ -168,9 +168,10 @@ data Declaration
   | DataSig    DefInfo QName GeneralizeTelescope Expr -- ^ lone data signature
   | DataDef    DefInfo QName UniverseCheck DataDefParams [Constructor]
   | RecSig     DefInfo QName GeneralizeTelescope Expr -- ^ lone record signature
-  | RecDef     DefInfo QName UniverseCheck (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe QName) DataDefParams Expr [Declaration]
+  | RecDef     DefInfo QName UniverseCheck (Maybe (Ranged Induction)) (Maybe HasEta0) (Maybe Range) (Maybe QName) DataDefParams Expr [Declaration]
       -- ^ The 'Expr' gives the constructor type telescope, @(x1 : A1)..(xn : An) -> Prop@,
       --   and the optional name is the constructor's name.
+      --   The optional 'Range' is for the @pattern@ attribute.
   | PatternSynDef QName [Arg BindName] (Pattern' Void)
       -- ^ Only for highlighting purposes
   | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
@@ -551,7 +552,7 @@ instance Eq Declaration where
   DataSig a1 b1 c1 d1            == DataSig a2 b2 c2 d2            = (a1, b1, c1, d1) == (a2, b2, c2, d2)
   DataDef a1 b1 c1 d1 e1         == DataDef a2 b2 c2 d2 e2         = (a1, b1, c1, d1, e1) == (a2, b2, c2, d2, e2)
   RecSig a1 b1 c1 d1             == RecSig a2 b2 c2 d2             = (a1, b1, c1, d1) == (a2, b2, c2, d2)
-  RecDef a1 b1 c1 d1 e1 f1 g1 h1 i1 == RecDef a2 b2 c2 d2 e2 f2 g2 h2 i2 = (a1, b1, c1, d1, e1, f1, g1, h1, i1) == (a2, b2, c2, d2, e2, f2, g2, h2, i2)
+  RecDef a1 b1 c1 d1 e1 f1 g1 h1 i1 j1 == RecDef a2 b2 c2 d2 e2 f2 g2 h2 i2 j2 = (a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) == (a2, b2, c2, d2, e2, f2, g2, h2, i2, j2)
   PatternSynDef a1 b1 c1         == PatternSynDef a2 b2 c2         = (a1, b1, c1) == (a2, b2, c2)
   UnquoteDecl a1 b1 c1 d1        == UnquoteDecl a2 b2 c2 d2        = (a1, b1, c1, d1) == (a2, b2, c2, d2)
   UnquoteDef a1 b1 c1            == UnquoteDef a2 b2 c2            = (a1, b1, c1) == (a2, b2, c2)
@@ -633,7 +634,7 @@ instance HasRange Declaration where
     getRange (DataSig    i _ _ _    ) = getRange i
     getRange (DataDef    i _ _ _ _  ) = getRange i
     getRange (RecSig     i _ _ _    ) = getRange i
-    getRange (RecDef i _ _ _ _ _ _ _ _) = getRange i
+    getRange (RecDef i _ _ _ _ _ _ _ _ _) = getRange i
     getRange (PatternSynDef x _ _   ) = getRange x
     getRange (UnquoteDecl _ i _ _)    = getRange i
     getRange (UnquoteDef i _ _)       = getRange i
@@ -764,7 +765,7 @@ instance KillRange Declaration where
   killRange (DataSig i a b c          ) = killRange4 DataSig i a b c
   killRange (DataDef i a b c d        ) = killRange5 DataDef i a b c d
   killRange (RecSig  i a b c          ) = killRange4 RecSig  i a b c
-  killRange (RecDef  i a b c d e f g h) = killRange9 RecDef  i a b c d e f g h
+  killRange (RecDef  i a b c d e f g h j) = killRange10 RecDef  i a b c d e f g h j
   killRange (PatternSynDef x xs p     ) = killRange3 PatternSynDef x xs p
   killRange (UnquoteDecl mi i x e     ) = killRange4 UnquoteDecl mi i x e
   killRange (UnquoteDef i x e         ) = killRange3 UnquoteDef i x e
@@ -856,7 +857,7 @@ instance AnyAbstract Declaration where
   anyAbstract (Section _ _ _ ds)     = anyAbstract ds
   anyAbstract (FunDef i _ _ _)       = defAbstract i == AbstractDef
   anyAbstract (DataDef i _ _ _ _)    = defAbstract i == AbstractDef
-  anyAbstract (RecDef i _ _ _ _ _ _ _ _) = defAbstract i == AbstractDef
+  anyAbstract (RecDef i _ _ _ _ _ _ _ _ _) = defAbstract i == AbstractDef
   anyAbstract (DataSig i _ _ _)      = defAbstract i == AbstractDef
   anyAbstract (RecSig i _ _ _)       = defAbstract i == AbstractDef
   anyAbstract _                      = __IMPOSSIBLE__

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

@@ -106,8 +106,8 @@ deepUnscopeDecl :: A.Declaration -> [A.Declaration]
 deepUnscopeDecl (A.ScopedDecl _ ds)              = deepUnscopeDecls ds
 deepUnscopeDecl (A.Mutual i ds)                  = [A.Mutual i (deepUnscopeDecls ds)]
 deepUnscopeDecl (A.Section i m tel ds)           = [A.Section i m (deepUnscope tel) (deepUnscopeDecls ds)]
-deepUnscopeDecl (A.RecDef i x uc ind eta c bs e ds) = [A.RecDef i x uc ind eta c (deepUnscope bs) (deepUnscope e)
-                                                                           (deepUnscopeDecls ds)]
+deepUnscopeDecl (A.RecDef i x uc ind eta pat c bs e ds) =
+  [ A.RecDef i x uc ind eta pat c (deepUnscope bs) (deepUnscope e) (deepUnscopeDecls ds) ]
 deepUnscopeDecl d                                = [deepUnscope d]
 
 -- * Traversal
@@ -398,7 +398,7 @@ instance ExprLike Declaration where
       DataSig i d tel e         -> DataSig i d <$> rec tel <*> rec e
       DataDef i d uc bs cs      -> DataDef i d uc <$> rec bs <*> rec cs
       RecSig i r tel e          -> RecSig i r <$> rec tel <*> rec e
-      RecDef i r uc n co c bs e ds -> RecDef i r uc n co c <$> rec bs <*> rec e <*> rec ds
+      RecDef i r uc ind eta pat c bs e ds -> RecDef i r uc ind eta pat c <$> rec bs <*> rec e <*> rec ds
       PatternSynDef f xs p      -> PatternSynDef f xs <$> rec p
       UnquoteDecl i is xs e     -> UnquoteDecl i is xs <$> rec e
       UnquoteDef i xs e         -> UnquoteDef i xs <$> rec e
@@ -453,7 +453,7 @@ instance DeclaredNames Declaration where
       DataSig _ q _ _              -> singleton (WithKind DataName q)
       DataDef _ q _ _ decls        -> singleton (WithKind DataName q) <> foldMap con decls
       RecSig _ q _ _               -> singleton (WithKind RecName q)
-      RecDef _ q _ i _ c _ _ decls -> singleton (WithKind RecName q) <> kc <> declaredNames decls
+      RecDef _ q _ i _ _ c _ _ decls -> singleton (WithKind RecName q) <> kc <> declaredNames decls
         where
         kc = maybe mempty (singleton . WithKind k) c
         k  = maybe ConName (conKindOfName . rangedThing) i

src/full/Agda/Syntax/Common.hs

@@ -78,18 +78,73 @@ instance Pretty FileType where
 -- * Eta-equality
 ---------------------------------------------------------------------------
 
-data HasEta = NoEta | YesEta
-  deriving (Data, Show, Eq, Ord)
+-- | Does a record come with eta-equality?
+data HasEta' a
+  = YesEta
+  | NoEta a
+  deriving (Data, Show, Eq, Ord, Functor, Foldable, Traversable)
+
+instance HasRange a => HasRange (HasEta' a) where
+  getRange = foldMap getRange
+
+instance KillRange a => KillRange (HasEta' a) where
+  killRange = fmap killRange
+
+instance NFData a => NFData (HasEta' a) where
+  rnf YesEta    = ()
+  rnf (NoEta p) = rnf p
+
+-- | Pattern and copattern matching is allowed in the presence of eta.
+--
+--   In the absence of eta, we have to choose whether we want to allow
+--   matching on the constructor or copattern matching with the projections.
+--   Having both leads to breakage of subject reduction (issue #4560).
+
+type HasEta  = HasEta' PatternOrCopattern
+type HasEta0 = HasEta' ()
+
+-- | For a record without eta, which type of matching do we allow?
+data PatternOrCopattern
+  = PatternMatching
+      -- ^ Can match on the record constructor.
+  | CopatternMatching
+      -- ^ Can copattern match using the projections. (Default.)
+  deriving (Data, Show, Eq, Ord, Enum, Bounded)
 
-instance HasRange HasEta where
+instance NFData PatternOrCopattern where
+  rnf PatternMatching   = ()
+  rnf CopatternMatching = ()
+
+instance HasRange PatternOrCopattern where
   getRange _ = noRange
 
-instance KillRange HasEta where
+instance KillRange PatternOrCopattern where
   killRange = id
 
-instance NFData HasEta where
-  rnf NoEta  = ()
-  rnf YesEta = ()
+-- | Can we pattern match on the record constructor?
+class PatternMatchingAllowed a where
+  patternMatchingAllowed :: a -> Bool
+
+instance PatternMatchingAllowed PatternOrCopattern where
+  patternMatchingAllowed = (== PatternMatching)
+
+instance PatternMatchingAllowed HasEta where
+  patternMatchingAllowed = \case
+    YesEta -> True
+    NoEta p -> patternMatchingAllowed p
+
+
+-- | Can we construct a record by copattern matching?
+class CopatternMatchingAllowed a where
+  copatternMatchingAllowed :: a -> Bool
+
+instance CopatternMatchingAllowed PatternOrCopattern where
+  copatternMatchingAllowed = (== CopatternMatching)
+
+instance CopatternMatchingAllowed HasEta where
+  copatternMatchingAllowed = \case
+    YesEta -> True
+    NoEta p -> copatternMatchingAllowed p
 
 ---------------------------------------------------------------------------
 -- * Induction
@@ -113,6 +168,9 @@ instance NFData Induction where
   rnf Inductive   = ()
   rnf CoInductive = ()
 
+instance PatternMatchingAllowed Induction where
+  patternMatchingAllowed = (== Inductive)
+
 ---------------------------------------------------------------------------
 -- * Hiding
 ---------------------------------------------------------------------------

src/full/Agda/Syntax/Concrete.hs

@@ -388,9 +388,10 @@ data Declaration
   | Data        Range Name [LamBinding] Expr [TypeSignatureOrInstanceBlock]
   | DataDef     Range Name [LamBinding] [TypeSignatureOrInstanceBlock]
   | RecordSig   Range Name [LamBinding] Expr -- ^ lone record signature in mutual block
-  | RecordDef   Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] [Declaration]
-  | Record      Range Name (Maybe (Ranged Induction)) (Maybe HasEta) (Maybe (Name, IsInstance)) [LamBinding] Expr [Declaration]
+  | RecordDef   Range Name (Maybe (Ranged Induction)) (Maybe HasEta0) (Maybe Range) (Maybe (Name, IsInstance)) [LamBinding] [Declaration]
+  | Record      Range Name (Maybe (Ranged Induction)) (Maybe HasEta0) (Maybe Range) (Maybe (Name, IsInstance)) [LamBinding] Expr [Declaration]
     -- ^ The optional name is a name for the record constructor.
+    --   The optional 'Range' is the range of the @pattern@ declaration.
   | Infix Fixity (List1 Name)
   | Syntax      Name Notation -- ^ notation declaration for a name
   | PatternSyn  Range Name [Arg Name] Pattern
@@ -744,8 +745,8 @@ instance HasRange Declaration where
   getRange (Data r _ _ _ _)        = r
   getRange (DataDef r _ _ _)       = r
   getRange (RecordSig r _ _ _)     = r
-  getRange (RecordDef r _ _ _ _ _ _) = r
-  getRange (Record r _ _ _ _ _ _ _)  = r
+  getRange (RecordDef r _ _ _ _ _ _ _) = r
+  getRange (Record r _ _ _ _ _ _ _ _)  = r
   getRange (Mutual r _)            = r
   getRange (Abstract r _)          = r
   getRange (Generalize r _)        = r
@@ -882,8 +883,8 @@ instance KillRange Declaration where
   killRange (Data _ n l e c)        = killRange4 (Data noRange) n l e c
   killRange (DataDef _ n l c)       = killRange3 (DataDef noRange) n l c
   killRange (RecordSig _ n l e)     = killRange3 (RecordSig noRange) n l e
-  killRange (RecordDef _ n mi mb mn k d) = killRange6 (RecordDef noRange) n mi mb mn k d
-  killRange (Record _ n mi mb mn k e d)  = killRange7 (Record noRange) n mi mb mn k e d
+  killRange (RecordDef _ n mi mb mp mn k d) = killRange7 (RecordDef noRange) n mi mb mp mn k d
+  killRange (Record _ n mi mb mp mn k e d)  = killRange8 (Record noRange) n mi mb mp mn k e d
   killRange (Infix f n)             = killRange2 Infix f n
   killRange (Syntax n no)           = killRange1 (\n -> Syntax n no) n
   killRange (PatternSyn _ n ns p)   = killRange3 (PatternSyn noRange) n ns p
@@ -1096,8 +1097,8 @@ instance NFData Declaration where
   rnf (Data _ a b c d)        = rnf a `seq` rnf b `seq` rnf c `seq` rnf d
   rnf (DataDef _ a b c)       = rnf a `seq` rnf b `seq` rnf c
   rnf (RecordSig _ a b c)     = rnf a `seq` rnf b `seq` rnf c
-  rnf (RecordDef _ a b c d e f) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d `seq` rnf e `seq` rnf f
-  rnf (Record _ a b c d e f g)  = rnf a `seq` rnf b `seq` rnf c `seq` rnf d `seq` rnf e `seq` rnf f `seq` rnf g
+  rnf (RecordDef _ a b c _ d e f) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d `seq` rnf e `seq` rnf f
+  rnf (Record _ a b c _ d e f g)  = rnf a `seq` rnf b `seq` rnf c `seq` rnf d `seq` rnf e `seq` rnf f `seq` rnf g
   rnf (Infix a b)             = rnf a `seq` rnf b
   rnf (Syntax a b)            = rnf a `seq` rnf b
   rnf (PatternSyn _ a b c)    = rnf a `seq` rnf b `seq` rnf c