Expand type synonyms with :kind!wip/T13795-T18828

The User's Guide claims that `:kind!` should expand type synonyms,
but GHCi wasn't doing this in practice. Let's just update the implementation
to match the specification in the User's Guide.

Fixes #13795. Fixes #18828.

Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>

8 files changed, 68 insertions, 6 deletions

diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 94582b00a9..2d44a9aacf 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -2629,12 +2629,13 @@ tcRnType hsc_env flexi normalise rdr_type
        -- Do validity checking on type
        ; checkValidType (GhciCtxt True) ty
 
-       ; ty' <- if normalise
-                then do { fam_envs <- tcGetFamInstEnvs
-                        ; let (_, ty')
-                                = normaliseType fam_envs Nominal ty
-                        ; return ty' }
-                else return ty ;
+       -- Optionally (:k vs :k!) normalise the type. Does two things:
+       --   normaliseType: expand type-family applications
+       --   expandTypeSynonyms: expand type synonyms (#18828)
+       ; fam_envs <- tcGetFamInstEnvs
+       ; let ty' | normalise = expandTypeSynonyms $ snd $
+                               normaliseType fam_envs Nominal ty
+                 | otherwise = ty
 
        ; return (ty', mkInfForAllTys kvs (tcTypeKind ty')) }
 
diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index aa495444db..4ba4fc911f 100644
--- a/docs/users_guide/9.2.1-notes.rst
+++ b/docs/users_guide/9.2.1-notes.rst
@@ -37,6 +37,9 @@ Compiler
 - Type checker plugins which work with the natural numbers now
   should use ``naturalTy`` kind instead of ``typeNatKind``, which has been removed.
 
+- GHCi's ``:kind!`` command now expands through type synonyms in addition to type
+  families. See :ghci-cmd:`:kind`.
+
 ``ghc-prim`` library
 ~~~~~~~~~~~~~~~~~~~~
 
diff --git a/testsuite/tests/ghci/scripts/T13795.script b/testsuite/tests/ghci/scripts/T13795.script
new file mode 100644
index 0000000000..269d575ddf
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T13795.script
@@ -0,0 +1,2 @@
+type A = ()
+:kind! A
diff --git a/testsuite/tests/ghci/scripts/T13795.stdout b/testsuite/tests/ghci/scripts/T13795.stdout
new file mode 100644
index 0000000000..1a0bb561e2
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T13795.stdout
@@ -0,0 +1,2 @@
+A :: *
+= ()
diff --git a/testsuite/tests/ghci/scripts/T18828.hs b/testsuite/tests/ghci/scripts/T18828.hs
new file mode 100644
index 0000000000..9688584150
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T18828.hs
@@ -0,0 +1,31 @@
+{-# Language ConstraintKinds          #-}
+{-# Language DataKinds                #-}
+{-# Language GADTs                    #-}
+{-# Language PolyKinds                #-}
+{-# Language RankNTypes               #-}
+{-# Language StandaloneKindSignatures #-}
+{-# Language TypeFamilies             #-}
+{-# Language TypeOperators            #-}
+module T18828 where
+
+import Data.Kind
+
+type Cat :: Type -> Type
+type Cat ob = ob -> ob -> Type
+
+type Dict :: Constraint -> Type
+data Dict cls where
+ Dict :: cls => Dict cls
+
+type    (:-) :: Cat Constraint
+newtype cls1 :- cls2 where
+ Sub :: (cls1 => Dict cls2) -> (cls1 :- cls2)
+
+type ObjectSyn :: Cat ob -> Type
+type ObjectSyn (cat :: ob -> ob -> Type) = ob
+
+type
+  ObjectFam :: Cat ob -> Type
+type family
+  ObjectFam cat where
+  ObjectFam @ob cat = ob
diff --git a/testsuite/tests/ghci/scripts/T18828.script b/testsuite/tests/ghci/scripts/T18828.script
new file mode 100644
index 0000000000..ebc062367d
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T18828.script
@@ -0,0 +1,9 @@
+:load T18828
+:set -XDataKinds -XKindSignatures -XRankNTypes
+import Data.Type.Equality
+:k! ObjectSyn (->)
+:k! forall ob. ObjectSyn ((:~:) :: Cat ob)
+:k! ObjectSyn (:-)
+:k! ObjectFam (->)
+:k! forall ob. ObjectFam ((:~:) :: Cat ob)
+:k! ObjectFam (:-)
diff --git a/testsuite/tests/ghci/scripts/T18828.stdout b/testsuite/tests/ghci/scripts/T18828.stdout
new file mode 100644
index 0000000000..8736ff036f
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T18828.stdout
@@ -0,0 +1,12 @@
+ObjectSyn (->) :: *
+= *
+forall ob. ObjectSyn ((:~:) :: Cat ob) :: *
+= ob
+ObjectSyn (:-) :: *
+= Constraint
+ObjectFam (->) :: *
+= *
+forall ob. ObjectFam ((:~:) :: Cat ob) :: *
+= ob
+ObjectFam (:-) :: *
+= Constraint
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index dde0e90539..29b01a0b0c 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -279,6 +279,7 @@ test('T13591', expect_broken(13591), ghci_script, ['T13591.script'])
 test('T13699', normal, ghci_script, ['T13699.script'])
 test('T13988', normal, ghci_script, ['T13988.script'])
 test('T13407', normal, ghci_script, ['T13407.script'])
+test('T13795', normal, ghci_script, ['T13795.script'])
 test('T13963', normal, ghci_script, ['T13963.script'])
 test('T14342', [extra_hc_opts("-XOverloadedStrings -XRebindableSyntax")],
                ghci_script, ['T14342.script'])
@@ -322,3 +323,4 @@ test('T17669', [extra_run_opts('-fexternal-interpreter -fobject-code'), expect_b
 test('T18501', normal, ghci_script, ['T18501.script'])
 test('T18644', normal, ghci_script, ['T18644.script'])
 test('T18755', normal, ghci_script, ['T18755.script'])
+test('T18828', normal, ghci_script, ['T18828.script'])