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

CHANGELOG.md

@@ -36,6 +36,45 @@ Pragmas and options
   the mouse-hovered symbol (see
   [#4535](https://github.com/agda/agda/pull/4535)).
 
+Language
+--------
+
+* Inductive records without η-equality no longer support both matching
+  on the record constructor and construction of record elements by
+  copattern matching.  It has been discovered that the combination of
+  both leads to loss of subject reduction, i.e., reduction does not
+  preserve typing.  See issue
+  [#4560](https://github.com/agda/agda/issues/4560).
+
+  η-equality for a record can be turned off manually with directive
+  `no-eta-equality` or command-line option `--no-eta-equality`, but it
+  is also automatically turned off for some recursive records.  For
+  records without η, matching on the record constructor is now off by
+  default and construction by copattern matching is on.  If you want
+  the converse, you can add the new record directive `pattern`.
+
+  Example with record pattern:
+  ```agda
+  record N : Set where
+    inductive
+    no-eta-equality
+    pattern
+    field out : Maybe N
+
+  pred : N → Maybe N
+  pred record{ out = m } = m
+  ```
+  Example with record constructor and use of `;` instead of newline:
+  ```agda
+  record N : Set where
+    inductive; no-eta-equality
+    pattern; constructor inn
+    field out : Maybe N
+
+  pred : N → Maybe N
+  pred (inn m) = m
+  ```
+
 Reflection
 ----------
 

doc/user-manual/language/record-types.lagda.rst

@@ -126,7 +126,8 @@ particular, fields can be given in more than one block, interspersed
 with other declarations. Each field is a component of the
 record. Types of later fields can depend on earlier fields.
 
-The directives available are ``eta-equality``, ``no-eta-equality``
+The directives available are ``eta-equality``, ``no-eta-equality``,
+``pattern``
 (see :ref:`eta-expansion`), ``inductive`` and ``co-inductive`` (see
 :ref:`recursive-records`).
 
@@ -373,7 +374,7 @@ inside the record declaration
 Eta-expansion
 -------------
 
-The eta rule for a record type
+The eta (η) rule for a record type
 
 .. code-block:: agda
 
@@ -385,9 +386,9 @@ The eta rule for a record type
 
 states that every ``x : R`` is definitionally equal to ``record { a =
 R.a x ; b = R.b x ; c = R.c x }``. By default, all (inductive) record
-types enjoy eta-equality if the positivity checker has confirmed it is
+types enjoy η-equality if the positivity checker has confirmed it is
 safe to have it. The keywords ``eta-equality``/``no-eta-equality``
-enable/disable eta rules for the record type being declared.
+enable/disable η rules for the record type being declared.
 
 .. _recursive-records:
 
@@ -421,6 +422,24 @@ at your own risk by using the pragma ``ETA`` instead.
 It is possible to pattern match on inductive records, but not on
 coinductive ones.
 
+However, inductive records without η-equality do not support both matching on
+the record constructor and construction of record elements by
+copattern matching.  It has been discovered that the combination of
+both leads to loss of subject reduction, i.e., reduction does not
+preserve typing. For records without η, matching on the record
+constructor is off by default and construction by copattern matching
+is on.  If you want the converse, you can add the record directive
+``pattern``::
+
+  record HereditaryList : Set where
+    inductive
+    no-eta-equality
+    pattern
+    field sublists : List HereditaryList
+
+  pred : HereditaryList → List HereditaryList
+  pred record{ sublists = ts } = ts
+
 .. _instance-fields:
 
 Instance fields
@@ -505,4 +524,3 @@ types. For instance we can define ``Nat`` instances for ``Eq``, ``Ord`` and
 
     NumNat : Num Nat
     fromNat {{NumNat}} n = n
-

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 NFData PatternOrCopattern where
+  rnf PatternMatching   = ()
+  rnf CopatternMatching = ()
 
-instance HasRange HasEta where
+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
 ---------------------------------------------------------------------------
@@ -1810,9 +1868,6 @@ data ProjOrigin
 instance KillRange ProjOrigin where
   killRange = id
 
-data DataOrRecord = IsData | IsRecord
-  deriving (Data, Eq, Ord, Show)
-
 ---------------------------------------------------------------------------
 -- * Infixity, access, abstract, etc.
 ---------------------------------------------------------------------------

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