Tweak function `quantifyType` to fix #12449

In function `compiler/GHC/Runtime/Heap/Inspect.hs:quantifyType` replace
`tcSplitForAllInvisTyVars` by `tcSplitNestedSigmaTys`. This will properly split
off the nested foralls in examples like `:print fmap`.

Do not remove the `forall`s from the `snd` part of the tuple returned
by `quantifyType`. It's not necessary and the reason for the bug in #12449.

Some code simplifications at the calling sites of `quantifyTypes`.

9 files changed, 75 insertions, 38 deletions

diff --git a/compiler/GHC/Runtime/Heap/Inspect.hs b/compiler/GHC/Runtime/Heap/Inspect.hs
index 0ec936265e..0aa8eb53f8 100644
--- a/compiler/GHC/Runtime/Heap/Inspect.hs
+++ b/compiler/GHC/Runtime/Heap/Inspect.hs
@@ -606,7 +606,8 @@ polytype (specifically, see ghci_tv in GHC.Tc.Utils.Unify.preCheck).
 This allows metavariables to unify with types that have
 nested (or higher-rank) `forall`s/`=>`s, which makes `:print fmap`
 display as
-`fmap = (_t1::forall a b. Functor f => (a -> b) -> f a -> f b)`, as expected.
+`fmap = (_t1::forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b)`,
+as expected.
 -}
 
 
@@ -690,13 +691,12 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
   -- we quantify existential tyvars as universal,
   -- as this is needed to be able to manipulate
   -- them properly
-   let quant_old_ty@(old_tvs, old_tau) = quantifyType old_ty
-       sigma_old_ty = mkInfForAllTys old_tvs old_tau
+   let quant_old_ty@(old_tvs, _) = quantifyType old_ty
    traceTR (text "Term reconstruction started with initial type " <> ppr old_ty)
    term <-
      if null old_tvs
       then do
-        term  <- go max_depth sigma_old_ty sigma_old_ty hval
+        term  <- go max_depth old_ty old_ty hval
         term' <- zonkTerm term
         return $ fixFunDictionaries $ expandNewtypes term'
       else do
@@ -704,7 +704,7 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
               my_ty <- newOpenVar
               when (check1 quant_old_ty) (traceTR (text "check1 passed") >>
                                           addConstraint my_ty old_ty')
-              term  <- go max_depth my_ty sigma_old_ty hval
+              term  <- go max_depth my_ty old_ty hval
               new_ty <- zonkTcType (termType term)
               if isMonomorphic new_ty || check2 (quantifyType new_ty) quant_old_ty
                  then do
@@ -734,10 +734,6 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
   unit_env = hsc_unit_env hsc_env
 
   go :: Int -> Type -> Type -> ForeignHValue -> TcM Term
-   -- I believe that my_ty should not have any enclosing
-   -- foralls, nor any free RuntimeUnk skolems;
-   -- that is partly what the quantifyType stuff achieved
-   --
    -- [SPJ May 11] I don't understand the difference between my_ty and old_ty
 
   go 0 my_ty _old_ty a = do
@@ -1080,8 +1076,6 @@ getDataConArgTys :: DataCon -> Type -> TR [Type]
 -- return the types of the arguments.  This is RTTI-land, so 'ty' might
 -- not be fully known.  Moreover, the arg types might involve existentials;
 -- if so, make up fresh RTTI type variables for them
---
--- I believe that con_app_ty should not have any enclosing foralls
 getDataConArgTys dc con_app_ty
   = do { let rep_con_app_ty = unwrapType con_app_ty
        ; traceTR (text "getDataConArgTys 1" <+> (ppr con_app_ty $$ ppr rep_con_app_ty
@@ -1384,18 +1378,12 @@ tyConPhantomTyVars _ = []
 
 type QuantifiedType = ([TyVar], Type)
    -- Make the free type variables explicit
-   -- The returned Type should have no top-level foralls (I believe)
 
 quantifyType :: Type -> QuantifiedType
--- Generalize the type: find all free and forall'd tyvars
--- and return them, together with the type inside, which
--- should not be a forall type.
---
--- Thus (quantifyType (forall a. a->[b]))
--- returns ([a,b], a -> [b])
-
+-- Find all free and forall'd tyvars and return them
+-- together with the unmodified input type.
 quantifyType ty = ( filter isTyVar $
                     tyCoVarsOfTypeWellScoped rho
-                  , rho)
+                  , ty)
   where
-    (_tvs, rho) = tcSplitForAllInvisTyVars ty
+    (_tvs, _, rho) = tcSplitNestedSigmaTys ty
diff --git a/testsuite/tests/ghci.debugger/scripts/T12449.script b/testsuite/tests/ghci.debugger/scripts/T12449.script
new file mode 100644
index 0000000000..5a582ca28b
--- /dev/null
+++ b/testsuite/tests/ghci.debugger/scripts/T12449.script
@@ -0,0 +1,20 @@
+:set -fprint-explicit-foralls
+:print fmap
+:t fmap
+:t _t1
+:print show
+:t show
+:t _t2
+_t2 "foo"
+_t1 _t2 [7, 42]
+:print _t1
+:t _t3
+:print _t2
+:t _t4
+_t3 _t4 [7, 42]
+:print id
+:t id
+:t _t5
+:print print
+:t print
+:t _t6
diff --git a/testsuite/tests/ghci.debugger/scripts/T12449.stdout b/testsuite/tests/ghci.debugger/scripts/T12449.stdout
new file mode 100644
index 0000000000..ca04690b69
--- /dev/null
+++ b/testsuite/tests/ghci.debugger/scripts/T12449.stdout
@@ -0,0 +1,26 @@
+fmap = (_t1::forall (f :: * -> *) a b.
+             Functor f =>
+             (a -> b) -> f a -> f b)
+fmap
+  :: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
+_t1
+  :: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
+show = (_t2::forall a. Show a => a -> String)
+show :: forall a. Show a => a -> String
+_t2 :: forall a. Show a => a -> String
+"\"foo\""
+["7","42"]
+_t1 = (_t3::forall (f :: * -> *) a b.
+            Functor f =>
+            (a -> b) -> f a -> f b)
+_t3
+  :: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
+_t2 = (_t4::forall a. Show a => a -> String)
+_t4 :: forall a. Show a => a -> String
+["7","42"]
+id = (_t5::forall a. a -> a)
+id :: forall a. a -> a
+_t5 :: forall a. a -> a
+print = (_t6::forall a. Show a => a -> IO ())
+print :: forall a. Show a => a -> IO ()
+_t6 :: forall a. Show a => a -> IO ()
diff --git a/testsuite/tests/ghci.debugger/scripts/T12458.stdout b/testsuite/tests/ghci.debugger/scripts/T12458.stdout
index 2a616b0f71..64c8134355 100644
--- a/testsuite/tests/ghci.debugger/scripts/T12458.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/T12458.stdout
@@ -1,2 +1,2 @@
-d = (_t1::D a)
+d = (_t1::forall {k} {a :: k}. D a)
 ()
diff --git a/testsuite/tests/ghci.debugger/scripts/all.T b/testsuite/tests/ghci.debugger/scripts/all.T
index 489fa89d36..d6de0b3151 100644
--- a/testsuite/tests/ghci.debugger/scripts/all.T
+++ b/testsuite/tests/ghci.debugger/scripts/all.T
@@ -113,6 +113,7 @@ test('getargs', extra_files(['../getargs.hs']), ghci_script, ['getargs.script'])
 test('T7386', normal, ghci_script, ['T7386.script'])
 test('T8487', normal, ghci_script, ['T8487.script'])
 test('T8557', normal, ghci_script, ['T8557.script'])
+test('T12449', normal, ghci_script, ['T12449.script'])
 test('T12458', normal, ghci_script, ['T12458.script'])
 test('T13825-debugger',
       [when(arch('powerpc64'), expect_broken(14455)),
diff --git a/testsuite/tests/ghci.debugger/scripts/break012.stdout b/testsuite/tests/ghci.debugger/scripts/break012.stdout
index 5d478ae04e..0726b3357d 100644
--- a/testsuite/tests/ghci.debugger/scripts/break012.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break012.stdout
@@ -9,6 +9,6 @@ b :: a3 -> a3
 c :: ()
 d :: a -> a -> a
 a = (_t1::a1)
-b = (_t2::a3 -> a3)
+b = (_t2::forall {a3}. a3 -> a3)
 c = (_t3::())
 d = (_t4::a -> a -> a)
diff --git a/testsuite/tests/ghci.debugger/scripts/print027.stdout b/testsuite/tests/ghci.debugger/scripts/print027.stdout
index 3117eace87..38c46a9118 100644
--- a/testsuite/tests/ghci.debugger/scripts/print027.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/print027.stdout
@@ -1,6 +1,6 @@
-+ = (_t1::Num a => a -> a -> a)
-print = (_t2::Show a1 => a1 -> IO ())
-log = (_t3::Floating a2 => a2 -> a2)
-head = (_t4::[a4] -> a4)
-tail = (_t5::[a7] -> [a7])
-fst = (_t6::(a11, b) -> a11)
++ = (_t1::forall a. Num a => a -> a -> a)
+print = (_t2::forall a. Show a => a -> IO ())
+log = (_t3::forall a. Floating a => a -> a)
+head = (_t4::forall a. [a] -> a)
+tail = (_t5::forall a. [a] -> [a])
+fst = (_t6::forall a b. (a, b) -> a)
diff --git a/testsuite/tests/ghci.debugger/scripts/print033.stdout b/testsuite/tests/ghci.debugger/scripts/print033.stdout
index 62b39bbaea..0e5780318e 100644
--- a/testsuite/tests/ghci.debugger/scripts/print033.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/print033.stdout
@@ -1 +1 @@
-u = (_t1::ST s (forall s'. ST s' a))
+u = (_t1::forall {s} {a}. ST s (forall s'. ST s' a))
diff --git a/testsuite/tests/ghci/scripts/T14828.stdout b/testsuite/tests/ghci/scripts/T14828.stdout
index dfc7fb4059..c7b100a137 100644
--- a/testsuite/tests/ghci/scripts/T14828.stdout
+++ b/testsuite/tests/ghci/scripts/T14828.stdout
@@ -1,14 +1,16 @@
 foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
-foldl = (_t1::forall b a.
+foldl = (_t1::forall (t :: * -> *) b a.
               Foldable t =>
               (b -> a -> b) -> b -> t a -> b)
 fmap :: Functor f => (a -> b) -> f a -> f b
-fmap = (_t2::forall a b. Functor f => (a -> b) -> f a -> f b)
+fmap = (_t2::forall (f :: * -> *) a b.
+             Functor f =>
+             (a -> b) -> f a -> f b)
 return :: Monad m => a -> m a
-return = (_t3::forall a. Monad m => a -> m a)
+return = (_t3::forall (m :: * -> *) a. Monad m => a -> m a)
 pure :: Applicative f => a -> f a
-pure = (_t4::forall a. Applicative f1 => a -> f1 a)
-mempty = (_t5::Monoid a => a)
-mappend = (_t6::Monoid a => a -> a -> a)
-foldl' = (_t7::(b -> a1 -> b) -> b -> [a1] -> b)
-f = (_t8::(forall a. a -> a) -> b1 -> b1)
+pure = (_t4::forall (f :: * -> *) a. Applicative f => a -> f a)
+mempty = (_t5::forall a. Monoid a => a)
+mappend = (_t6::forall a. Monoid a => a -> a -> a)
+foldl' = (_t7::forall a b. (b -> a -> b) -> b -> [a] -> b)
+f = (_t8::forall b. (forall a. a -> a) -> b -> b)