GHCi: don't normalise partially instantiated types

  This patch skips performing type normalisation when we haven't
  fully instantiated the type. That is, in tcRnExpr
  (used only for :type in GHCi), skip normalisation if
  the result type responds True to isSigmaTy.

  Fixes #20974

6 files changed, 56 insertions, 8 deletions

diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 40bc5188f6..11278d6bc7 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -2576,14 +2576,12 @@ tcRnExpr hsc_env mode rdr_expr
                         mkPhiTy (map idType dicts) res_ty } ;
     ty <- zonkTcType all_expr_ty ;
 
-    -- We normalise type families, so that the type of an expression is the
-    -- same as of a bound expression (GHC.Tc.Gen.Bind.mkInferredPolyId). See Trac
-    -- #10321 for further discussion.
+    -- See Note [Normalising the type in :type]
     fam_envs <- tcGetFamInstEnvs ;
-    -- normaliseType returns a coercion which we discard, so the Role is
-    -- irrelevant
-    return (reductionReducedType (normaliseType fam_envs Nominal ty))
-    }
+    let { normalised_type = reductionReducedType $ normaliseType fam_envs Nominal ty
+          -- normaliseType returns a coercion which we discard, so the Role is irrelevant.
+        ; final_type = if isSigmaTy res_ty then ty else normalised_type } ;
+    return final_type }
   where
     -- Optionally instantiate the type of the expression
     -- See Note [TcRnExprMode]
@@ -2608,6 +2606,31 @@ and not        forall {b}. Int -> b -> Int
 
 Solution: use tcInferSigma, which in turn uses tcInferApp, which
 has a special case for application chains.
+
+Note [Normalising the type in :type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In :t <expr> we usually normalise the type (to simplify type functions)
+before displaying the result.  Reason (see #10321): otherwise we may show
+types like
+    <expr> :: Vec (1+2) Int
+rather than the simpler
+    <expr> :: Vec 3 Int
+In GHC.Tc.Gen.Bind.mkInferredPolyId we normalise for a very similar reason.
+
+However this normalisation is less helpful when <expr> is just
+an identifier, whose user-written type happens to contain type-function
+applications.  E.g. (#20974)
+    test :: F [Monad, A, B] m => m ()
+where F is a type family.  If we say `:t test`, we'd prefer to see
+the type family un-expanded.
+
+We adopt the following ad-hoc solution: if the type inferred for <expr>
+(before generalisation, namely res_ty) is a SigmaType (i.e. is not
+fully instantiated) then do not normalise; otherwise normalise.
+This is not ideal; for example, suppose  x :: F Int.  Then
+  :t x
+would be normalised because `F Int` is not a SigmaType.  But
+anything here is ad-hoc, and it's a user-sought improvement.
 -}
 
 --------------------------
diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst
index cb98b15f6a..c26dedb5c3 100644
--- a/docs/users_guide/ghci.rst
+++ b/docs/users_guide/ghci.rst
@@ -2981,13 +2981,19 @@ commonly used commands.
 
     Infers and prints the type of ⟨expression⟩.  For polymorphic types
     it instantiates the 'inferred' forall quantifiers (but not the
-    'specified' ones; see :ref:`inferred-vs-specified`), solves constraints, and re-generalises.
+    'specified' ones; see :ref:`inferred-vs-specified`), solves constraints,
+    re-generalises, and then reduces type families as much as possible.
 
     .. code-block:: none
 
 	*X> :type length
 	length :: Foldable t => t a -> Int
 
+    Type family reduction is skipped if the function is not fully instantiated,
+    as this has been observed to give more intuitive results.
+    You may want to use :ghci-cmd:`:info` if you are not applying any arguments,
+    as that will return the original type of the function without instantiating.
+
 .. ghci-cmd:: :type +d; ⟨expression⟩
 
     Infers and prints the type of ⟨expression⟩, instantiating *all* the forall
diff --git a/testsuite/tests/ghci/scripts/T20974.hs b/testsuite/tests/ghci/scripts/T20974.hs
new file mode 100644
index 0000000000..6d02dea7cf
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T20974.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
+
+module T20974 where
+
+import Data.Kind
+
+class A (m :: Type -> Type)
+class B (m :: Type -> Type)
+
+type family F cs (m :: Type -> Type) :: Constraint where
+  F '[]      m = ()
+  F (c : cs) m = (c m, F cs m)
+
+test :: F [Monad, A, B] m => m ()
+test = pure ()
diff --git a/testsuite/tests/ghci/scripts/T20974.script b/testsuite/tests/ghci/scripts/T20974.script
new file mode 100644
index 0000000000..730444a54b
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T20974.script
@@ -0,0 +1,2 @@
+:l T20974
+:type test
diff --git a/testsuite/tests/ghci/scripts/T20974.stdout b/testsuite/tests/ghci/scripts/T20974.stdout
new file mode 100644
index 0000000000..6cfee4e9a4
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T20974.stdout
@@ -0,0 +1 @@
+test :: F '[Monad, A, B] m => m ()
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index e35d3b804d..bccfa977e5 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -362,3 +362,4 @@ test('T20587', [extra_files(['../shell.hs'])], ghci_script,
                 ['T20587.script'])
 test('T20909', normal, ghci_script, ['T20909.script'])
 test('T20150', normal, ghci_script, ['T20150.script'])
+test('T20974', normal, ghci_script, ['T20974.script'])