Minor comments, update linear types docs

- Update comments: placeHolderTypeTc no longer exists
  "another level check problem" was a temporary comment from linear types
- Use Mult type synonym (reported in #18676)
- Mention multiplicity-polymorphic fields in linear types docs

5 files changed, 22 insertions, 12 deletions

diff --git a/compiler/GHC/Builtin/Types/Prim.hs b/compiler/GHC/Builtin/Types/Prim.hs
index ed1f10a382..1b3d22fc21 100644
--- a/compiler/GHC/Builtin/Types/Prim.hs
+++ b/compiler/GHC/Builtin/Types/Prim.hs
@@ -423,7 +423,7 @@ funTyConName = mkPrimTyConName (fsLit "FUN") funTyConKey funTyCon
 -- @
 -- type Arr :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep).
 --             TYPE rep1 -> TYPE rep2 -> Type
--- type Arr = FUN
+-- type Arr = FUN 'Many
 -- @
 --
 funTyCon :: TyCon
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 49dd3f97b9..626fa55b46 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -1119,14 +1119,14 @@ In the compiler we maintain the invariant that all saturated applications of
 See #11714.
 -}
 
-splitFunTy :: Type -> (Type, Type, Type)
--- ^ Attempts to extract the argument and result types from a type, and
--- panics if that is not possible. See also 'splitFunTy_maybe'
+splitFunTy :: Type -> (Mult, Type, Type)
+-- ^ Attempts to extract the multiplicity, argument and result types from a type,
+-- and panics if that is not possible. See also 'splitFunTy_maybe'
 splitFunTy = expectJust "splitFunTy" . splitFunTy_maybe
 
 {-# INLINE splitFunTy_maybe #-}
-splitFunTy_maybe :: Type -> Maybe (Type, Type, Type)
--- ^ Attempts to extract the argument and result types from a type
+splitFunTy_maybe :: Type -> Maybe (Mult, Type, Type)
+-- ^ Attempts to extract the multiplicity, argument and result types from a type
 splitFunTy_maybe ty
   | FunTy _ w arg res <- coreFullView ty = Just (w, arg, res)
   | otherwise                            = Nothing
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index 5adcc140e2..9976334956 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -351,9 +351,10 @@ mkPsBindStmt pat body = BindStmt noExtField pat body
 mkRnBindStmt pat body = BindStmt (XBindStmtRn { xbsrn_bindOp = noSyntaxExpr, xbsrn_failOp = Nothing }) pat body
 mkTcBindStmt pat body = BindStmt (XBindStmtTc { xbstc_bindOp = noSyntaxExpr,
                                                 xbstc_boundResultType = unitTy,
+                                                   -- unitTy is a dummy value
+                                                   -- can't panic here: it's forced during zonking
                                                 xbstc_boundResultMult = Many,
                                                 xbstc_failOp = Nothing }) pat body
-  -- don't use placeHolderTypeTc above, because that panics during zonking
 
 emptyRecStmt' :: forall idL idR body. IsPass idR
               => XRecStmt (GhcPass idL) (GhcPass idR) body
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 2d2430e7d9..452c795c3b 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -999,7 +999,6 @@ writeMetaTyVarRef tyvar ref ty
        -- Check for level OK
        -- See Note [Level check when unifying]
        ; MASSERT2( level_check_ok, level_check_msg )
-       -- another level check problem, see #97
 
        -- Check Kinds ok
        ; MASSERT2( kind_check_ok, kind_msg )
diff --git a/docs/users_guide/exts/linear_types.rst b/docs/users_guide/exts/linear_types.rst
index d868adf3f0..a989d3b610 100644
--- a/docs/users_guide/exts/linear_types.rst
+++ b/docs/users_guide/exts/linear_types.rst
@@ -101,13 +101,23 @@ Whether a data constructor field is linear or not can be customized using the GA
 ::
 
     data T2 a b c where
-        MkT2 :: a -> b %1 -> c %1 -> T2 a b  -- Note unrestricted arrow in the first argument
+        MkT2 :: a -> b %1 -> c %1 -> T2 a b c -- Note unrestricted arrow in the first argument
 
 the value ``MkT2 x y z`` can be constructed only if ``x`` is
 unrestricted. On the other hand, a linear function which is matching
 on ``MkT2 x y z`` must consume ``y`` and ``z`` exactly once, but there
 is no restriction on ``x``.
 
+It is also possible to define a multiplicity-polymorphic field:
+
+::
+    data T3 a m where
+        MkT3 :: a %m -> T3 a m
+
+While linear fields are generalized (``MkT1 :: forall {m} a. a %m -> T1 a``
+in the previous example), multiplicity-polymorphic fields are not;
+it is not possible to directly use ``MkT3`` as a function ``a -> T3 a 'One``.
+
 If :extension:`LinearTypes` is disabled, all fields are considered to be linear
 fields, including GADT fields defined with the ``->`` arrow.
 
@@ -143,9 +153,9 @@ missing pieces.
   have success using it, or you may not. Expect it to be really unreliable.
 - There is currently no support for multiplicity annotations such as
   ``x :: a %p``, ``\(x :: a %p) -> ...``.
-- All ``case``, ``let`` and ``where`` statements consume their
-  right-hand side, or scrutiny, ``Many`` times. That is, the following
-  will not type check:
+- All ``case`` expressions consume their scrutinee ``Many`` times.
+  All ``let`` and ``where`` statements consume their right hand side
+  ``Many`` times. That is, the following will not type check:
 
   ::