diff --git a/src/comp/CVPrint.hs b/src/comp/CVPrint.hs
index 8f97ace07..c556221b3 100644
--- a/src/comp/CVPrint.hs
+++ b/src/comp/CVPrint.hs
@@ -50,6 +50,7 @@ module CVPrint (
 import Prelude hiding ((<>))
 #endif
 
+import Control.Applicative((<|>))
 import Data.Char(toLower)
 import Data.List(genericReplicate)
 import Lex(isIdChar)
@@ -152,9 +153,13 @@ p2defs :: PDetail -> CDefn -> CDefn -> Doc
 p2defs d (CPragma (Pproperties _ props))
          (CValueSign df2@(CDef i qt@(CQType ps ty) cs@[CClause cps [] cexp])) | all isVar cps =
       let (ys, x) = getArrows ty
-          ity = case x of (TAp (TCon _) y) -> y;
-                          (TAp (TVar _) y) -> y;
-                          z -> z
+          -- mModTC will be `Just modTC` if the return type is an application of
+          -- a type constructor (e.g., `Module`) to some type, where modTC is
+          -- the type constructor. Otherwise, mModTC will be Nothing.
+          (mModTC, ity) = case x of
+                            TAp (TCon modTC) y -> (Just modTC, y)
+                            TAp (TVar _) y -> (Nothing, y)
+                            z -> (Nothing, z)
           f [] = empty
           f xs = t"#(" <>
                  sepList (zipWith (\ x c -> -- t"parameter" <+>
@@ -162,7 +167,16 @@ p2defs d (CPragma (Pproperties _ props))
                                   xs cps)
                  (t",") <> t")"
           (mId,ps') = findModId ps
-          line1 = t"module" <+> pvpId d i <> f ys <> t"(" <> pvPrint d 0 ity <> t")"
+          -- Check if we need to print `[<module-ty>]` after the `module`
+          -- keyword. This can happen if the return type is an application of a
+          -- type constructor (e.g., `Module`) to some type, or if the return
+          -- type is an application of a type variable with a corresponding
+          -- IsModule constraint. If one of these conditions hold, then mPPMod
+          -- will be `Just <pretty-printed-module>`. Otherwise, mPPMod will be
+          -- Nothing.
+          mPPMod = fmap (pvPrint d 0) mModTC <|> fmap (pvPrint d 0) mId
+          line1 = t"module" <+> maybe empty brackets mPPMod
+                            <+> pvpId d i <> f ys <> t"(" <> pvPrint d 0 ity <> t")"
        in
         if isModule mId x then
          (pProps d props $+$
@@ -976,12 +990,14 @@ ppBody d isMod (Cletrec ds e) =
 ppBody d True e = (pparen True (pp d e) <> t";")
 ppBody d _ e = (t"  return" <+> pparen True (pvPrint d 1 e) <> t";")
 
+-- Search for a CPred of the form IsModule#(m, c) in the list of CPreds `ps`. If
+-- one is found, return (Just m, ps). Otherwise, return (Nothing, []).
 findModId :: [CPred] -> (Maybe Id, [CPred])
 findModId [] = (Nothing,[])
 findModId (p:ps) =
    case p of
      (CPred (CTypeclass isM) [TVar (TyVar iM _ _), _]) | getIdBaseString isM == getIdBaseString idIsModule
-       -> (Just iM,ps)
+       -> (Just iM,p:ps)
      _ -> let (i,ps') = findModId ps in (i,p:ps')
 
 ppValueSignRest :: PDetail -> Doc -> [CPred] -> Bool -> Bool -> Doc -> CExpr -> String -> Doc
diff --git a/testsuite/bsc.syntax/bsv05_parse_pretty/.gitignore b/testsuite/bsc.syntax/bsv05_parse_pretty/.gitignore
index 0fc27f7bb..46ba4ca8f 100644
--- a/testsuite/bsc.syntax/bsv05_parse_pretty/.gitignore
+++ b/testsuite/bsc.syntax/bsv05_parse_pretty/.gitignore
@@ -4,6 +4,7 @@ EmptyRule.bsv-pretty-out.bsv
 Map.bsv-pretty-out.bsv
 MethodCalledMethodI.bsv-pretty-out.bsv
 MethodCalledMethodII.bsv-pretty-out.bsv
+ModuleArgument.bsv-pretty-out.bsv
 MethodReturn.bsv-pretty-out.bsv
 PopCount0.bsv-pretty-out.bsv
 TypedefStruct.bsv-pretty-out.bsv
diff --git a/testsuite/bsc.syntax/bsv05_parse_pretty/ModuleArgument.bsv b/testsuite/bsc.syntax/bsv05_parse_pretty/ModuleArgument.bsv
new file mode 100644
index 000000000..587804fe6
--- /dev/null
+++ b/testsuite/bsc.syntax/bsv05_parse_pretty/ModuleArgument.bsv
@@ -0,0 +1,12 @@
+package ModuleArgument;
+
+module [Module] helloWorld#(Module#(Empty) mod)(Empty);
+  let e <- mod;
+endmodule
+
+module [m] fooBar#(m#(Empty) mod)(Empty)
+  provisos (IsModule#(m, c));
+  let e <- mod;
+endmodule
+
+endpackage
diff --git a/testsuite/bsc.syntax/bsv05_parse_pretty/bsv05-parse-pretty.exp b/testsuite/bsc.syntax/bsv05_parse_pretty/bsv05-parse-pretty.exp
index 328d974ca..38ae5f833 100644
--- a/testsuite/bsc.syntax/bsv05_parse_pretty/bsv05-parse-pretty.exp
+++ b/testsuite/bsc.syntax/bsv05_parse_pretty/bsv05-parse-pretty.exp
@@ -11,7 +11,7 @@ proc bsc_compile_prettyprint_parse { source { options "" } } {
 }
 
 proc compile_ppp_pass { source {options ""} } {
-    incr_stat "compile_ppp_pass" 
+    incr_stat "compile_ppp_pass"
     if [bsc_compile_prettyprint_parse $source $options] {
         pass "`$source' compiles, pretty-prints, and compiles again"
     } else {
@@ -54,3 +54,6 @@ compile_ppp_pass PopCount0.bsv
 
 # Map (function arguments)
 compile_ppp_pass Map.bsv
+
+# a function with a Module as an argument (regression test for #663)
+compile_ppp_pass ModuleArgument.bsv