[ re agda#305 ] Set the checkpoint in the context of the module rathe…

…r than the clause

src/Agda2Hs/Compile/ClassInstance.hs

@@ -25,9 +25,9 @@ import Agda.Syntax.Scope.Monad ( resolveName )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
 import Agda.TypeChecking.Pretty
-import Agda.TypeChecking.Substitute ( Apply(applyE), absBody, absApp )
+import Agda.TypeChecking.Substitute ( Apply(applyE), absBody, absApp, apply )
 import Agda.TypeChecking.Records
-import Agda.TypeChecking.Telescope ( mustBePi )
+import Agda.TypeChecking.Telescope ( mustBePi, piApplyM )
 
 import Agda.Utils.Lens
 import Agda.Utils.Monad ( ifNotM )
@@ -83,14 +83,20 @@ compileInstance ToDefinition def@Defn{..} =
         map (nest 2 . prettyTCM) funClauses
       let mod = qnameModule defName
       reportSDoc "agda2hs.compile.instance" 25 $ text "compileInstance module: " <+> prettyTCM mod
-      (ds, rs) <- concatUnzip
-              <$> 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
-      when (length (nub rs) > 1) $
-        genericDocError =<< fsep (pwords "More than one minimal record used.")
-      return $ Hs.InstDecl () Nothing ir (Just ds)
+      tel <- lookupSection mod
+      addContext tel $ do
+        liftTCM $ setModuleCheckpoint mod
+        pars <- getContextArgs
+        ty <- defType `piApplyM` pars
+        let clauses = funClauses `apply` pars
+        (ds, rs) <- concatUnzip
+                <$> mapM (\c -> withClauseLocals mod c $ compileInstanceClause mod ty c) clauses
+        reportSDoc "agda2hs.compile.instance" 20 $ vcat $
+          text "compileInstance compiled clauses: " :
+          map (nest 2 . text . pp) ds
+        when (length (nub rs) > 1) $
+          genericDocError =<< fsep (pwords "More than one minimal record used.")
+        return $ Hs.InstDecl () Nothing ir (Just ds)
     where Function{..} = theDef
 
 
@@ -182,6 +188,13 @@ compileInstanceClause' curModule ty (p:ps) c
     (q, _, _) <- origProjection q
     arg <- fieldArgInfo q
 
+
+    reportSDoc "agda2hs.compile.instance" 15 $
+      text "Compiling instance clause for" <+> prettyTCM (Arg arg $ Def q [])
+
+    reportSDoc "agda2hs.compile.instance" 15 $
+      text "Instance type: " <+> prettyTCM ty
+
     -- retrieve the type of the projection
     Just (unEl -> Pi a b) <- getDefType q ty
     -- We don't really have the information available to reconstruct the instance
@@ -190,9 +203,6 @@ compileInstanceClause' curModule ty (p:ps) c
     let instanceHead = __DUMMY_TERM__ 
         ty' = b `absApp` instanceHead
 
-    reportSDoc "agda2hs.compile.instance" 15 $
-      text "Compiling instance clause for" <+> prettyTCM (Arg arg $ Def q [])
-
     reportSDoc "agda2hs.compile.instance" 15 $
       text "Clause type: " <+> prettyTCM ty'
 

src/Agda2Hs/Compile/Function.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 module Agda2Hs.Compile.Function where
 
+import Control.Arrow ( (***) )
 import Control.Monad ( (>=>), filterM, forM_ )
 import Control.Monad.Reader ( asks, local )
 
@@ -40,7 +41,7 @@ import Agda.Utils.Size ( Sized(size) )
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName )
 import Agda2Hs.Compile.Term ( compileTerm, usableDom )
-import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..) )
+import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileDomType )
 import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
@@ -115,23 +116,29 @@ compileFun withSig def@Defn{..} =
     $ compileFun' withSig def
 
 -- inherit existing (instantiated) locals
-compileFun' withSig def@Defn{..} = inTopContext $ do
+compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
   reportSDoc "agda2hs.compile" 6 $ "Compiling function: " <+> prettyTCM defName
 
   whenM ((withSig &&) <$> inRecordMod defName) $
     genericDocError =<< text "not supported by agda2hs: functions inside a record module"
 
