Deeply instantiate in :type

See Trac #11376 and
 Note [Deeply instantiate in :type] in TcRnDriver

Sadly this showed up one new problem (Trac #11786) and one opportunity
(Trac #11787), so test T11549 is now marked expect-broken on these two.

7 files changed, 56 insertions, 23 deletions

diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 550f84fe7d..640d74dfc8 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -33,6 +33,7 @@ import RnSplice ( rnTopSpliceDecls, traceSplice, SpliceInfo(..) )
 import IfaceEnv( externaliseName )
 import TcHsType
 import TcMatches
+import Inst( deeplyInstantiate )
 import RnTypes
 import RnExpr
 import MkId
@@ -1977,9 +1978,16 @@ tcRnExpr hsc_env rdr_expr
         -- Now typecheck the expression, and generalise its type
         -- it might have a rank-2 type (e.g. :t runST)
     uniq <- newUnique ;
-    let { fresh_it  = itName uniq (getLoc rdr_expr) } ;
-    (tclvl, lie, (_tc_expr, res_ty)) <- pushLevelAndCaptureConstraints $
-                                        tcInferSigma rn_expr ;
+    let { fresh_it  = itName uniq (getLoc rdr_expr)
+        ; orig = OccurrenceOf fresh_it } ;  -- Not a very satisfactory origin
+    (tclvl, lie, res_ty)
+          <- pushLevelAndCaptureConstraints $
+             do { (_tc_expr, expr_ty) <- tcInferSigma rn_expr
+                ; (_wrap, res_ty)   <- deeplyInstantiate orig expr_ty
+                     -- See [Note Deeply instantiate in :type]
+                ; return res_ty } ;
+
+    -- Generalise
     ((qtvs, dicts, _), lie_top) <- captureConstraints $
                                    {-# SCC "simplifyInfer" #-}
                                    simplifyInfer tclvl
@@ -2055,7 +2063,22 @@ tcRnType hsc_env normalise rdr_type
 
        ; return (ty', mkInvForAllTys kvs (typeKind ty')) }
 
-{- Note [Kind-generalise in tcRnType]
+{- Note [Deeply instantiate in :type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose (Trac #11376)
+  bar :: forall a b. Show a => a -> b -> a
+What should `:t bar @Int` show?
+
+ 1. forall b. Show Int => Int -> b -> Int
+ 2. forall b. Int -> b -> Int
+ 3. forall {b}. Int -> b -> Int
+ 4. Int -> b -> Int
+
+We choose (3), which is the effect of deeply instantiating and
+re-generalising.  All the others seem deeply confusing.  That is
+why we deeply instantiate here.
+
+Note [Kind-generalise in tcRnType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We switch on PolyKinds when kind-checking a user type, so that we will
 kind-generalise the type, even when PolyKinds is not otherwise on.
diff --git a/testsuite/tests/dependent/ghci/T11549.script b/testsuite/tests/dependent/ghci/T11549.script
index 5f8c500519..bb35589671 100644
--- a/testsuite/tests/dependent/ghci/T11549.script
+++ b/testsuite/tests/dependent/ghci/T11549.script
@@ -3,12 +3,12 @@ import GHC.Exts
 
 putStrLn "-fno-print-explicit-runtime-reps"
 :set -fno-print-explicit-runtime-reps
-:ty ($)
+:info ($)
 :kind TYPE
-:ty error
+:info error
 
 putStrLn "\n-fprint-explicit-runtime-reps"
 :set -fprint-explicit-runtime-reps
-:ty ($)
+:info ($)
 :kind TYPE
-:ty error
+:info error
diff --git a/testsuite/tests/dependent/ghci/all.T b/testsuite/tests/dependent/ghci/all.T
index 6d9332adaa..956272fa55 100644
--- a/testsuite/tests/dependent/ghci/all.T
+++ b/testsuite/tests/dependent/ghci/all.T
@@ -1,3 +1,4 @@
 test('T11549',
-     normal,
+     [ expect_broken( 11787 ),
+       expect_broken( 11786 ) ],
      ghci_script, ['T11549.script'])
diff --git a/testsuite/tests/ghci/scripts/T11376.script b/testsuite/tests/ghci/scripts/T11376.script
new file mode 100644
index 0000000000..780db3c088
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T11376.script
@@ -0,0 +1,6 @@
+:set -XTypeApplications
+let { bar :: Show a => a -> b -> a; bar = error "urk" }
+:type bar @Int
+:set -fprint-explicit-foralls
+:type bar @Int
+
diff --git a/testsuite/tests/ghci/scripts/T11376.stdout b/testsuite/tests/ghci/scripts/T11376.stdout
new file mode 100644
index 0000000000..0b0b95922f
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T11376.stdout
@@ -0,0 +1,2 @@
+bar @Int :: Int -> b -> Int
+bar @Int :: forall {b}. Int -> b -> Int
diff --git a/testsuite/tests/ghci/scripts/TypeAppData.stdout b/testsuite/tests/ghci/scripts/TypeAppData.stdout
index 5a4880a6df..0fd5506638 100644
--- a/testsuite/tests/ghci/scripts/TypeAppData.stdout
+++ b/testsuite/tests/ghci/scripts/TypeAppData.stdout
@@ -1,14 +1,14 @@
-P1 :: forall {k} (a :: k). P1 a
-P2 :: forall k (a :: k). P2 a
-P3 :: forall k (a :: k). P3 k a
-P4 :: forall {k} (a :: k). P1 a -> P4 a
-P5 :: forall {k} (a :: k). P1 a -> P5
-P6 :: forall k (a :: k). P1 a -> P6
-P7 :: forall {k} (a :: k). P1 a
-P8 :: forall {k} (a :: k). P1 a
-P9 :: forall k (a :: k). P1 a
-P10 :: forall k (a :: k). P1 a
-P11 :: forall {k} (a :: k). P1 a -> P5
-P12 :: forall {k} (a :: k). P1 a -> P5
-P13 :: forall k (a :: k). P1 a -> P5
-P14 :: forall k (a :: k). P1 a -> P5
+P1 :: forall {k} {a :: k}. P1 a
+P2 :: forall {k} {a :: k}. P2 a
+P3 :: forall {k} {a :: k}. P3 k a
+P4 :: forall {k} {a :: k}. P1 a -> P4 a
+P5 :: forall {k} {a :: k}. P1 a -> P5
+P6 :: forall {k} {a :: k}. P1 a -> P6
+P7 :: forall {k} {a :: k}. P1 a
+P8 :: forall {k} {a :: k}. P1 a
+P9 :: forall {k} {a :: k}. P1 a
+P10 :: forall {k} {a :: k}. P1 a
+P11 :: forall {k} {a :: k}. P1 a -> P5
+P12 :: forall {k} {a :: k}. P1 a -> P5
+P13 :: forall {k} {a :: k}. P1 a -> P5
+P14 :: forall {k} {a :: k}. P1 a -> P5
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index 8fab9566a2..2d21772434 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -248,3 +248,4 @@ test('T11524a', normal, ghci_script, ['T11524a.script'])
 test('T11456', normal, ghci_script, ['T11456.script'])
 test('TypeAppData', normal, ghci_script, ['TypeAppData.script'])
 test('T11728', normal, ghci_script, ['T11728.script'])
+test('T11376', normal, ghci_script, ['T11376.script'])