Allow dot patterns on non-dependent args

Author: NathanielB123

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

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 []

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

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

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

test/Cubical/StreamFusion.agda

@@ -1,28 +0,0 @@
-module Cubical.StreamFusion where
-
-open import Haskell.Prelude
-
-open import Agda.Primitive.Cubical
-open import Agda.Builtin.Equality
-open import Agda.Builtin.Size
-
-variable
-  @0 i : Size
-
-record Stream (a : Type) (@0 i : Size) : Type where
-  pattern; inductive; constructor _:>_
-  field
-    shead : a
-    stail : ∀ {@0 j} → Stream a j
-open Stream public
-
-{-# COMPILE AGDA2HS Stream #-}
-
-smap  : (a → b) → Stream a i → Stream b i
-smap  f (x :> xs) = (f x) :> smap f xs
-
-{-# COMPILE AGDA2HS smap #-}
-
-smap-fusion  : (f : a → b) (g : b → c) (s : Stream a i)
-             → PathP (λ _ → Stream c i) (smap {i = i} g (smap {i = i} f s)) (smap {i = i} (λ x → g (f x)) s)
-smap-fusion  f g (hd :> tl) i = (g (f hd)) :> smap-fusion f g tl i

test/Fail/ErasedPatternLambda.agda renamed to test/ErasedPatternLambda.agda

@@ -1,5 +1,3 @@
-module Fail.ErasedPatternLambda where
-
 open import Haskell.Prelude
 
 Scope = List Bool

test/golden/AllTests.hs

@@ -82,6 +82,7 @@ import Issue309
 import Issue317
 import Issue353
 import RankNTypes
+import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
 import FunCon

test/golden/ErasedPatternLambda.err

@@ -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)
+