-  -- We add the module parameters to the context
-  -- if we are compiling a local function (e.g. a where declaration or pattern-matching lambda)
-  isLocalFun <- asks compilingLocal
-  tel <- if isLocalFun then lookupSection m else return EmptyTel
-
-  withCurrentModule m $ addContext tel $ do
-    ifM (endsInSort defType)
-        -- if the function type ends in Sort, it's a type alias!
-        (ensureNoLocals err >> compileTypeDef x def) 
-        -- otherwise, we have to compile clauses.
-        $ do
+  ifM (endsInSort defType)
+    -- if the function type ends in Sort, it's a type alias!
+    (ensureNoLocals err >> compileTypeDef x def) 
+    -- otherwise, we have to compile clauses.
+    $ do
+    tel <- lookupSection m
+
+    -- If this is a top-level function, we compile the module parameters so
+    -- we can add them to the type signature and patterns.
+    (paramTy , paramPats) <- ifM (asks compilingLocal) (return (id, [])) $ compileModuleParams tel
+
+    addContext tel $ do
+
+      -- Jesper: we need to set the checkpoint for the current module so that
+      -- the canonicity check for typeclass instances picks up the
+      -- module parameters (see https://github.com/agda/agda2hs/issues/305).
+      liftTCM $ setModuleCheckpoint m
 
       pars <- getContextArgs
       reportSDoc "agda2hs.compile.type" 8 $ "Function module parameters: " <+> prettyTCM pars
@@ -142,12 +149,13 @@ compileFun' withSig def@Defn{..} = inTopContext $ do
 
       sig <- if not withSig then return [] else do
         checkValidFunName x
-        ty <- compileType $ unEl typ
+        ty <- paramTy <$> compileType (unEl typ)
         reportSDoc "agda2hs.compile.type" 8 $ "Compiled function type: " <+> text (Hs.prettyPrint ty) 
         return [Hs.TypeSig () [x] ty]
 
       let clauses = funClauses `apply` pars
-      cs  <- mapMaybeM (compileClause m (Just defName) x typ) clauses
+      cs  <- map (addPats paramPats) <$>
+        mapMaybeM (compileClause m (Just defName) x typ) clauses
 
       when (null cs) $ genericDocError
         =<< text "Functions defined with absurd patterns exclusively are not supported."
@@ -161,6 +169,23 @@ compileFun' withSig def@Defn{..} = inTopContext $ do
     x = hsName $ prettyShow n
     err = "Not supported: type definition with `where` clauses"
 
+    addPats :: [Hs.Pat ()] -> Hs.Match () -> Hs.Match ()
+    addPats [] cl = cl
+    addPats ps (Hs.Match l f qs rhs bs) = Hs.Match l f (ps++qs) rhs bs
+    addPats (p:ps) (Hs.InfixMatch l q f qs rhs bs) = Hs.InfixMatch l p f (ps++q:qs) rhs bs
+
+compileModuleParams :: Telescope -> C (Hs.Type () -> Hs.Type () , [Hs.Pat ()])
+compileModuleParams EmptyTel = return (id, [])
+compileModuleParams (ExtendTel a tel) = do
+  (f , p) <- compileDomType (absName tel) a >>= \case
+    DomDropped -> return (id, [])
+    DomConstraint c -> return (constrainType c, [])
+    DomForall a -> return (qualifyType a, [])
+    DomType s a -> do
+      let n = hsName $ absName tel
+      checkValidVarName n
+      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 =
@@ -181,11 +206,6 @@ compileClause' curModule projName x ty c@Clause{..} = do
     ls <- asks locals
     reportSDoc "agda2hs.compile" 18 $ "Clause locals:" <+> prettyTCM ls
 
-    -- Jesper: we need to set the checkpoint for the current module so that
-    -- the canonicity check for typeclass instances picks up the
-    -- module parameters (see https://github.com/agda/agda2hs/issues/305).
-    liftTCM $ setModuleCheckpoint curModule
-
     toDrop <- case projName of
       Nothing -> pure 0
       Just q  -> maybe 0 (pred . projIndex) <$> isProjection q

src/Agda2Hs/Compile/Term.hs

@@ -75,7 +75,7 @@ lambdaCase q ty args = compileLocal $ setCurrentRangeQ q $ do
 
   ty' <- piApplyM ty pars
 
-  cs <- mapMaybeM (compileClause' (qnameModule q) (Just q) (hsName "(lambdaCase)") ty') cs
+  cs <- mapMaybeM (compileClause' mname (Just q) (hsName "(lambdaCase)") ty') cs
 
   case cs of
     -- If there is a single clause and all patterns got erased, we

test/Issue305.agda

@@ -31,6 +31,16 @@ anotherTest = test
 
 {-# COMPILE AGDA2HS anotherTest #-}
 
+yetAnotherTest : Int
+yetAnotherTest = case Just True of λ where
+  Nothing → error "unreachable"
+  (Just y) → foo 5
+{-# COMPILE AGDA2HS yetAnotherTest #-}
+
+andOneMoreTest : Int → Int
+andOneMoreTest x = foo 5
+{-# COMPILE AGDA2HS andOneMoreTest #-}
+
 record Subclass (a : Set) : Set where
   field
     overlap {{super}} : Class a

test/golden/Issue305.hs

@@ -15,6 +15,15 @@ test = foo 41
 anotherTest :: Int
 anotherTest = test
 
+yetAnotherTest :: Int
+yetAnotherTest
+  = case Just True of
+        Nothing -> error "unreachable"
+        Just y -> foo 5
+
+andOneMoreTest :: Int -> Int
+andOneMoreTest x = foo 5
+
 class Class a => Subclass a where
     bar :: a