Have mkCastTy look more closely for reflexivity.

This may have performance implications.

compiler/coreSyn/CoreSubst.hs

@@ -1302,12 +1302,11 @@ dealWithStringLiteral fun str co
 dealWithCoercion :: Coercion -> DataCon -> [CoreExpr]
                  -> Maybe (DataCon, [Type], [CoreExpr])
 dealWithCoercion co dc dc_args
-  | isReflCo co
+  | isReflCo co || from_ty `eqType` to_ty  -- try cheap test first
   , let (univ_ty_args, rest_args) = splitAtList (dataConUnivTyVars dc) dc_args
   = Just (dc, map exprToType univ_ty_args, rest_args)
 
-  | Pair _from_ty to_ty <- coercionKind co
-  , Just (to_tc, to_tc_arg_tys) <- splitTyConApp_maybe to_ty
+  | Just (to_tc, to_tc_arg_tys) <- splitTyConApp_maybe to_ty
   , to_tc == dataConTyCon dc
         -- These two tests can fail; we might see
         --      (C x y) `cast` (g :: T a ~ S [a]),
@@ -1347,15 +1346,19 @@ dealWithCoercion co dc dc_args
 
         dump_doc = vcat [ppr dc,      ppr dc_univ_tyvars, ppr dc_ex_tyvars,
                          ppr arg_tys, ppr dc_args,
-                         ppr ex_args, ppr val_args, ppr co, ppr _from_ty, ppr to_ty, ppr to_tc ]
+                         ppr ex_args, ppr val_args, ppr co, ppr from_ty, ppr to_ty, ppr to_tc ]
     in
-    ASSERT2( eqType _from_ty (mkTyConApp to_tc (map exprToType $ takeList dc_univ_tyvars dc_args)), dump_doc )
+    ASSERT2( eqType from_ty (mkTyConApp to_tc (map exprToType $ takeList dc_univ_tyvars dc_args)), dump_doc )
     ASSERT2( equalLength val_args arg_tys, dump_doc )
     Just (dc, to_tc_arg_tys, to_ex_args ++ new_val_args)
 
   | otherwise
   = Nothing
 
