{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Michelson.Typed.Haskell.Instr.Sum
( InstrWrapC
, InstrCaseC
, InstrUnwrapC
, instrWrap
, hsWrap
, instrCase
, (//->)
, instrUnwrapUnsafe
, hsUnwrap
, CaseClauseParam (..)
, CaseClause (..)
, CaseClauses
, GCaseClauses
, GCaseBranchInput
, Branch (..)
, Path
, CtorField (..)
, ExtractCtorField
, AppendCtorField
, AppendCtorFieldAxiom
, appendCtorFieldAxiom
, GetCtorField
, CtorHasOnlyField
, CtorOnlyField
, MyCompoundType
, IsPrimitiveValue
) where
import Data.Constraint (Dict(..))
import qualified Data.Kind as Kind
import Data.Singletons (SingI(..))
import Data.Type.Bool (If, type (||))
import Data.Type.Equality (type (==))
import Data.Vinyl.Core (Rec(..))
import Data.Vinyl.Derived (Label)
import Data.Vinyl.TypeLevel (type (++))
import GHC.Generics ((:*:)(..), (:+:)(..))
import qualified GHC.Generics as G
import GHC.TypeLits (AppendSymbol, ErrorMessage(..), Symbol, TypeError)
import Named ((:!), NamedF)
import Type.Reflection ((:~:)(Refl))
import Unsafe.Coerce (unsafeCoerce)
import Michelson.Typed.Haskell.Instr.Helpers
import Michelson.Typed.Haskell.Value
import Michelson.Typed.Instr
import Michelson.Typed.T
import Michelson.Typed.EntryPoints
import Michelson.Text (MText, mt)
import Michelson.Typed.Value
import Tezos.Address (Address)
import Tezos.Core (Mutez, Timestamp)
import Tezos.Crypto (KeyHash, PublicKey, Signature)
import Util.Type
import Util.TypeTuple
data CtorField
= OneField Kind.Type
| NoFields
type family ExtractCtorField (cf :: CtorField) where
ExtractCtorField ('OneField t) = t
ExtractCtorField 'NoFields = ()
type family AppendCtorField (cf :: CtorField) (l :: [k]) :: [k] where
AppendCtorField ('OneField t) (l :: [T]) = ToT t ': l
AppendCtorField ('OneField t) (l :: [Kind.Type]) = t ': l
AppendCtorField 'NoFields (l :: [T]) = l
AppendCtorField 'NoFields (l :: [Kind.Type]) = l
type AppendCtorFieldAxiom (cf :: CtorField) (st :: [Kind.Type]) =
ToTs (AppendCtorField cf st) ~ AppendCtorField cf (ToTs st)
appendCtorFieldAxiom
:: ( AppendCtorFieldAxiom ('OneField Word) '[Int]
, AppendCtorFieldAxiom 'NoFields '[Int]
)
=> Dict (AppendCtorFieldAxiom cf st)
appendCtorFieldAxiom =
unsafeCoerce $ Dict @(AppendCtorFieldAxiom 'NoFields '[])
data LookupNamedResult = LNR CtorField Path
type family LnrFieldType (lnr :: LookupNamedResult) where
LnrFieldType ('LNR f _) = f
type family LnrBranch (lnr :: LookupNamedResult) :: Path where
LnrBranch ('LNR _ p) = p
type GetNamed name a = LNRequireFound name a (GLookupNamed name (G.Rep a))
type family LNRequireFound
(name :: Symbol)
(a :: Kind.Type)
(mf :: Maybe LookupNamedResult)
:: LookupNamedResult where
LNRequireFound _ _ ('Just lnr) = lnr
LNRequireFound name a 'Nothing = TypeError
('Text "Datatype " ':<>: 'ShowType a ':<>:
'Text " has no (sub)constructor " ':<>: 'ShowType name)
type family GLookupNamed (name :: Symbol) (x :: Kind.Type -> Kind.Type)
:: Maybe LookupNamedResult where
GLookupNamed name (G.D1 _ x) = GLookupNamed name x
GLookupNamed name (G.C1 ('G.MetaCons ctorName _ _) x) =
PrependS
(If (name == ctorName || name == ("c" `AppendSymbol` ctorName))
('Just $ 'LNR (GExtractFields x) '[])
(If (GCanGoDeeper x)
(GLookupNamedDeeper name x)
'Nothing
)
)
GLookupNamed name (x :+: y) =
LNMergeFound name (GLookupNamed name x) (GLookupNamed name y)
GLookupNamed _ G.V1 = 'Nothing
type family PrependS (x :: Maybe LookupNamedResult) :: Maybe LookupNamedResult where
PrependS 'Nothing = 'Nothing
PrependS ('Just ('LNR cf path)) = 'Just ('LNR cf ('S ': path))
type family GCanGoDeeper (x :: Kind.Type -> Kind.Type) :: Bool where
GCanGoDeeper (_ :+: _) = 'True
GCanGoDeeper (G.D1 _ x) = GCanGoDeeper x
GCanGoDeeper (G.S1 _ (G.Rec0 x)) = CanGoDeeper x
GCanGoDeeper (G.C1 _ _) = 'True
GCanGoDeeper G.V1 = 'False
GCanGoDeeper G.U1 = 'False
GCanGoDeeper (_ :*: _) = 'False
GCanGoDeeper x = TypeError
('Text "GCanGoDeeper encountered unexpected pattern: " ':<>: 'ShowType x)
type family IsPrimitiveValue (x :: Kind.Type) :: Bool where
IsPrimitiveValue (Maybe _) = 'True
IsPrimitiveValue (NamedF _ _ _) = 'True
IsPrimitiveValue Integer = 'True
IsPrimitiveValue Natural = 'True
IsPrimitiveValue Text = 'True
IsPrimitiveValue MText = 'True
IsPrimitiveValue Bool = 'True
IsPrimitiveValue ByteString = 'True
IsPrimitiveValue Mutez = 'True
IsPrimitiveValue Address = 'True
IsPrimitiveValue EpAddress = 'True
IsPrimitiveValue KeyHash = 'True
IsPrimitiveValue Timestamp = 'True
IsPrimitiveValue PublicKey = 'True
IsPrimitiveValue Signature = 'True
IsPrimitiveValue (ContractRef _) = 'True
IsPrimitiveValue (BigMap _ _) = 'True
IsPrimitiveValue (Map _ _) = 'True
IsPrimitiveValue (Set _) = 'True
IsPrimitiveValue ([_]) = 'True
IsPrimitiveValue (Operation' _) = 'True
IsPrimitiveValue _ = 'False
type CanGoDeeper (x :: Kind.Type) =
If (IsPrimitiveValue x)
'False
(GCanGoDeeper (G.Rep x))
type family GLookupNamedDeeper (name :: Symbol) (x :: Kind.Type -> Kind.Type)
:: Maybe LookupNamedResult where
GLookupNamedDeeper name (G.S1 _ (G.Rec0 y)) = GLookupNamed name (G.Rep y)
GLookupNamedDeeper name _ = TypeError
('Text "Attempt to go deeper failed while looking for sum type constructor"
':<>: 'ShowType name
':$$:
'Text "Make sure that all constructors have exactly one field inside."
)
type family LNMergeFound
(name :: Symbol)
(f1 :: Maybe LookupNamedResult)
(f2 :: Maybe LookupNamedResult)
:: Maybe LookupNamedResult where
LNMergeFound _ 'Nothing 'Nothing = 'Nothing
LNMergeFound _ ('Just ('LNR a p)) 'Nothing = 'Just $ 'LNR a ('L ': p)
LNMergeFound _ 'Nothing ('Just ('LNR a p)) = 'Just $ 'LNR a ('R ': p)
LNMergeFound name ('Just _) ('Just _) = TypeError
('Text "Ambiguous reference to datatype constructor: " ':<>: 'ShowType name)
type family GExtractFields (x :: Kind.Type -> Kind.Type)
:: CtorField where
GExtractFields (G.S1 _ x) = GExtractFields x
GExtractFields (G.Rec0 a) = 'OneField a
GExtractFields G.U1 = 'NoFields
GExtractFields (_ :*: _) = TypeError
('Text "Cannot automatically lookup constructors having multiple fields"
':$$:
'Text "Consider using tuple instead")
type GetCtorField dt ctor =
LnrFieldType (GetNamed ctor dt)
type CtorHasOnlyField ctor dt f =
GetCtorField dt ctor ~ 'OneField f
type family RequireOneField (ctor :: Symbol) (cf :: CtorField) :: Kind.Type where
RequireOneField _ ('OneField f) = f
RequireOneField ctor 'NoFields = TypeError
('Text "Expected exactly one field" ':$$:
'Text "In constructor " ':<>: 'ShowType ctor)
type CtorOnlyField name dt =
RequireOneField name (GetCtorField dt name)
instrWrap
:: forall dt name st.
InstrWrapC dt name
=> Label name
-> Instr (AppendCtorField (GetCtorField dt name) st)
(ToT dt ': st)
instrWrap _ =
gInstrWrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))
@(LnrFieldType (GetNamed name dt))
type InstrWrapC dt name =
( GenericIsoValue dt
, GInstrWrap (G.Rep dt)
(LnrBranch (GetNamed name dt))
(LnrFieldType (GetNamed name dt))
)
hsWrap
:: forall dt name.
InstrWrapC dt name
=> Label name
-> ExtractCtorField (GetCtorField dt name)
-> dt
hsWrap _ =
G.to . gHsWrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))
@(LnrFieldType (GetNamed name dt))
class GIsoValue x =>
GInstrWrap
(x :: Kind.Type -> Kind.Type)
(path :: Path)
(entryTy :: CtorField) where
gInstrWrap
:: GIsoValue x
=> Instr (AppendCtorField entryTy s) (GValueType x ': s)
gHsWrap
:: GIsoValue x
=> ExtractCtorField entryTy -> x p
instance GInstrWrap x path e => GInstrWrap (G.D1 i x) path e where
gInstrWrap = gInstrWrap @x @path @e
gHsWrap = G.M1 . gHsWrap @x @path @e
instance (GInstrWrap x path e, GIsoValue y, SingI (GValueType y)) =>
GInstrWrap (x :+: y) ('L ': path) e where
gInstrWrap = gInstrWrap @x @path @e `Seq` LEFT
gHsWrap = G.L1 . gHsWrap @x @path @e
instance (GInstrWrap y path e, GIsoValue x, SingI (GValueType x)) =>
GInstrWrap (x :+: y) ('R ': path) e where
gInstrWrap = gInstrWrap @y @path @e `Seq` RIGHT
gHsWrap = G.R1 . gHsWrap @y @path @e
instance (IsoValue e) =>
GInstrWrap (G.C1 c (G.S1 i (G.Rec0 e))) '[ 'S] ('OneField e) where
gInstrWrap = Nop
gHsWrap = G.M1 . G.M1 . G.K1
instance ( path ~ (x ': xs)
, GInstrWrap (G.Rep sub) path e
, GenericIsoValue sub
, GIsoValue (G.Rep sub)
) =>
GInstrWrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where
gInstrWrap = gInstrWrap @(G.Rep sub) @path @e
gHsWrap = G.M1 . G.M1 . G.K1 . G.to . gHsWrap @(G.Rep sub) @path @e
instance GInstrWrap (G.C1 c G.U1) '[ 'S] 'NoFields where
gInstrWrap = PUSH VUnit
gHsWrap () = G.M1 G.U1
data MyType
= MyCtor Integer
| ComplexThing ()
| UselessThing ("field1" :! ByteString, "field2" :! ())
deriving stock Generic
deriving anyclass IsoValue
_MyTypeMyCtor ::
GetNamed "cMyCtor" MyType :~: 'LNR ('OneField Integer) '[ 'L, 'S]
_MyTypeMyCtor = Refl
_MyTypeComplexThing ::
GetNamed "cComplexThing" MyType :~: 'LNR ('OneField ()) '[ 'R, 'L, 'S]
_MyTypeComplexThing = Refl
_wrapMyType1 :: Instr (ToT Integer ': s) (ToT MyType ': s)
_wrapMyType1 = instrWrap @MyType #cMyCtor
_wrapMyType1' :: Instr (ToT Integer ': s) (ToT MyType ': s)
_wrapMyType1' = instrWrap @MyType @"MyCtor" fromLabel
_wrapMyType2 :: Instr (ToT () ': s) (ToT MyType ': s)
_wrapMyType2 = instrWrap @MyType #cComplexThing
_wrapMyType3 :: Instr (ToT (ByteString, ()) ': s) (ToT MyType ': s)
_wrapMyType3 = instrWrap @MyType #cUselessThing
data MyType' = WrapBool Bool
deriving stock Generic
deriving anyclass IsoValue
_MyType'WrapBool ::
GetNamed "cWrapBool" MyType' :~: 'LNR ('OneField Bool) '[ 'S]
_MyType'WrapBool = Refl
_wrapMyType' :: Instr (ToT Bool ': s) (ToT MyType' ': s)
_wrapMyType' = instrWrap @MyType' #cWrapBool
data MyCompoundType
= CompoundPart1 MyType
| CompoundPart2 Integer
| CompoundPart3 Address
| CompoundPart4 MyType'
deriving stock Generic
deriving anyclass IsoValue
_MyCompoundTypeCompoundPart1 ::
GetNamed "cCompoundPart1" MyCompoundType :~: 'LNR ('OneField MyType) '[ 'L, 'L, 'S]
_MyCompoundTypeCompoundPart1 = Refl
_MyCompoundTypeMyCtor ::
GetNamed "cMyCtor" MyCompoundType :~: 'LNR ('OneField Integer) '[ 'L, 'L, 'S, 'L, 'S]
_MyCompoundTypeMyCtor = Refl
_MyCompoundTypeCompoundPart2 ::
GetNamed "cCompoundPart2" MyCompoundType :~: 'LNR ('OneField Integer) '[ 'L, 'R, 'S]
_MyCompoundTypeCompoundPart2 = Refl
_MyCompoundTypeCompoundPart4 ::
GetNamed "cCompoundPart4" MyCompoundType :~: 'LNR ('OneField MyType') '[ 'R, 'R, 'S]
_MyCompoundTypeCompoundPart4 = Refl
_MyCompoundTypeWrapBool ::
GetNamed "cWrapBool" MyCompoundType :~: 'LNR ('OneField Bool) '[ 'R, 'R, 'S, 'S]
_MyCompoundTypeWrapBool = Refl
_wrapMyCompoundType1 :: Instr (ToT Integer ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType1 = instrWrap @MyCompoundType #cMyCtor
_wrapMyCompoundType2 :: Instr (ToT Integer ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType2 = instrWrap @MyCompoundType #cCompoundPart2
_wrapMyCompoundType3 :: Instr (ToT Bool ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType3 = instrWrap @MyCompoundType #cWrapBool
_wrapMyCompoundType4 :: Instr (ToT MyType' ': s) (ToT MyCompoundType ': s)
_wrapMyCompoundType4 = instrWrap @MyCompoundType #cCompoundPart4
data MyEnum = Case1 | Case2 | CaseN Integer | CaseDef
deriving stock Generic
deriving anyclass IsoValue
_wrapMyEnum1 :: Instr s (ToT MyEnum ': s)
_wrapMyEnum1 = instrWrap @MyEnum #cCase1
_wrapMyEnum2 :: Instr (ToT Integer ': s) (ToT MyEnum ': s)
_wrapMyEnum2 = instrWrap @MyEnum #cCaseN
data MyTypeWithNamedField
= MeaninglessCtor
| CtorWithNamedField ("name" :! Natural)
deriving stock Generic
deriving anyclass IsoValue
_accessMyTypeWithNamedField :: Instr (ToT Natural ': s) (ToT MyTypeWithNamedField ': s)
_accessMyTypeWithNamedField = instrWrap @MyTypeWithNamedField #cCtorWithNamedField
instrCase
:: forall dt out inp.
InstrCaseC dt inp out
=> Rec (CaseClause inp out) (CaseClauses dt) -> RemFail Instr (ToT dt ': inp) out
instrCase = gInstrCase @(G.Rep dt)
type InstrCaseC dt inp out = (GenericIsoValue dt, GInstrCase (G.Rep dt))
data CaseClauseParam = CaseClauseParam Symbol CtorField
data CaseClause (inp :: [T]) (out :: [T]) (param :: CaseClauseParam) where
CaseClause
:: RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
(//->)
:: Label ("c" `AppendSymbol` ctor)
-> RemFail Instr (AppendCtorField x inp) out
-> CaseClause inp out ('CaseClauseParam ctor x)
(//->) _ = CaseClause
infixr 8 //->
type CaseClauses a = GCaseClauses (G.Rep a)
class GIsoValue x => GInstrCase (x :: Kind.Type -> Kind.Type) where
type GCaseClauses x :: [CaseClauseParam]
gInstrCase
:: GIsoValue x
=> Rec (CaseClause inp out) (GCaseClauses x) -> RemFail Instr (GValueType x ': inp) out
instance GInstrCase x => GInstrCase (G.D1 i x) where
type GCaseClauses (G.D1 i x) = GCaseClauses x
gInstrCase = gInstrCase @x
instance (GInstrCase x, GInstrCase y, RSplit (GCaseClauses x) (GCaseClauses y)) =>
GInstrCase (x :+: y) where
type GCaseClauses (x :+: y) = GCaseClauses x ++ GCaseClauses y
gInstrCase clauses =
let (leftClauses, rightClauses) = rsplit clauses
in rfMerge IF_LEFT (gInstrCase @x leftClauses) (gInstrCase @y rightClauses)
instance GInstrCaseBranch ctor x => GInstrCase (G.C1 ('G.MetaCons ctor _1 _2) x) where
type GCaseClauses (G.C1 ('G.MetaCons ctor _1 _2) x) = '[GCaseBranchInput ctor x]
gInstrCase (clause :& RNil) = gInstrCaseBranch @ctor @x clause
class GIsoValue x =>
GInstrCaseBranch (ctor :: Symbol) (x :: Kind.Type -> Kind.Type) where
type GCaseBranchInput ctor x :: CaseClauseParam
gInstrCaseBranch
:: CaseClause inp out (GCaseBranchInput ctor x)
-> RemFail Instr (GValueType x ': inp) out
instance
( GIsoValue x, GIsoValue y
, TypeError ('Text "Cannot pattern match on constructors with more than 1 field"
':$$: 'Text "Consider using tuples instead")
) => GInstrCaseBranch ctor (x :*: y) where
type GCaseBranchInput ctor (x :*: y) = 'CaseClauseParam ctor 'NoFields
gInstrCaseBranch = error "impossible"
instance GInstrCaseBranch ctor x => GInstrCaseBranch ctor (G.S1 i x) where
type GCaseBranchInput ctor (G.S1 i x) = GCaseBranchInput ctor x
gInstrCaseBranch = gInstrCaseBranch @ctor @x
instance IsoValue a => GInstrCaseBranch ctor (G.Rec0 a) where
type GCaseBranchInput ctor (G.Rec0 a) = 'CaseClauseParam ctor ('OneField a)
gInstrCaseBranch (CaseClause i) = i
instance GInstrCaseBranch ctor G.U1 where
type GCaseBranchInput ctor G.U1 = 'CaseClauseParam ctor 'NoFields
gInstrCaseBranch (CaseClause i) = rfMapAnyInstr (DROP `Seq`) i
_caseMyType :: RemFail Instr (ToT MyType ': s) (ToT Integer ': s)
_caseMyType = instrCase @MyType $
#cMyCtor //-> RfNormal Nop
:& #cComplexThing //-> RfNormal (DROP `Seq` PUSH (toVal @Integer 5))
:& #cUselessThing //-> RfNormal (DROP `Seq` PUSH (toVal @Integer 0))
:& RNil
_caseMyType2 :: RemFail Instr (ToT MyType ': s) (ToT Integer ': s)
_caseMyType2 = instrCase @MyType $ recFromTuple
( #cMyCtor //->
RfNormal Nop
, #cComplexThing //->
RfNormal (DROP `Seq` PUSH (toVal @Integer 5))
, #cUselessThing //->
RfNormal (DROP `Seq` PUSH (toVal @Integer 0))
)
_caseMyEnum :: RemFail Instr (ToT MyEnum ': ToT Integer ': s) (ToT Integer ': s)
_caseMyEnum = instrCase @MyEnum $ recFromTuple
( #cCase1 //-> RfNormal (DROP `Seq` PUSH (toVal @Integer 1))
, #cCase2 //-> RfNormal (DROP `Seq` PUSH (toVal @Integer 2))
, #cCaseN //-> RfNormal (DIP DROP `Seq` Nop)
, #cCaseDef //-> RfNormal Nop
)
instrUnwrapUnsafe
:: forall dt name st.
InstrUnwrapC dt name
=> Label name
-> Instr (ToT dt ': st)
(ToT (CtorOnlyField name dt) ': st)
instrUnwrapUnsafe _ =
gInstrUnwrapUnsafe @(G.Rep dt) @(LnrBranch (GetNamed name dt))
@(CtorOnlyField name dt)
type InstrUnwrapC dt name =
( GenericIsoValue dt
, GInstrUnwrap (G.Rep dt)
(LnrBranch (GetNamed name dt))
(CtorOnlyField name dt)
)
hsUnwrap
:: forall dt name.
InstrUnwrapC dt name
=> Label name
-> dt
-> Maybe (CtorOnlyField name dt)
hsUnwrap _ =
gHsUnwrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))
@(CtorOnlyField name dt) .
G.from
class GIsoValue x =>
GInstrUnwrap
(x :: Kind.Type -> Kind.Type)
(path :: Path)
(entryTy :: Kind.Type) where
gInstrUnwrapUnsafe
:: GIsoValue x
=> Instr (GValueType x ': s) (ToT entryTy ': s)
gHsUnwrap
:: x p -> Maybe entryTy
instance GInstrUnwrap x path e => GInstrUnwrap (G.D1 i x) path e where
gInstrUnwrapUnsafe = gInstrUnwrapUnsafe @x @path @e
gHsUnwrap = gHsUnwrap @x @path @e . G.unM1
instance (GInstrUnwrap x path e, GIsoValue y, SingI (GValueType y)) =>
GInstrUnwrap (x :+: y) ('L ': path) e where
gInstrUnwrapUnsafe = IF_LEFT (gInstrUnwrapUnsafe @x @path @e) failWithWrongCtor
gHsUnwrap = \case
G.L1 x -> gHsUnwrap @x @path @e x
G.R1 _ -> Nothing
instance (GInstrUnwrap y path e, GIsoValue x, SingI (GValueType x)) =>
GInstrUnwrap (x :+: y) ('R ': path) e where
gInstrUnwrapUnsafe = IF_LEFT failWithWrongCtor (gInstrUnwrapUnsafe @y @path @e)
gHsUnwrap = \case
G.R1 y -> gHsUnwrap @y @path @e y
G.L1 _ -> Nothing
instance (IsoValue e) =>
GInstrUnwrap (G.C1 c (G.S1 i (G.Rec0 e))) '[ 'S] e where
gInstrUnwrapUnsafe = Nop
gHsUnwrap = Just . G.unK1 . G.unM1 . G.unM1
instance ( path ~ (x ': xs)
, GInstrUnwrap (G.Rep sub) path e
, GenericIsoValue sub
, GIsoValue (G.Rep sub)
) =>
GInstrUnwrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where
gInstrUnwrapUnsafe = gInstrUnwrapUnsafe @(G.Rep sub) @path @e
gHsUnwrap = gHsUnwrap @(G.Rep sub) @path @e . G.from . G.unK1 . G.unM1 . G.unM1
failWithWrongCtor :: Instr i o
failWithWrongCtor =
PUSH (toVal [mt|BadCtor|]) `Seq`
FAILWITH
_unwrapMyType :: Instr (ToT MyType ': s) (ToT Integer ': s)
_unwrapMyType = instrUnwrapUnsafe @MyType #cMyCtor
_unwrapMyCompoundType :: Instr (ToT MyCompoundType ': s) (ToT Integer ': s)
_unwrapMyCompoundType = instrUnwrapUnsafe @MyCompoundType #cMyCtor
_unwrapMyCompoundType2 :: Instr (ToT MyCompoundType ': s) (ToT Address ': s)
_unwrapMyCompoundType2 = instrUnwrapUnsafe @MyCompoundType #cCompoundPart3
_unwrapMyCompoundType3 :: Instr (ToT MyCompoundType ': s) (ToT Bool ': s)
_unwrapMyCompoundType3 = instrUnwrapUnsafe @MyCompoundType #cWrapBool
_unwrapMyCompoundType4 :: Instr (ToT MyCompoundType ': s) (ToT MyType' ': s)
_unwrapMyCompoundType4 = instrUnwrapUnsafe @MyCompoundType #cCompoundPart4