From 52da6bdc17bb491d6d2f462b3680eb44b9be92e5 Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Sat, 26 Dec 2015 09:11:33 -0500 Subject: [PATCH] Have mkCastTy look more closely for reflexivity. This may have performance implications. --- compiler/coreSyn/CoreSubst.hs | 13 +- compiler/typecheck/TcForeign.hs | 2 +- compiler/types/Coercion.hs | 31 +- compiler/types/Coercion.hs-boot | 1 + compiler/types/Type.hs | 15 +- .../tests/dependent/should_compile/all.T | 1 + .../dependent/should_compile/dynamic-paper.hs | 341 ++++++++++++++++++ 7 files changed, 392 insertions(+), 12 deletions(-) create mode 100644 testsuite/tests/dependent/should_compile/dynamic-paper.hs diff --git a/compiler/coreSyn/CoreSubst.hs b/compiler/coreSyn/CoreSubst.hs index 0b48bbf0ca..bc96d0f756 100644 --- a/compiler/coreSyn/CoreSubst.hs +++ b/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] ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcForeign.hs b/compiler/typecheck/TcForeign.hs index 4d474d4206..3f10fe1c54 100644 --- a/compiler/typecheck/TcForeign.hs +++ b/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) diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 3aa56e2e04..f8647a0319 100644 --- a/compiler/types/Coercion.hs +++ b/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 diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot index 29f814a628..acd6aaf918 100644 --- a/compiler/types/Coercion.hs-boot +++ b/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 diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index fbb59542f8..42263d8b4c 100644 --- a/compiler/types/Type.hs +++ b/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 |> -> -> -> 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 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 -- GitLab