Commit eefe86d9 authored by Simon Peyton Jones's avatar Simon Peyton Jones

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
parent f9308c2a
......@@ -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.
-}
{-# 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"
{-# 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
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment