-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA
{-# LANGUAGE DeriveLift #-}

{-# OPTIONS_GHC -Wno-orphans #-}

-- | Module, providing @Notes t@ data type, which holds annotations for a
-- given type @t@.
--
-- Annotation type @Notes t@ is a tree, each leaf is either a star (@*@) or a
-- constructor holding some annotation data for a given type @t@.
-- Star corresponds to the case when given Michelson type contains no
-- annotations.
--
-- This module also provides some
-- utility functions which are used to combine two annotations trees
-- @a@ and @b@ into a new one @c@ in such a way that @c@ can be obtained from
-- both @a@ and @b@ by replacing some @*@ leaves with type or/and field
-- annotations.

module Morley.Michelson.Typed.Annotation
  ( Notes (..)
  , insertTypeAnn
  , isStar
  , starNotes
  , mkUType
  , notesSing
  , notesT
    -- * Helpers
  , AnnVar
  , Anns(.., Anns1, Anns2, Anns2', Anns3, Anns3', Anns3'', Anns4, Anns4'', Anns5')
  , AnnotateInstr(..)
  ) where

import Data.Default (Default(def))
import Data.Singletons (Sing, SingI(..), fromSing)
import Fmt (Buildable(..))
import Language.Haskell.TH.Syntax (Lift)

import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDoc)
import Morley.Michelson.Typed.Sing
import Morley.Michelson.Typed.T (T(..))
import Morley.Michelson.Untyped qualified as Un
import Morley.Michelson.Untyped.Annotation (Annotation, FieldAnn, TypeAnn, VarAnn, noAnn)
import Morley.Util.Peano qualified as Peano
import Morley.Util.PeanoNatural (singPeanoVal)
import Morley.Util.TH

{-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-}

-- | Data type, holding annotation data for a given Michelson type @t@.
--
-- Each constructor corresponds to exactly one constructor of 'T'
-- and holds all type and field annotations that can be attributed to a
-- Michelson type corresponding to @t@.
data Notes t where
  NTKey       :: TypeAnn -> Notes 'TKey
  NTUnit      :: TypeAnn -> Notes 'TUnit
  NTSignature :: TypeAnn -> Notes 'TSignature
  NTChainId   :: TypeAnn -> Notes 'TChainId
  NTOption    :: TypeAnn -> Notes t -> Notes ('TOption t)
  NTList      :: TypeAnn -> Notes t -> Notes ('TList t)
  NTSet       :: TypeAnn -> Notes t -> Notes ('TSet t)
  NTOperation :: TypeAnn -> Notes 'TOperation
  NTContract  :: TypeAnn -> Notes t -> Notes ('TContract t)
  NTTicket    :: TypeAnn -> Notes t -> Notes ('TTicket t)
  NTPair      :: TypeAnn -> FieldAnn -> FieldAnn
              -> VarAnn -> VarAnn
              -> Notes p -> Notes q -> Notes ('TPair p q)
  NTOr        :: TypeAnn -> FieldAnn -> FieldAnn
              -> Notes p -> Notes q -> Notes ('TOr p q)
  NTLambda    :: TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
  NTMap       :: TypeAnn -> Notes k -> Notes v -> Notes ('TMap k v)
  NTBigMap    :: TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
  NTInt       :: TypeAnn -> Notes 'TInt
  NTNat       :: TypeAnn -> Notes 'TNat
  NTString    :: TypeAnn -> Notes 'TString
  NTBytes     :: TypeAnn -> Notes 'TBytes
  NTMutez     :: TypeAnn -> Notes 'TMutez
  NTBool      :: TypeAnn -> Notes 'TBool
  NTKeyHash   :: TypeAnn -> Notes 'TKeyHash
  NTBls12381Fr :: TypeAnn -> Notes 'TBls12381Fr
  NTBls12381G1 :: TypeAnn -> Notes 'TBls12381G1
  NTBls12381G2 :: TypeAnn -> Notes 'TBls12381G2
  NTTimestamp :: TypeAnn -> Notes 'TTimestamp
  NTAddress   :: TypeAnn -> Notes 'TAddress
  NTChest     :: TypeAnn -> Notes 'TChest
  NTChestKey  :: TypeAnn -> Notes 'TChestKey
  NTNever     :: TypeAnn -> Notes 'TNever
  NTTxRollupL2Address     :: TypeAnn -> Notes 'TTxRollupL2Address
  NTSaplingState :: forall (n :: Peano.Peano). TypeAnn -> Sing n -> Notes ('TSaplingState n)
  NTSaplingTransaction :: forall (n :: Peano.Peano). TypeAnn -> Sing n -> Notes ('TSaplingTransaction n)

deriving stock instance Eq (Notes t)
deriving stock instance Show (Notes t)
deriving stock instance Lift (Notes t)
$(deriveGADTNFData ''Notes)


instance Buildable (Notes t) where
  build :: Notes t -> Builder
build = Notes t -> Builder
forall a. RenderDoc a => a -> Builder
buildRenderDoc

instance RenderDoc (Notes t) where
  renderDoc :: RenderContext -> Notes t -> Doc
renderDoc RenderContext
pn = RenderContext -> Ty -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn (Ty -> Doc) -> (Notes t -> Ty) -> Notes t -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType

-- | Forget information about annotations, pick singleton with the same type.
notesSing :: Notes t -> Sing t
notesSing :: forall (t :: T). Notes t -> Sing t
notesSing = \case
  NTInt TypeAnn
_        -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTNat TypeAnn
_        -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTString TypeAnn
_     -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTBytes TypeAnn
_      -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTMutez TypeAnn
_      -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTBool TypeAnn
_       -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTKeyHash TypeAnn
_    -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTBls12381Fr TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTBls12381G1 TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTBls12381G2 TypeAnn
_ -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTTimestamp TypeAnn
_  -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTAddress TypeAnn
_    -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTKey TypeAnn
_        -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTUnit TypeAnn
_       -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTSignature TypeAnn
_  -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTChainId TypeAnn
_    -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTOption TypeAnn
_ Notes t
n   -> Sing t -> SingT ('TOption t)
forall (n :: T). Sing n -> SingT ('TOption n)
STOption (Notes t -> Sing t
forall (t :: T). Notes t -> Sing t
notesSing Notes t
n)
  NTList TypeAnn
_ Notes t
n     -> Sing t -> SingT ('TList t)
forall (n :: T). Sing n -> SingT ('TList n)
STList (Notes t -> Sing t
forall (t :: T). Notes t -> Sing t
notesSing Notes t
n)
  NTSet TypeAnn
_ Notes t
n      -> Sing t -> SingT ('TSet t)
forall (n :: T). Sing n -> SingT ('TSet n)
STSet (Notes t -> Sing t
forall (t :: T). Notes t -> Sing t
notesSing Notes t
n)
  NTOperation TypeAnn
_  -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTChest TypeAnn
_      -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTChestKey TypeAnn
_   -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTTxRollupL2Address TypeAnn
_  -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTNever TypeAnn
_      -> Sing t
forall {k} (a :: k). SingI a => Sing a
sing
  NTSaplingState TypeAnn
_ Sing n
s -> Sing n -> SingT ('TSaplingState n)
forall (n :: Peano). Sing n -> SingT ('TSaplingState n)
STSaplingState Sing n
s
  NTSaplingTransaction TypeAnn
_ Sing n
s -> Sing n -> SingT ('TSaplingTransaction n)
forall (n :: Peano). Sing n -> SingT ('TSaplingTransaction n)
STSaplingTransaction Sing n
s
  NTContract TypeAnn
_ Notes t
n -> Sing t -> SingT ('TContract t)
forall (n :: T). Sing n -> SingT ('TContract n)
STContract (Notes t -> Sing t
forall (t :: T). Notes t -> Sing t
notesSing Notes t
n)
  NTTicket TypeAnn
_ Notes t
n   -> Sing t -> SingT ('TTicket t)
forall (n :: T). Sing n -> SingT ('TTicket n)
STTicket (Notes t -> Sing t
forall (t :: T). Notes t -> Sing t
notesSing Notes t
n)
  NTPair TypeAnn
_ FieldAnn
_ FieldAnn
_ VarAnn
_ VarAnn
_ Notes p
l Notes q
r -> Sing p -> Sing q -> SingT ('TPair p q)
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TPair n1 n2)
STPair   (Notes p -> Sing p
forall (t :: T). Notes t -> Sing t
notesSing Notes p
l) (Notes q -> Sing q
forall (t :: T). Notes t -> Sing t
notesSing Notes q
r)
  NTOr TypeAnn
_ FieldAnn
_ FieldAnn
_ Notes p
l Notes q
r       -> Sing p -> Sing q -> SingT ('TOr p q)
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TOr n1 n2)
STOr     (Notes p -> Sing p
forall (t :: T). Notes t -> Sing t
notesSing Notes p
l) (Notes q -> Sing q
forall (t :: T). Notes t -> Sing t
notesSing Notes q
r)
  NTLambda TypeAnn
_ Notes p
l Notes q
r       -> Sing p -> Sing q -> SingT ('TLambda p q)
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TLambda n1 n2)
STLambda (Notes p -> Sing p
forall (t :: T). Notes t -> Sing t
notesSing Notes p
l) (Notes q -> Sing q
forall (t :: T). Notes t -> Sing t
notesSing Notes q
r)
  NTMap TypeAnn
_ Notes k
l Notes v
r          -> Sing k -> Sing v -> SingT ('TMap k v)
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TMap n1 n2)
STMap    (Notes k -> Sing k
forall (t :: T). Notes t -> Sing t
notesSing Notes k
l) (Notes v -> Sing v
forall (t :: T). Notes t -> Sing t
notesSing Notes v
r)
  NTBigMap TypeAnn
_ Notes k
l Notes v
r       -> Sing k -> Sing v -> SingT ('TBigMap k v)
forall (n1 :: T) (n2 :: T).
Sing n1 -> Sing n2 -> SingT ('TBigMap n1 n2)
STBigMap (Notes k -> Sing k
forall (t :: T). Notes t -> Sing t
notesSing Notes k
l) (Notes v -> Sing v
forall (t :: T). Notes t -> Sing t
notesSing Notes v
r)

-- | Get term-level type of notes.
notesT :: Notes t -> T
notesT :: forall (t :: T). Notes t -> T
notesT = SingT t -> T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (SingT t -> T) -> (Notes t -> SingT t) -> Notes t -> T
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Notes t -> SingT t
forall (t :: T). Notes t -> Sing t
notesSing

-- | Get the term-level type of notes, preserving annotations.
mkUType :: Notes x -> Un.Ty
mkUType :: forall (x :: T). Notes x -> Ty
mkUType = \case
  NTInt TypeAnn
tn        -> T -> TypeAnn -> Ty
Un.Ty T
Un.TInt TypeAnn
tn
  NTNat TypeAnn
tn        -> T -> TypeAnn -> Ty
Un.Ty T
Un.TNat TypeAnn
tn
  NTString TypeAnn
tn     -> T -> TypeAnn -> Ty
Un.Ty T
Un.TString TypeAnn
tn
  NTBytes TypeAnn
tn      -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBytes TypeAnn
tn
  NTMutez TypeAnn
tn      -> T -> TypeAnn -> Ty
Un.Ty T
Un.TMutez TypeAnn
tn
  NTBool TypeAnn
tn       -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBool TypeAnn
tn
  NTKeyHash TypeAnn
tn    -> T -> TypeAnn -> Ty
Un.Ty T
Un.TKeyHash TypeAnn
tn
  NTBls12381Fr TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381Fr TypeAnn
tn
  NTBls12381G1 TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381G1 TypeAnn
tn
  NTBls12381G2 TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381G2 TypeAnn
tn
  NTTimestamp TypeAnn
tn  -> T -> TypeAnn -> Ty
Un.Ty T
Un.TTimestamp TypeAnn
tn
  NTAddress TypeAnn
tn    -> T -> TypeAnn -> Ty
Un.Ty T
Un.TAddress TypeAnn
tn
  NTKey TypeAnn
tn        -> T -> TypeAnn -> Ty
Un.Ty T
Un.TKey TypeAnn
tn
  NTUnit TypeAnn
tn       -> T -> TypeAnn -> Ty
Un.Ty T
Un.TUnit TypeAnn
tn
  NTSignature TypeAnn
tn  -> T -> TypeAnn -> Ty
Un.Ty T
Un.TSignature TypeAnn
tn
  NTChainId TypeAnn
tn    -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChainId TypeAnn
tn
  NTOption TypeAnn
tn Notes t
n   -> T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TOption (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
n) TypeAnn
tn
  NTList TypeAnn
tn Notes t
n     -> T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TList (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
n) TypeAnn
tn
  NTSet TypeAnn
tn Notes t
n      -> T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TSet (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
n) TypeAnn
tn
  NTOperation TypeAnn
tn  -> T -> TypeAnn -> Ty
Un.Ty T
Un.TOperation TypeAnn
tn
  NTChest TypeAnn
tn      -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChest TypeAnn
tn
  NTChestKey TypeAnn
tn   -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChestKey TypeAnn
tn
  NTTxRollupL2Address TypeAnn
tn -> T -> TypeAnn -> Ty
Un.Ty T
Un.TTxRollupL2Address TypeAnn
tn
  NTNever TypeAnn
tn      -> T -> TypeAnn -> Ty
Un.Ty T
Un.TNever TypeAnn
tn
  NTSaplingState TypeAnn
tn Sing n
s -> T -> TypeAnn -> Ty
Un.Ty (Natural -> T
Un.TSaplingState (SingNat n -> Natural
forall (n :: Peano). SingNat n -> Natural
singPeanoVal Sing n
SingNat n
s)) TypeAnn
tn
  NTSaplingTransaction TypeAnn
tn Sing n
s -> T -> TypeAnn -> Ty
Un.Ty (Natural -> T
Un.TSaplingTransaction (SingNat n -> Natural
forall (n :: Peano). SingNat n -> Natural
singPeanoVal Sing n
SingNat n
s)) TypeAnn
tn
  NTContract TypeAnn
tn Notes t
n -> T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TContract (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
n) TypeAnn
tn
  NTTicket TypeAnn
tn Notes t
n   -> T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TTicket (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
n) TypeAnn
tn
  NTPair TypeAnn
tn FieldAnn
fl FieldAnn
fr VarAnn
vl VarAnn
vr Notes p
nl Notes q
nr ->
    T -> TypeAnn -> Ty
Un.Ty (FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Ty -> Ty -> T
Un.TPair FieldAnn
fl FieldAnn
fr VarAnn
vl VarAnn
vr (Notes p -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes p
nl) (Notes q -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes q
nr)) TypeAnn
tn
  NTOr TypeAnn
tn FieldAnn
fl FieldAnn
fr Notes p
nl Notes q
nr -> T -> TypeAnn -> Ty
Un.Ty (FieldAnn -> FieldAnn -> Ty -> Ty -> T
Un.TOr FieldAnn
fl FieldAnn
fr (Notes p -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes p
nl) (Notes q -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes q
nr)) TypeAnn
tn
  NTLambda TypeAnn
tn Notes p
np Notes q
nq   -> T -> TypeAnn -> Ty
Un.Ty (Ty -> Ty -> T
Un.TLambda (Notes p -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes p
np) (Notes q -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes q
nq)) TypeAnn
tn
  NTMap TypeAnn
tn Notes k
nk Notes v
nv      -> T -> TypeAnn -> Ty
Un.Ty (Ty -> Ty -> T
Un.TMap (Notes k -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes k
nk) (Notes v -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes v
nv)) TypeAnn
tn
  NTBigMap TypeAnn
tn Notes k
nk Notes v
nv   -> T -> TypeAnn -> Ty
Un.Ty (Ty -> Ty -> T
Un.TBigMap (Notes k -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes k
nk) (Notes v -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes v
nv)) TypeAnn
tn


-- | In memory of @NStar@ constructor.
--   Generates notes with no annotations.
starNotes :: forall t. SingI t => Notes t
starNotes :: forall (t :: T). SingI t => Notes t
starNotes = Sing t -> Notes t
forall (t :: T). Sing t -> Notes t
starNotes' Sing t
forall {k} (a :: k). SingI a => Sing a
sing

starNotes' :: Sing t -> Notes t
starNotes' :: forall (t :: T). Sing t -> Notes t
starNotes' = \case
  Sing t
SingT t
STInt -> TypeAnn -> Notes 'TInt
NTInt TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STNat -> TypeAnn -> Notes 'TNat
NTNat TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STString -> TypeAnn -> Notes 'TString
NTString TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STBytes -> TypeAnn -> Notes 'TBytes
NTBytes TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STMutez -> TypeAnn -> Notes 'TMutez
NTMutez TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STBool -> TypeAnn -> Notes 'TBool
NTBool TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STKeyHash -> TypeAnn -> Notes 'TKeyHash
NTKeyHash TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STBls12381Fr -> TypeAnn -> Notes 'TBls12381Fr
NTBls12381Fr TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STBls12381G1 -> TypeAnn -> Notes 'TBls12381G1
NTBls12381G1 TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STBls12381G2 -> TypeAnn -> Notes 'TBls12381G2
NTBls12381G2 TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STTimestamp -> TypeAnn -> Notes 'TTimestamp
NTTimestamp TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STAddress -> TypeAnn -> Notes 'TAddress
NTAddress TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STKey -> TypeAnn -> Notes 'TKey
NTKey TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STUnit -> TypeAnn -> Notes 'TUnit
NTUnit TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STTxRollupL2Address -> TypeAnn -> Notes 'TTxRollupL2Address
NTTxRollupL2Address TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STNever -> TypeAnn -> Notes 'TNever
NTNever TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  STSaplingState Sing n
s -> TypeAnn -> Sing n -> Notes ('TSaplingState n)
forall (t :: Peano). TypeAnn -> Sing t -> Notes ('TSaplingState t)
NTSaplingState TypeAnn
forall {k} (a :: k). Annotation a
noAnn Sing n
s
  STSaplingTransaction Sing n
s -> TypeAnn -> Sing n -> Notes ('TSaplingTransaction n)
forall (t :: Peano).
TypeAnn -> Sing t -> Notes ('TSaplingTransaction t)
NTSaplingTransaction TypeAnn
forall {k} (a :: k). Annotation a
noAnn Sing n
s
  Sing t
SingT t
STSignature -> TypeAnn -> Notes 'TSignature
NTSignature TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STChainId -> TypeAnn -> Notes 'TChainId
NTChainId TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STOperation -> TypeAnn -> Notes 'TOperation
NTOperation TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  STSet Sing n
t -> TypeAnn -> Notes n -> Notes ('TSet n)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TSet t)
NTSet TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Notes n -> Notes ('TSet n)) -> Notes n -> Notes ('TSet n)
forall a b. (a -> b) -> a -> b
$ Sing n -> Notes n
forall (t :: T). Sing t -> Notes t
starNotes' Sing n
t
  STList Sing n
t -> TypeAnn -> Notes n -> Notes ('TList n)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TList t)
NTList TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Notes n -> Notes ('TList n)) -> Notes n -> Notes ('TList n)
forall a b. (a -> b) -> a -> b
$ Sing n -> Notes n
forall (t :: T). Sing t -> Notes t
starNotes' Sing n
t
  STOption Sing n
t -> TypeAnn -> Notes n -> Notes ('TOption n)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Notes n -> Notes ('TOption n)) -> Notes n -> Notes ('TOption n)
forall a b. (a -> b) -> a -> b
$ Sing n -> Notes n
forall (t :: T). Sing t -> Notes t
starNotes' Sing n
t
  STContract Sing n
t -> TypeAnn -> Notes n -> Notes ('TContract n)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TContract t)
NTContract TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Notes n -> Notes ('TContract n))
-> Notes n -> Notes ('TContract n)
forall a b. (a -> b) -> a -> b
$ Sing n -> Notes n
forall (t :: T). Sing t -> Notes t
starNotes' Sing n
t
  STTicket Sing n
t -> TypeAnn -> Notes n -> Notes ('TTicket n)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TTicket t)
NTTicket TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Notes n -> Notes ('TTicket n)) -> Notes n -> Notes ('TTicket n)
forall a b. (a -> b) -> a -> b
$ Sing n -> Notes n
forall (t :: T). Sing t -> Notes t
starNotes' Sing n
t
  STMap Sing n1
t Sing n2
t' -> TypeAnn -> Notes n1 -> Notes n2 -> Notes ('TMap n1 n2)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TMap t xs)
NTMap TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Sing n1 -> Notes n1
forall (t :: T). Sing t -> Notes t
starNotes' Sing n1
t) (Sing n2 -> Notes n2
forall (t :: T). Sing t -> Notes t
starNotes' Sing n2
t')
  STBigMap Sing n1
t Sing n2
t' -> TypeAnn -> Notes n1 -> Notes n2 -> Notes ('TBigMap n1 n2)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TBigMap t xs)
NTBigMap TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Sing n1 -> Notes n1
forall (t :: T). Sing t -> Notes t
starNotes' Sing n1
t) (Sing n2 -> Notes n2
forall (t :: T). Sing t -> Notes t
starNotes' Sing n2
t')
  STPair Sing n1
t Sing n2
t' ->
    TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes n1
-> Notes n2
-> Notes ('TPair n1 n2)
forall (t :: T) (xs :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes t
-> Notes xs
-> Notes ('TPair t xs)
NTPair TypeAnn
forall {k} (a :: k). Annotation a
noAnn FieldAnn
forall {k} (a :: k). Annotation a
noAnn FieldAnn
forall {k} (a :: k). Annotation a
noAnn VarAnn
forall {k} (a :: k). Annotation a
noAnn VarAnn
forall {k} (a :: k). Annotation a
noAnn (Sing n1 -> Notes n1
forall (t :: T). Sing t -> Notes t
starNotes' Sing n1
t) (Sing n2 -> Notes n2
forall (t :: T). Sing t -> Notes t
starNotes' Sing n2
t')
  STOr Sing n1
t Sing n2
t' -> TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes n1
-> Notes n2
-> Notes ('TOr n1 n2)
forall (t :: T) (xs :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes t -> Notes xs -> Notes ('TOr t xs)
NTOr TypeAnn
forall {k} (a :: k). Annotation a
noAnn FieldAnn
forall {k} (a :: k). Annotation a
noAnn FieldAnn
forall {k} (a :: k). Annotation a
noAnn (Sing n1 -> Notes n1
forall (t :: T). Sing t -> Notes t
starNotes' Sing n1
t) (Sing n2 -> Notes n2
forall (t :: T). Sing t -> Notes t
starNotes' Sing n2
t')
  STLambda Sing n1
t Sing n2
t' -> TypeAnn -> Notes n1 -> Notes n2 -> Notes ('TLambda n1 n2)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TLambda t xs)
NTLambda TypeAnn
forall {k} (a :: k). Annotation a
noAnn (Sing n1 -> Notes n1
forall (t :: T). Sing t -> Notes t
starNotes' Sing n1
t) (Sing n2 -> Notes n2
forall (t :: T). Sing t -> Notes t
starNotes' Sing n2
t')
  Sing t
SingT t
STChest -> TypeAnn -> Notes 'TChest
NTChest TypeAnn
forall {k} (a :: k). Annotation a
noAnn
  Sing t
SingT t
STChestKey -> TypeAnn -> Notes 'TChestKey
NTChestKey TypeAnn
forall {k} (a :: k). Annotation a
noAnn

-- | Checks if no annotations are present.
isStar :: SingI t => Notes t -> Bool
isStar :: forall (t :: T). SingI t => Notes t -> Bool
isStar = (Notes t -> Notes t -> Bool
forall a. Eq a => a -> a -> Bool
== Notes t
forall (t :: T). SingI t => Notes t
starNotes)

-- | Insert the provided type annotation into the provided notes.
insertTypeAnn :: forall (b :: T). TypeAnn -> Notes b -> Notes b
insertTypeAnn :: forall (b :: T). TypeAnn -> Notes b -> Notes b
insertTypeAnn TypeAnn
nt Notes b
s = case Notes b
s of
  NTInt TypeAnn
_ -> TypeAnn -> Notes 'TInt
NTInt TypeAnn
nt
  NTNat TypeAnn
_ -> TypeAnn -> Notes 'TNat
NTNat TypeAnn
nt
  NTString TypeAnn
_ -> TypeAnn -> Notes 'TString
NTString TypeAnn
nt
  NTBytes TypeAnn
_ -> TypeAnn -> Notes 'TBytes
NTBytes TypeAnn
nt
  NTMutez TypeAnn
_ -> TypeAnn -> Notes 'TMutez
NTMutez TypeAnn
nt
  NTBool TypeAnn
_ -> TypeAnn -> Notes 'TBool
NTBool TypeAnn
nt
  NTKeyHash TypeAnn
_ -> TypeAnn -> Notes 'TKeyHash
NTKeyHash TypeAnn
nt
  NTBls12381Fr TypeAnn
_ -> TypeAnn -> Notes 'TBls12381Fr
NTBls12381Fr TypeAnn
nt
  NTBls12381G1 TypeAnn
_ -> TypeAnn -> Notes 'TBls12381G1
NTBls12381G1 TypeAnn
nt
  NTBls12381G2 TypeAnn
_ -> TypeAnn -> Notes 'TBls12381G2
NTBls12381G2 TypeAnn
nt
  NTTimestamp TypeAnn
_ -> TypeAnn -> Notes 'TTimestamp
NTTimestamp TypeAnn
nt
  NTAddress TypeAnn
_ -> TypeAnn -> Notes 'TAddress
NTAddress TypeAnn
nt
  NTKey TypeAnn
_ -> TypeAnn -> Notes 'TKey
NTKey TypeAnn
nt
  NTUnit TypeAnn
_ -> TypeAnn -> Notes 'TUnit
NTUnit TypeAnn
nt
  NTSignature TypeAnn
_ -> TypeAnn -> Notes 'TSignature
NTSignature TypeAnn
nt
  NTOption TypeAnn
_ Notes t
n1  -> TypeAnn -> Notes t -> Notes ('TOption t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
nt Notes t
n1
  NTList TypeAnn
_ Notes t
n1 -> TypeAnn -> Notes t -> Notes ('TList t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TList t)
NTList TypeAnn
nt Notes t
n1
  NTSet TypeAnn
_ Notes t
n1 -> TypeAnn -> Notes t -> Notes ('TSet t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TSet t)
NTSet TypeAnn
nt Notes t
n1
  NTOperation TypeAnn
_ -> TypeAnn -> Notes 'TOperation
NTOperation TypeAnn
nt
  NTContract TypeAnn
_ Notes t
n1 -> TypeAnn -> Notes t -> Notes ('TContract t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TContract t)
NTContract TypeAnn
nt Notes t
n1
  NTTicket TypeAnn
_ Notes t
n1 -> TypeAnn -> Notes t -> Notes ('TTicket t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TTicket t)
NTTicket TypeAnn
nt Notes t
n1
  NTPair TypeAnn
_ FieldAnn
n1 FieldAnn
n2 VarAnn
n3 VarAnn
n4 Notes p
n5 Notes q
n6 -> TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes q
-> Notes ('TPair p q)
forall (t :: T) (xs :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes t
-> Notes xs
-> Notes ('TPair t xs)
NTPair TypeAnn
nt FieldAnn
n1 FieldAnn
n2 VarAnn
n3 VarAnn
n4 Notes p
n5 Notes q
n6
  NTOr TypeAnn
_ FieldAnn
n1 FieldAnn
n2 Notes p
n3 Notes q
n4 -> TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q)
forall (t :: T) (xs :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes t -> Notes xs -> Notes ('TOr t xs)
NTOr TypeAnn
nt FieldAnn
n1 FieldAnn
n2 Notes p
n3 Notes q
n4
  NTLambda TypeAnn
_ Notes p
n1 Notes q
n2 -> TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TLambda t xs)
NTLambda TypeAnn
nt Notes p
n1 Notes q
n2
  NTMap TypeAnn
_ Notes k
n1 Notes v
n2 -> TypeAnn -> Notes k -> Notes v -> Notes ('TMap k v)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TMap t xs)
NTMap TypeAnn
nt Notes k
n1 Notes v
n2
  NTBigMap TypeAnn
_ Notes k
n1 Notes v
n2 -> TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
forall (t :: T) (xs :: T).
TypeAnn -> Notes t -> Notes xs -> Notes ('TBigMap t xs)
NTBigMap TypeAnn
nt Notes k
n1 Notes v
n2
  NTChainId TypeAnn
_ -> TypeAnn -> Notes 'TChainId
NTChainId TypeAnn
nt
  NTChest TypeAnn
_ -> TypeAnn -> Notes 'TChest
NTChest TypeAnn
nt
  NTChestKey TypeAnn
_ -> TypeAnn -> Notes 'TChestKey
NTChestKey TypeAnn
nt
  NTTxRollupL2Address TypeAnn
_ -> TypeAnn -> Notes 'TTxRollupL2Address
NTTxRollupL2Address TypeAnn
nt
  NTNever TypeAnn
_ -> TypeAnn -> Notes 'TNever
NTNever TypeAnn
nt
  NTSaplingState TypeAnn
_ Sing n
n -> TypeAnn -> Sing n -> Notes ('TSaplingState n)
forall (t :: Peano). TypeAnn -> Sing t -> Notes ('TSaplingState t)
NTSaplingState TypeAnn
nt Sing n
n
  NTSaplingTransaction TypeAnn
_ Sing n
n -> TypeAnn -> Sing n -> Notes ('TSaplingTransaction n)
forall (t :: Peano).
TypeAnn -> Sing t -> Notes ('TSaplingTransaction t)
NTSaplingTransaction TypeAnn
nt Sing n
n

-- | A typed heterogenous list of annotations. Simplified pattern synonyms for
-- common use cases are provided.
data Anns xs where
  AnnsCons :: Typeable tag => !(Annotation tag) -> Anns xs -> Anns (Annotation tag ': xs)
  AnnsTyCons :: SingI t => !(Notes t) -> Anns xs -> Anns (Notes t ': xs)
  AnnsNil :: Anns '[]

infixr 5 `AnnsCons`
infixr 5 `AnnsTyCons`

deriveGADTNFData ''Anns

deriving stock instance (Each '[Show] rs) => Show (Anns rs)
deriving stock instance (Eq r, Eq (Anns rs)) => Eq (Anns (r ': rs))

instance Eq (Anns '[]) where
  Anns '[]
AnnsNil == :: Anns '[] -> Anns '[] -> Bool
== Anns '[]
AnnsNil = Bool
True

-- | 'Anns' only containing a single 'VarAnn'.
type AnnVar = Anns '[VarAnn]

instance Default (Anns '[]) where
  def :: Anns '[]
def = Anns '[]
AnnsNil

instance (Typeable tag, Default (Anns xs)) => Default (Anns (Annotation tag ': xs)) where
  def :: Anns (Annotation tag : xs)
def = Annotation tag
forall {k} (a :: k). Annotation a
noAnn Annotation tag -> Anns xs -> Anns (Annotation tag : xs)
forall {t} (xs :: t) (xs :: [*]).
Typeable xs =>
Annotation xs -> Anns xs -> Anns (Annotation xs : xs)
`AnnsCons` Anns xs
forall a. Default a => a
def

instance (SingI t, Default (Anns xs)) => Default (Anns (Notes t ': xs)) where
  def :: Anns (Notes t : xs)
def = Notes t
forall (t :: T). SingI t => Notes t
starNotes Notes t -> Anns xs -> Anns (Notes t : xs)
forall (t :: T) (xs :: [*]).
SingI t =>
Notes t -> Anns xs -> Anns (Notes t : xs)
`AnnsTyCons` Anns xs
forall a. Default a => a
def

type family AnnotateInstrArg (xs :: [Type]) r where
  AnnotateInstrArg (Notes _ ': xs) r = Un.Ty -> AnnotateInstrArg xs r
  AnnotateInstrArg (x ': xs) r = x -> AnnotateInstrArg xs r
  AnnotateInstrArg '[] r = r

-- | Utility typeclass to simplify extracting annotations from 'Anns' and
-- passing those as arguments to an untyped instruction data constructor.
class AnnotateInstr (xs :: [Type]) r where
  annotateInstr :: Anns xs -> AnnotateInstrArg xs r -> r

instance AnnotateInstr '[] r where
  annotateInstr :: Anns '[] -> AnnotateInstrArg '[] r -> r
annotateInstr (Anns '[]
AnnsNil) AnnotateInstrArg '[] r
c = r
AnnotateInstrArg '[] r
c

instance AnnotateInstr xs r => AnnotateInstr (Annotation tag ': xs) r where
  annotateInstr :: Anns (Annotation tag : xs)
-> AnnotateInstrArg (Annotation tag : xs) r -> r
annotateInstr (AnnsCons Annotation tag
va Anns xs
xs) AnnotateInstrArg (Annotation tag : xs) r
c = forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr @_ @r Anns xs
xs (AnnotateInstrArg xs r -> r) -> AnnotateInstrArg xs r -> r
forall a b. (a -> b) -> a -> b
$ AnnotateInstrArg (Annotation tag : xs) r
Annotation tag -> AnnotateInstrArg xs r
c Annotation tag
va

instance AnnotateInstr xs r => AnnotateInstr (Notes t ': xs) r where
  annotateInstr :: Anns (Notes t : xs) -> AnnotateInstrArg (Notes t : xs) r -> r
annotateInstr (AnnsTyCons Notes t
va Anns xs
xs) AnnotateInstrArg (Notes t : xs) r
c = forall (xs :: [*]) r.
AnnotateInstr xs r =>
Anns xs -> AnnotateInstrArg xs r -> r
annotateInstr @_ @r Anns xs
xs (AnnotateInstrArg xs r -> r) -> AnnotateInstrArg xs r -> r
forall a b. (a -> b) -> a -> b
$ AnnotateInstrArg (Notes t : xs) r
Ty -> AnnotateInstrArg xs r
c (Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
va)

-- | Convenience pattern synonym matching a single simple annotation.
pattern Anns1 :: Typeable a => Annotation a -> Anns '[Annotation a]
pattern $bAnns1 :: forall {k} (a :: k).
Typeable a =>
Annotation a -> Anns '[Annotation a]
$mAnns1 :: forall {r} {k} {a :: k}.
Typeable a =>
Anns '[Annotation a] -> (Annotation a -> r) -> (Void# -> r) -> r
Anns1 x = x `AnnsCons` AnnsNil

-- | Convenience pattern synonym matching two simple annotations.
pattern Anns2
  :: Each '[Typeable] '[a, b]
  => Annotation a
  -> Annotation b
  -> Anns '[Annotation a, Annotation b]
pattern $bAnns2 :: forall {k} (a :: k) (b :: k).
Each '[Typeable] '[a, b] =>
Annotation a -> Annotation b -> Anns '[Annotation a, Annotation b]
$mAnns2 :: forall {r} {k} {a :: k} {b :: k}.
Each '[Typeable] '[a, b] =>
Anns '[Annotation a, Annotation b]
-> (Annotation a -> Annotation b -> r) -> (Void# -> r) -> r
Anns2 x y = x `AnnsCons` y `AnnsCons` AnnsNil

-- | Convenience pattern synonym matching two annotations, first being
-- a simple one, the second being 'Notes', corresponding to an annotated
-- type.
pattern Anns2' :: (Typeable a, SingI t) => Annotation a -> Notes t -> Anns '[Annotation a, Notes t]
pattern $bAnns2' :: forall {k} (a :: k) (t :: T).
(Typeable a, SingI t) =>
Annotation a -> Notes t -> Anns '[Annotation a, Notes t]
$mAnns2' :: forall {r} {k} {a :: k} {t :: T}.
(Typeable a, SingI t) =>
Anns '[Annotation a, Notes t]
-> (Annotation a -> Notes t -> r) -> (Void# -> r) -> r
Anns2' x y = x `AnnsCons` y `AnnsTyCons` AnnsNil

-- | Convenience pattern synonym matching three simple annotations.
pattern Anns3
  :: Each '[Typeable] '[a, b, c]
  => Annotation a
  -> Annotation b
  -> Annotation c
  -> Anns '[Annotation a, Annotation b, Annotation c]
pattern $bAnns3 :: forall {k} (a :: k) (b :: k) (c :: k).
Each '[Typeable] '[a, b, c] =>
Annotation a
-> Annotation b
-> Annotation c
-> Anns '[Annotation a, Annotation b, Annotation c]
$mAnns3 :: forall {r} {k} {a :: k} {b :: k} {c :: k}.
Each '[Typeable] '[a, b, c] =>
Anns '[Annotation a, Annotation b, Annotation c]
-> (Annotation a -> Annotation b -> Annotation c -> r)
-> (Void# -> r)
-> r
Anns3 x y z = x `AnnsCons` y `AnnsCons` z `AnnsCons` AnnsNil

-- | Convenience pattern synonym matching three annotations, first two being
-- simple, the last one being 'Notes', corresponding to an annotated
-- type.
pattern Anns3'
  :: (Each '[Typeable] '[a, b], SingI t)
  => Annotation a
  -> Annotation b
  -> Notes t
  -> Anns '[Annotation a, Annotation b, Notes t]
pattern $bAnns3' :: forall {k} (a :: k) (b :: k) (t :: T).
(Each '[Typeable] '[a, b], SingI t) =>
Annotation a
-> Annotation b
-> Notes t
-> Anns '[Annotation a, Annotation b, Notes t]
$mAnns3' :: forall {r} {k} {a :: k} {b :: k} {t :: T}.
(Each '[Typeable] '[a, b], SingI t) =>
Anns '[Annotation a, Annotation b, Notes t]
-> (Annotation a -> Annotation b -> Notes t -> r)
-> (Void# -> r)
-> r
Anns3' x y z = x `AnnsCons` y `AnnsCons` z `AnnsTyCons` AnnsNil

-- | Convenience pattern synonym matching three annotations, first being
-- a simple one, the last two being 'Notes', corresponding to annotated
-- types.
pattern Anns3''
  :: (Typeable a, SingI t, SingI u)
  => Annotation a
  -> Notes t
  -> Notes u
  -> Anns '[Annotation a, Notes t, Notes u]
pattern $bAnns3'' :: forall {k} (a :: k) (t :: T) (u :: T).
(Typeable a, SingI t, SingI u) =>
Annotation a
-> Notes t -> Notes u -> Anns '[Annotation a, Notes t, Notes u]
$mAnns3'' :: forall {r} {k} {a :: k} {t :: T} {u :: T}.
(Typeable a, SingI t, SingI u) =>
Anns '[Annotation a, Notes t, Notes u]
-> (Annotation a -> Notes t -> Notes u -> r) -> (Void# -> r) -> r
Anns3'' x y z = x `AnnsCons` y `AnnsTyCons` z `AnnsTyCons` AnnsNil

-- | Convenience pattern synonym matching four simple annotations.
pattern Anns4
  :: Each '[Typeable] '[a, b, c, d]
  => Annotation a
  -> Annotation b
  -> Annotation c
  -> Annotation d
  -> Anns '[Annotation a, Annotation b, Annotation c, Annotation d]
pattern $bAnns4 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
Each '[Typeable] '[a, b, c, d] =>
Annotation a
-> Annotation b
-> Annotation c
-> Annotation d
-> Anns '[Annotation a, Annotation b, Annotation c, Annotation d]
$mAnns4 :: forall {r} {k} {a :: k} {b :: k} {c :: k} {d :: k}.
Each '[Typeable] '[a, b, c, d] =>
Anns '[Annotation a, Annotation b, Annotation c, Annotation d]
-> (Annotation a
    -> Annotation b -> Annotation c -> Annotation d -> r)
-> (Void# -> r)
-> r
Anns4 x y z w = x `AnnsCons` y `AnnsCons` z `AnnsCons` w `AnnsCons` AnnsNil

-- | Convenience pattern synonym matching four annotations, first two being
-- simple, the last two being 'Notes', corresponding to annotated
-- types.
pattern Anns4''
  :: (Each '[Typeable] '[a, b], SingI t, SingI u)
  => Annotation a
  -> Annotation b
  -> Notes t
  -> Notes u
  -> Anns '[Annotation a, Annotation b, Notes t, Notes u]
pattern $bAnns4'' :: forall {k} (a :: k) (b :: k) (t :: T) (u :: T).
(Each '[Typeable] '[a, b], SingI t, SingI u) =>
Annotation a
-> Annotation b
-> Notes t
-> Notes u
-> Anns '[Annotation a, Annotation b, Notes t, Notes u]
$mAnns4'' :: forall {r} {k} {a :: k} {b :: k} {t :: T} {u :: T}.
(Each '[Typeable] '[a, b], SingI t, SingI u) =>
Anns '[Annotation a, Annotation b, Notes t, Notes u]
-> (Annotation a -> Annotation b -> Notes t -> Notes u -> r)
-> (Void# -> r)
-> r
Anns4'' x y z w
  = x `AnnsCons` y `AnnsCons` z `AnnsTyCons` w `AnnsTyCons` AnnsNil

-- | Convenience pattern synonym matching five annotations, first four being
-- simple, the last one being 'Notes', corresponding to an annotated
-- type.
pattern Anns5'
  :: (Each '[Typeable] '[a, b, c, d], SingI t)
  => Annotation a
  -> Annotation b
  -> Annotation c
  -> Annotation d
  -> Notes t
  -> Anns '[Annotation a, Annotation b, Annotation c, Annotation d, Notes t]
pattern $bAnns5' :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (t :: T).
(Each '[Typeable] '[a, b, c, d], SingI t) =>
Annotation a
-> Annotation b
-> Annotation c
-> Annotation d
-> Notes t
-> Anns
     '[Annotation a, Annotation b, Annotation c, Annotation d, Notes t]
$mAnns5' :: forall {r} {k} {a :: k} {b :: k} {c :: k} {d :: k} {t :: T}.
(Each '[Typeable] '[a, b, c, d], SingI t) =>
Anns
  '[Annotation a, Annotation b, Annotation c, Annotation d, Notes t]
-> (Annotation a
    -> Annotation b -> Annotation c -> Annotation d -> Notes t -> r)
-> (Void# -> r)
-> r
Anns5' x y z v w
  = x `AnnsCons` y `AnnsCons` z `AnnsCons` v `AnnsCons` w `AnnsTyCons` AnnsNil

{-# COMPLETE Anns1 #-}
{-# COMPLETE Anns2 #-}
{-# COMPLETE Anns2' #-}
{-# COMPLETE Anns3 #-}
{-# COMPLETE Anns3' #-}
{-# COMPLETE Anns3'' #-}
{-# COMPLETE Anns4 #-}
{-# COMPLETE Anns4'' #-}
{-# COMPLETE Anns5' #-}