Commit cc6be3a2 authored by Ben Gamari's avatar Ben Gamari Committed by Ben Gamari

Typeable: Allow App to match arrow types

Test Plan: T14236

Reviewers: austin, hvr, goldfire

Reviewed By: goldfire

Subscribers: RyanGlScott, simonpj, rwbarton, goldfire, thomie, dfeuer

GHC Trac Issues: #14236

Differential Revision: https://phabricator.haskell.org/D3969
parent 283eb1a0
......@@ -138,7 +138,7 @@ instance a ~ b => Enum (a :~: b) where
-- | @since 4.7.0.0
deriving instance a ~ b => Bounded (a :~: b)
-- | Kind heterogeneous propositional equality. Like '(:~:)', @a :~~: b@ is
-- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is
-- inhabited by a terminating value if and only if @a@ is the same type as @b@.
--
-- @since 4.10.0.0
......
......@@ -175,11 +175,17 @@ rnfTyCon (TyCon _ _ m n _ k) = rnfModule m `seq` rnfTrName n `seq` rnfKindRep k
data TypeRep (a :: k) where
TrTyCon :: {-# UNPACK #-} !Fingerprint -> !TyCon -> [SomeTypeRep]
-> TypeRep (a :: k)
-- | Invariant: Saturated arrow types (e.g. things of the form @a -> b@)
-- are represented with @'TrFun' a b@, not @TrApp (TrApp funTyCon a) b@.
TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
{-# UNPACK #-} !Fingerprint
-> TypeRep (a :: k1 -> k2)
-> TypeRep (b :: k1)
-> TypeRep (a b)
-- | @TrFun fpr a b@ represents a function type @a -> b@. We use this for
-- the sake of efficiency as functions are quite ubiquitous.
TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2).
{-# UNPACK #-} !Fingerprint
......@@ -224,6 +230,7 @@ instance Ord SomeTypeRep where
-- | The function type constructor.
--
-- For instance,
--
-- @
-- typeRep \@(Int -> Char) === Fun (typeRep \@Int) (typeRep \@Char)
-- @
......@@ -266,6 +273,13 @@ mkTrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
TypeRep (a :: k1 -> k2)
-> TypeRep (b :: k1)
-> TypeRep (a b)
mkTrApp rep@(TrApp _ (TrTyCon _ con _) (x :: TypeRep x)) (y :: TypeRep y)
| con == funTyCon -- cheap check first
, Just (IsTYPE (rx :: TypeRep rx)) <- isTYPE (typeRepKind x)
, Just (IsTYPE (ry :: TypeRep ry)) <- isTYPE (typeRepKind y)
, Just HRefl <- withTypeable x $ withTypeable rx $ withTypeable ry
$ typeRep @((->) x :: TYPE ry -> Type) `eqTypeRep` rep
= mkTrFun x y
mkTrApp a b = TrApp fpr a b
where
fpr_a = typeRepFingerprint a
......@@ -275,17 +289,39 @@ mkTrApp a b = TrApp fpr a b
-- | A type application.
--
-- For instance,
--
-- @
-- typeRep \@(Maybe Int) === App (typeRep \@Maybe) (typeRep \@Int)
-- @
-- Note that this will never match a function type (e.g. @Int -> Char@).
--
-- Note that this will also match a function type,
--
-- @
-- typeRep \@(Int# -> Char)
-- ===
-- App (App arrow (typeRep \@Int#)) (typeRep \@Char)
-- @
--
-- where @arrow :: TypeRep ((->) :: TYPE IntRep -> Type -> Type)@.
--
pattern App :: forall k2 (t :: k2). ()
=> forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b)
=> TypeRep a -> TypeRep b -> TypeRep t
pattern App f x <- TrApp _ f x
pattern App f x <- (splitApp -> Just (IsApp f x))
where App f x = mkTrApp f x
data IsApp (a :: k) where
IsApp :: forall k k' (f :: k' -> k) (x :: k'). ()
=> TypeRep f -> TypeRep x -> IsApp (f x)
splitApp :: forall k (a :: k). ()
=> TypeRep a
-> Maybe (IsApp a)
splitApp (TrApp _ f x) = Just (IsApp f x)
splitApp rep@(TrFun _ a b) = Just (IsApp (mkTrApp arr a) b)
where arr = bareArrow rep
splitApp (TrTyCon{}) = Nothing
-- | Use a 'TypeRep' as 'Typeable' evidence.
withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r
withTypeable rep k = unsafeCoerce k' rep
......@@ -303,10 +339,13 @@ pattern Con con <- TrTyCon _ con _
-- variables.
--
-- For instance,
--
-- @
-- App (Con' proxyTyCon ks) intRep = typeRep @(Proxy \@Int)
-- @
--
-- will bring into scope,
--
-- @
-- proxyTyCon :: TyCon
-- ks == [someTypeRep @Type] :: [SomeTypeRep]
......@@ -316,6 +355,7 @@ pattern Con con <- TrTyCon _ con _
pattern Con' :: forall k (a :: k). TyCon -> [SomeTypeRep] -> TypeRep a
pattern Con' con ks <- TrTyCon _ con ks
-- TODO: Remove Fun when #14253 is fixed
{-# COMPLETE Fun, App, Con #-}
{-# COMPLETE Fun, App, Con' #-}
......@@ -352,7 +392,7 @@ typeRepKind :: TypeRep (a :: k) -> TypeRep k
typeRepKind (TrTyCon _ tc args)
= unsafeCoerceRep $ tyConKind tc args
typeRepKind (TrApp _ f _)
| Fun _ res <- typeRepKind f
| TrFun _ _ res <- typeRepKind f
= res
| otherwise
= error ("Ill-kinded type application: " ++ show (typeRepKind f))
......@@ -382,9 +422,9 @@ instantiateKindRep vars = go
go (KindRepVar var)
= vars A.! var
go (KindRepApp f a)
= SomeTypeRep $ App (unsafeCoerceRep $ go f) (unsafeCoerceRep $ go a)
= SomeTypeRep $ mkTrApp (unsafeCoerceRep $ go f) (unsafeCoerceRep $ go a)
go (KindRepFun a b)
= SomeTypeRep $ Fun (unsafeCoerceRep $ go a) (unsafeCoerceRep $ go b)
= SomeTypeRep $ mkTrFun (unsafeCoerceRep $ go a) (unsafeCoerceRep $ go b)
go (KindRepTYPE r) = unkindedTypeRep $ tYPE `kApp` runtimeRepTypeRep r
go (KindRepTypeLitS sort s)
= mkTypeLitFromString sort (unpackCStringUtf8# s)
......@@ -407,7 +447,7 @@ kApp :: SomeKindedTypeRep (k -> k')
-> SomeKindedTypeRep k
-> SomeKindedTypeRep k'
kApp (SomeKindedTypeRep f) (SomeKindedTypeRep a) =
SomeKindedTypeRep (App f a)
SomeKindedTypeRep (mkTrApp f a)
kindedTypeRep :: forall (a :: k). Typeable a => SomeKindedTypeRep k
kindedTypeRep = SomeKindedTypeRep (typeRep @a)
......@@ -473,6 +513,32 @@ vecElemTypeRep e =
rep :: forall (a :: VecElem). Typeable a => SomeKindedTypeRep VecElem
rep = kindedTypeRep @VecElem @a
bareArrow :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2). ()
=> TypeRep (a -> b)
-> TypeRep ((->) :: TYPE r1 -> TYPE r2 -> Type)
bareArrow (TrFun _ a b) =
mkTrCon funTyCon [SomeTypeRep rep1, SomeTypeRep rep2]
where
rep1 = getRuntimeRep $ typeRepKind a :: TypeRep r1
rep2 = getRuntimeRep $ typeRepKind b :: TypeRep r2
bareArrow _ = error "Data.Typeable.Internal.bareArrow: impossible"
data IsTYPE (a :: Type) where
IsTYPE :: forall (r :: RuntimeRep). TypeRep r -> IsTYPE (TYPE r)
-- | Is a type of the form @TYPE rep@?
isTYPE :: TypeRep (a :: Type) -> Maybe (IsTYPE a)
isTYPE (TrApp _ f r)
| Just HRefl <- f `eqTypeRep` typeRep @TYPE
= Just (IsTYPE r)
isTYPE _ = Nothing
getRuntimeRep :: forall (r :: RuntimeRep). TypeRep (TYPE r) -> TypeRep r
getRuntimeRep (TrApp _ _ r) = r
getRuntimeRep _ = error "Data.Typeable.Internal.getRuntimeRep: impossible"
-------------------------------------------------------------
--
-- The Typeable class and friends
......
......@@ -47,6 +47,8 @@
* Make `zipWith` and `zipWith3` inlinable (#14224)
* `Type.Reflection.App` now matches on function types (fixes #14236)
## 4.10.0.0 *April 2017*
* Bundled with GHC *TBA*
......
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE MagicHash #-}
import GHC.Exts
import Type.Reflection
main = do
case typeRep @(Int -> Char) of
App a b -> print (a, b)
case typeRep @(Int# -> Char) of
App a b -> print (a, b)
case typeRep @(Int# -> Char) of
App a b -> print $ App a (typeRep @String)
((->) 'LiftedRep 'LiftedRep Int,Char)
((->) 'IntRep 'LiftedRep Int#,Char)
Int# -> [Char]
......@@ -123,3 +123,4 @@ test('TypeableEq', normal, compile_and_run, [''])
test('T13435', normal, compile_and_run, [''])
test('T11715', exit_code(1), compile_and_run, [''])
test('T13594a', normal, ghci_script, ['T13594a.script'])
test('T14236', normal, compile_and_run, [''])
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