Have mkCastTy look more closely for reflexivity.

This may have performance implications.

2 files changed, 342 insertions, 0 deletions

diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index e1e064a1c3..1063b6ec94 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -10,3 +10,4 @@ test('RaeBlogPost', normal, compile, [''])
 test('mkGADTVars', normal, compile, [''])
 test('TypeLevelVec',normal,compile, [''])
 test('T9632', normal, compile, [''])
+test('dynamic-paper', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.hs b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
new file mode 100644
index 0000000000..4e892099b2
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
@@ -0,0 +1,341 @@
+{- This is the code extracted from "A reflection on types", by Simon PJ,
+Stephanie Weirich, Richard Eisenberg, and Dimitrios Vytiniotis, 2016. -}
+
+{-#  LANGUAGE RankNTypes, PolyKinds, TypeOperators,
+             ScopedTypeVariables, GADTs, FlexibleInstances,
+             UndecidableInstances, RebindableSyntax,
+             DataKinds, MagicHash, AutoDeriveTypeable, TypeInType  #-}
+{-# OPTIONS_GHC -fno-warn-missing-methods -fno-warn-redundant-constraints #-}
+
+module Dynamic where
+
+import Data.Map ( Map )
+import qualified Data.Map as Map
+import Unsafe.Coerce ( unsafeCoerce )
+import Control.Monad ( (<=<) )
+import Prelude hiding ( lookup, fromInteger, replicate )
+import qualified Prelude
+import qualified Data.Typeable
+import qualified Data.Data
+import Data.Kind
+
+lookupMap = Map.lookup
+insertMap = Map.insert
+
+--  let's ignore overloaded numbers
+fromInteger :: Integer -> Int
+fromInteger = Prelude.fromInteger
+
+insertStore = undefined
+schema = undefined
+withTypeable = undefined
+throw# = undefined
+
+toDynamicST = undefined
+fromDynamicST = undefined
+
+extendStore  :: Typeable a => STRef s a -> a -> Store -> Store
+lookupStore  :: Typeable a => STRef s a -> Store -> Maybe a
+
+type Key = Int
+data STRef s a = STR Key
+type Store = Map Key Dynamic
+
+extendStore (STR k) v  s =  insertMap k (toDynamicST v) s
+lookupStore (STR k)    s =  case lookupMap k s of
+                              Just d   -> fromDynamicST d
+                              Nothing  -> Nothing
+
+toDynamicST    :: Typeable a => a -> Dynamic
+fromDynamicST  :: Typeable a => Dynamic -> Maybe a
+
+eval = undefined
+data Term
+
+data DynamicSilly  =  DIntSilly  Int
+              |  DBoolSilly Bool
+              |  DCharSilly Char
+              |  DPairSilly DynamicSilly DynamicSilly
+
+
+toDynInt :: Int -> DynamicSilly
+toDynInt = DIntSilly
+
+fromDynInt :: DynamicSilly -> Maybe Int
+fromDynInt (DIntSilly n)  = Just n
+fromDynInt _         = Nothing
+
+toDynPair :: DynamicSilly -> DynamicSilly -> DynamicSilly
+toDynPair = DPairSilly
+
+dynFstSilly :: DynamicSilly -> Maybe DynamicSilly
+dynFstSilly (DPairSilly x1 x2) = Just x1
+dynFstSilly _             = Nothing
+
+eval :: Term -> DynamicSilly
+
+eqT = undefined
+
+instance Typeable (->)
+instance Typeable Maybe
+instance Typeable Bool
+instance Typeable Int
+instance (Typeable a, Typeable b) => Typeable (a b)
+instance Typeable (,)
+
+instance Eq TypeRepX
+
+data Dynamic where
+   Dyn :: TypeRep a -> a -> Dynamic
+
+toDynamic :: Typeable a => a -> Dynamic
+toDynamic x = Dyn typeRep x
+
+eqTNoKind = undefined
+
+eqTNoKind :: TypeRep a -> TypeRep b -> Maybe (a :***: b)
+   --  Primitive; implemented by compiler
+
+data a :***: b where
+  ReflNoKind :: a :***: a
+
+fromDynamic :: forall d. Typeable d => Dynamic -> Maybe d
+fromDynamic (Dyn (ra :: TypeRep a) (x :: a))
+  =  case eqT ra (typeRep :: TypeRep d) of
+       Nothing    -> Nothing
+       Just Refl  -> Just x
+
+fromDynamicMonad :: forall d. Typeable d => Dynamic -> Maybe d
+
+fromDynamicMonad (Dyn ra x)
+  = do  Refl <- eqT ra (typeRep :: TypeRep d)
+        return x
+
+cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
+cast x = do  Refl <- eqT  (typeRep :: TypeRep a)
+                          (typeRep :: TypeRep b)
+             return x
+
+gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b)
+gcast x = do  Refl <- eqT  (typeRep :: TypeRep a)
+                           (typeRep :: TypeRep b)
+              return x
+
+data SameKind :: k -> k -> *
+type CheckAppResult = SameKind AppResult AppResultNoKind
+  --  not the most thorough check
+foo :: AppResult x -> AppResultNoKind x
+foo (App y z) = AppNoKind y z
+
+splitApp :: TypeRep a -> Maybe (AppResult a)
+splitApp = undefined
+splitAppNoKind = undefined
+splitAppNoKind :: TypeRep a -> Maybe (AppResultNoKind a)
+   --  Primitive; implemented by compiler
+
+data AppResultNoKind t where
+  AppNoKind :: TypeRep a -> TypeRep b -> AppResultNoKind (a b)
+
+dynFstNoKind :: Dynamic -> Maybe Dynamic
+dynFstNoKind (Dyn rpab x)
+  = do  AppNoKind rpa rb  <- splitAppNoKind rpab
+        AppNoKind rp  ra  <- splitAppNoKind rpa
+        Refl        <- eqT rp (typeRep :: TypeRep (,))
+        return (Dyn ra (fst x))
+
+dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
+dynApply (Dyn rf f) (Dyn rx x) = do
+    App ra rt2   <- splitApp rf
+    App rtc rt1  <- splitApp ra
+    Refl         <- eqT rtc (typeRep :: TypeRep (->))
+    Refl         <- eqT rt1 rx
+    return (Dyn rt2 (f x))
+
+data TypeRepAbstract (a :: k)  --  primitive, indexed by type and kind
+
+class Typeable (a :: k) where
+   typeRep :: TypeRep a
+
+data AppResult (t :: k) where
+  App ::  forall k1 k (a :: k1 -> k) (b :: k1).
+          TypeRep a -> TypeRep b -> AppResult (a b)
+
+dynFst :: Dynamic -> Maybe Dynamic
+dynFst (Dyn (rpab :: TypeRep pab) (x :: pab))
+
+  = do  App (rpa  :: TypeRep pa ) (rb :: TypeRep b)  <- splitApp rpab
+            --  introduces kind |k2|, and types |pa :: k2 -> *|, |b :: k2|
+
+        App (rp   :: TypeRep p  ) (ra :: TypeRep a)  <- splitApp rpa
+            --  introduces kind |k1|, and types |p :: k1 -> k2 -> *|, |a :: k1|
+
+        Refl       <- eqT rp (typeRep :: TypeRep (,))
+            --  introduces |p ~ (,)| and |(k1 -> k2 -> *) ~ (* -> * -> *)|
+
+        return (Dyn ra (fst x))
+
+eqT :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~: b)
+
+data (a :: k1) :~: (b :: k2) where
+  Refl :: forall k (a :: k). a :~: a
+
+castDance :: (Typeable a, Typeable b)  => a -> Maybe b
+castDance = castR typeRep typeRep
+
+withTypeable :: TypeRep a -> (Typeable a => r) -> r
+
+castR :: TypeRep a -> TypeRep b -> a -> Maybe b
+castR ta tb = withTypeable ta (withTypeable tb castDance)
+
+cmpT = undefined
+compareTypeRep = undefined
+
+data TypeRepX where
+   TypeRepX :: TypeRep a -> TypeRepX
+
+type TyMapLessTyped = Map TypeRepX Dynamic
+
+insertLessTyped    ::  forall a. Typeable a => a -> TyMapLessTyped -> TyMapLessTyped
+insertLessTyped x  =   Map.insert (TypeRepX (typeRep :: TypeRep a)) (toDynamic x)
+
+lookupLessTyped  ::  forall a. Typeable a => TyMapLessTyped -> Maybe a
+lookupLessTyped  =   fromDynamic <=< Map.lookup (TypeRepX (typeRep :: TypeRep a))
+
+instance Ord TypeRepX where
+  compare (TypeRepX tr1) (TypeRepX tr2) = compareTypeRep tr1 tr2
+
+compareTypeRep :: TypeRep a -> TypeRep b -> Ordering  --  primitive
+
+data TyMap = Empty | Node Dynamic TyMap TyMap
+
+lookup :: TypeRep a -> TyMap -> Maybe a
+lookup tr1 (Node (Dyn tr2 v) left right) =
+  case compareTypeRep tr1 tr2 of
+    LT  -> lookup tr1 left
+    EQ  -> castR tr2 tr1 v   --  know this cast will succeed
+    GT  -> lookup tr1 right
+lookup tr1 Empty = Nothing
+
+cmpT :: TypeRep a -> TypeRep b -> OrderingT a b
+  --  definition is primitive
+
+data OrderingT a b where
+  LTT  :: OrderingT a b
+  EQT  :: OrderingT t t
+  GTT  :: OrderingT a b
+
+data TypeRep (a :: k) where
+  TrApp    :: TypeRep a -> TypeRep b -> TypeRep (a b)
+  TrTyCon  :: TyCon -> TypeRep k -> TypeRep (a :: k)
+
+data TyCon = TyCon { tc_module :: Module, tc_name :: String }
+data Module = Module { mod_pkg :: String, mod_name :: String }
+
+tcMaybe  :: TyCon
+tcMaybe  = TyCon  { tc_module  = Module  { mod_pkg   = "base"
+                                               , mod_name  = "Data.Maybe" }
+                        , tc_name    = "Maybe" }
+
+rt = undefined
+
+delta1 :: Dynamic -> Dynamic
+delta1 dn = case fromDynamic dn of
+             Just f   -> f dn
+             Nothing  -> dn
+loop1 = delta1 (toDynamic delta1)
+
+data Rid = MkT (forall a. TypeRep a -> a -> a)
+rt :: TypeRep Rid
+delta :: forall a. TypeRep a -> a -> a
+delta ra x = case (eqT ra rt) of
+             Just Refl  -> case x of MkT y -> y rt x
+             Nothing    -> x
+loop = delta rt (MkT delta)
+
+throw# :: SomeException -> a
+
+data SomeException where
+  SomeException :: Exception e => e -> SomeException
+
+class (Typeable e, Show e) => Exception e where {   }
+
+data Company
+data Salary
+incS :: Float -> Salary -> Salary
+incS = undefined
+
+--  some impedance matching with SYB
+instance Data.Data.Data Company
+instance {-#  INCOHERENT  #-} Data.Typeable.Typeable a => Typeable a
+
+mkT :: (Typeable a, Typeable b) => (b -> b) -> a -> a
+mkT f x = case (cast f) of
+            Just g   -> g x
+            Nothing  -> x
+
+data Expr a
+frontEnd = undefined
+
+data DynExp where
+  DE :: TypeRep a -> Expr a -> DynExp
+
+frontEnd :: String -> DynExp
+
+data TyConOld
+
+typeOf = undefined
+eqTOld = undefined
+funTcOld = undefined :: TyConOld
+splitTyConApp = undefined
+mkTyCon3 = undefined
+boolTcOld = undefined
+tupleTc = undefined
+mkTyConApp = undefined
+instance Eq TypeRepOld
+instance Eq TyConOld
+
+data TypeRepOld       --  Abstract
+
+class TypeableOld a where
+  typeRepOld :: proxy a -> TypeRepOld
+
+data DynamicOld where
+   DynOld :: TypeRepOld -> a -> DynamicOld
+
+data Proxy a = Proxy
+
+fromDynamicOld :: forall d. TypeableOld d => DynamicOld -> Maybe d
+fromDynamicOld (DynOld trx x)
+ | typeRepOld (Proxy :: Proxy d) == trx  = Just (unsafeCoerce x)
+ | otherwise                          = Nothing
+
+dynApplyOld :: DynamicOld -> DynamicOld -> Maybe DynamicOld
+dynApplyOld (DynOld trf f) (DynOld trx x) =
+  case splitTyConApp trf of
+      (tc, [t1,t2]) | tc == funTcOld && t1 == trx ->
+          Just (DynOld t2 ((unsafeCoerce f) x))
+      _ -> Nothing
+
+data DynamicClosed where
+  DynClosed :: TypeRepClosed a -> a -> DynamicClosed
+
+data TypeRepClosed (a :: *) where
+  TBool  :: TypeRepClosed Bool
+  TFun   :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a -> b)
+  TProd  :: TypeRepClosed a -> TypeRepClosed b -> TypeRepClosed (a, b)
+
+
+lookupPil = undefined
+
+lookupPil :: Typeable a => [Dynamic] -> Maybe a
+
+data Dyn1 = Dyn1 Int
+         | DynFun (Dyn1 -> Dyn1)
+         | DynPair (Dyn1, Dyn1)
+
+data TypeEnum = IntType | FloatType | BoolType | DateType | StringType
+data Schema = Object [Schema] |
+              Field TypeEnum |
+              Array Schema
+
+schema :: Typeable a => a -> Schema