[ fix #306 ] Correctly error on dot patterns corresponding to module arguments (#439)

* [ #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

* Make golden

* Rename checkForced

checkForced now also checks the pattern is non-erased, so that should
probably be made clear with the name

* 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?

* Allow dot patterns on non-dependent args

Author: NathanielB123

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,16 +97,16 @@ 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
       fty <- defType <$> getConstInfo f
       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
+  checkIllegalForced a (namedArg p)
   compileInstanceClause' curModule (absApp b (patternToTerm $ namedArg p)) ps c
 
 fieldArgInfo :: QName -> C ArgInfo

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
@@ -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
@@ -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 checkIllegalForced) 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,25 @@ keepClause c@Clause{..} = case (clauseBody, clauseType) of
     DOType     -> __IMPOSSIBLE__
     DOTerm     -> True
 
+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 []
+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,15 +298,13 @@ 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
   compileDom a >>= \case
     DOInstance -> rest
     DODropped  -> rest
     DOType     -> rest
     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 ())

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 ()))

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 )
@@ -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)
@@ -501,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,3 +41,6 @@ import Fail.Issue125
 import Fail.Issue357a
 import Fail.Issue357b
 import Fail.DerivingParseFailure
+import Fail.Issue306a
+import Fail.Issue306b
+import Fail.Issue306c

test/AllTests.agda

@@ -102,6 +102,7 @@ import Issue346
 import Issue408
 import CompileTo
 import RuntimeCast
+import Issue306
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -201,4 +202,5 @@ import Issue346
 import Issue408
 import CompileTo
 import RuntimeCast
+import Issue306
 #-}

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 #-}

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 #-}

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 #-}

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 #-}