Typeable: Allow App to match arrow types
authorBen Gamari <bgamari.foss@gmail.com>
Tue, 19 Sep 2017 22:57:38 +0000 (18:57 -0400)
committerBen Gamari <ben@smart-cactus.org>
Thu, 21 Sep 2017 15:30:38 +0000 (11:30 -0400)
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

libraries/base/Data/Type/Equality.hs
libraries/base/Data/Typeable/Internal.hs
libraries/base/changelog.md
testsuite/tests/typecheck/should_run/T14236.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_run/T14236.stdout [new file with mode: 0644]
testsuite/tests/typecheck/should_run/all.T

index 5caa35a..2b95a58 100644 (file)
@@ -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
index f094d96..bc36fb1 100644 (file)
@@ -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
index 5fd7ba3..dcd2e5e 100644 (file)
@@ -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*
 
diff --git a/testsuite/tests/typecheck/should_run/T14236.hs b/testsuite/tests/typecheck/should_run/T14236.hs
new file mode 100644 (file)
index 0000000..c08682b
--- /dev/null
@@ -0,0 +1,14 @@
+{-# 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)
diff --git a/testsuite/tests/typecheck/should_run/T14236.stdout b/testsuite/tests/typecheck/should_run/T14236.stdout
new file mode 100644 (file)
index 0000000..a168ea8
--- /dev/null
@@ -0,0 +1,3 @@
+((->) 'LiftedRep 'LiftedRep Int,Char)
+((->) 'IntRep 'LiftedRep Int#,Char)
+Int# -> [Char]
index 3fc1928..1958001 100755 (executable)
@@ -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, [''])