recover-rtti 0.1.0.0 → 0.2.0.0

raw patch · 19 files changed

+302/−236 lines, 19 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• recover-rtti.cabal +5/−6
• src/Debug/RecoverRTTI.hs +61/−7
• src/Debug/RecoverRTTI/Classifier.hs +1/−1
• src/Debug/RecoverRTTI/Classify.hs +1/−1
• src/Debug/RecoverRTTI/Constr.hs +11/−4
• src/Debug/RecoverRTTI/Modules.hs +1/−1
• src/Debug/RecoverRTTI/Tuple.hs +6/−18
• src/Debug/RecoverRTTI/Tuple/Recursive.hs +7/−6
• src/Debug/RecoverRTTI/Tuple/Size.hs +14/−1
• src/Debug/RecoverRTTI/TypeLevel.hs +167/−0
• src/Debug/RecoverRTTI/Util.hs +1/−15
• src/Debug/RecoverRTTI/Util/TypeLevel.hs +0/−166
• tests/Test/RecoverRTTI/Arbitrary.hs +1/−2
• tests/Test/RecoverRTTI/Classify.hs +0/−1
• tests/Test/RecoverRTTI/ConcreteClassifier.hs +2/−3
• tests/Test/RecoverRTTI/Sanity.hs +1/−1
• tests/Test/RecoverRTTI/Show.hs +0/−1
• tests/Test/RecoverRTTI/Staged.hs +19/−2

@@ -1,5 +1,9 @@ # Revision history for recover-rtti +## 0.2.0.0 -- 2021-03-15++* Reorganize module structure (primarily to improve Haddocks)+ ## 0.1.0.0 -- 2021-03-11  * Alpha release

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               recover-rtti-version:            0.1.0.0+version:            0.2.0.0 synopsis:           Recover run-time type information from the GHC heap description:        The main function in this package is 'classify', which looks                     at the GHC heap to recover type information about arbitrary@@ -24,22 +24,21 @@  library     exposed-modules:  Debug.RecoverRTTI--                      -- Other modules exported primarily for the tests-                      Debug.RecoverRTTI.FlatClosure-                      Debug.RecoverRTTI.Util-                      Debug.RecoverRTTI.Util.TypeLevel+                      Debug.RecoverRTTI.TypeLevel      other-modules:    Debug.RecoverRTTI.Classifier                       Debug.RecoverRTTI.Classify                       Debug.RecoverRTTI.ClosureTree                       Debug.RecoverRTTI.Constr+                      Debug.RecoverRTTI.FlatClosure                       Debug.RecoverRTTI.Modules                       Debug.RecoverRTTI.Tuple                       Debug.RecoverRTTI.Tuple.Recursive                       Debug.RecoverRTTI.Tuple.Size                       Debug.RecoverRTTI.UserDefined+                      Debug.RecoverRTTI.Util                       Debug.RecoverRTTI.Wrappers+     build-depends:    base        >= 4.13  && < 4.16                     , aeson       >= 1.5   && < 1.6                     , bytestring  >= 0.10  && < 0.11

