Re #2829: Make instance arguments in pattern synonyms work in express…

…ions.

If a pattern synonym is used in an expression, we need to make sure
that its instance arguments become instance metas.

Agda only turns an instance argument into an instance meta when the
argument is entirely omitted.  That is, `{{_}}` does not create an
instance meta, but this is exactly what the pattern synonym expansion
produces in expressions.

Having added `metaKind` to the `MetaInfo` record, we can now create
instance underscores in the abstract syntax, which fixes our dilemma.

CHANGELOG.md

@@ -56,6 +56,32 @@ Additions to the Agda syntax.
   As in a `with`, multiple bindings can be separated by a `|`, and variables to
   the left are in scope in bindings to the right.
 
+* Pattern synonyms can now expose existing instance arguments
+  ([PR 7173](https://github.com/agda/agda/pull/7173)).
+  Example:
+  ```agda
+  data D : Set where
+    c : {{D}} → D
+
+  pattern p {{d}} = c {{d}}
+  ```
+  This allows us to explicitly bind these argument in a pattern match
+  and supply them explicitly when using the pattern synonym in an expression.
+  ```agda
+  f : D → D
+  f (p {{d = x}}) = p {{d = x}}
+  ```
+
+  We cannot create new instance arguments this way, though.
+  The following is rejected:
+  ```agda
+  data D : Set where
+    c : D → D
+
+  pattern p {{d}} = c d
+  ```
+
+
 Language
 --------
 

src/full/Agda/Syntax/Abstract.hs

@@ -1082,7 +1082,7 @@ instance SubstExpr Expr where
 
 -- TODO: more informative failure
 insertImplicitPatSynArgs :: forall a. HasRange a
-  => (Range -> a)
+  => (Hiding -> Range -> a)
        -- ^ Thing to insert (wildcard).
   -> Range
        -- ^ Range of the whole pattern synonym expression/pattern.
@@ -1099,7 +1099,7 @@ insertImplicitPatSynArgs wild r ns as = matchArgs r ns as
       | not (null as)
       , matchNext n a  = return (namedArg a, as')
       | visible n      = Nothing
-      | otherwise      = return (wild r, as)
+      | otherwise      = return (wild (getHiding n) r, as)
 
     matchNext ::
          WithHiding Name  -- Pattern synonym parameter

src/full/Agda/TypeChecking/Patterns/Abstract.hs

@@ -95,7 +95,7 @@ expandPatternSynonyms' = postTraverseAPatternM $ \case
       , "- patsyn parameters: " <+> (text . show) (killRange ns)
       , "- patsyn arguments:  " <+> (text . show) (fmap (fmap void) as)
       ]
-    case A.insertImplicitPatSynArgs (A.WildP . PatRange) (getRange x) ns as of
+    case A.insertImplicitPatSynArgs (\ _h r -> A.WildP (PatRange r)) (getRange x) ns as of
       Nothing       -> typeError $ BadArgumentsToPatternSynonym x
       Just (_, _:_) -> typeError $ TooFewArgumentsToPatternSynonym x
       Just (s, [])  -> do

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

@@ -147,7 +147,7 @@ checkApplication cmp hd args e t =
       -- Expand the pattern synonym by substituting for
       -- the arguments we have got and lambda-lifting
       -- over the ones we haven't.
-      let meta r = A.Underscore $ A.emptyMetaInfo{ A.metaRange = r }   -- TODO: name suggestion
+      let meta h r = A.Underscore $ A.emptyMetaInfo{ A.metaRange = r, A.metaKind = A.hidingToMetaKind h }   -- TODO: name suggestion
       case A.insertImplicitPatSynArgs meta (getRange n) ns args of
         Nothing      -> typeError $ BadArgumentsToPatternSynonym n
         Just (s, ns) -> do

test/Succeed/PatternSynVarInstance.agda

@@ -17,3 +17,9 @@ module _ where
 
   h : D → D
   h p = c
+
+  i : D → D
+  i p = p  -- Should solve.
+
+  j : D → D
+  j (p {{d}}) = p {{d = d}}