[Git][ghc/ghc][master] Minor comments, update linear types docs

[Marge Bot]

 Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
6c7a5c0c by Krzysztof Gogolewski at 2020-10-20T00:48:29-04:00
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 changed files:

- compiler/GHC/Builtin/Types/Prim.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Hs/Utils.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- docs/users_guide/exts/linear_types.rst


Changes:

=====================================
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


=====================================
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


=====================================
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


=====================================
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 )


=====================================
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:
 
   ::
 



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6c7a5c0ca07085f31a3e2f8286bb57a0f35961cb

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6c7a5c0ca07085f31a3e2f8286bb57a0f35961cb
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201020/7c117e96/attachment-0001.html>