recover-rtti 0.2.1.0 → 0.3.0.0

raw patch · 20 files changed

+299/−697 lines, 20 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• recover-rtti.cabal +3/−4
• src/Debug/RecoverRTTI.hs +6/−19
• src/Debug/RecoverRTTI/Classifier.hs +2/−4
• src/Debug/RecoverRTTI/Classify.hs +14/−34
• src/Debug/RecoverRTTI/Constr.hs +0/−190
• src/Debug/RecoverRTTI/Modules.hs +31/−29
• src/Debug/RecoverRTTI/Nat.hs +53/−0
• src/Debug/RecoverRTTI/Tuple.hs +1/−1
• src/Debug/RecoverRTTI/Tuple/Recursive.hs +1/−1
• src/Debug/RecoverRTTI/Tuple/Size.hs +67/−67
• src/Debug/RecoverRTTI/TypeLevel.hs +0/−167
• src/Debug/RecoverRTTI/UserDefined.hs +0/−71
• src/Debug/RecoverRTTI/Util.hs +3/−3
• src/Debug/RecoverRTTI/Wrappers.hs +14/−1
• tests/Test/RecoverRTTI/Arbitrary.hs +11/−5
• tests/Test/RecoverRTTI/Classify.hs +4/−1
• tests/Test/RecoverRTTI/ConcreteClassifier.hs +7/−4
• tests/Test/RecoverRTTI/Staged.hs +35/−71
• tests/Test/RecoverRTTI/UserDefined.hs +42/−25

@@ -1,5 +1,10 @@ # Revision history for recover-rtti +## 0.3.0.0 -- 2021-03-17++* Fix bug that could cause `anythingToString` to fail on lists with an+  `elemUserDefined` exception (issue #6). Thanks to Bit Connor for the report!+ ## 0.2.1.0 -- 2021-03-17  * Add support for unordered-containers and boxed vectors.

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               recover-rtti-version:            0.2.1.0+version:            0.3.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,18 +24,17 @@  library     exposed-modules:  Debug.RecoverRTTI-                      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.Nat                       Debug.RecoverRTTI.Tuple                       Debug.RecoverRTTI.Tuple.Recursive                       Debug.RecoverRTTI.Tuple.Size-                      Debug.RecoverRTTI.UserDefined                       Debug.RecoverRTTI.Util                       Debug.RecoverRTTI.Wrappers 

@@ -21,25 +21,8 @@     -- * User-defined types   , UserDefined -- opaque     -- ** Classify constructor arguments-  , KnownConstr   , fromUserDefined   , Some(..)-    -- ** Constructor information-  , Constr(..)-    -- ** Type-level constructor information-  , ConstrPkg-  , ConstrModl-  , ConstrName-  , prettyKnownConstr-    -- ** Casting-  , unsafeCoerceUserDefined-  , ConstrOf-  , Constrs-  , GConstrs-  , GConstrsOfType-    -- ** Constructor check-  , checkIsConstrOf-  , IsConstrOf(..)     -- * Inductive tuples   , WrappedTuple(..)   , Tuple@@ -53,12 +36,16 @@   , smallerIsValid   , toValidSize   , liftValidSize+    -- * Type-level naturals+  , Nat(..)+  , SNat(..)+  , KnownNat(..)+  , Length   ) where  import Debug.RecoverRTTI.Classifier import Debug.RecoverRTTI.Classify-import Debug.RecoverRTTI.Constr+import Debug.RecoverRTTI.Nat import Debug.RecoverRTTI.Tuple-import Debug.RecoverRTTI.UserDefined import Debug.RecoverRTTI.Util import Debug.RecoverRTTI.Wrappers