@@ -1,10 +1,64 @@+-- | Recover runtime type information module Debug.RecoverRTTI (-    module X+    -- * Take advance of the recovered type information+    anythingToString+    -- * Recover type information+  , classify+  , Classifier(..)+  , Classifiers(..)+    -- ** Pair value with its classifier+  , Classified(..)+  , classified+    -- ** Unknown or partially known type arguments+  , MaybeF(..)+  , EitherF(..)+  , MaybePairF(..)+    -- ** Newtype wrappers for unshowable types+  , SomeSTRef(..)+  , SomeTVar(..)+  , SomeMVar(..)+  , SomeFun(..)+    -- * User-defined types+  , UserDefined -- opaque+    -- ** Classify constructor arguments+  , KnownConstr+  , fromUserDefined+  , Some(..)+    -- ** Constructor information+  , Constr(..)+    -- ** Type-level constructor informatino+  , ConstrPkg+  , ConstrModl+  , ConstrName+  , prettyKnownConstr+    -- ** Casting+  , unsafeCoerceUserDefined+  , ConstrOf+  , Constrs+  , GConstrs+  , GConstrsOfType+    -- ** Constructor check+  , checkIsConstrOf+  , IsConstrOf(..)+    -- * Inductive tuples+  , WrappedTuple(..)+  , Tuple+    -- ** Translation to/from NP+  , tupleFromNP+  , tupleToNP+    -- ** Valid tuple size+  , IsValidSize(..)+  , ValidSize(..)+  , TooBig(..)+  , smallerIsValid+  , toValidSize+  , liftValidSize   ) where -import Debug.RecoverRTTI.Classifier  as X-import Debug.RecoverRTTI.Classify    as X-import Debug.RecoverRTTI.Constr      as X-import Debug.RecoverRTTI.UserDefined as X-import Debug.RecoverRTTI.Wrappers    as X-import Debug.RecoverRTTI.Tuple       as X+import Debug.RecoverRTTI.Classifier+import Debug.RecoverRTTI.Classify+import Debug.RecoverRTTI.Constr+import Debug.RecoverRTTI.Tuple+import Debug.RecoverRTTI.UserDefined+import Debug.RecoverRTTI.Util+import Debug.RecoverRTTI.Wrappers

@@ -35,9 +35,9 @@  import Debug.RecoverRTTI.Constr import Debug.RecoverRTTI.Tuple+import Debug.RecoverRTTI.TypeLevel import Debug.RecoverRTTI.UserDefined import Debug.RecoverRTTI.Wrappers-import Debug.RecoverRTTI.Util.TypeLevel  {-------------------------------------------------------------------------------   Classifier

@@ -47,9 +47,9 @@ import Debug.RecoverRTTI.FlatClosure import Debug.RecoverRTTI.Modules import Debug.RecoverRTTI.Tuple+import Debug.RecoverRTTI.TypeLevel import Debug.RecoverRTTI.UserDefined import Debug.RecoverRTTI.Util-import Debug.RecoverRTTI.Util.TypeLevel  {-------------------------------------------------------------------------------   Classification

@@ -23,6 +23,10 @@   , knownConstr   , prettyKnownConstr   , elimKnownConstr+    -- | Type-level extracts+  , ConstrPkg+  , ConstrModl+  , ConstrName     -- | Compute all known constructors   , Constrs   , GConstrs@@ -40,17 +44,18 @@ import GHC.Generics import GHC.TypeLits +import Debug.RecoverRTTI.TypeLevel import Debug.RecoverRTTI.Util-import Debug.RecoverRTTI.Util.TypeLevel  {-------------------------------------------------------------------------------   Type-level metadata -------------------------------------------------------------------------------} +-- | Information about a constructor data Constr a = Constr {-      constrPkg  :: a-    , constrModl :: a-    , constrName :: a+      constrPkg  :: a  -- ^ Package+    , constrModl :: a  -- ^ Module+    , constrName :: a  -- ^ Constructor name     }   deriving (Show, Eq) @@ -170,9 +175,11 @@                   )           )) +-- | Evidence that @c@ is a constructor of @a@ data IsConstrOf (a :: Type) (c :: Constr Symbol) where   IsConstrOf :: Elem c (Constrs a) ~ 'True => IsConstrOf a c +-- | Check if @c@ is a constructof of @a@ checkIsConstrOf :: forall (a :: Type) (c :: Constr Symbol).       SingI (Constrs a)    => Sing c -> Maybe (IsConstrOf a c)