+  where
+    Pair from_ty to_ty = coercionKind co
+
+
 {-
 Note [Unfolding DFuns]
 ~~~~~~~~~~~~~~~~~~~~~~

compiler/typecheck/TcForeign.hs

@@ -164,7 +164,7 @@ normaliseFfiType' env ty0 = go initRecTc ty0
 
         | isFamilyTyCon tc              -- Expand open tycons
         , (co, ty) <- normaliseTcApp env Representational tc tys
-        , not (isReflCo co)
+        , not (isReflexiveCo co)
         = do (co', ty', gres) <- go rec_nts ty
              return (mkTransCo co co', ty', gres)
 

compiler/types/Coercion.hs

@@ -57,7 +57,7 @@ module Coercion (
 
         pickLR,
 
-        isReflCo, isReflCo_maybe,
+        isReflCo, isReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
 
         -- ** Coercion variables
         mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
@@ -428,14 +428,36 @@ mkHeteroCoercionType Nominal          = mkHeteroPrimEqPred
 mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
 mkHeteroCoercionType Phantom          = panic "mkHeteroCoercionType"
 
+-- | Tests if this coercion is obviously reflexive. Guaranteed to work
+-- very quickly. Sometimes a coercion can be reflexive, but not obviously
+-- so. c.f. 'isReflexiveCo'
 isReflCo :: Coercion -> Bool
 isReflCo (Refl {}) = True
 isReflCo _         = False
 
+-- | Returns the type coerced if this coercion is reflexive. Guaranteed
+-- to work very quickly. Sometimes a coercion can be reflexive, but not
+-- obviously so. c.f. 'isReflexiveCo_maybe'
 isReflCo_maybe :: Coercion -> Maybe (Type, Role)
 isReflCo_maybe (Refl r ty) = Just (ty, r)
 isReflCo_maybe _           = Nothing
 
+-- | Slowly checks if the coercion is reflexive. Don't call this in a loop,
+-- as it walks over the entire coercion.
+isReflexiveCo :: Coercion -> Bool
+isReflexiveCo = isJust . isReflexiveCo_maybe
+
+-- | Extracts the coerced type from a reflexive coercion. This potentially
+-- walks over the entire coercion, so avoid doing this in a loop.
+isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
+isReflexiveCo_maybe (Refl r ty) = Just (ty, r)
+isReflexiveCo_maybe co
+  | ty1 `eqType` ty2
+  = Just (ty1, r)
+  | otherwise
+  = Nothing
+  where (Pair ty1 ty2, r) = coercionKindRole co
+
 {-
 %************************************************************************
 %*                                                                      *
@@ -1700,7 +1722,7 @@ coercionKind co = go co
       = let Pair _ k2          = go k_co
             tv2                = setTyVarKind tv1 k2
             Pair ty1 ty2       = go co
-            ty2' = substTyWith [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo k_co] ty2 in
+            ty2' = substTyWith [tv1] [TyVarTy tv2 `mk_cast_ty` mkSymCo k_co] ty2 in
         mkNamedForAllTy <$> Pair tv1 tv2 <*> pure Invisible <*> Pair ty1 ty2'
     go (CoVarCo cv)         = toPair $ coVarTypes cv
     go (AxiomInstCo ax ind cos)
@@ -1751,6 +1773,11 @@ coercionKind co = go co
     go_app (InstCo co arg) args = go_app co (arg:args)
     go_app co              args = applyTys <$> go co <*> (sequenceA $ map go args)
 
+    -- The real mkCastTy is too slow, and we can easily have nested ForAllCos.
+    mk_cast_ty :: Type -> Coercion -> Type
+    mk_cast_ty ty (Refl {}) = ty
+    mk_cast_ty ty co        = CastTy ty co
+
 -- | Apply 'coercionKind' to multiple 'Coercion's
 coercionKinds :: [Coercion] -> Pair [Type]
 coercionKinds tys = sequenceA $ map coercionKind tys

compiler/types/Coercion.hs-boot

@@ -30,6 +30,7 @@ mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
 mkFunCos :: Role -> [Coercion] -> Coercion -> Coercion
 
 isReflCo :: Coercion -> Bool
+isReflexiveCo :: Coercion -> Bool
 coVarKindsTypesRole :: CoVar -> (Kind, Kind, Type, Type, Role)
 coVarRole :: CoVar -> Role
 

compiler/types/Type.hs

@@ -941,7 +941,10 @@ splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty'
 splitCastTy_maybe (CastTy ty co)               = Just (ty, co)
 splitCastTy_maybe _                            = Nothing
 
--- | Make a 'CastTy'. The Coercion must be nominal.
+-- | Make a 'CastTy'. The Coercion must be nominal. This function looks
+-- at the entire structure of the type and coercion in an attempt to
+-- maintain representation invariance (that is, any two types that are `eqType`
+-- look the same). Be very wary of calling this in a loop.
 mkCastTy :: Type -> Coercion -> Type
 -- Running example:
 --   T :: forall k1. k1 -> forall k2. k2 -> Bool -> Maybe k1 -> *
@@ -955,9 +958,13 @@ mkCastTy :: Type -> Coercion -> Type
 --   (T Nat 3 Symbol |> <Symbol> -> <Bool> -> <Maybe Nat> -> co)
 --      "foo" True (Just 2)
 --
--- General approach:
---
-mkCastTy ty (Refl {}) = ty
+mkCastTy ty co | isReflexiveCo co = ty
+-- NB: Do the slow check here. This is important to keep the splitXXX
+-- functions working properly. Otherwise, we may end up with something
+-- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
+-- fails under splitFunTy_maybe. This happened with the cheaper check
+-- in test dependent/should_compile/dynamic-paper.
+
 mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2)
 -- See Note [Weird typing rule for ForAllTy]
 mkCastTy (ForAllTy (Named tv vis) inner_ty) co

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, [''])

testsuite/tests/dependent/should_compile/dynamic-paper.hs

+{- 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