[commit: ghc] master: Allow levity-polymorpic arrows (eefe86d)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/eefe86d96d40697707c3ddfb9973a30a1897241f/ghc

>---------------------------------------------------------------

commit eefe86d96d40697707c3ddfb9973a30a1897241f
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Oct 26 15:34:56 2016 +0100

    Allow levity-polymorpic arrows
    
    This cures Trac #12668 (and cures the Lint errors you get from
    Trac #12718).
    
    The idea is explained in Note [Levity polymorphism], in Kind.hs


>---------------------------------------------------------------

eefe86d96d40697707c3ddfb9973a30a1897241f
 compiler/types/Kind.hs              | 33 +++++++++++++++++++++++++++++++--
 testsuite/tests/polykinds/T12668.hs | 15 +++++++++++++++
 testsuite/tests/polykinds/T12718.hs | 30 ++++++++++++++++++++++++++++++
 testsuite/tests/polykinds/all.T     |  2 ++
 4 files changed, 78 insertions(+), 2 deletions(-)

diff --git a/compiler/types/Kind.hs b/compiler/types/Kind.hs
index c38a533..01a62e2 100644
--- a/compiler/types/Kind.hs
+++ b/compiler/types/Kind.hs
@@ -25,7 +25,6 @@ import TyCoRep
 import TyCon
 import VarSet ( isEmptyVarSet )
 import PrelNames
-import Util  ( (<&&>) )
 
 {-
 ************************************************************************
@@ -88,9 +87,11 @@ isRuntimeRepPolymorphic k
 --            Kinding for arrow (->)
 -- Says when a kind is acceptable on lhs or rhs of an arrow
 --     arg -> res
+--
+-- See Note [Levity polymorphism]
 
 okArrowArgKind, okArrowResultKind :: Kind -> Bool
-okArrowArgKind = classifiesTypeWithValues <&&> (not . isRuntimeRepPolymorphic)
+okArrowArgKind    = classifiesTypeWithValues
 okArrowResultKind = classifiesTypeWithValues
 
 -----------------------------------------
@@ -120,3 +121,31 @@ isStarKind _ = False
 -- | Is the tycon @Constraint@?
 isStarKindSynonymTyCon :: TyCon -> Bool
 isStarKindSynonymTyCon tc = tc `hasKey` constraintKindTyConKey
+
+
+{- Note [Levity polymorphism]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Is this type legal?
+   (a :: TYPE rep) -> Int
+   where 'rep :: RuntimeRep'
+
+You might think not, because no lambda can have a
+runtime-rep-polymorphic binder.  So no lambda has the
+above type.  BUT here's a way it can be useful (taken from
+Trac #12708):
+
+  data T rep (a :: TYPE rep)
+     = MkT (a -> Int)
+
+  x1 :: T LiftedPtrRep Int
+  x1 =  MkT LiftedPtrRep Int  (\x::Int -> 3)
+
+  x2 :: T IntRep INt#
+  x2 = MkT IntRep Int# (\x:Int# -> 3)
+
+Note that the lambdas are just fine!
+
+Hence, okArrowArgKind and okArrowResultKind both just
+check that the type is of the form (TYPE r) for some
+representation type r.
+-}
diff --git a/testsuite/tests/polykinds/T12668.hs b/testsuite/tests/polykinds/T12668.hs
new file mode 100644
index 0000000..4640903
--- /dev/null
+++ b/testsuite/tests/polykinds/T12668.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE RankNTypes #-}
+
+module T12668 where
+
+import GHC.Exts
+
+data Some r = Some (TYPE r -> TYPE r)
+
+doSomething :: forall (r :: RuntimeRep). forall (a :: TYPE r). ()
+            => Int -> (a -> Int) -> a -> a
+doSomething n f =
+    case n of
+      1 -> error "hello"
+      3 -> error "hello"
diff --git a/testsuite/tests/polykinds/T12718.hs b/testsuite/tests/polykinds/T12718.hs
new file mode 100644
index 0000000..82d6dcd
--- /dev/null
+++ b/testsuite/tests/polykinds/T12718.hs
@@ -0,0 +1,30 @@
+{-# Language RebindableSyntax, NoImplicitPrelude, MagicHash, RankNTypes,
+             PolyKinds, ViewPatterns, TypeInType, FlexibleInstances #-}
+
+module Main where
+
+import Prelude hiding (Eq (..), Num(..))
+import qualified Prelude as P
+import GHC.Prim
+import GHC.Types
+
+class XNum (a :: TYPE rep) where
+  (+) :: a -> a -> a
+  fromInteger :: Integer -> a
+
+instance P.Num a => XNum a where
+  (+) = (P.+)
+  fromInteger = P.fromInteger
+
+instance XNum Int# where
+  (+) = (+#)
+  fromInteger i = case fromInteger i of
+                   I# n -> n
+
+u :: Bool
+u = isTrue# v_
+  where
+    v_ :: forall rep (a :: TYPE rep). XNum a => a
+    v_ = fromInteger 10
+
+main = print u
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 6da6ae4..6ec2a43 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -152,3 +152,5 @@ test('T11554', normal, compile_fail, [''])
 test('T12055', normal, compile, [''])
 test('T12055a', normal, compile_fail, [''])
 test('T12593', normal, compile_fail, [''])
+test('T12668', normal, compile, [''])
+test('T12718', normal, compile, [''])