From 003d0df52b8aeeb05e0ba4e5d68c7c78e9ee5dd6 Mon Sep 17 00:00:00 2001
From: Nathaniel Burke <nathanielrburke3@gmail.com>
Date: Mon, 3 Nov 2025 19:06:44 +0000
Subject: [PATCH 1/5] [ agda#306 ] Error on module param dot pat

Delay applying getContextArgs until after we have checked for dot
patterns
Also stop throwing __IMPOSSIBLE__ on instances inside modules
---
 src/Agda2Hs/Compile/ClassInstance.hs     | 32 ++++++++--------
 src/Agda2Hs/Compile/Function.hs          | 47 ++++++++++++++++++------
 src/Agda2Hs/Compile/Function.hs-boot     |  4 +-
 src/Agda2Hs/Compile/Term.hs              |  6 +--
 test/AllFailTests.agda                   |  4 ++
 test/AllTests.agda                       |  4 +-
 test/{ => Fail}/ErasedPatternLambda.agda |  2 +
 test/Fail/Issue306a.agda                 | 11 ++++++
 test/Fail/Issue306b.agda                 | 16 ++++++++
 test/Fail/Issue306c.agda                 | 17 +++++++++
 test/Issue306.agda                       | 20 ++++++++++
 11 files changed, 129 insertions(+), 34 deletions(-)
 rename test/{ => Fail}/ErasedPatternLambda.agda (94%)
 create mode 100644 test/Fail/Issue306a.agda
 create mode 100644 test/Fail/Issue306b.agda
 create mode 100644 test/Fail/Issue306c.agda
 create mode 100644 test/Issue306.agda

diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs
index 9fb06649..5cbd8fa3 100644
--- a/src/Agda2Hs/Compile/ClassInstance.hs
+++ b/src/Agda2Hs/Compile/ClassInstance.hs
@@ -46,7 +46,7 @@ disableCopatterns :: C a -> C a
 disableCopatterns = local $ \e -> e { copatternsEnabled = False }
 
 
--- | Enable the approriate extensions for a given Haskell deriving strategy.
+-- | Enable the appropriate extensions for a given Haskell deriving strategy.
 enableStrategy :: Maybe (Hs.DerivStrategy ()) -> C ()
 enableStrategy Nothing = return ()
 enableStrategy (Just s) = do
@@ -66,14 +66,14 @@ compileInstance (ToDerivation strategy) def@Defn{..} =
       text "compiling instance" <+> prettyTCM defName <+> text "to standalone deriving"
     tellExtension Hs.StandaloneDeriving
     enableStrategy strategy
-    ir <- compileInstRule [] (unEl defType)
+    ir <- compileInstRule [] [] (unEl defType)
     return $ Hs.DerivDecl () strategy Nothing ir
 
 compileInstance ToDefinition def@Defn{..} =
   enableCopatterns $ setCurrentRangeQ defName $ do
     reportSDoc "agda2hs.compile.instance" 13 $
       text "compiling instance" <+> prettyTCM defName <+> text "to instance definition"
-    ir <- compileInstRule [] (unEl defType)
+    ir <- compileInstRule [] [] (unEl defType)
     withFunctionLocals defName $ do
       reportSDoc "agda2hs.compile.instance" 20 $ vcat $
         text "compileInstance clauses: " :
@@ -83,11 +83,11 @@ compileInstance ToDefinition def@Defn{..} =
       tel <- lookupSection mod
       addContext tel $ do
         liftTCM $ setModuleCheckpoint mod
-        pars <- getContextArgs
-        ty <- defType `piApplyM` pars
-        let clauses = funClauses `apply` pars
+        -- We intentionally do not apply getContextArgs eagerly here so dotted
+        -- patterns corresponding to module parameters are correctly detected
+        -- (https://github.com/agda/agda2hs/issues/306)
         (ds, rs) <- concatUnzip
-                <$> mapM (\c -> withClauseLocals mod c $ compileInstanceClause mod ty c) clauses
+                <$> mapM (\c -> withClauseLocals mod c $ compileInstanceClause mod defType c) funClauses
         reportSDoc "agda2hs.compile.instance" 20 $ vcat $
           text "compileInstance compiled clauses: " :
           map (nest 2 . text . pp) ds
@@ -97,8 +97,8 @@ compileInstance ToDefinition def@Defn{..} =
     where Function{..} = theDef
 
 
-compileInstRule :: [Hs.Asst ()] -> Term -> C (Hs.InstRule ())
-compileInstRule cs ty = do
+compileInstRule :: [Hs.TyVarBind ()] -> [Hs.Asst ()] -> Term -> C (Hs.InstRule ())
+compileInstRule xs cs ty = do
   reportSDoc "agda2hs.compile.instance" 20 $ text "compileInstRule" <+> prettyTCM ty
   case unSpine1 ty of
     Def f es | Just args <- allApplyElims es -> do
@@ -106,7 +106,7 @@ compileInstRule cs ty = do
       vs <- compileTypeArgs fty args
       f <- compileQName f
       return $
-        Hs.IRule () Nothing (ctx cs) $ foldl (Hs.IHApp ()) (Hs.IHCon () f) (map pars vs)
+        Hs.IRule () (Just xs) (ctx cs) $ foldl (Hs.IHApp ()) (Hs.IHCon () f) (map pars vs)
       where ctx [] = Nothing
             ctx cs = Just (Hs.CxTuple () cs)
             -- put parens around anything except a var or a constant
@@ -115,11 +115,12 @@ compileInstRule cs ty = do
             pars t@(Hs.TyCon () _) = t
             pars t = Hs.TyParen () t
     Pi a b -> compileDomType (absName b) a >>= \case
-      DomDropped -> underAbstr a b (compileInstRule cs . unEl)
+      DomDropped -> underAbstr a b (compileInstRule xs cs . unEl)
       DomConstraint hsA ->
-        underAbstraction a b (compileInstRule (cs ++ [hsA]) . unEl)
+        underAbstraction a b (compileInstRule xs (cs ++ [hsA]) . unEl)
       DomType _ t -> __IMPOSSIBLE__
-      DomForall _ -> __IMPOSSIBLE__
+      DomForall x ->
+        underAbstraction a b (compileInstRule (xs ++ [x]) cs . unEl)
     _ -> __IMPOSSIBLE__
 
 
@@ -170,7 +171,7 @@ compileInstanceClause curModule ty c = ifNotM (keepClause c) (return ([], [])) $
 -- abuse compileClause:
 -- 1. drop any patterns before record projection to suppress the instance arg
 -- 2. use record proj. as function name
--- 3. process remaing patterns as usual
+-- 3. process remaining patterns as usual
 compileInstanceClause' :: ModuleName -> Type -> NAPs -> Clause -> C ([Hs.InstDecl ()], [QName])
 compileInstanceClause' curModule ty [] c = __IMPOSSIBLE__
 compileInstanceClause' curModule ty (p:ps) c
@@ -289,7 +290,7 @@ compileInstanceClause' curModule ty (p:ps) c
       -- No minimal dictionary used, proceed with compiling as a regular clause.
       | otherwise -> do
         reportSDoc "agda2hs.compile.instance" 20 $ text "Compiling instance clause" <+> prettyTCM c'
-        ms <- disableCopatterns $ compileClause curModule Nothing uf ty' c'
+        ms <- disableCopatterns $ compileClause curModule [] Nothing uf ty' c'
         let cc = Hs.FunBind () (toList ms)
         reportSDoc "agda2hs.compile.instance" 20 $ vcat
           [ text "compileInstanceClause compiled clause"
@@ -302,6 +303,7 @@ compileInstanceClause' curModule ty (p:ps) c
 --              if there is something other than erased parameters
 compileInstanceClause' curModule ty (p:ps) c = do
   (a, b) <- mustBePi ty
+  checkForced a (namedArg p)
   compileInstanceClause' curModule (absApp b (patternToTerm $ namedArg p)) ps c
 
 fieldArgInfo :: QName -> C ArgInfo
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
index a5a425b9..988888ca 100644
--- a/src/Agda2Hs/Compile/Function.hs
+++ b/src/Agda2Hs/Compile/Function.hs
@@ -9,7 +9,7 @@ import Data.List
 import Data.Maybe ( fromMaybe, isJust )
 import qualified Data.Text as Text
 
-import Agda.Compiler.Backend
+import Agda.Compiler.Backend hiding (Args)
 import Agda.Compiler.Common
 
 import Agda.Syntax.Common
@@ -152,9 +152,8 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
         reportSDoc "agda2hs.compile.type" 8 $ "Compiled function type: " <+> text (Hs.prettyPrint ty)
         return [Hs.TypeSig () [x] ty]
 
-      let clauses = funClauses `apply` pars
       cs  <- map (addPats paramPats) <$>
-        mapMaybeM (compileClause m (Just defName) x typ) clauses
+        mapMaybeM (compileClause m pars (Just defName) x defType) funClauses
 
       when (null cs) $ agda2hsErrorM $
             text "Functions defined with absurd patterns exclusively are not supported."
@@ -185,13 +184,22 @@ compileModuleParams (ExtendTel a tel) = do
       return (Hs.TyFun () a, [Hs.PVar () n])
   ((f .) *** (p++)) <$> underAbstraction a tel compileModuleParams
 
-compileClause :: ModuleName -> Maybe QName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
-compileClause curModule mproj x t c =
+compileClause :: ModuleName -> Args -> Maybe QName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
+compileClause curModule pars mproj x t c =
   withClauseLocals curModule c $ do
-    compileClause' curModule mproj x t c
-
-compileClause' :: ModuleName -> Maybe QName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
-compileClause' curModule projName x ty c@Clause{..} = do
+    compileClause' curModule pars mproj x t c
+
+compileClause' :: ModuleName -> Args -> Maybe QName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
+compileClause' curModule pars projName x ty c = do
+  -- Check whether any parameters (including module parameters) are forced
+  -- See https://github.com/agda/agda2hs/issues/306
+  annPats <- annPats ty (namedClausePats c)
+  traverse (uncurry checkForced) annPats
+  ty' <- piApplyM ty pars
+  compileClause'' curModule projName x ty' (c `apply` pars)
+
+compileClause'' :: ModuleName -> Maybe QName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
+compileClause'' curModule projName x ty c@Clause{..} = do
   reportSDoc "agda2hs.compile" 7  $ "compiling clause: " <+> prettyTCM c
 
   ifNotM (keepClause c) (pure Nothing) $ addContext (KeepNames clauseTel) $ do
@@ -251,6 +259,24 @@ keepClause c@Clause{..} = case (clauseBody, clauseType) of
     DOType     -> __IMPOSSIBLE__
     DOTerm     -> True
 
+checkForced :: Dom Type -> DeBruijnPattern -> C ()
+checkForced a pat
+  = when (usableDom a) $ when (isForcedPat pat)
+  $ agda2hsError "not supported: forced (dot) patterns in non-erased positions"
+
+annPats :: Type -> NAPs -> C [(Dom Type, DeBruijnPattern)]
+annPats ty []       = pure []
+annPats ty (p : ps) = do
+  (a, b) <- recTy (namedArg p)
+  ps'    <- annPats b ps
+  pure $ (a, namedArg p) : ps'
+  where recTy (ProjP po pn) = do
+          ty' <- fromMaybe __IMPOSSIBLE__ <$> getDefType pn ty
+          (a, b) <- mustBePi ty'
+          pure (a, absBody b)
+        recTy pat = do
+          (a, b) <- mustBePi ty
+          pure (a, absApp b (patternToTerm pat))
 
 -- TODO(flupe): projection-like definitions are missing the first (variable) patterns
 --             (that are however present in the type)
@@ -271,7 +297,7 @@ compilePats ty ((namedArg -> pat):ps) = do
   (a, b) <- mustBePi ty
   reportSDoc "agda2hs.compile.pattern" 10 $ text "Compiling pattern:" <+> prettyTCM pat
   let rest = compilePats (absApp b (patternToTerm pat)) ps
-  when (usableDom a) checkForced
+  checkForced a pat
   compileDom a >>= \case
     DOInstance -> rest
     DODropped  -> rest
@@ -279,7 +305,6 @@ compilePats ty ((namedArg -> pat):ps) = do
     DOTerm     -> do
       checkNoAsPatterns pat
       (:) <$> compilePat (unDom a) pat <*> rest
-  where checkForced  = when (isForcedPat pat) $ agda2hsError "not supported: forced (dot) patterns in non-erased positions"
 
 
 compilePat :: Type -> DeBruijnPattern -> C (Hs.Pat ())
diff --git a/src/Agda2Hs/Compile/Function.hs-boot b/src/Agda2Hs/Compile/Function.hs-boot
index e65ac027..ffe0c299 100644
--- a/src/Agda2Hs/Compile/Function.hs-boot
+++ b/src/Agda2Hs/Compile/Function.hs-boot
@@ -1,7 +1,7 @@
 module Agda2Hs.Compile.Function where
 
 import qualified Agda2Hs.Language.Haskell as Hs ( Match, Name )
-import Agda.Syntax.Internal ( Clause, ModuleName, QName, Type )
+import Agda.Syntax.Internal ( Clause, ModuleName, QName, Type, Args )
 import Agda2Hs.Compile.Types ( C )
 
-compileClause' :: ModuleName -> Maybe QName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
+compileClause' :: ModuleName -> Args -> Maybe QName -> Hs.Name () -> Type -> Clause -> C (Maybe (Hs.Match ()))
diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
index 1b93bb8e..6dcd6fc7 100644
--- a/src/Agda2Hs/Compile/Term.hs
+++ b/src/Agda2Hs/Compile/Term.hs
@@ -80,11 +80,8 @@ lambdaCase q ty args = compileLocal $ setCurrentRangeQ q $ do
   npars <- size <$> lookupSection mname
 
   let (pars, rest) = splitAt npars args
-      cs           = applys cls pars
 
-  ty' <- piApplyM ty pars
-
-  cs <- mapMaybeM (compileClause' mname (Just q) (hsName "(lambdaCase)") ty') cs
+  cs <- mapMaybeM (compileClause' mname (map defaultArg pars) (Just q) (hsName "(lambdaCase)") ty) cls
 
   case cs of
     -- If there is a single clause and all proper patterns got erased,
@@ -93,6 +90,7 @@ lambdaCase q ty args = compileLocal $ setCurrentRangeQ q $ do
       | null ps -> return rhs
       | all isVarPat ps -> return $ Hs.Lambda () ps rhs
     _ -> do
+      ty'   <- piApplyM ty pars
       lcase <- hsLCase =<< mapM clauseToAlt cs -- Pattern lambdas cannot have where blocks
       eApp lcase <$> compileArgs ty' rest
       -- undefined -- compileApp lcase (undefined, undefined, rest)
diff --git a/test/AllFailTests.agda b/test/AllFailTests.agda
index 4a5ff11c..b24a5a6e 100644
--- a/test/AllFailTests.agda
+++ b/test/AllFailTests.agda
@@ -41,3 +41,7 @@ import Fail.Issue125
 import Fail.Issue357a
 import Fail.Issue357b
 import Fail.DerivingParseFailure
+import Fail.ErasedPatternLambda
+import Fail.Issue306a
+import Fail.Issue306b
+import Fail.Issue306c
diff --git a/test/AllTests.agda b/test/AllTests.agda
index 753b4067..9430572e 100644
--- a/test/AllTests.agda
+++ b/test/AllTests.agda
@@ -87,7 +87,6 @@ import Issue309
 import Issue317
 import Issue353
 import RankNTypes
-import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
 import FunCon
@@ -102,6 +101,7 @@ import Issue346
 import Issue408
 import CompileTo
 import RuntimeCast
+import Issue306
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -186,7 +186,6 @@ import Issue309
 import Issue317
 import Issue353
 import RankNTypes
-import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
 import FunCon
@@ -201,4 +200,5 @@ import Issue346
 import Issue408
 import CompileTo
 import RuntimeCast
+import Issue306
 #-}
diff --git a/test/ErasedPatternLambda.agda b/test/Fail/ErasedPatternLambda.agda
similarity index 94%
rename from test/ErasedPatternLambda.agda
rename to test/Fail/ErasedPatternLambda.agda
index 29a4a7b0..b60b273c 100644
--- a/test/ErasedPatternLambda.agda
+++ b/test/Fail/ErasedPatternLambda.agda
@@ -1,3 +1,5 @@
+module Fail.ErasedPatternLambda where
+
 open import Haskell.Prelude
 
 Scope = List Bool
diff --git a/test/Fail/Issue306a.agda b/test/Fail/Issue306a.agda
new file mode 100644
index 00000000..b2ef0705
--- /dev/null
+++ b/test/Fail/Issue306a.agda
@@ -0,0 +1,11 @@
+open import Haskell.Prelude
+
+module Fail.Issue306a where
+
+cast : {a b : Set} → @0 a ≡ b → a → b
+cast {a} {b} = cast'
+  where
+  cast' : @0 a ≡ b → a → b
+  cast' refl x = x
+
+{-# COMPILE AGDA2HS cast #-}
diff --git a/test/Fail/Issue306b.agda b/test/Fail/Issue306b.agda
new file mode 100644
index 00000000..d89c12b5
--- /dev/null
+++ b/test/Fail/Issue306b.agda
@@ -0,0 +1,16 @@
+open import Haskell.Prelude
+
+module Fail.Issue306b where
+
+record Foo (a b : Set) : Set where
+  no-eta-equality
+  field
+    coe : a → b
+open Foo public
+
+instance
+  foo : ∀ {a b : Set} → {{@0 _ : a ≡ b}} → Foo a b
+  foo {{refl}} .coe x = x
+
+{-# COMPILE AGDA2HS Foo class #-}
+{-# COMPILE AGDA2HS foo #-}
diff --git a/test/Fail/Issue306c.agda b/test/Fail/Issue306c.agda
new file mode 100644
index 00000000..97e71ec4
--- /dev/null
+++ b/test/Fail/Issue306c.agda
@@ -0,0 +1,17 @@
+open import Haskell.Prelude
+
+module Fail.Issue306c where
+
+record Foo (a b : Set) : Set where
+  no-eta-equality
+  field
+    coe : a → b
+open Foo public
+
+module _ {a b : Set} where
+  instance
+    foo : {{@0 _ : a ≡ b}} → Foo a b
+    foo {{refl}} .coe x = x
+
+{-# COMPILE AGDA2HS Foo class #-}
+{-# COMPILE AGDA2HS foo #-}
diff --git a/test/Issue306.agda b/test/Issue306.agda
new file mode 100644
index 00000000..1e8d6cb5
--- /dev/null
+++ b/test/Issue306.agda
@@ -0,0 +1,20 @@
+open import Haskell.Prelude
+
+-- Unlike the tests in Fail/ related to issue #306, here we check that
+-- instances in modules WITHOUT dot patterns can actually work (previously
+-- threw __IMPOSSIBLE__)
+module Issue306 where
+
+record Foo (a b : Set) : Set where
+  no-eta-equality
+  field
+    coe : a → b
+open Foo public
+
+module _ {a : Set} where
+  instance
+    foo : Foo a a
+    foo .coe x = x
+
+{-# COMPILE AGDA2HS Foo class #-}
+{-# COMPILE AGDA2HS foo #-}

From 51bb9e428cf0e902924effdc5c5a48cc7bb0e508 Mon Sep 17 00:00:00 2001
From: Nathaniel Burke <nathanielrburke3@gmail.com>
Date: Tue, 4 Nov 2025 10:55:22 +0000
Subject: [PATCH 2/5] Make golden

---
 test/golden/AllTests.hs             |  2 +-
 test/golden/ErasedPatternLambda.err |  3 +++
 test/golden/ErasedPatternLambda.hs  | 10 ----------
 test/golden/Issue306.hs             |  9 +++++++++
 test/golden/Issue306a.err           |  3 +++
 test/golden/Issue306b.err           |  3 +++
 test/golden/Issue306c.err           |  3 +++
 7 files changed, 22 insertions(+), 11 deletions(-)
 create mode 100644 test/golden/ErasedPatternLambda.err
 delete mode 100644 test/golden/ErasedPatternLambda.hs
 create mode 100644 test/golden/Issue306.hs
 create mode 100644 test/golden/Issue306a.err
 create mode 100644 test/golden/Issue306b.err
 create mode 100644 test/golden/Issue306c.err

diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index e4eb808b..e3e52384 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -82,7 +82,6 @@ import Issue309
 import Issue317
 import Issue353
 import RankNTypes
-import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
 import FunCon
@@ -97,4 +96,5 @@ import Issue346
 import Issue408
 import CompileTo
 import RuntimeCast
+import Issue306
 
diff --git a/test/golden/ErasedPatternLambda.err b/test/golden/ErasedPatternLambda.err
new file mode 100644
index 00000000..b7991f94
--- /dev/null
+++ b/test/golden/ErasedPatternLambda.err
@@ -0,0 +1,3 @@
+test/Fail/ErasedPatternLambda.agda:19.42-61: error: [CustomBackendError]
+agda2hs:
+  not supported: forced (dot) patterns in non-erased positions
diff --git a/test/golden/ErasedPatternLambda.hs b/test/golden/ErasedPatternLambda.hs
deleted file mode 100644
index 62c0cf9e..00000000
--- a/test/golden/ErasedPatternLambda.hs
+++ /dev/null
@@ -1,10 +0,0 @@
-module ErasedPatternLambda where
-
-data Telescope = ExtendTel Bool Telescope
-
-caseTelBind :: Telescope -> (Bool -> Telescope -> d) -> d
-caseTelBind (ExtendTel a tel) f = f a tel
-
-checkSubst :: Telescope -> Bool
-checkSubst t = caseTelBind t (\ ty rest -> True)
-
diff --git a/test/golden/Issue306.hs b/test/golden/Issue306.hs
new file mode 100644
index 00000000..bd3ab406
--- /dev/null
+++ b/test/golden/Issue306.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables #-}
+module Issue306 where
+
+class Foo a b where
+    coe :: a -> b
+
+instance forall a . Foo a a where
+    coe x = x
+
diff --git a/test/golden/Issue306a.err b/test/golden/Issue306a.err
new file mode 100644
index 00000000..d65b6599
--- /dev/null
+++ b/test/golden/Issue306a.err
@@ -0,0 +1,3 @@
+test/Fail/Issue306a.agda:5.1-5: error: [CustomBackendError]
+agda2hs:
+  not supported: forced (dot) patterns in non-erased positions
diff --git a/test/golden/Issue306b.err b/test/golden/Issue306b.err
new file mode 100644
index 00000000..9f24377f
--- /dev/null
+++ b/test/golden/Issue306b.err
@@ -0,0 +1,3 @@
+test/Fail/Issue306b.agda:12.3-6: error: [CustomBackendError]
+agda2hs:
+  not supported: forced (dot) patterns in non-erased positions
diff --git a/test/golden/Issue306c.err b/test/golden/Issue306c.err
new file mode 100644
index 00000000..ab595537
--- /dev/null
+++ b/test/golden/Issue306c.err
@@ -0,0 +1,3 @@
+test/Fail/Issue306c.agda:13.5-8: error: [CustomBackendError]
+agda2hs:
+  not supported: forced (dot) patterns in non-erased positions

From c66a5bcbc22386a4cc55bc1dbdb9a2087b5e8631 Mon Sep 17 00:00:00 2001
From: Nathaniel Burke <nathanielrburke3@gmail.com>
Date: Tue, 4 Nov 2025 12:55:40 +0000
Subject: [PATCH 3/5] Rename checkForced

checkForced now also checks the pattern is non-erased, so that should
probably be made clear with the name
---
 src/Agda2Hs/Compile/ClassInstance.hs |  2 +-
 src/Agda2Hs/Compile/Function.hs      | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs
index 5cbd8fa3..9a41b94b 100644
--- a/src/Agda2Hs/Compile/ClassInstance.hs
+++ b/src/Agda2Hs/Compile/ClassInstance.hs
@@ -303,7 +303,7 @@ compileInstanceClause' curModule ty (p:ps) c
 --              if there is something other than erased parameters
 compileInstanceClause' curModule ty (p:ps) c = do
   (a, b) <- mustBePi ty
-  checkForced a (namedArg p)
+  checkNonErasedForced a (namedArg p)
   compileInstanceClause' curModule (absApp b (patternToTerm $ namedArg p)) ps c
 
 fieldArgInfo :: QName -> C ArgInfo
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
index 988888ca..9697cced 100644
--- a/src/Agda2Hs/Compile/Function.hs
+++ b/src/Agda2Hs/Compile/Function.hs
@@ -194,7 +194,7 @@ compileClause' curModule pars projName x ty c = do
   -- Check whether any parameters (including module parameters) are forced
   -- See https://github.com/agda/agda2hs/issues/306
   annPats <- annPats ty (namedClausePats c)
-  traverse (uncurry checkForced) annPats
+  traverse (uncurry checkNonErasedForced) annPats
   ty' <- piApplyM ty pars
   compileClause'' curModule projName x ty' (c `apply` pars)
 
@@ -259,9 +259,9 @@ keepClause c@Clause{..} = case (clauseBody, clauseType) of
     DOType     -> __IMPOSSIBLE__
     DOTerm     -> True
 
-checkForced :: Dom Type -> DeBruijnPattern -> C ()
-checkForced a pat
-  = when (usableDom a) $ when (isForcedPat pat)
+checkNonErasedForced :: Dom Type -> DeBruijnPattern -> C ()
+checkNonErasedForced a pat
+  = when (usableDom a && isForcedPat pat)
   $ agda2hsError "not supported: forced (dot) patterns in non-erased positions"
 
 annPats :: Type -> NAPs -> C [(Dom Type, DeBruijnPattern)]
@@ -297,7 +297,7 @@ compilePats ty ((namedArg -> pat):ps) = do
   (a, b) <- mustBePi ty
   reportSDoc "agda2hs.compile.pattern" 10 $ text "Compiling pattern:" <+> prettyTCM pat
   let rest = compilePats (absApp b (patternToTerm pat)) ps
-  checkForced a pat
+  checkNonErasedForced a pat
   compileDom a >>= \case
     DOInstance -> rest
     DODropped  -> rest

From b26e677dd99b931d2d14f2d29a160f3b639d26e3 Mon Sep 17 00:00:00 2001
From: Nathaniel Burke <nathanielrburke3@gmail.com>
Date: Tue, 4 Nov 2025 12:58:51 +0000
Subject: [PATCH 4/5] Remove redundant forced pattern check

Actually, given we check for dotted patterns earlier in compileClause',
I don't think there is any need to checkNonErasedForced in compilePats?
---
 src/Agda2Hs/Compile/Function.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
index 9697cced..54018e74 100644
--- a/src/Agda2Hs/Compile/Function.hs
+++ b/src/Agda2Hs/Compile/Function.hs
@@ -297,7 +297,6 @@ compilePats ty ((namedArg -> pat):ps) = do
   (a, b) <- mustBePi ty
   reportSDoc "agda2hs.compile.pattern" 10 $ text "Compiling pattern:" <+> prettyTCM pat
   let rest = compilePats (absApp b (patternToTerm pat)) ps
-  checkNonErasedForced a pat
   compileDom a >>= \case
     DOInstance -> rest
     DODropped  -> rest

From 8125ca211d74172f6f5078c30f141300436edd52 Mon Sep 17 00:00:00 2001
From: Nathaniel Burke <nathanielrburke3@gmail.com>
Date: Tue, 4 Nov 2025 15:21:44 +0000
Subject: [PATCH 5/5] Allow dot patterns on non-dependent args

---
 src/Agda2Hs/Compile/ClassInstance.hs     |  2 +-
 src/Agda2Hs/Compile/Function.hs          | 13 +++++++------
 src/Agda2Hs/Compile/Term.hs              | 12 +++++++++++-
 test/AllFailTests.agda                   |  1 -
 test/AllTests.agda                       |  2 ++
 test/{Fail => }/ErasedPatternLambda.agda |  2 --
 test/golden/AllTests.hs                  |  1 +
 test/golden/ErasedPatternLambda.err      |  3 ---
 test/golden/ErasedPatternLambda.hs       | 10 ++++++++++
 9 files changed, 32 insertions(+), 14 deletions(-)
 rename test/{Fail => }/ErasedPatternLambda.agda (94%)
 delete mode 100644 test/golden/ErasedPatternLambda.err
 create mode 100644 test/golden/ErasedPatternLambda.hs

diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs
index 9a41b94b..0e5aa5b3 100644
--- a/src/Agda2Hs/Compile/ClassInstance.hs
+++ b/src/Agda2Hs/Compile/ClassInstance.hs
@@ -303,7 +303,7 @@ compileInstanceClause' curModule ty (p:ps) c
 --              if there is something other than erased parameters
 compileInstanceClause' curModule ty (p:ps) c = do
   (a, b) <- mustBePi ty
-  checkNonErasedForced a (namedArg p)
+  checkIllegalForced a (namedArg p)
   compileInstanceClause' curModule (absApp b (patternToTerm $ namedArg p)) ps c
 
 fieldArgInfo :: QName -> C ArgInfo
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
index 54018e74..bff80df0 100644
--- a/src/Agda2Hs/Compile/Function.hs
+++ b/src/Agda2Hs/Compile/Function.hs
@@ -37,7 +37,7 @@ import Agda.Utils.Size ( Sized(size) )
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName )
-import Agda2Hs.Compile.Term ( compileTerm, usableDom )
+import Agda2Hs.Compile.Term ( compileTerm, usableDom, dependentDom )
 import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileDomType )
 import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )
 import Agda2Hs.Compile.Types
@@ -194,7 +194,7 @@ compileClause' curModule pars projName x ty c = do
   -- Check whether any parameters (including module parameters) are forced
   -- See https://github.com/agda/agda2hs/issues/306
   annPats <- annPats ty (namedClausePats c)
-  traverse (uncurry checkNonErasedForced) annPats
+  traverse (uncurry checkIllegalForced) annPats
   ty' <- piApplyM ty pars
   compileClause'' curModule projName x ty' (c `apply` pars)
 
@@ -259,10 +259,11 @@ keepClause c@Clause{..} = case (clauseBody, clauseType) of
     DOType     -> __IMPOSSIBLE__
     DOTerm     -> True
 
-checkNonErasedForced :: Dom Type -> DeBruijnPattern -> C ()
-checkNonErasedForced a pat
-  = when (usableDom a && isForcedPat pat)
-  $ agda2hsError "not supported: forced (dot) patterns in non-erased positions"
+checkIllegalForced :: Dom Type -> DeBruijnPattern -> C ()
+checkIllegalForced a pat = do
+  dep <- dependentDom a
+  when (dep && isForcedPat pat) $ agda2hsError
+    "not supported: forced (dot) patterns in non-erased positions"
 
 annPats :: Type -> NAPs -> C [(Dom Type, DeBruijnPattern)]
 annPats ty []       = pure []
diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs
index 6dcd6fc7..175ad957 100644
--- a/src/Agda2Hs/Compile/Term.hs
+++ b/src/Agda2Hs/Compile/Term.hs
@@ -41,7 +41,7 @@ import Agda.Utils.Size
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName, importInstance )
 
-import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTelSize )
+import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTelSize, compileDomType )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )
@@ -499,6 +499,16 @@ usableDom :: Dom Type -> Bool
 usableDom dom | Prop _ <- getSort dom = False
 usableDom dom = usableModality dom
 
+-- | Check whether a domain is dependent on the Haskell side (i.e. it is
+-- compiled to a forall)
+dependentDom :: Dom Type -> C Bool
+dependentDom dom = do
+  d' <- compileDom dom
+  pure $ case d' of
+    DOType     -> True
+    DOTerm     -> False
+    DOInstance -> False
+    DODropped  -> False
 
 compileLam :: Type -> ArgInfo -> Abs Term -> C (Hs.Exp ())
 compileLam ty argi abs = do
diff --git a/test/AllFailTests.agda b/test/AllFailTests.agda
index b24a5a6e..50933dbc 100644
--- a/test/AllFailTests.agda
+++ b/test/AllFailTests.agda
@@ -41,7 +41,6 @@ import Fail.Issue125
 import Fail.Issue357a
 import Fail.Issue357b
 import Fail.DerivingParseFailure
-import Fail.ErasedPatternLambda
 import Fail.Issue306a
 import Fail.Issue306b
 import Fail.Issue306c
diff --git a/test/AllTests.agda b/test/AllTests.agda
index 9430572e..c1e1c2c6 100644
--- a/test/AllTests.agda
+++ b/test/AllTests.agda
@@ -87,6 +87,7 @@ import Issue309
 import Issue317
 import Issue353
 import RankNTypes
+import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
 import FunCon
@@ -186,6 +187,7 @@ import Issue309
 import Issue317
 import Issue353
 import RankNTypes
+import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
 import FunCon
diff --git a/test/Fail/ErasedPatternLambda.agda b/test/ErasedPatternLambda.agda
similarity index 94%
rename from test/Fail/ErasedPatternLambda.agda
rename to test/ErasedPatternLambda.agda
index b60b273c..29a4a7b0 100644
--- a/test/Fail/ErasedPatternLambda.agda
+++ b/test/ErasedPatternLambda.agda
@@ -1,5 +1,3 @@
-module Fail.ErasedPatternLambda where
-
 open import Haskell.Prelude
 
 Scope = List Bool
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index e3e52384..3c1b53b5 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -82,6 +82,7 @@ import Issue309
 import Issue317
 import Issue353
 import RankNTypes
+import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
 import FunCon
diff --git a/test/golden/ErasedPatternLambda.err b/test/golden/ErasedPatternLambda.err
deleted file mode 100644
index b7991f94..00000000
--- a/test/golden/ErasedPatternLambda.err
+++ /dev/null
@@ -1,3 +0,0 @@
-test/Fail/ErasedPatternLambda.agda:19.42-61: error: [CustomBackendError]
-agda2hs:
-  not supported: forced (dot) patterns in non-erased positions
diff --git a/test/golden/ErasedPatternLambda.hs b/test/golden/ErasedPatternLambda.hs
new file mode 100644
index 00000000..62c0cf9e
--- /dev/null
+++ b/test/golden/ErasedPatternLambda.hs
@@ -0,0 +1,10 @@
+module ErasedPatternLambda where
+
+data Telescope = ExtendTel Bool Telescope
+
+caseTelBind :: Telescope -> (Bool -> Telescope -> d) -> d
+caseTelBind (ExtendTel a tel) f = f a tel
+
+checkSubst :: Telescope -> Bool
+checkSubst t = caseTelBind t (\ ty rest -> True)
+