Allow levity-polymorpic arrows
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 26 Oct 2016 14:34:56 +0000 (15:34 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 27 Oct 2016 07:28:33 +0000 (08:28 +0100)
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

compiler/types/Kind.hs
testsuite/tests/polykinds/T12668.hs [new file with mode: 0644]
testsuite/tests/polykinds/T12718.hs [new file with mode: 0644]
testsuite/tests/polykinds/all.T

index c38a533..01a62e2 100644 (file)
@@ -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 (file)
index 0000000..4640903
--- /dev/null
@@ -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 (file)
index 0000000..82d6dcd
--- /dev/null
@@ -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
index 6da6ae4..6ec2a43 100644 (file)
@@ -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, [''])