@@ -37,10 +37,8 @@ import qualified Data.Text.Lazy              as Text.Lazy import qualified Data.Vector                 as Vector.Boxed -import Debug.RecoverRTTI.Constr+import Debug.RecoverRTTI.Nat import Debug.RecoverRTTI.Tuple-import Debug.RecoverRTTI.TypeLevel-import Debug.RecoverRTTI.UserDefined import Debug.RecoverRTTI.Wrappers  {-------------------------------------------------------------------------------@@ -136,7 +134,7 @@    -- User-defined -  C_Custom :: Sing c -> Classifier (UserDefined c)+  C_Custom :: Classifier UserDefined  newtype Classifiers xs = Classifiers (NP Classified xs) 

@@ -5,6 +5,7 @@ {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE TupleSections         #-} {-# LANGUAGE TypeApplications      #-} {-# LANGUAGE TypeOperators         #-} {-# LANGUAGE UndecidableInstances  #-}@@ -33,7 +34,6 @@ import Data.Tree (Tree) import GHC.Exts.Heap (Closure) import GHC.Real-import GHC.Stack import System.IO.Unsafe (unsafePerformIO) import Unsafe.Coerce (unsafeCoerce) @@ -48,13 +48,12 @@ import qualified Data.Vector                 as Vector.Boxed  import Debug.RecoverRTTI.Classifier-import Debug.RecoverRTTI.Constr import Debug.RecoverRTTI.FlatClosure import Debug.RecoverRTTI.Modules+import Debug.RecoverRTTI.Nat import Debug.RecoverRTTI.Tuple-import Debug.RecoverRTTI.TypeLevel-import Debug.RecoverRTTI.UserDefined import Debug.RecoverRTTI.Util+import Debug.RecoverRTTI.Wrappers  {-------------------------------------------------------------------------------   Classification@@ -244,9 +243,8 @@       -- User defined       -- -      ConstrClosure {pkg, modl, name} ->-        elimKnownConstr (Constr pkg modl name) $ \p ->-        return $ mustBe (C_Custom p)+      ConstrClosure {} ->+        return $ mustBe C_Custom        --       -- Classification failed@@ -435,34 +433,16 @@  -- | Classify the arguments to the constructor ----- We only look at pointers and ignore any @UNPACK@ed data. Arguments we cannot--- classify (like unlifted arguments) will be ignored.-fromUserDefined :: forall c.-     (HasCallStack, KnownConstr c)-  => UserDefined c -> [Some Classified]+-- Additionally returns the constructor name itself.+fromUserDefined :: UserDefined -> (String, [Some Classified]) fromUserDefined = \(UserDefined x) -> unsafePerformIO $ go x   where-    go :: x -> IO [Some Classified]+    go :: x -> IO (String, [Some Classified])     go x = do         closure <- getBoxedClosureData (asBox x)         case closure of-          ConstrClosure {pkg, modl, name, ptrArgs} -> do-            let expected, actual :: Constr String-                expected = knownConstr (sing @_ @c)-                actual   = Constr pkg modl name-            if expected == actual then do-              goArgs [] ptrArgs-            else do---              tree <- showClosureTree 5 x-              error $ unlines [-                  "elimUserDefined: unexpected constructor"-                , "  closure:  " ++ show closure-                , "  expected: " ++ show expected-                , "  actual:   " ++ show actual---                , "** TREE **"---                , tree---                , "** END OF TREE **"-                ]+          ConstrClosure {name, ptrArgs} ->+            (name,) <$> goArgs [] ptrArgs           _otherwise ->             error $ "elimUserDefined: unexpected closure: "                  ++ show closure@@ -579,7 +559,7 @@     go C_Fun = Dict      -- User-defined-    go (C_Custom SConstr) = Dict+    go C_Custom = Dict      --     -- Compound@@ -634,9 +614,9 @@                                          ) of                                       (Dict, Dict) -> Dict -instance KnownConstr c => Show (UserDefined c) where+instance Show UserDefined where   showsPrec p x =-      case fromUserDefined x of+      case args of         [] -> showString constrName         xs -> showParen (p >= 11)             . (showString constrName .)@@ -644,4 +624,4 @@             . map (\(Some x') -> showString " " . showClassifiedValue 11 x')             $ xs     where-      Constr{constrName} = knownConstr (sing @_ @c)+      (constrName, args) = fromUserDefined x

@@ -1,190 +0,0 @@-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE GADTs                 #-}-{-# LANGUAGE InstanceSigs          #-}-{-# LANGUAGE KindSignatures        #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE NamedFieldPuns        #-}-{-# LANGUAGE PolyKinds             #-}-{-# LANGUAGE RankNTypes            #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeApplications      #-}-{-# LANGUAGE TypeFamilies          #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE UndecidableInstances  #-}--{-# OPTIONS_GHC -Wno-redundant-constraints #-}---- | Type-level metadata-module Debug.RecoverRTTI.Constr (-    Constr(..)-  , KnownConstr-  , knownConstr-  , prettyKnownConstr-  , elimKnownConstr-    -- | Type-level extracts-  , ConstrPkg-  , ConstrModl-  , ConstrName-    -- | Compute all known constructors-  , Constrs-  , GConstrs-  , GConstrsOfType-  , ConstrOf-  , IsConstrOf(..)-  , checkIsConstrOf-  , Sing(..)-  ) where--import Data.Kind-import Data.List (intercalate)-import Data.SOP-import Data.Type.Equality-import GHC.Generics-import GHC.TypeLits--import Debug.RecoverRTTI.TypeLevel-import Debug.RecoverRTTI.Util--{--------------------------------------------------------------------------------  Type-level metadata--------------------------------------------------------------------------------}---- | Information about a constructor-data Constr a = Constr {-      constrPkg  :: a  -- ^ Package-    , constrModl :: a  -- ^ Module-    , constrName :: a  -- ^ Constructor name-    }-  deriving (Show, Eq)--type family ConstrPkg  (c :: Constr a) :: a where ConstrPkg  ('Constr p _ _) = p-type family ConstrModl (c :: Constr a) :: a where ConstrModl ('Constr _ m _) = m-type family ConstrName (c :: Constr a) :: a where ConstrName ('Constr _ _ c) = c--class (-      KnownSymbol (ConstrPkg  c)-    , KnownSymbol (ConstrModl c)-    , KnownSymbol (ConstrName c)-    , c ~ 'Constr (ConstrPkg c) (ConstrModl c) (ConstrName c)-    ) => KnownConstr c-instance (-      KnownSymbol (ConstrPkg  c)-    , KnownSymbol (ConstrModl c)-    , KnownSymbol (ConstrName c)-    , c ~ 'Constr (ConstrPkg c) (ConstrModl c) (ConstrName c)-    ) => KnownConstr c--knownConstr ::-     forall c. Sing (c :: Constr Symbol) -> Constr String-knownConstr SConstr = Constr {-      constrPkg  = symbolVal (Proxy @(ConstrPkg  c))-    , constrModl = symbolVal (Proxy @(ConstrModl c))-    , constrName = symbolVal (Proxy @(ConstrName c))-    }--prettyKnownConstr :: Sing (c :: Constr Symbol) -> String-prettyKnownConstr s = intercalate "." [constrPkg, constrModl, constrName]-  where-    Constr{constrPkg, constrModl, constrName} = knownConstr s--elimKnownConstr :: forall r.-     Constr String-  -> (forall c. Sing (c :: Constr Symbol) -> r)-  -> r-elimKnownConstr Constr{constrPkg, constrModl, constrName} k =-    elimKnownSymbol constrPkg  $ \pPkg  ->-    elimKnownSymbol constrModl $ \pModl ->-    elimKnownSymbol constrName $ \pName ->-      go pPkg pModl pName-  where-    go :: forall pkg modl constr. (-              KnownSymbol pkg-            , KnownSymbol modl-            , KnownSymbol constr-            )-       => Proxy pkg -> Proxy modl -> Proxy constr -> r-    go _ _ _ = k (sing :: Sing ('Constr pkg modl constr))--{--------------------------------------------------------------------------------  Singleton--------------------------------------------------------------------------------}--data instance Sing (c :: Constr Symbol) where-  SConstr :: KnownConstr c => Sing c--instance KnownConstr c => SingI (c :: Constr Symbol) where-  sing = SConstr--instance Show (Sing (c :: Constr Symbol)) where-  showsPrec p proxy = showParen (p >= 11) $-        showString "SConstr "-      . showsPrec 11 (knownConstr proxy)--instance DecidableEquality (Constr Symbol) where-  decideEquality :: forall c c'.-       Sing (c  :: Constr Symbol)-    -> Sing (c' :: Constr Symbol)-    -> Maybe (c :~: c')-  decideEquality SConstr SConstr =-    case ( decideEquality (sing :: Sing (ConstrPkg  c)) (sing :: Sing (ConstrPkg  c'))-         , decideEquality (sing :: Sing (ConstrModl c)) (sing :: Sing (ConstrModl c'))-         , decideEquality (sing :: Sing (ConstrName c)) (sing :: Sing (ConstrName c'))-         ) of-      (Just Refl, Just Refl, Just Refl) ->-        Just Refl-      _otherwise ->-        Nothing--{--------------------------------------------------------------------------------  Reverse direction: from type to the known constructors--------------------------------------------------------------------------------}---- | Compute all constructors of the given type-type family Constrs (a :: Type) :: [Constr Symbol] where-  Constrs a = GConstrs (Rep a)--type family GConstrs f :: [Constr Symbol] where-  GConstrs (M1 D ('MetaData typ modl pkg isNewtype) f) =-    GConstrsOfType pkg modl f '[]--type family GConstrsOfType pkg modl f acc :: [Constr Symbol] where-  GConstrsOfType pkg modl (f :+: g) acc =-    GConstrsOfType pkg modl g (GConstrsOfType pkg modl f acc)-  GConstrsOfType pkg modl (M1 C ('MetaCons constr fixity isRecord) f) acc =-    'Constr pkg modl constr ': acc---- | Require that specified type has the given constructor------ Intended usage:------ > castUserDefined :: forall c a. ConstrOf a c => UserDefined c -> a--- > castUserDefined = unsafeCoerce-type family ConstrOf (a :: Type) (c :: Constr Symbol) :: Constraint where-  ConstrOf a c =-      Assert-        (Elem c (Constrs a))-        (TypeError (-                  (       'ShowType c-                    ':<>: 'Text " is not a valid constructor of "-                    ':<>: 'ShowType a-                  )-            ':$$: (       'Text "Valid constructors are: "-                    ':<>: 'ShowType (Constrs a)-                  )-          ))---- | 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)-checkIsConstrOf s =-    aux <$> checkIsElem s (sing @_ @(Constrs a))-  where-    aux :: IsElem c (Constrs a) -> IsConstrOf a c-    aux IsElem = IsConstrOf

@@ -8,7 +8,7 @@ module Debug.RecoverRTTI.Modules (     KnownPkg(..)   , KnownModule(..)-  , Sing(..)+  , IsKnownPkg(..)     -- * Matching   , inKnownModule   , inKnownModuleNested@@ -18,7 +18,6 @@ import Data.List (isPrefixOf)  import Debug.RecoverRTTI.FlatClosure-import Debug.RecoverRTTI.TypeLevel  {-------------------------------------------------------------------------------   Packages@@ -42,29 +41,32 @@   Singleton instance for KnownPkg -------------------------------------------------------------------------------} -data instance Sing (pkg :: KnownPkg) where-  SGhcPrim             :: Sing 'PkgGhcPrim-  SBase                :: Sing 'PkgBase-  SByteString          :: Sing 'PkgByteString-  SText                :: Sing 'PkgText-  SIntegerWiredIn      :: Sing 'PkgIntegerWiredIn-  SGhcBignum           :: Sing 'PkgGhcBignum-  SContainers          :: Sing 'PkgContainers-  SAeson               :: Sing 'PkgAeson-  SUnorderedContainers :: Sing 'PkgUnorderedContainers-  SVector              :: Sing 'PkgVector+data SPkg (pkg :: KnownPkg) where+  SGhcPrim             :: SPkg 'PkgGhcPrim+  SBase                :: SPkg 'PkgBase+  SByteString          :: SPkg 'PkgByteString+  SText                :: SPkg 'PkgText+  SIntegerWiredIn      :: SPkg 'PkgIntegerWiredIn+  SGhcBignum           :: SPkg 'PkgGhcBignum+  SContainers          :: SPkg 'PkgContainers+  SAeson               :: SPkg 'PkgAeson+  SUnorderedContainers :: SPkg 'PkgUnorderedContainers+  SVector              :: SPkg 'PkgVector -instance SingI 'PkgGhcPrim             where sing = SGhcPrim-instance SingI 'PkgBase                where sing = SBase-instance SingI 'PkgByteString          where sing = SByteString-instance SingI 'PkgText                where sing = SText-instance SingI 'PkgIntegerWiredIn      where sing = SIntegerWiredIn-instance SingI 'PkgGhcBignum           where sing = SGhcBignum-instance SingI 'PkgContainers          where sing = SContainers-instance SingI 'PkgAeson               where sing = SAeson-instance SingI 'PkgUnorderedContainers where sing = SUnorderedContainers-instance SingI 'PkgVector              where sing = SVector+class IsKnownPkg pkg where+  singPkg :: SPkg pkg +instance IsKnownPkg 'PkgGhcPrim             where singPkg = SGhcPrim+instance IsKnownPkg 'PkgBase                where singPkg = SBase+instance IsKnownPkg 'PkgByteString          where singPkg = SByteString+instance IsKnownPkg 'PkgText                where singPkg = SText+instance IsKnownPkg 'PkgIntegerWiredIn      where singPkg = SIntegerWiredIn+instance IsKnownPkg 'PkgGhcBignum           where singPkg = SGhcBignum+instance IsKnownPkg 'PkgContainers          where singPkg = SContainers+instance IsKnownPkg 'PkgAeson               where singPkg = SAeson+instance IsKnownPkg 'PkgUnorderedContainers where singPkg = SUnorderedContainers+instance IsKnownPkg 'PkgVector              where singPkg = SVector+ {-------------------------------------------------------------------------------   Modules in @ghc-pri@ -------------------------------------------------------------------------------}@@ -157,25 +159,25 @@ -------------------------------------------------------------------------------}  -- | Check if the given closure is from a known package/module-inKnownModule :: SingI pkg+inKnownModule :: IsKnownPkg pkg   => KnownModule pkg   -> FlatClosure -> Maybe String inKnownModule modl = fmap fst . inKnownModuleNested modl  -- | Generalization of 'inKnownModule' that additionally returns nested pointers-inKnownModuleNested :: SingI pkg+inKnownModuleNested :: IsKnownPkg pkg   => KnownModule pkg   -> FlatClosure -> Maybe (String, [Box])-inKnownModuleNested = go sing+inKnownModuleNested = go singPkg   where-    go :: Sing pkg -> KnownModule pkg -> FlatClosure -> Maybe (String, [Box])+    go :: SPkg pkg -> KnownModule pkg -> FlatClosure -> Maybe (String, [Box])     go knownPkg knownModl ConstrClosure{pkg, modl, name, ptrArgs} = do         guard (namePkg knownPkg `isPrefixOf` pkg) -- ignore the version number         guard (modl == nameModl knownPkg knownModl)         return (name, ptrArgs)     go _ _ _otherClosure = Nothing -    namePkg :: Sing (pkg :: KnownPkg) -> String+    namePkg :: SPkg pkg -> String     namePkg SGhcPrim             = "ghc-prim"     namePkg SBase                = "base"     namePkg SByteString          = "bytestring"@@ -187,7 +189,7 @@     namePkg SUnorderedContainers = "unordered-containers"     namePkg SVector              = "vector" -    nameModl :: Sing (pkg :: KnownPkg) -> KnownModule pkg -> String+    nameModl :: SPkg pkg -> KnownModule pkg -> String     nameModl SGhcPrim             GhcTypes                    = "GHC.Types"     nameModl SGhcPrim             GhcTuple                    = "GHC.Tuple"     nameModl SBase                GhcInt                      = "GHC.Int"

@@ -0,0 +1,53 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}++-- | Inductive type-level natural numbers+module Debug.RecoverRTTI.Nat (+    -- * Type-level natural numbers+    Nat(..)+  , SNat(..)+  , KnownNat(..)+  , natVal+    -- * Type level functions computing natural numbers+  , Length+  ) where++{-------------------------------------------------------------------------------+  Natural numbers+-------------------------------------------------------------------------------}++-- | Natural numbers+--+-- Intended to be used lifted to the type level; unlike @ghc@'s type level+-- natural numbers, these are inductive.+data Nat = Z | S Nat++-- | Singleton for 'Nat'+data SNat (n :: Nat) where+  SZ :: SNat 'Z+  SS :: SNat n -> SNat ('S n)++class KnownNat (n :: Nat) where+  singNat :: SNat n++instance               KnownNat 'Z     where singNat = SZ+instance KnownNat n => KnownNat ('S n) where singNat = SS singNat++natVal :: forall n proxy. KnownNat n => proxy n -> Int+natVal _ = go (singNat :: SNat n)+  where+    go :: forall m. SNat m -> Int+    go SZ     = 0+    go (SS n) = go n + 1++{-------------------------------------------------------------------------------+  Type-level functions computing natural numbers+-------------------------------------------------------------------------------}++type family Length (xs :: [k]) :: Nat where+  Length '[]       = 'Z+  Length (_ ': xs) = 'S (Length xs)

@@ -21,9 +21,9 @@  import Data.SOP hiding (NS(..)) +import Debug.RecoverRTTI.Nat import Debug.RecoverRTTI.Tuple.Recursive import Debug.RecoverRTTI.Tuple.Size-import Debug.RecoverRTTI.TypeLevel  {-------------------------------------------------------------------------------   Wrapped tuple

@@ -26,8 +26,8 @@  import Data.SOP +import Debug.RecoverRTTI.Nat import Debug.RecoverRTTI.Tuple.Size-import Debug.RecoverRTTI.TypeLevel  {-------------------------------------------------------------------------------   Generated

@@ -24,7 +24,7 @@ import Data.Proxy import Data.SOP.Dict -import Debug.RecoverRTTI.TypeLevel+import Debug.RecoverRTTI.Nat import Debug.RecoverRTTI.Util  {-------------------------------------------------------------------------------@@ -32,7 +32,7 @@ -------------------------------------------------------------------------------}  data ValidSize (n :: Nat) where-  ValidSize :: Sing n -> (forall r. TooBig n -> r) -> ValidSize n+  ValidSize :: SNat n -> (forall r. TooBig n -> r) -> ValidSize n  smallerIsValid' :: forall n. ValidSize ('S n) -> ValidSize n smallerIsValid' = \(ValidSize (SS n) tooBig) -> ValidSize n $ aux tooBig@@ -62,7 +62,7 @@ -- 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+class KnownNat n => IsValidSize n where   isValidSize :: ValidSize n  {-------------------------------------------------------------------------------@@ -77,7 +77,7 @@ liftValidSize :: forall n. ValidSize n -> Dict IsValidSize n liftValidSize (ValidSize n notTooBig) = go n   where-    go :: Sing n -> Dict IsValidSize n+    go :: SNat n -> Dict IsValidSize n     go SZ =         Dict     go (SS SZ) =@@ -208,193 +208,193 @@         notTooBig (TooBig :: TooBig n)  instance IsValidSize 'Z where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S 'Z) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S 'Z)) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S 'Z))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S 'Z)))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S 'Z))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S 'Z)))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S 'Z))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('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+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('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+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('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+  isValidSize = ValidSize singNat $ \case  instance IsValidSize ('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+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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 'Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) where-  isValidSize = ValidSize sing $ \case+  isValidSize = ValidSize singNat $ \case  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+  isValidSize = ValidSize singNat $ \case  -- | Check the given size is a valid tuple size toValidSize :: Int -> Maybe (Some ValidSize)

@@ -1,167 +0,0 @@-{-# 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))

@@ -1,71 +0,0 @@-{-# LANGUAGE DataKinds           #-}-{-# LANGUAGE KindSignatures      #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications    #-}---- | User-defined types------ For user-defined types, we have no way of actually inferring the /type/ at--- runtime. Instead, we merely reflect (at the type level) which /constructor/--- was used to construct the value. This gives the library sufficient context--- to /show/ values, and it gives client code that /is/ aware of these custom--- types sufficient context to recover the full type information, if desired.--- See "Test.RecoverRTTI.Staged" for an example of the latter.-module Debug.RecoverRTTI.UserDefined (-    -- | Type inferred for user-defined types-    UserDefined(..)-  , unsafeCoerceUserDefined-  ) where--import Data.Proxy-import GHC.TypeLits-import GHC.Exts-import Unsafe.Coerce (unsafeCoerce)--import Debug.RecoverRTTI.Constr-import Debug.RecoverRTTI.Util--{--------------------------------------------------------------------------------  User-defined types--------------------------------------------------------------------------------}---- | User-defined type------ For user-defined types we recover, at the type level, information about the--- constructor. In /principle/ of course this means that this tells us what--- the type of this thing is; if------ > data MyType .. = MyConstr .. | ...------ then @coerce :: UserDefined "MyConstr" -> MyType@ should be safe.------ We defer classification of the /arguments/ to the constructor. This is--- necessary, because if we tried to do this eagerly---recording those types as--- part of the 'UserDefined' type---we might end up "unwinding" recursive types--- at the type level; for example, something like------ > data MyList = MyNil | MyCons a (MyList a)------ could then result in something like------ > UserDefined "MyCons" '[ Int, UserDefined "MyCons" '[ Int , ... ] .. ]------ Detecting recursion is undecidable (that's why Haskell uses isorecursive--- rather than equirecursive types), so instead we defer.-newtype UserDefined (c :: Constr Symbol) = UserDefined Any---- | Safer wrapper around 'unsafeCoerce'------ This is safer than 'unsafeCoerce', because we require (at the type level)--- that the value was constructed with a constructor of the target type. This--- means that 'unsafeCoerceUserDefined' is in fact /safe/ for types without--- type parameters; however, for a type such as------ > data MyType a = MkMyType a------ 'unsafeCoerceUserDefined' can still be used to cast, say, @MyType Int@ to--- @MyType Bool@, and so this is still unsafe.-unsafeCoerceUserDefined :: forall a c. ConstrOf a c => UserDefined c -> a-unsafeCoerceUserDefined = unsafeCoerce-  where-    _ = keepRedundantConstraint (Proxy @(ConstrOf a c))

@@ -28,7 +28,7 @@ import Data.SOP import GHC.TypeLits (KnownSymbol, SomeSymbol(..), someSymbolVal) -import Debug.RecoverRTTI.TypeLevel+import Debug.RecoverRTTI.Nat  {-------------------------------------------------------------------------------   Existentials@@ -86,10 +86,10 @@          (SListI xs, Length xs ~ n)       => NP (K a) xs -> VerifiedSize n a -verifySize :: Sing n -> [a] -> Maybe (VerifiedSize n a)+verifySize :: SNat n -> [a] -> Maybe (VerifiedSize n a) verifySize = go   where-    go :: Sing n -> [a] -> Maybe (VerifiedSize n a)+    go :: SNat n -> [a] -> Maybe (VerifiedSize n a)     go SZ     []     = Just (VerifiedSize Nil)     go (SS n) (x:xs) = do VerifiedSize np <- go n xs                           return $ VerifiedSize (K x :* np)

@@ -12,8 +12,10 @@ -- nonetheless stil useful, as it means that we can show /everything/, which is -- kind of the point. module Debug.RecoverRTTI.Wrappers (+    -- * User-defined types+    UserDefined(..)     -- * Functions-    SomeFun(..)+  , SomeFun(..)     -- * Reference cells   , SomeSTRef(..)   , SomeMVar(..)@@ -24,6 +26,17 @@ import Control.Concurrent.STM (TVar) import Data.STRef (STRef) import GHC.Exts++{-------------------------------------------------------------------------------+  User-defined types+-------------------------------------------------------------------------------}++-- | User-defined type+--+-- We defer classification of the arguments to the constructor (the type might+-- be recursive, so if we tried to classify all arguments, we might end up+-- unrolling the recursion at the type level).+newtype UserDefined = UserDefined Any  {-------------------------------------------------------------------------------   Functions

@@ -56,7 +56,6 @@ import Test.QuickCheck hiding (classify, NonEmpty)  import Debug.RecoverRTTI-import Debug.RecoverRTTI.TypeLevel  import Test.RecoverRTTI.ConcreteClassifier import Test.RecoverRTTI.Orphans ()@@ -333,6 +332,10 @@           -- User-defined           -- +          -- SimpleType+        , return $ return $ Some (defaultClassifiedGen CC_User_Simple)++          -- NonRecursive         , guard (typSz >= 1) >> (return $ do               Some a <- arbitraryClassifiedGen (typSz - 1)               genMaybeF@@ -344,6 +347,7 @@                 a             ) +          -- Recursive         , guard (typSz >= 1) >> (return $ do               Some a <- arbitraryClassifiedGen (typSz - 1)               genMaybeF@@ -353,11 +357,13 @@                 a             ) -        , return $ do-            return $ Some $ ClassifiedGen (CC_User_Unlifted (FJust CC_Unit)) $ SizedGen $ \_ ->-              return exampleContainsUnlifted+          -- ContainsUnlifted+        , return $ return $ Some (defaultClassifiedGen CC_User_Unlifted) +          --           -- Tuples+          --+         , guard (typSz >= 2) >> (return $               arbitraryTuple typSz $ \np ->               case ( all_NP (hmap canShowClassifiedGen np)@@ -465,7 +471,7 @@              of Dict -> k np   where     go :: Int-       -> Sing (n :: Nat)+       -> SNat n        -> (forall xs.                 (SListI xs, Length xs ~ n)              => NP ClassifiedGen xs -> Gen r

@@ -151,11 +151,13 @@        -- User defined +    , compareClassifier $ Value  CC_User_Simple                    SimpleA+    , compareClassifier $ Value  CC_User_Simple                    SimpleB     , compareClassifier $ Value (CC_User_NonRec    FNothing)       (NR1 1234)     , compareClassifier $ Value (CC_User_NonRec   (FJust CC_Char)) (NR2 'a' True)     , compareClassifier $ Value (CC_User_Rec       FNothing)        RNil     , compareClassifier $ Value (CC_User_Rec      (FJust CC_Char)) (RCons 'a' RNil)-    , compareClassifier $ Value (CC_User_Unlifted (FJust CC_Unit)) exampleContainsUnlifted+    , compareClassifier $ Value  CC_User_Unlifted                  exampleContainsUnlifted     ]   where     _checkAllCases :: ConcreteClassifier a -> ()@@ -223,6 +225,7 @@          -- User-defined +        CC_User_Simple{}   -> ()         CC_User_NonRec{}   -> ()         CC_User_Rec{}      -> ()         CC_User_Unlifted{} -> ()

@@ -44,7 +44,6 @@ import qualified Data.Vector                 as Vector.Boxed  import Debug.RecoverRTTI-import Debug.RecoverRTTI.TypeLevel  import Test.RecoverRTTI.UserDefined @@ -129,9 +128,10 @@      -- User-defined +    CC_User_Simple   :: ConcreteClassifier SimpleType     CC_User_NonRec   :: MaybeF ConcreteClassifier a -> ConcreteClassifier (NonRecursive a)     CC_User_Rec      :: MaybeF ConcreteClassifier a -> ConcreteClassifier (Recursive    a)-    CC_User_Unlifted :: MaybeF ConcreteClassifier a -> ConcreteClassifier (ContainsUnlifted a)+    CC_User_Unlifted :: ConcreteClassifier ContainsUnlifted  newtype ConcreteClassifiers xs = ConcreteClassifiers (NP ConcreteClassifier xs) @@ -218,9 +218,10 @@     go CC_MVar  = 1      -- User-defined+    go  CC_User_Simple      = 1     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    = 1      goMaybeF :: MaybeF ConcreteClassifier a -> Int     goMaybeF FNothing  = 0@@ -328,9 +329,10 @@      -- User-defined +    go  CC_User_Simple       CC_User_Simple       = Just Refl     go (CC_User_NonRec   c) (CC_User_NonRec   c') = goMaybeF c c'     go (CC_User_Rec      c) (CC_User_Rec      c') = goMaybeF c c'-    go (CC_User_Unlifted c) (CC_User_Unlifted c') = goMaybeF c c'+    go  CC_User_Unlifted     CC_User_Unlifted     = Just Refl      -- Otherwise, not equal @@ -442,6 +444,7 @@          -- User-defined +        CC_User_Simple{}   -> ()         CC_User_NonRec{}   -> ()         CC_User_Rec{}      -> ()         CC_User_Unlifted{} -> ()

@@ -3,6 +3,7 @@ {-# LANGUAGE FlexibleInstances   #-} {-# LANGUAGE GADTs               #-} {-# LANGUAGE KindSignatures      #-}+{-# LANGUAGE PolyKinds           #-} {-# LANGUAGE RankNTypes          #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications    #-}@@ -37,15 +38,11 @@ import Data.Bifunctor import Data.HashMap.Lazy (HashMap) import Data.HashSet (HashSet)-import Data.Kind import Data.Map (Map) import Data.Set (Set) import Data.SOP hiding (NS(..))-import Data.Typeable import Data.Void-import GHC.Exts (Any) import GHC.Real-import GHC.TypeLits import Unsafe.Coerce (unsafeCoerce)  import qualified Data.HashMap.Internal.Array as HashMap (Array)@@ -54,7 +51,6 @@ import qualified Data.Set                    as Set  import Debug.RecoverRTTI-import Debug.RecoverRTTI.TypeLevel  import Test.RecoverRTTI.ConcreteClassifier import Test.RecoverRTTI.UserDefined@@ -161,11 +157,13 @@        -- User-defined -      C_Custom s ->-        firstMatch ("Unknown constructor: " ++ prettyKnownConstr s) [-            reclassifyF CC_User_NonRec   s x-          , reclassifyF CC_User_Rec      s x-          , reclassifyF CC_User_Unlifted s x+      C_Custom -> do+        let (constr, _args) = fromUserDefined x+        firstMatch ("Unknown constructor: " ++ constr) [+            reclassifySimple      CC_User_Simple    constr+          , reclassifyTraversable CC_User_NonRec   (constr, x)+          , reclassifyTraversable CC_User_Rec      (constr, x)+          , reclassifySimple      CC_User_Unlifted  constr           ]      goMaybeF :: forall f a.@@ -282,71 +280,37 @@   of @T x@ for /some/ @x@, and then as a second step figure out what @x@ is. -------------------------------------------------------------------------------} -data ConstrOfF f c a = ConstrOfF (IsConstrOf (f a) c)--unsafeCoerceF :: Poly (ConstrOfF f c) -> UserDefined c -> f a-unsafeCoerceF (Poly (ConstrOfF isConstrOf)) = aux isConstrOf-  where-    aux :: forall a c. IsConstrOf a c -> UserDefined c -> a-    aux IsConstrOf = unsafeCoerceUserDefined--checkConstrOfF ::-     forall f c. (-         Phantom (ConstrOfF f c)-       , SingI (Constrs (f Any))-       )-  => Sing c -> Maybe (Poly (ConstrOfF f c))-checkConstrOfF c = maybePoly (ConstrOfF <$> checkIsConstrOf @(f Any) c)+-- | Reclassification of user-defined types with no arguments+reclassifySimple ::+     forall a. ConstrsOf a+  => ConcreteClassifier a+  -> String+  -> Except String (Maybe (Reclassified UserDefined))+reclassifySimple cc constr =+    if constr `notElem` constrsOf (Proxy @a)+      then return Nothing+      else return . Just $ Reclassified cc unsafeCoerce -reclassifyF ::-     forall (f :: Type -> Type) (c :: Constr Symbol). (-         Phantom (ConstrOfF f c)-       , SingI (Constrs (f Any))-       , Traversable f-       , Typeable f-       )+-- | Reclassification of user-defined types with a single argument+reclassifyTraversable ::+     forall f. (Traversable f, ConstrsOf f)   => (forall a. MaybeF ConcreteClassifier a -> ConcreteClassifier (f a))-  -> Sing (c :: Constr Symbol)-  -> UserDefined c-  -> Except String (Maybe (Reclassified (UserDefined c)))-reclassifyF cc = \c x ->-    case checkConstrOfF @f c of-      Nothing ->-        return Nothing-      Just constrOfF ->-        case checkEmptyTraversable (unsafeCoerceF constrOfF x) of-          Right _ ->-            return . Just $ Reclassified (cc FNothing) (unsafeCoerceF constrOfF)-          Left x' -> do-            Just . aux constrOfF <$> classifyThenReclassify x'+  -> (String, UserDefined)+  -> Except String (Maybe (Reclassified UserDefined))+reclassifyTraversable cc = \(constr, x) ->+    if constr `notElem` constrsOf (Proxy @f)+      then return Nothing+      else case checkEmptyTraversable (coerceToF x) of+             Right _ -> return . Just $ Reclassified (cc FNothing) coerceToF+             Left x' -> Just . aux <$> classifyThenReclassify x'   where-    aux :: Poly (ConstrOfF f c)-        -> Reclassified a               -- Classification of the elements-        -> Reclassified (UserDefined c) -- Classification of the container-    aux constrOfF (Reclassified c f) =-        Reclassified (cc (FJust c)) (fmap f . unsafeCoerceF constrOfF)--{--------------------------------------------------------------------------------  Prove that the functors of our user-defined types are indeed parametric--  NOTE: It's kinda frustrating that we have to repeat this for every type.-  That's non-trivial to fix though; a polymorphic function would need as-  quantified constraint that--  > forall a b. Constrs (f a) ~ Constrs (f b)--  but that is not legal Haskell: we cannot use type synonyms in quantified-  constraints (frustratingly and unnecessarily).--------------------------------------------------------------------------------}--instance Phantom (ConstrOfF NonRecursive c) where-  phantom (ConstrOfF IsConstrOf) = ConstrOfF IsConstrOf--instance Phantom (ConstrOfF Recursive c) where-  phantom (ConstrOfF IsConstrOf) = ConstrOfF IsConstrOf+    coerceToF :: forall a. UserDefined -> f a+    coerceToF = unsafeCoerce -instance Phantom (ConstrOfF ContainsUnlifted c) where-  phantom (ConstrOfF IsConstrOf) = ConstrOfF IsConstrOf+    aux :: Reclassified a            -- Classification of the elements+        -> Reclassified UserDefined  -- Classification of the container+    aux (Reclassified c f) =+        Reclassified (cc (FJust c)) (fmap f . coerceToF)  {-------------------------------------------------------------------------------   Auxiliary

@@ -3,27 +3,37 @@ {-# LANGUAGE DeriveGeneric     #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE MagicHash         #-}+{-# LANGUAGE PolyKinds         #-} {-# LANGUAGE TypeFamilies      #-} {-# LANGUAGE TypeOperators     #-} {-# LANGUAGE UnboxedTuples     #-}  -- | Just some examples of user-defined types module Test.RecoverRTTI.UserDefined (-    NonRecursive(..)+    SimpleType(..)+  , NonRecursive(..)   , Recursive(..)   , recursiveFromList   , ContainsUnlifted -- opaque   , exampleContainsUnlifted+  , ConstrsOf(..)   ) where +import Data.Proxy import GHC.Generics import GHC.IO import GHC.Prim +import Test.QuickCheck+ {-------------------------------------------------------------------------------   User-defined datatypes -------------------------------------------------------------------------------} +-- | Example of a simple monomorphic user-defined type+data SimpleType = SimpleA | SimpleB+  deriving (Show, Eq, Generic)+ -- | Example of a non-recursive user-defined type data NonRecursive a = NR1 Int | NR2 a Bool   deriving (Show, Eq, Generic, Functor, Foldable, Traversable)@@ -43,37 +53,44 @@ -------------------------------------------------------------------------------}  -- | Example of a user-defined type containing something unlifted-data ContainsUnlifted a = NothingHere | ContainsUnlifted (MutableArray# RealWorld Int) a-  deriving (Functor, Foldable, Traversable)---- We can't derive a Generic instance, we must produce just enough info so that--- we can do the right type casts-instance Generic (ContainsUnlifted a) where-  type Rep (ContainsUnlifted a) = Rep_ContainsUnlifted--  from = error "'from' not defined for ContainsUnlifted"-  to   = error "'to' not defined for ContainsUnlifted"---- We don't bother specifiying the arguments to the constructors-type Rep_ContainsUnlifted =-    M1 D ('MetaData "ContainsUnlifted" "Test.RecoverRTTI.UserDefined" "main" 'False)-     (     M1 C ('MetaCons "NothingHere" 'PrefixI 'False) U1-       :+:-           M1 C ('MetaCons "ContainsUnlifted" 'PrefixI 'False) U1-     )+data ContainsUnlifted = ContainsUnlifted (MutableArray# RealWorld Int) Bool -instance Show a => Show (ContainsUnlifted a) where-  showsPrec _ NothingHere =-        showString "NothingHere"+instance Show ContainsUnlifted where   showsPrec p (ContainsUnlifted _ x) = showParen (p >= 11) $         showString "ContainsUnlifted "       . showsPrec 11 x -instance Eq (ContainsUnlifted a) where+instance Eq ContainsUnlifted where   _ == _ = True -exampleContainsUnlifted :: ContainsUnlifted ()+exampleContainsUnlifted :: ContainsUnlifted {-# NOINLINE exampleContainsUnlifted #-} exampleContainsUnlifted = unsafePerformIO $ IO $ \world ->     let !(# world', arr #) = newArray# 5# 0 world-    in (# world', ContainsUnlifted arr () #)+    in (# world', ContainsUnlifted arr True #)++{-------------------------------------------------------------------------------+  ConstrsOf+-------------------------------------------------------------------------------}++-- | Constructors of this type+--+-- This could be defined in terms of generics, but this is kind polymorphic.+-- Used for testing only.+class ConstrsOf (f :: k) where+  constrsOf :: Proxy f -> [String]++instance ConstrsOf SimpleType       where constrsOf _ = ["SimpleA", "SimpleB"]+instance ConstrsOf Recursive        where constrsOf _ = ["RNil", "RCons"]+instance ConstrsOf NonRecursive     where constrsOf _ = ["NR1", "NR2"]+instance ConstrsOf ContainsUnlifted where constrsOf _ = ["NothingHere", "ContainsUnlifted"]++{-------------------------------------------------------------------------------+  Arbitrary instances+-------------------------------------------------------------------------------}++instance Arbitrary SimpleType where+  arbitrary = elements [SimpleA, SimpleB]++instance Arbitrary ContainsUnlifted where+  arbitrary = return exampleContainsUnlifted