diff --git a/src/Lean/Compiler/LCNF/PrettyPrinter.lean b/src/Lean/Compiler/LCNF/PrettyPrinter.lean
index ecfec3a5b1..6d3f0c5c90 100644
--- a/src/Lean/Compiler/LCNF/PrettyPrinter.lean
+++ b/src/Lean/Compiler/LCNF/PrettyPrinter.lean
@@ -79,9 +79,12 @@ def ppLetDecl (letDecl : LetDecl) : M Format := do
   else
     return f!"let {letDecl.binderName} := {← ppValue letDecl.value}"
 
+def getFunType (ps : Array Param) (type : Expr) : CoreM Expr :=
+  instantiateForall type (ps.map (mkFVar ·.fvarId))
+
 mutual
   partial def ppFunDecl (funDecl : FunDecl) : M Format := do
-    return f!"{funDecl.binderName}{← ppParams funDecl.params} :={indentD (← ppCode funDecl.value)}"
+    return f!"{funDecl.binderName}{← ppParams funDecl.params} : {← ppExpr (← getFunType funDecl.params funDecl.type)} :={indentD (← ppCode funDecl.value)}"
 
   partial def ppAlt (alt : Alt) : M Format := do
     match alt with
@@ -110,11 +113,11 @@ def ppCode (code : Code) : CompilerM Format :=
 
 def ppDecl (decl : Decl) : CompilerM Format :=
   PP.run do
-    return f!"def {decl.name}{← PP.ppParams decl.params} :={indentD (← PP.ppCode decl.value)}"
+    return f!"def {decl.name}{← PP.ppParams decl.params} : {← PP.ppExpr (← PP.getFunType decl.params decl.type)} :={indentD (← PP.ppCode decl.value)}"
 
 def ppFunDecl (decl : FunDecl) : CompilerM Format :=
   PP.run do
-    return f!"fun {decl.binderName}{← PP.ppParams decl.params} :={indentD (← PP.ppCode decl.value)}"
+    return f!"fun {← PP.ppFunDecl decl}"
 
 /--
 Similar to `ppDecl`, but in `CoreM`, and it does not assume