@@ -18,7 +18,7 @@ import Data.List (isPrefixOf)  import Debug.RecoverRTTI.FlatClosure-import Debug.RecoverRTTI.Util.TypeLevel+import Debug.RecoverRTTI.TypeLevel  {-------------------------------------------------------------------------------   Packages

@@ -11,8 +11,6 @@ module Debug.RecoverRTTI.Tuple (     -- * Wrapped tuple     WrappedTuple(WrappedTuple, TNil, TCons)-    -- * Auxiliary-  , bimapTuple     -- * Conversion between tuples and NP   , tupleFromNP   , tupleToNP@@ -25,7 +23,7 @@  import Debug.RecoverRTTI.Tuple.Recursive import Debug.RecoverRTTI.Tuple.Size-import Debug.RecoverRTTI.Util.TypeLevel+import Debug.RecoverRTTI.TypeLevel  {-------------------------------------------------------------------------------   Wrapped tuple@@ -35,6 +33,11 @@   wrapped tuple. -------------------------------------------------------------------------------} +-- | Inductive tuple+--+-- Inductive view on tuples that can be constructed with or pattern matched on+-- using 'TNil' and 'TCons'. The underlying representation is a /true/ tuple+-- however; for example, @Tuple '[Int, Bool, Char] ~ (Int, Bool, Char)@. newtype WrappedTuple xs = WrappedTuple (Tuple xs)  pattern TNil ::@@ -54,21 +57,6 @@     TCons x xs = consWrapped (x, xs)  {-# COMPLETE TNil, TCons #-}--{--------------------------------------------------------------------------------  Auxiliary--------------------------------------------------------------------------------}--bimapTuple ::-      ( SListI xs-      , SListI ys-      , IsValidSize (Length (x ': xs))-      , Length xs ~ Length ys-      )-   => (x -> y)-   -> (WrappedTuple xs -> WrappedTuple ys)-   -> WrappedTuple (x ': xs) -> WrappedTuple (y ': ys)-bimapTuple f g (TCons x xs) = TCons (f x) (g xs)  {-------------------------------------------------------------------------------   Conversion to/from NP

@@ -1,12 +1,16 @@+{-# OPTIONS_GHC -Wno-overlapping-patterns -Wno-incomplete-patterns -Wno-incomplete-uni-patterns -fno-opt-coercion #-}+ {-# LANGUAGE DataKinds               #-} {-# LANGUAGE FlexibleContexts        #-} {-# LANGUAGE ScopedTypeVariables     #-} {-# LANGUAGE TypeFamilies            #-} {-# LANGUAGE TypeOperators           #-}--- {-# LANGUAGE UndecidableSuperClasses #-} --- Disable the GHC pattern match checker (this makes compilation /much/ faster)+-- | Provide a recursive views on tuples --+-- NOTE: We disable the GHC pattern match checker (this makes compilation /much/+-- faster).+-- -- Verified that this module compiles without warnings for smaller maximum -- tuple size. --@@ -14,9 +18,6 @@ -- -- * https://gitlab.haskell.org/ghc/ghc/-/issues/17836 -- * https://gitlab.haskell.org/ghc/ghc/-/issues/16382-{-# OPTIONS_GHC -Wno-overlapping-patterns -Wno-incomplete-patterns -Wno-incomplete-uni-patterns -fno-opt-coercion #-}---- | Provide a recursive views on tuples module Debug.RecoverRTTI.Tuple.Recursive (     Tuple   , cons@@ -26,7 +27,7 @@ import Data.SOP  import Debug.RecoverRTTI.Tuple.Size-import Debug.RecoverRTTI.Util.TypeLevel+import Debug.RecoverRTTI.TypeLevel  {-------------------------------------------------------------------------------   Generated

@@ -24,8 +24,8 @@ import Data.Proxy import Data.SOP.Dict +import Debug.RecoverRTTI.TypeLevel import Debug.RecoverRTTI.Util-import Debug.RecoverRTTI.Util.TypeLevel  {-------------------------------------------------------------------------------   Not generated@@ -40,6 +40,11 @@     aux :: (TooBig ('S n) -> r) -> TooBig n -> r     aux tooBig TooBig = tooBig (TooBig :: TooBig ('S n)) +-- | Smaller tuple sizes are always valid+--+-- This function is primarily useful when doing recursion on tuples: we may have+-- in scope evidence that @('S n)@ is a valid tuple size, and need to know that+-- @n@ is a valid tuple size in order to be able to make the recursive call. smallerIsValid :: forall n r.      IsValidSize ('S n)   => Proxy ('S n)@@ -52,6 +57,11 @@     valid :: ValidSize ('S n)     valid = isValidSize +-- | Valid tuple sizes+--+-- GHC does not support tuples larger than 62 fields. We do allow for tuples of+-- zero size (which we interpret as unit @()@) and tuples of size one+-- (where @Tuple '[x] ~ x@). class SingI n => IsValidSize n where   isValidSize :: ValidSize n @@ -59,9 +69,11 @@   Generated -------------------------------------------------------------------------------} +-- | Tuples with too many fields (more than 62) data TooBig (n :: Nat) where   TooBig :: TooBig ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +-- | Lift term-level evidence to type-level liftValidSize :: forall n. ValidSize n -> Dict IsValidSize n liftValidSize (ValidSize n notTooBig) = go n   where@@ -384,6 +396,7 @@ instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where   isValidSize = ValidSize sing $ \case +-- | Check the given size is a valid tuple size toValidSize :: Int -> Maybe (Some ValidSize) toValidSize = go   where

@@ -0,0 +1,167 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE FlexibleInstances    #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE RankNTypes           #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Generic type-level utilities+module Debug.RecoverRTTI.TypeLevel (+    -- * Singletons+    Sing(..)+  , SingI(..)+  , DecidableEquality(..)+    -- ** Natural numbers+  , Nat(..)+  , knownNat+  , Length+    -- * General purpose type level functions+  , Or+  , Equal+  , Elem+  , Assert+    -- * Type-level membership check+  , IsElem(..)+  , checkIsElem+    -- * Phantom type parameters+  , Phantom(..)+  , Poly(..)+  , maybePoly+  ) where++import Data.Kind+import Data.Proxy+import Data.Type.Equality+import GHC.TypeLits (ErrorMessage, Symbol, KnownSymbol, TypeError, sameSymbol)++{-------------------------------------------------------------------------------+  Singletons+-------------------------------------------------------------------------------}++data family Sing :: k -> Type++class SingI (a :: k) where+  sing :: Sing a++class DecidableEquality k where+  decideEquality :: Sing (a :: k) -> Sing (b :: k) -> Maybe (a :~: b)++{-------------------------------------------------------------------------------+  For kind 'Type', Sing is just a proxy+-------------------------------------------------------------------------------}++data instance Sing (a :: Type) where+  SProxy :: Sing (a :: Type)++instance SingI (a :: Type) where+  sing = SProxy++{-------------------------------------------------------------------------------+  Natural numbers++  Unlike @ghc@'s, these are inductively defined.+-------------------------------------------------------------------------------}++data Nat = Z | S Nat++data instance Sing (n :: Nat) where+  SZ :: Sing 'Z+  SS :: Sing n -> Sing ('S n)++instance            SingI 'Z     where sing = SZ+instance SingI n => SingI ('S n) where sing = SS sing++knownNat :: Sing (n :: Nat) -> Int+knownNat SZ     = 0+knownNat (SS n) = knownNat n + 1++type family Length (xs :: [k]) :: Nat where+  Length '[]       = 'Z+  Length (_ ': xs) = 'S (Length xs)++{-------------------------------------------------------------------------------+  Singleton instance for type-level symbols+-------------------------------------------------------------------------------}++data instance Sing (n :: Symbol) where+  SSymbol :: KnownSymbol n => Sing n++instance KnownSymbol n => SingI (n :: Symbol) where+  sing = SSymbol++instance DecidableEquality Symbol where+  decideEquality SSymbol SSymbol = sameSymbol Proxy Proxy++{-------------------------------------------------------------------------------+  Singleton instance for lists+-------------------------------------------------------------------------------}++data instance Sing (xs :: [k]) where+  SN :: Sing '[]+  SC :: Sing x -> Sing xs -> Sing (x ': xs)++instance                        SingI '[]       where sing = SN+instance (SingI x, SingI xs) => SingI (x ': xs) where sing = SC sing sing++{-------------------------------------------------------------------------------+  General purpose type level functions+-------------------------------------------------------------------------------}++type family Or (a :: Bool) (b :: Bool) where+  Or 'True b     = 'True+  Or a     'True = 'True+  Or _     _     = 'False++type family Equal (x :: k) (y :: k) where+  Equal x x = 'True+  Equal x y = 'False++type family Elem (x :: k) (xs :: [k]) where+  Elem x '[]       = 'False+  Elem x (y ': ys) = Or (Equal x y) (Elem x ys)++-- | Assert type-level predicate+--+-- We cannot define this in terms of a more general @If@ construct, because+-- @ghc@'s type-level language has an undefined reduction order and so we get+-- no short-circuiting.+type family Assert (b :: Bool) (err :: ErrorMessage) :: Constraint where+  Assert 'True  err = ()+  Assert 'False err = TypeError err++{-------------------------------------------------------------------------------+  Decidable equality gives a decidable membership check+-------------------------------------------------------------------------------}++data IsElem (x :: k) (xs :: [k]) where+  IsElem :: Elem x xs ~ 'True => IsElem x xs++shiftIsElem :: IsElem x ys -> IsElem x (y ': ys)+shiftIsElem IsElem = IsElem++checkIsElem ::+     DecidableEquality k+  => Sing (x :: k) -> Sing (xs :: [k]) -> Maybe (IsElem x xs)+checkIsElem _ SN         = Nothing+checkIsElem x (SC y ys) = case decideEquality x y of+                            Just Refl -> Just IsElem+                            Nothing   -> shiftIsElem <$> checkIsElem x ys++{-------------------------------------------------------------------------------+  Phantom type parameters+-------------------------------------------------------------------------------}++-- | Functors with phantom arguments+class Phantom (f :: k -> Type) where+  -- | Similar to 'Data.Functor.Contravariant.phantom', but without requiring+  -- 'Functor' or 'Contravariant'+  phantom :: forall a b. f a -> f b++data Poly (f :: k -> Type) = Poly (forall (a :: k). f a)++-- | Commute @Maybe@ and @forall@+maybePoly :: Phantom f => Maybe (f a) -> Maybe (Poly f)+maybePoly = fmap (\v -> Poly (phantom v))

@@ -16,8 +16,6 @@   , elimKnownSymbol     -- * Constraints   , keepRedundantConstraint-    -- * Traversable-  , checkEmptyTraversable     -- * Lists   , dropEnds     -- * SOP@@ -28,10 +26,9 @@ import Data.Kind import Data.Proxy import Data.SOP-import Data.Void import GHC.TypeLits (KnownSymbol, SomeSymbol(..), someSymbolVal) -import Debug.RecoverRTTI.Util.TypeLevel+import Debug.RecoverRTTI.TypeLevel  {-------------------------------------------------------------------------------   Existentials@@ -58,17 +55,6 @@ -- >     _ = keepRedundantConstraint (Proxy @ConstraintUsefulForDebugging)) keepRedundantConstraint :: c => proxy c -> () keepRedundantConstraint _ = ()--{--------------------------------------------------------------------------------  Traversable--------------------------------------------------------------------------------}---- | Check if a traversable data structure is empty------ Returns evidence: an element of the data-structure if it's non-empty,--- or evidence that it is empty otherwise.-checkEmptyTraversable :: Traversable t => t a -> Either a (t Void)-checkEmptyTraversable = traverse Left  {-------------------------------------------------------------------------------   Lists

@@ -1,166 +0,0 @@-{-# LANGUAGE DataKinds            #-}-{-# LANGUAGE FlexibleInstances    #-}-{-# LANGUAGE GADTs                #-}-{-# LANGUAGE PolyKinds            #-}-{-# LANGUAGE RankNTypes           #-}-{-# LANGUAGE ScopedTypeVariables  #-}-{-# LANGUAGE TypeFamilies         #-}-{-# LANGUAGE TypeOperators        #-}-{-# LANGUAGE UndecidableInstances #-}--module Debug.RecoverRTTI.Util.TypeLevel (-    -- * Singletons-    Sing(..)-  , SingI(..)-  , DecidableEquality(..)-    -- ** Natural numbers-  , Nat(..)-  , knownNat-  , Length-    -- * General purpose type level functions-  , Or-  , Equal-  , Elem-  , Assert-    -- * Type-level membership check-  , IsElem(..)-  , checkIsElem-    -- * Phantom type parameters-  , Phantom(..)-  , Poly(..)-  , maybePoly-  ) where--import Data.Kind-import Data.Proxy-import Data.Type.Equality-import GHC.TypeLits (ErrorMessage, Symbol, KnownSymbol, TypeError, sameSymbol)--{--------------------------------------------------------------------------------  Singletons--------------------------------------------------------------------------------}--data family Sing :: k -> Type--class SingI (a :: k) where-  sing :: Sing a--class DecidableEquality k where-  decideEquality :: Sing (a :: k) -> Sing (b :: k) -> Maybe (a :~: b)--{--------------------------------------------------------------------------------  For kind 'Type', Sing is just a proxy--------------------------------------------------------------------------------}--data instance Sing (a :: Type) where-  SProxy :: Sing (a :: Type)--instance SingI (a :: Type) where-  sing = SProxy--{--------------------------------------------------------------------------------  Natural numbers--  Unlike @ghc@'s, these are inductively defined.--------------------------------------------------------------------------------}--data Nat = Z | S Nat--data instance Sing (n :: Nat) where-  SZ :: Sing 'Z-  SS :: Sing n -> Sing ('S n)--instance            SingI 'Z     where sing = SZ-instance SingI n => SingI ('S n) where sing = SS sing--knownNat :: Sing (n :: Nat) -> Int-knownNat SZ     = 0-knownNat (SS n) = knownNat n + 1--type family Length (xs :: [k]) :: Nat where-  Length '[]       = 'Z-  Length (_ ': xs) = 'S (Length xs)--{--------------------------------------------------------------------------------  Singleton instance for type-level symbols--------------------------------------------------------------------------------}--data instance Sing (n :: Symbol) where-  SSymbol :: KnownSymbol n => Sing n--instance KnownSymbol n => SingI (n :: Symbol) where-  sing = SSymbol--instance DecidableEquality Symbol where-  decideEquality SSymbol SSymbol = sameSymbol Proxy Proxy--{--------------------------------------------------------------------------------  Singleton instance for lists--------------------------------------------------------------------------------}--data instance Sing (xs :: [k]) where-  SN :: Sing '[]-  SC :: Sing x -> Sing xs -> Sing (x ': xs)--instance                        SingI '[]       where sing = SN-instance (SingI x, SingI xs) => SingI (x ': xs) where sing = SC sing sing--{--------------------------------------------------------------------------------  General purpose type level functions--------------------------------------------------------------------------------}--type family Or (a :: Bool) (b :: Bool) where-  Or 'True b     = 'True-  Or a     'True = 'True-  Or _     _     = 'False--type family Equal (x :: k) (y :: k) where-  Equal x x = 'True-  Equal x y = 'False--type family Elem (x :: k) (xs :: [k]) where-  Elem x '[]       = 'False-  Elem x (y ': ys) = Or (Equal x y) (Elem x ys)---- | Assert type-level predicate------ We cannot define this in terms of a more general @If@ construct, because--- @ghc@'s type-level language has an undefined reduction order and so we get--- no short-circuiting.-type family Assert (b :: Bool) (err :: ErrorMessage) :: Constraint where-  Assert 'True  err = ()-  Assert 'False err = TypeError err--{--------------------------------------------------------------------------------  Decidable equality gives a decidable membership check--------------------------------------------------------------------------------}--data IsElem (x :: k) (xs :: [k]) where-  IsElem :: Elem x xs ~ 'True => IsElem x xs--shiftIsElem :: IsElem x ys -> IsElem x (y ': ys)-shiftIsElem IsElem = IsElem--checkIsElem ::-     DecidableEquality k-  => Sing (x :: k) -> Sing (xs :: [k]) -> Maybe (IsElem x xs)-checkIsElem _ SN         = Nothing-checkIsElem x (SC y ys) = case decideEquality x y of-                            Just Refl -> Just IsElem-                            Nothing   -> shiftIsElem <$> checkIsElem x ys--{--------------------------------------------------------------------------------  Phantom type parameters--------------------------------------------------------------------------------}---- | Functors with phantom arguments-class Phantom (f :: k -> Type) where-  -- | Similar to 'Data.Functor.Contravariant.phantom', but without requiring-  -- 'Functor' or 'Contravariant'-  phantom :: forall a b. f a -> f b--data Poly (f :: k -> Type) = Poly (forall (a :: k). f a)---- | Commute @Maybe@ and @forall@-maybePoly :: Phantom f => Maybe (f a) -> Maybe (Poly f)-maybePoly = fmap (\v -> Poly (phantom v))

@@ -52,8 +52,7 @@ import Test.QuickCheck hiding (classify, NonEmpty)  import Debug.RecoverRTTI-import Debug.RecoverRTTI.Util-import Debug.RecoverRTTI.Util.TypeLevel+import Debug.RecoverRTTI.TypeLevel  import Test.RecoverRTTI.ConcreteClassifier import Test.RecoverRTTI.Orphans ()

@@ -24,7 +24,6 @@ import Test.Tasty.QuickCheck hiding (classify, NonEmpty)  import Debug.RecoverRTTI-import Debug.RecoverRTTI.Util  import Test.RecoverRTTI.Arbitrary import Test.RecoverRTTI.ConcreteClassifier

@@ -40,8 +40,7 @@ import qualified Data.Text.Lazy        as Text.Lazy  import Debug.RecoverRTTI-import Debug.RecoverRTTI.Util-import Debug.RecoverRTTI.Util.TypeLevel+import Debug.RecoverRTTI.TypeLevel  import Test.RecoverRTTI.UserDefined @@ -209,7 +208,7 @@     -- User-defined     go (CC_User_NonRec   c) = 1 + goMaybeF c     go (CC_User_Rec      c) = 1 + goMaybeF c-    go (CC_User_Unlifted c) = 1 + goMaybeF c +    go (CC_User_Unlifted c) = 1 + goMaybeF c      goMaybeF :: MaybeF ConcreteClassifier a -> Int     goMaybeF FNothing  = 0

@@ -2,7 +2,7 @@  module Test.RecoverRTTI.Sanity (tests) where -import Debug.RecoverRTTI.Util+import Debug.RecoverRTTI  import Test.Tasty import Test.Tasty.QuickCheck

@@ -7,7 +7,6 @@ import Test.Tasty.QuickCheck hiding (classify)  import Debug.RecoverRTTI-import Debug.RecoverRTTI.Util  import Test.RecoverRTTI.Arbitrary () import Test.RecoverRTTI.ConcreteClassifier

@@ -49,8 +49,7 @@ import qualified Data.Set as Set  import Debug.RecoverRTTI-import Debug.RecoverRTTI.Util-import Debug.RecoverRTTI.Util.TypeLevel+import Debug.RecoverRTTI.TypeLevel  import Test.RecoverRTTI.ConcreteClassifier import Test.RecoverRTTI.UserDefined@@ -338,3 +337,21 @@     go :: [Except e (Maybe a)] -> Except e a     go []     = throwError err     go (x:xs) = x >>= maybe (go xs) return++bimapTuple ::+      ( SListI xs+      , SListI ys+      , IsValidSize (Length (x ': xs))+      , Length xs ~ Length ys+      )+   => (x -> y)+   -> (WrappedTuple xs -> WrappedTuple ys)+   -> WrappedTuple (x ': xs) -> WrappedTuple (y ': ys)+bimapTuple f g (TCons x xs) = TCons (f x) (g xs)++-- | Check if a traversable data structure is empty+--+-- Returns evidence: an element of the data-structure if it's non-empty,+-- or evidence that it is empty otherwise.+checkEmptyTraversable :: Traversable t => t a -> Either a (t Void)+checkEmptyTraversable = traverse Left