Fix #7176: turn absurd pattern in instance position to instance meta

Fix #7176: turn absurd pattern in instance position to instance meta rather than unification meta.
So when we use a pattern synonym like `pattern p = c {{()}}` in an expression, the absurd pattern becomes an instance meta.

src/full/Agda/Syntax/Abstract.hs

@@ -994,23 +994,6 @@ mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
 mkLet _ []     e = e
 mkLet i (d:ds) e = Let i (d :| ds) e
 
-patternToExpr :: Pattern -> Expr
-patternToExpr = \case
-  VarP x             -> Var (unBind x)
-  ConP _ c ps        -> Con c `app` map (fmap (fmap patternToExpr)) ps
-  ProjP _ o ds       -> Proj o ds
-  DefP _ fs ps       -> Def (headAmbQ fs) `app` map (fmap (fmap patternToExpr)) ps
-  WildP _            -> Underscore emptyMetaInfo
-  AsP _ _ p          -> patternToExpr p
-  DotP _ e           -> e
-  AbsurdP _          -> Underscore emptyMetaInfo  -- TODO: could this happen?
-  LitP (PatRange r) l-> Lit (ExprRange r) l
-  PatternSynP _ c ps -> PatternSyn c `app` (map . fmap . fmap) patternToExpr ps
-  RecP _ as          -> Rec exprNoRange $ map (Left . fmap patternToExpr) as
-  EqualP{}           -> __IMPOSSIBLE__  -- Andrea TODO: where is this used?
-  WithP r p          -> __IMPOSSIBLE__
-  AnnP _ _ p         -> patternToExpr p
-
 type PatternSynDefn = ([WithHiding Name], Pattern' Void)
 type PatternSynDefns = Map QName PatternSynDefn
 

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

@@ -10,6 +10,7 @@ import Prelude hiding (null)
 import Control.Arrow           ( (***), second )
 import Control.Monad           ( (>=>) )
 import Control.Monad.Identity  ( Identity(..), runIdentity )
+import Control.Monad.Reader    ( Reader, runReader, asks, local )
 import Control.Applicative     ( liftA2 )
 
 
@@ -291,6 +292,54 @@ substPattern' subE s = mapAPattern $ \ p -> case p of
   PatternSynP _ _ _ -> p
   WithP _ _         -> p
 
+-- | Convert a pattern to an expression.
+--
+-- Does not support all cases of patterns.
+-- Result has no 'Range' info, except in identifiers.
+--
+-- This function is only used in expanding pattern synonyms
+-- and in "Agda.Syntax.Translation.InternalToAbstract",
+-- so we can cut some corners.
+patternToExpr :: Pattern -> Expr
+patternToExpr p = patToExpr p `runReader` empty
+
+-- | Converting a pattern to an expression.
+--
+--   The 'Hiding' context is remembered to create instance metas
+--   when translating absurd patterns in instance position.
+--
+class PatternToExpr p e where
+  patToExpr :: p -> Reader Hiding e
+
+  default patToExpr :: (Traversable t, PatternToExpr p' e', p ~ t p', e ~ t e')
+    => p -> Reader Hiding e
+  patToExpr = traverse patToExpr
+
+instance PatternToExpr p e => PatternToExpr [p] [e]
+instance PatternToExpr p e => PatternToExpr (Named n p) (Named n e)
+instance PatternToExpr p e => PatternToExpr (FieldAssignment' p) (FieldAssignment' e)
+
+instance PatternToExpr p e => PatternToExpr (Arg p) (Arg e) where
+  patToExpr (Arg ai p) = local (const $ getHiding ai) $ Arg ai <$> patToExpr p
+
+instance PatternToExpr Pattern Expr where
+  patToExpr = \case
+    VarP x             -> return $ Var (unBind x)
+    ConP _ c ps        -> app (Con c) <$> patToExpr ps
+    ProjP _ o ds       -> return $ Proj o ds
+    DefP _ fs ps       -> app (Def $ headAmbQ fs) <$> patToExpr ps
+    WildP _            -> return $ Underscore emptyMetaInfo
+    AsP _ _ p          -> patToExpr p
+    DotP _ e           -> return e
+    -- Issue #7176: An absurd pattern in an instance position should turn into an instance meta:
+    AbsurdP _          -> asks hidingToMetaKind <&> \ k -> Underscore emptyMetaInfo{ metaKind = k }
+    LitP _ l           -> return $ Lit empty l
+    PatternSynP _ c ps -> app (PatternSyn c) <$> patToExpr ps
+    RecP _ as          -> Rec exprNoRange . map Left <$> patToExpr as
+    EqualP{}           -> __IMPOSSIBLE__  -- Andrea TODO: where is this used?
+    WithP r p          -> __IMPOSSIBLE__
+    AnnP _ _ p         -> patToExpr p
+
 
 -- * Other pattern utilities
 ------------------------------------------------------------------------

src/full/Agda/Syntax/Translation/InternalToAbstract.hs

@@ -415,7 +415,7 @@ reifyDisplayFormP f ps wps = do
               -- even the pattern variables @n < len@ can be
               -- applied to some args @vs@.
               e <- if n < len
-                   then return $ A.patternToExpr $ namedArg $ indexWithDefault __IMPOSSIBLE__ ps n
+                   then return $ patternToExpr $ namedArg $ indexWithDefault __IMPOSSIBLE__ ps n
                    else reify (I.var (n - len))
               apps e =<< argsToExpr vs
             _ -> return underscore

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

@@ -28,6 +28,7 @@ import Agda.Interaction.Highlighting.Generate
   ( storeDisambiguatedConstructor, storeDisambiguatedProjection )
 
 import qualified Agda.Syntax.Abstract as A
+import Agda.Syntax.Abstract.Pattern (patternToExpr)
 import Agda.Syntax.Abstract.Views as A
 import qualified Agda.Syntax.Info as A
 import Agda.Syntax.Concrete.Pretty () -- only Pretty instances
@@ -151,7 +152,7 @@ checkApplication cmp hd args e t =
       case A.insertImplicitPatSynArgs meta (getRange n) ns args of
         Nothing      -> typeError $ BadArgumentsToPatternSynonym n
         Just (s, ns) -> do
-          let p' = A.patternToExpr p
+          let p' = patternToExpr p
               e' = A.lambdaLiftExpr ns (A.substExpr s p')
           checkExpr' cmp e' t
 

test/Succeed/PatternSynonyms.agda

@@ -278,6 +278,32 @@ data ⊥ : Set where
 ⊥-elim : ∀ {A : Set} → ⊥ → A
 ⊥-elim absurd
 
+------------------------------------------------------------------------
+-- Andreas, 2024-03-12, issue #7176:
+-- preserve instanceness in absurd pattern on rhs
+
+module Issue7176 where
+
+  data D : Set where
+    c : {{ i : 0 ≡ 1 }} → D
+
+  pattern ff = c {{ () }}
+
+  works : D → D
+  works ff
+
+  works' : D → D
+  works' c = c
+
+  issue7176 : D → D
+  issue7176 c = ff
+
+  -- Problem was:
+  -- Unsolved meta in last rhs:
+  -- _i : 0 ≡ 1
+
+  -- Should succeed.
+
 ------------------------------------------------------------------------
 -- ambiguous constructors