[Git][ghc/ghc][wip/boxed-rep] 4 commits: Add tests for levity polymorphism
Andrew Martin
gitlab at gitlab.haskell.org
Sun Nov 29 19:20:34 UTC 2020
Andrew Martin pushed to branch wip/boxed-rep at Glasgow Haskell Compiler / GHC
Commits:
b5bd116b by Andrew Martin at 2020-11-18T09:28:28-05:00
Add tests for levity polymorphism
- - - - -
fd251750 by Andrew Martin at 2020-11-18T10:02:03-05:00
Add table documenting built-in types
- - - - -
c7d210f5 by Andrew Martin at 2020-11-18T10:17:58-05:00
Fix test T13963
- - - - -
0dace92a by Andrew Martin at 2020-11-18T10:19:53-05:00
Update the user manual
- - - - -
14 changed files:
- compiler/GHC/Builtin/Types.hs
- docs/users_guide/9.2.1-notes.rst
- docs/users_guide/exts/levity_polymorphism.rst
- docs/users_guide/exts/typed_holes.rst
- testsuite/tests/ghci/scripts/T13963.script
- testsuite/tests/ghci/scripts/T13963.stdout
- + testsuite/tests/typecheck/should_compile/LevPolyResult.hs
- testsuite/tests/typecheck/should_compile/all.T
- + testsuite/tests/typecheck/should_fail/LevPolyLet.hs
- + testsuite/tests/typecheck/should_fail/LevPolyLet.stderr
- testsuite/tests/typecheck/should_fail/all.T
- + testsuite/tests/typecheck/should_run/LevPolyResultInst.hs
- + testsuite/tests/typecheck/should_run/LevPolyResultInst.stdout
- testsuite/tests/typecheck/should_run/all.T
Changes:
=====================================
compiler/GHC/Builtin/Types.hs
=====================================
@@ -215,6 +215,41 @@ to this Note, so a search for this Note's name should find all the lists.
See also Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType.
+
+Note [Wired-in Types and Type Constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+This module include a lot of wired-in types and type constructors. Here,
+these are presented in a tabular format to make it easier to find the
+wired-in type identifier corresponding to a known Haskell type. Data
+constructors are nested under their corresponding types with two spaces
+of indentation.
+
+Identifier Type Haskell name Notes
+----------------------------------------------------------------------------
+liftedTypeKindTyCon TyCon GHC.Types.Type Synonym for: TYPE LiftedRep
+liftedRepTyCon TyCon GHC.Types.LiftedRep Synonym for: 'BoxedRep 'Lifted
+levityTyCon TyCon GHC.Types.Levity Data type
+ liftedDataConTyCon TyCon GHC.Types.Lifted Data constructor
+ unliftedDataConTyCon TyCon GHC.Types.Unlifted Data constructor
+vecCountTyCon TyCon GHC.Types.VecCount Data type
+ vec2DataConTy Type GHC.Types.Vec2 Data constructor
+ vec4DataConTy Type GHC.Types.Vec4 Data constructor
+ vec8DataConTy Type GHC.Types.Vec8 Data constructor
+ vec16DataConTy Type GHC.Types.Vec16 Data constructor
+ vec32DataConTy Type GHC.Types.Vec32 Data constructor
+ vec64DataConTy Type GHC.Types.Vec64 Data constructor
+runtimeRepTyCon TyCon GHC.Types.RuntimeRep Data type
+ boxedRepDataConTyCon TyCon GHC.Types.BoxedRep Data constructor
+ intRepDataConTy Type GHC.Types.IntRep Data constructor
+ doubleRepDataConTy Type GHC.Types.DoubleRep Data constructor
+ floatRepDataConTy Type GHC.Types.FloatRep Data constructor
+boolTyCon TyCon GHC.Types.Bool Data type
+ trueDataCon DataCon GHC.Types.True Data constructor
+ falseDataCon DataCon GHC.Types.False Data constructor
+ promotedTrueDataCon TyCon GHC.Types.True Data constructor
+ promotedFalseDataCon TyCon GHC.Types.False Data constructor
+
************************************************************************
* *
\subsection{Wired in type constructors}
@@ -223,8 +258,10 @@ See also Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType.
If you change which things are wired in, make sure you change their
names in GHC.Builtin.Names, so they use wTcQual, wDataQual, etc
+
-}
+
-- This list is used only to define GHC.Builtin.Utils.wiredInThings. That in turn
-- is used to initialise the name environment carried around by the renamer.
-- This means that if we look up the name of a TyCon (or its implicit binders)
=====================================
docs/users_guide/9.2.1-notes.rst
=====================================
@@ -13,6 +13,12 @@ Language
<https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/>`__
(Serrano et al, ICFP 2020). More information here: :ref:`impredicative-polymorphism`.
This replaces the old (undefined, flaky) behaviour of the :extension:`ImpredicativeTypes` extension.
+* The first stage of the `Pointer Rep Proposal`_ has been implemented. All
+ boxed types, both lifted and unlifted, now have representation kinds of
+ the shape ``BoxedRep r``. Code that references ``LiftedRep`` and ``UnliftedRep``
+ will need to be updated.
+
+.. _Pointer Rep Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0203-pointer-rep.rst
Compiler
~~~~~~~~
=====================================
docs/users_guide/exts/levity_polymorphism.rst
=====================================
@@ -13,21 +13,25 @@ Here are the key definitions, all available from ``GHC.Exts``: ::
TYPE :: RuntimeRep -> Type -- highly magical, built into GHC
- data RuntimeRep = LiftedRep -- for things like `Int`
- | UnliftedRep -- for things like `Array#`
- | IntRep -- for `Int#`
+ data Levity = Lifted -- for things like `Int`
+ | Unlifted -- for things like `Array#`
+
+ data RuntimeRep = BoxedRep Levity -- for anything represented by a GC-managed pointer
+ | IntRep -- for `Int#`
| TupleRep [RuntimeRep] -- unboxed tuples, indexed by the representations of the elements
| SumRep [RuntimeRep] -- unboxed sums, indexed by the representations of the disjuncts
| ...
+ type LiftedRep = BoxedRep Lifted
+
type Type = TYPE LiftedRep -- Type is just an ordinary type synonym
The idea is that we have a new fundamental type constant ``TYPE``, which
is parameterised by a ``RuntimeRep``. We thus get ``Int# :: TYPE 'IntRep``
-and ``Bool :: TYPE 'LiftedRep``. Anything with a type of the form
+and ``Bool :: TYPE LiftedRep``. Anything with a type of the form
``TYPE x`` can appear to either side of a function arrow ``->``. We can
thus say that ``->`` has type
-``TYPE r1 -> TYPE r2 -> TYPE 'LiftedRep``. The result is always lifted
+``TYPE r1 -> TYPE r2 -> TYPE LiftedRep``. The result is always lifted
because all functions are lifted in GHC.
.. _levity-polymorphic-restrictions:
@@ -102,13 +106,13 @@ Printing levity-polymorphic types
:category: verbosity
Print ``RuntimeRep`` parameters as they appear; otherwise, they are
- defaulted to ``'LiftedRep``.
+ defaulted to ``LiftedRep``.
Most GHC users will not need to worry about levity polymorphism
or unboxed types. For these users, seeing the levity polymorphism
in the type of ``$`` is unhelpful. And thus, by default, it is suppressed,
-by supposing all type variables of type ``RuntimeRep`` to be ``'LiftedRep``
-when printing, and printing ``TYPE 'LiftedRep`` as ``Type`` (or ``*`` when
+by supposing all type variables of type ``RuntimeRep`` to be ``LiftedRep``
+when printing, and printing ``TYPE LiftedRep`` as ``Type`` (or ``*`` when
:extension:`StarIsType` is on).
Should you wish to see levity polymorphism in your types, enable
=====================================
docs/users_guide/exts/typed_holes.rst
=====================================
@@ -443,7 +443,7 @@ it will additionally offer up a list of refinement hole fits, in this case: ::
with const @Integer @[Integer]
where const :: forall a b. a -> b -> a
($) (_ :: [Integer] -> Integer)
- with ($) @'GHC.Types.LiftedRep @[Integer] @Integer
+ with ($) @GHC.Types.LiftedRep @[Integer] @Integer
where ($) :: forall a b. (a -> b) -> a -> b
fail (_ :: String)
with fail @((->) [Integer]) @Integer
=====================================
testsuite/tests/ghci/scripts/T13963.script
=====================================
@@ -1,13 +1,13 @@
:set -XPolyKinds -XDataKinds -XRankNTypes
-import GHC.Exts (TYPE, RuntimeRep(BoxedRep), Levity(Lifted))
+import GHC.Exts (TYPE, RuntimeRep, LiftedRep)
type Pair (a :: TYPE rep) (b :: TYPE rep') rep'' = forall (r :: TYPE rep''). (a -> b -> r)
:kind Pair
:kind Pair Int
:kind Pair Int Float
-:kind Pair Int Float ('BoxedRep 'Lifted)
+:kind Pair Int Float LiftedRep
:set -fprint-explicit-runtime-reps
:kind Pair
:kind Pair Int
:kind Pair Int Float
-:kind Pair Int Float ('BoxedRep 'Lifted)
+:kind Pair Int Float LiftedRep
=====================================
testsuite/tests/ghci/scripts/T13963.stdout
=====================================
@@ -1,8 +1,8 @@
Pair :: * -> * -> RuntimeRep -> *
Pair Int :: * -> RuntimeRep -> *
Pair Int Float :: RuntimeRep -> *
-Pair Int Float ('BoxedRep 'Lifted) :: *
+Pair Int Float LiftedRep :: *
Pair :: TYPE rep -> TYPE rep' -> RuntimeRep -> *
Pair Int :: * -> RuntimeRep -> *
Pair Int Float :: RuntimeRep -> *
-Pair Int Float ('BoxedRep 'Lifted) :: *
+Pair Int Float LiftedRep :: *
=====================================
testsuite/tests/typecheck/should_compile/LevPolyResult.hs
=====================================
@@ -0,0 +1,11 @@
+{-# language DataKinds #-}
+{-# language KindSignatures #-}
+{-# language PolyKinds #-}
+{-# language RankNTypes #-}
+
+module LevPolyResult (example) where
+
+import GHC.Exts
+
+example :: forall (v :: Levity) (a :: TYPE ('BoxedRep v)). (Int -> a) -> a
+example f = f 42
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -688,6 +688,7 @@ test('UnliftedNewtypesForall', normal, compile, [''])
test('UnlifNewUnify', normal, compile, [''])
test('UnliftedNewtypesLPFamily', normal, compile, [''])
test('UnliftedNewtypesDifficultUnification', normal, compile, [''])
+test('LevPolyResult', normal, compile, [''])
test('T16832', normal, ghci_script, ['T16832.script'])
test('T16995', normal, compile, [''])
test('T17007', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/LevPolyLet.hs
=====================================
@@ -0,0 +1,19 @@
+{-# language DataKinds #-}
+{-# language KindSignatures #-}
+{-# language PolyKinds #-}
+{-# language RankNTypes #-}
+
+module LevPolyLet
+ ( example
+ ) where
+
+import GHC.Exts
+
+-- This should be rejected because of the let binding.
+example :: forall (v :: Levity) (a :: TYPE ('BoxedRep v)).
+ (Int -> a)
+ -> (a -> Bool)
+ -> Bool
+example f g =
+ let x = f 42
+ in g x
=====================================
testsuite/tests/typecheck/should_fail/LevPolyLet.stderr
=====================================
@@ -0,0 +1,5 @@
+LevPolyLet.hs:18:7:
+ A levity-polymorphic type is not allowed here:
+ Type: a
+ Kind: TYPE ('BoxedRep v)
+ In the type of binder ‘x’
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -440,6 +440,7 @@ test('T13068', [extra_files(['T13068.hs', 'T13068a.hs', 'T13068.hs-boot', 'T1306
test('T13075', normal, compile_fail, [''])
test('T13105', normal, compile_fail, [''])
test('LevPolyBounded', normal, compile_fail, [''])
+test('LevPolyLet', normal, compile_fail, [''])
test('T13487', normal, compile, [''])
test('T13292', normal, multimod_compile, ['T13292', '-v0 -fdefer-type-errors'])
test('T13300', normal, compile_fail, [''])
=====================================
testsuite/tests/typecheck/should_run/LevPolyResultInst.hs
=====================================
@@ -0,0 +1,27 @@
+{-# language BangPatterns #-}
+{-# language DataKinds #-}
+{-# language MagicHash #-}
+{-# language PolyKinds #-}
+{-# language RankNTypes #-}
+{-# language UnboxedTuples #-}
+
+import GHC.Exts
+
+main :: IO ()
+main = do
+ print (example (\x -> I# x > 7))
+ case indexArray# (example replicateFalse) 0# of
+ (# r #) -> print r
+
+-- Combines base:runST, primitive:newArray, and primitive:unsafeFreezeArray
+replicateFalse :: Int# -> Array# Bool
+replicateFalse n =
+ let !(# _, r #) = runRW#
+ (\s -> case newArray# n False s of
+ (# s', arr #) -> unsafeFreezeArray# arr s'
+ )
+ in r
+
+example :: forall (v :: Levity) (a :: TYPE ('BoxedRep v)). (Int# -> a) -> a
+{-# noinline example #-}
+example f = f 8#
=====================================
testsuite/tests/typecheck/should_run/LevPolyResultInst.stdout
=====================================
@@ -0,0 +1,2 @@
+True
+False
=====================================
testsuite/tests/typecheck/should_run/all.T
=====================================
@@ -145,5 +145,6 @@ test('UnliftedNewtypesFamilyRun', normal, compile_and_run, [''])
test('UnliftedNewtypesDependentFamilyRun', normal, compile_and_run, [''])
test('UnliftedNewtypesIdentityRun', normal, compile_and_run, [''])
test('UnliftedNewtypesCoerceRun', normal, compile_and_run, [''])
+test('LevPolyResultInst', normal, compile_and_run, [''])
test('T17104', normal, compile_and_run, [''])
test('T18627', normal, compile_and_run, ['-O']) # Optimisation shows up the bug
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/39caf4f1edde204edd323596ba2b2b2890dce093...0dace92a5867ced6f979b4543c49865165d4c49a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/39caf4f1edde204edd323596ba2b2b2890dce093...0dace92a5867ced6f979b4543c49865165d4c49a
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/20201129/fc3c4516/attachment-0001.html>
More information about the ghc-commits
mailing list