-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | 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 type class 'Converge' along with 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 @*@ leafs with type or/and field
-- annotations.

module Michelson.Typed.Annotation
  ( Notes (..)
  , AnnConvergeError(..)
  , converge
  , convergeAnns
  , convergeDestrAnns
  , insertTypeAnn
  , isStar
  , starNotes
  , notesSing
  , notesT
  ) where

import qualified Data.Kind as Kind
import Data.Singletons (Sing, SingI(..))
import Fmt (Buildable(..), (+|), (|+))
import Text.PrettyPrint.Leijen.Text (Doc, (<+>))
import qualified Text.Show

import Michelson.Printer.Util
  (RenderDoc(..), addParens, buildRenderDoc, doesntNeedParens, needsParens, printDocS)
import Michelson.Typed.Sing
import Michelson.Typed.T (T(..))
import Michelson.Untyped.Annotation
  (Annotation, FieldAnn, TypeAnn, VarAnn, convergeVarAnns, fullAnnSet, noAnn, singleAnnSet, unifyAnn, unifyPairFieldAnn)
import Util.TH
import Util.Typeable

-- | 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)
  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
  NTNever     :: TypeAnn -> Notes 'TNever

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


instance Show (Notes t) where
  show :: Notes t -> String
show = Bool -> Doc -> String
printDocS Bool
True (Doc -> String) -> (Notes t -> Doc) -> Notes t -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RenderContext -> Notes t -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
doesntNeedParens

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 pn :: RenderContext
pn n :: Notes t
n = RenderContext -> Doc -> Doc
addParens RenderContext
pn (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ case Notes t
n of
    NTInt ta :: TypeAnn
ta                -> "NTInt" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTNat ta :: TypeAnn
ta                -> "NTNat" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTString ta :: TypeAnn
ta             -> "NTString" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTBytes ta :: TypeAnn
ta              -> "NTBytes" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTMutez ta :: TypeAnn
ta              -> "NTMutez" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTBool ta :: TypeAnn
ta               -> "NTBool" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTKeyHash ta :: TypeAnn
ta            -> "NTKeyHash" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTBls12381Fr ta :: TypeAnn
ta         -> "NTBls12381Fr" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTBls12381G1 ta :: TypeAnn
ta         -> "NTBls12381G1" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTBls12381G2 ta :: TypeAnn
ta         -> "NTBls12381G2" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTTimestamp ta :: TypeAnn
ta          -> "NTTimestamp" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTAddress ta :: TypeAnn
ta            -> "NTAddress" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTKey ta :: TypeAnn
ta                -> "NTKey" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTUnit ta :: TypeAnn
ta               -> "NTUnit" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTSignature ta :: TypeAnn
ta          -> "NTSignature" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTChainId ta :: TypeAnn
ta            -> "NTChainId" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTNever ta :: TypeAnn
ta              -> "NTNever" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTOption ta :: TypeAnn
ta nt :: Notes t
nt          -> "NTOption" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta Doc -> Doc -> Doc
<+> Notes t -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes t
nt
    NTList ta :: TypeAnn
ta nt :: Notes t
nt            -> "NTList" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta Doc -> Doc -> Doc
<+> Notes t -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes t
nt
    NTSet ta :: TypeAnn
ta nt :: Notes t
nt             -> "NTSet" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta Doc -> Doc -> Doc
<+> Notes t -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes t
nt
    NTOperation ta :: TypeAnn
ta          -> "NTOperation" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta
    NTContract ta :: TypeAnn
ta nt :: Notes t
nt        -> "NTContract" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta Doc -> Doc -> Doc
<+> Notes t -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes t
nt
    NTPair ta :: TypeAnn
ta fa1 :: FieldAnn
fa1 fa2 :: FieldAnn
fa2 va1 :: VarAnn
va1 va2 :: VarAnn
va2 np :: Notes p
np nq :: Notes q
nq -> "NTPair" Doc -> Doc -> Doc
<+> TypeAnn -> FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Doc
rendTFV2 TypeAnn
ta FieldAnn
fa1 FieldAnn
fa2 VarAnn
va1 VarAnn
va2 Doc -> Doc -> Doc
<+> Notes p -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes p
np Doc -> Doc -> Doc
<+> Notes q -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes q
nq
    NTOr ta :: TypeAnn
ta fa1 :: FieldAnn
fa1 fa2 :: FieldAnn
fa2 np :: Notes p
np nq :: Notes q
nq   -> "NTOr" Doc -> Doc -> Doc
<+> TypeAnn -> FieldAnn -> FieldAnn -> Doc
rendTF2 TypeAnn
ta FieldAnn
fa1 FieldAnn
fa2 Doc -> Doc -> Doc
<+> Notes p -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes p
np Doc -> Doc -> Doc
<+> Notes q -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes q
nq
    NTLambda ta :: TypeAnn
ta np :: Notes p
np nq :: Notes q
nq       -> "NTLambda" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta Doc -> Doc -> Doc
<+> Notes p -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes p
np Doc -> Doc -> Doc
<+> Notes q -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes q
nq
    NTMap ta :: TypeAnn
ta np :: Notes k
np nq :: Notes v
nq          -> "NTMap" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta Doc -> Doc -> Doc
<+> Notes k -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes k
np Doc -> Doc -> Doc
<+> Notes v -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes v
nq
    NTBigMap ta :: TypeAnn
ta np :: Notes k
np nq :: Notes v
nq       -> "NTBigMap" Doc -> Doc -> Doc
<+> TypeAnn -> Doc
rendT TypeAnn
ta Doc -> Doc -> Doc
<+> Notes k -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes k
np Doc -> Doc -> Doc
<+> Notes v -> Doc
forall (n :: T). Notes n -> Doc
rendN Notes v
nq
    where
      rendN :: Notes n -> Doc
      rendN :: Notes n -> Doc
rendN = RenderContext -> Notes n -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
needsParens

      rendT :: TypeAnn -> Doc
      rendT :: TypeAnn -> Doc
rendT = RenderContext -> AnnotationSet -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
doesntNeedParens (AnnotationSet -> Doc)
-> (TypeAnn -> AnnotationSet) -> TypeAnn -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeAnn -> AnnotationSet
forall tag. KnownAnnTag tag => Annotation tag -> AnnotationSet
singleAnnSet

      rendTF2 :: TypeAnn -> FieldAnn -> FieldAnn -> Doc
      rendTF2 :: TypeAnn -> FieldAnn -> FieldAnn -> Doc
rendTF2 t :: TypeAnn
t f1 :: FieldAnn
f1 f2 :: FieldAnn
f2 = RenderContext -> AnnotationSet -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
doesntNeedParens (AnnotationSet -> Doc) -> AnnotationSet -> Doc
forall a b. (a -> b) -> a -> b
$ [TypeAnn] -> [FieldAnn] -> [VarAnn] -> AnnotationSet
fullAnnSet [TypeAnn
t] [FieldAnn
f1, FieldAnn
f2] []

      rendTFV2 :: TypeAnn -> FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Doc
      rendTFV2 :: TypeAnn -> FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Doc
rendTFV2 t :: TypeAnn
t f1 :: FieldAnn
f1 f2 :: FieldAnn
f2 v1 :: VarAnn
v1 v2 :: VarAnn
v2 = RenderContext -> AnnotationSet -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
doesntNeedParens (AnnotationSet -> Doc) -> AnnotationSet -> Doc
forall a b. (a -> b) -> a -> b
$ [TypeAnn] -> [FieldAnn] -> [VarAnn] -> AnnotationSet
fullAnnSet [TypeAnn
t] [FieldAnn
f1, FieldAnn
f2] [VarAnn
v1, VarAnn
v2]

-- | Forget information about annotations, pick singleton with the same type.
--
-- Note: currently we cannot derive 'Sing' from 'Notes' without 'SingI' because
-- for comparable types notes do not remember which exact comparable was used.
notesSing :: SingI t => Notes t -> Sing t
notesSing :: Notes t -> Sing t
notesSing _ = Sing t
forall k (a :: k). SingI a => Sing a
sing

-- | Get term-level type of notes.
notesT :: SingI t => Notes t -> T
notesT :: Notes t -> T
notesT = SingT t -> T
forall (a :: T). Sing a -> T
fromSingT (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). SingI t => Notes t -> Sing t
notesSing

-- | In memory of `NStar` constructor.
--   Generates notes with no annotations.
starNotes :: forall t. SingI t => Notes t
starNotes :: Notes t
starNotes = case SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @t of
  STInt -> TypeAnn -> Notes 'TInt
NTInt TypeAnn
forall k (a :: k). Annotation a
noAnn
  STNat -> TypeAnn -> Notes 'TNat
NTNat TypeAnn
forall k (a :: k). Annotation a
noAnn
  STString -> TypeAnn -> Notes 'TString
NTString TypeAnn
forall k (a :: k). Annotation a
noAnn
  STBytes -> TypeAnn -> Notes 'TBytes
NTBytes TypeAnn
forall k (a :: k). Annotation a
noAnn
  STMutez -> TypeAnn -> Notes 'TMutez
NTMutez TypeAnn
forall k (a :: k). Annotation a
noAnn
  STBool -> TypeAnn -> Notes 'TBool
NTBool TypeAnn
forall k (a :: k). Annotation a
noAnn
  STKeyHash -> TypeAnn -> Notes 'TKeyHash
NTKeyHash TypeAnn
forall k (a :: k). Annotation a
noAnn
  STBls12381Fr -> TypeAnn -> Notes 'TBls12381Fr
NTBls12381Fr TypeAnn
forall k (a :: k). Annotation a
noAnn
  STBls12381G1 -> TypeAnn -> Notes 'TBls12381G1
NTBls12381G1 TypeAnn
forall k (a :: k). Annotation a
noAnn
  STBls12381G2 -> TypeAnn -> Notes 'TBls12381G2
NTBls12381G2 TypeAnn
forall k (a :: k). Annotation a
noAnn
  STTimestamp -> TypeAnn -> Notes 'TTimestamp
NTTimestamp TypeAnn
forall k (a :: k). Annotation a
noAnn
  STAddress -> TypeAnn -> Notes 'TAddress
NTAddress TypeAnn
forall k (a :: k). Annotation a
noAnn
  STKey -> TypeAnn -> Notes 'TKey
NTKey TypeAnn
forall k (a :: k). Annotation a
noAnn
  STUnit -> TypeAnn -> Notes 'TUnit
NTUnit TypeAnn
forall k (a :: k). Annotation a
noAnn
  STNever -> TypeAnn -> Notes 'TNever
NTNever TypeAnn
forall k (a :: k). Annotation a
noAnn
  STSignature -> TypeAnn -> Notes 'TSignature
NTSignature TypeAnn
forall k (a :: k). Annotation a
noAnn
  STChainId -> TypeAnn -> Notes 'TChainId
NTChainId TypeAnn
forall k (a :: k). Annotation a
noAnn
  STOperation -> TypeAnn -> Notes 'TOperation
NTOperation TypeAnn
forall k (a :: k). Annotation a
noAnn
  STSet _ -> TypeAnn -> Notes a -> Notes ('TSet a)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TSet t)
NTSet TypeAnn
forall k (a :: k). Annotation a
noAnn Notes a
forall (t :: T). SingI t => Notes t
starNotes
  STList _ -> TypeAnn -> Notes a -> Notes ('TList a)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TList t)
NTList TypeAnn
forall k (a :: k). Annotation a
noAnn Notes a
forall (t :: T). SingI t => Notes t
starNotes
  STOption _ -> TypeAnn -> Notes a -> Notes ('TOption a)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall k (a :: k). Annotation a
noAnn Notes a
forall (t :: T). SingI t => Notes t
starNotes
  STContract _ -> TypeAnn -> Notes a -> Notes ('TContract a)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TContract t)
NTContract TypeAnn
forall k (a :: k). Annotation a
noAnn Notes a
forall (t :: T). SingI t => Notes t
starNotes
  STMap _ _ -> TypeAnn -> Notes a -> Notes b -> Notes ('TMap a b)
forall (q :: T) (k :: T).
TypeAnn -> Notes q -> Notes k -> Notes ('TMap q k)
NTMap TypeAnn
forall k (a :: k). Annotation a
noAnn Notes a
forall (t :: T). SingI t => Notes t
starNotes Notes b
forall (t :: T). SingI t => Notes t
starNotes
  STBigMap _ _ -> TypeAnn -> Notes a -> Notes b -> Notes ('TBigMap a b)
forall (k :: T) (v :: T).
TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
NTBigMap TypeAnn
forall k (a :: k). Annotation a
noAnn Notes a
forall (t :: T). SingI t => Notes t
starNotes Notes b
forall (t :: T). SingI t => Notes t
starNotes
  STPair _ _ -> TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes a
-> Notes b
-> Notes ('TPair a b)
forall (p :: T) (p :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes p
-> Notes ('TPair p p)
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 Notes a
forall (t :: T). SingI t => Notes t
starNotes Notes b
forall (t :: T). SingI t => Notes t
starNotes
  STOr _ _ -> TypeAnn
-> FieldAnn -> FieldAnn -> Notes a -> Notes b -> Notes ('TOr a b)
forall (p :: T) (p :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes p -> Notes ('TOr p p)
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 Notes a
forall (t :: T). SingI t => Notes t
starNotes Notes b
forall (t :: T). SingI t => Notes t
starNotes
  STLambda _ _ -> TypeAnn -> Notes a -> Notes b -> Notes ('TLambda a b)
forall (p :: T) (q :: T).
TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
NTLambda TypeAnn
forall k (a :: k). Annotation a
noAnn Notes a
forall (t :: T). SingI t => Notes t
starNotes Notes b
forall (t :: T). SingI t => Notes t
starNotes

-- | Checks if no annotations are present.
isStar :: SingI t => Notes t -> Bool
isStar :: 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)

-- | Combines 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 empty leaves with type or/and field annotations.
converge :: Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge :: Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge n1 :: Notes t
n1 n2 :: Notes t
n2 = case (Notes t
n1, Notes t
n2) of
  (NTInt a :: TypeAnn
a, NTInt b :: TypeAnn
b) -> TypeAnn -> Notes 'TInt
NTInt (TypeAnn -> Notes 'TInt)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TInt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTNat a :: TypeAnn
a, NTNat b :: TypeAnn
b) -> TypeAnn -> Notes 'TNat
NTNat (TypeAnn -> Notes 'TNat)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TNat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTString a :: TypeAnn
a, NTString b :: TypeAnn
b) -> TypeAnn -> Notes 'TString
NTString (TypeAnn -> Notes 'TString)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TString)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTBytes a :: TypeAnn
a, NTBytes b :: TypeAnn
b) -> TypeAnn -> Notes 'TBytes
NTBytes (TypeAnn -> Notes 'TBytes)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TBytes)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTMutez a :: TypeAnn
a, NTMutez b :: TypeAnn
b) -> TypeAnn -> Notes 'TMutez
NTMutez (TypeAnn -> Notes 'TMutez)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TMutez)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTBool a :: TypeAnn
a, NTBool b :: TypeAnn
b) -> TypeAnn -> Notes 'TBool
NTBool (TypeAnn -> Notes 'TBool)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTKeyHash a :: TypeAnn
a, NTKeyHash b :: TypeAnn
b) -> TypeAnn -> Notes 'TKeyHash
NTKeyHash (TypeAnn -> Notes 'TKeyHash)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TKeyHash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTBls12381Fr a :: TypeAnn
a, NTBls12381Fr b :: TypeAnn
b) -> TypeAnn -> Notes 'TBls12381Fr
NTBls12381Fr (TypeAnn -> Notes 'TBls12381Fr)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TBls12381Fr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTBls12381G1 a :: TypeAnn
a, NTBls12381G1 b :: TypeAnn
b) -> TypeAnn -> Notes 'TBls12381G1
NTBls12381G1 (TypeAnn -> Notes 'TBls12381G1)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TBls12381G1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTBls12381G2 a :: TypeAnn
a, NTBls12381G2 b :: TypeAnn
b) -> TypeAnn -> Notes 'TBls12381G2
NTBls12381G2 (TypeAnn -> Notes 'TBls12381G2)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TBls12381G2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTTimestamp a :: TypeAnn
a, NTTimestamp b :: TypeAnn
b) -> TypeAnn -> Notes 'TTimestamp
NTTimestamp (TypeAnn -> Notes 'TTimestamp)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TTimestamp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTAddress a :: TypeAnn
a, NTAddress b :: TypeAnn
b) -> TypeAnn -> Notes 'TAddress
NTAddress (TypeAnn -> Notes 'TAddress)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TAddress)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTKey a :: TypeAnn
a, NTKey b :: TypeAnn
b) -> TypeAnn -> Notes 'TKey
NTKey (TypeAnn -> Notes 'TKey)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TKey)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTUnit a :: TypeAnn
a, NTUnit b :: TypeAnn
b) -> TypeAnn -> Notes 'TUnit
NTUnit (TypeAnn -> Notes 'TUnit)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TUnit)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTNever a :: TypeAnn
a, NTNever b :: TypeAnn
b) -> TypeAnn -> Notes 'TNever
NTNever (TypeAnn -> Notes 'TNever)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TNever)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTSignature a :: TypeAnn
a, NTSignature b :: TypeAnn
b) ->
    TypeAnn -> Notes 'TSignature
NTSignature (TypeAnn -> Notes 'TSignature)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TSignature)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTChainId a :: TypeAnn
a, NTChainId b :: TypeAnn
b) ->
    TypeAnn -> Notes 'TChainId
NTChainId (TypeAnn -> Notes 'TChainId)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TChainId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTOption a :: TypeAnn
a n :: Notes t
n, NTOption b :: TypeAnn
b m :: Notes t
m) ->
    TypeAnn -> Notes t -> Notes ('TOption t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption (TypeAnn -> Notes t -> Notes ('TOption t))
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes t -> Notes ('TOption t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b Either AnnConvergeError (Notes t -> Notes ('TOption t))
-> Either AnnConvergeError (Notes t)
-> Either AnnConvergeError (Notes ('TOption t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes t -> Notes t -> Either AnnConvergeError (Notes t)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes t
n Notes t
Notes t
m
  (NTList a :: TypeAnn
a n :: Notes t
n, NTList b :: TypeAnn
b m :: Notes t
m) ->
    TypeAnn -> Notes t -> Notes ('TList t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TList t)
NTList (TypeAnn -> Notes t -> Notes ('TList t))
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes t -> Notes ('TList t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b Either AnnConvergeError (Notes t -> Notes ('TList t))
-> Either AnnConvergeError (Notes t)
-> Either AnnConvergeError (Notes ('TList t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes t -> Notes t -> Either AnnConvergeError (Notes t)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes t
n Notes t
Notes t
m
  (NTSet a :: TypeAnn
a n :: Notes t
n, NTSet b :: TypeAnn
b m :: Notes t
m) ->
    TypeAnn -> Notes t -> Notes ('TSet t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TSet t)
NTSet (TypeAnn -> Notes t -> Notes ('TSet t))
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes t -> Notes ('TSet t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b Either AnnConvergeError (Notes t -> Notes ('TSet t))
-> Either AnnConvergeError (Notes t)
-> Either AnnConvergeError (Notes ('TSet t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes t -> Notes t -> Either AnnConvergeError (Notes t)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes t
n Notes t
Notes t
m
  (NTOperation a :: TypeAnn
a, NTOperation b :: TypeAnn
b) ->
    TypeAnn -> Notes 'TOperation
NTOperation (TypeAnn -> Notes 'TOperation)
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes 'TOperation)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
  (NTContract a :: TypeAnn
a n :: Notes t
n, NTContract b :: TypeAnn
b m :: Notes t
m) ->
    TypeAnn -> Notes t -> Notes ('TContract t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TContract t)
NTContract (TypeAnn -> Notes t -> Notes ('TContract t))
-> Either AnnConvergeError TypeAnn
-> Either AnnConvergeError (Notes t -> Notes ('TContract t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b Either AnnConvergeError (Notes t -> Notes ('TContract t))
-> Either AnnConvergeError (Notes t)
-> Either AnnConvergeError (Notes ('TContract t))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes t -> Notes t -> Either AnnConvergeError (Notes t)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes t
n Notes t
Notes t
m
  (NTPair a :: TypeAnn
a pF :: FieldAnn
pF qF :: FieldAnn
qF pV :: VarAnn
pV qV :: VarAnn
qV pN :: Notes p
pN qN :: Notes q
qN, NTPair b :: TypeAnn
b pG :: FieldAnn
pG qG :: FieldAnn
qG pW :: VarAnn
pW qW :: VarAnn
qW pM :: Notes p
pM qM :: Notes q
qM) ->
    TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes q
-> Notes ('TPair p q)
forall (p :: T) (p :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes p
-> Notes ('TPair p p)
NTPair (TypeAnn
 -> FieldAnn
 -> FieldAnn
 -> VarAnn
 -> VarAnn
 -> Notes p
 -> Notes q
 -> Notes ('TPair p q))
-> Either AnnConvergeError TypeAnn
-> Either
     AnnConvergeError
     (FieldAnn
      -> FieldAnn
      -> VarAnn
      -> VarAnn
      -> Notes p
      -> Notes q
      -> Notes ('TPair p q))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b
           Either
  AnnConvergeError
  (FieldAnn
   -> FieldAnn
   -> VarAnn
   -> VarAnn
   -> Notes p
   -> Notes q
   -> Notes ('TPair p q))
-> Either AnnConvergeError FieldAnn
-> Either
     AnnConvergeError
     (FieldAnn
      -> VarAnn -> VarAnn -> Notes p -> Notes q -> Notes ('TPair p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FieldAnn -> FieldAnn -> Either AnnConvergeError FieldAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns FieldAnn
pF FieldAnn
pG Either
  AnnConvergeError
  (FieldAnn
   -> VarAnn -> VarAnn -> Notes p -> Notes q -> Notes ('TPair p q))
-> Either AnnConvergeError FieldAnn
-> Either
     AnnConvergeError
     (VarAnn -> VarAnn -> Notes p -> Notes q -> Notes ('TPair p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FieldAnn -> FieldAnn -> Either AnnConvergeError FieldAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns FieldAnn
qF FieldAnn
qG
           Either
  AnnConvergeError
  (VarAnn -> VarAnn -> Notes p -> Notes q -> Notes ('TPair p q))
-> Either AnnConvergeError VarAnn
-> Either
     AnnConvergeError
     (VarAnn -> Notes p -> Notes q -> Notes ('TPair p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VarAnn -> Either AnnConvergeError VarAnn
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarAnn -> VarAnn -> VarAnn
convergeVarAnns VarAnn
pV VarAnn
pW) Either
  AnnConvergeError
  (VarAnn -> Notes p -> Notes q -> Notes ('TPair p q))
-> Either AnnConvergeError VarAnn
-> Either
     AnnConvergeError (Notes p -> Notes q -> Notes ('TPair p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VarAnn -> Either AnnConvergeError VarAnn
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarAnn -> VarAnn -> VarAnn
convergeVarAnns VarAnn
qV VarAnn
qW)
           Either AnnConvergeError (Notes p -> Notes q -> Notes ('TPair p q))
-> Either AnnConvergeError (Notes p)
-> Either AnnConvergeError (Notes q -> Notes ('TPair p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes p -> Notes p -> Either AnnConvergeError (Notes p)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes p
pN Notes p
Notes p
pM Either AnnConvergeError (Notes q -> Notes ('TPair p q))
-> Either AnnConvergeError (Notes q)
-> Either AnnConvergeError (Notes ('TPair p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes q -> Notes q -> Either AnnConvergeError (Notes q)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes q
qN Notes q
Notes q
qM
  (NTOr a :: TypeAnn
a pF :: FieldAnn
pF qF :: FieldAnn
qF pN :: Notes p
pN qN :: Notes q
qN, NTOr b :: TypeAnn
b pG :: FieldAnn
pG qG :: FieldAnn
qG pM :: Notes p
pM qM :: Notes q
qM) ->
    TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q)
forall (p :: T) (p :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes p -> Notes ('TOr p p)
NTOr (TypeAnn
 -> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q))
-> Either AnnConvergeError TypeAnn
-> Either
     AnnConvergeError
     (FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b Either
  AnnConvergeError
  (FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q))
-> Either AnnConvergeError FieldAnn
-> Either
     AnnConvergeError
     (FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FieldAnn -> FieldAnn -> Either AnnConvergeError FieldAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns FieldAnn
pF FieldAnn
pG Either
  AnnConvergeError
  (FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q))
-> Either AnnConvergeError FieldAnn
-> Either AnnConvergeError (Notes p -> Notes q -> Notes ('TOr p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FieldAnn -> FieldAnn -> Either AnnConvergeError FieldAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns FieldAnn
qF FieldAnn
qG
         Either AnnConvergeError (Notes p -> Notes q -> Notes ('TOr p q))
-> Either AnnConvergeError (Notes p)
-> Either AnnConvergeError (Notes q -> Notes ('TOr p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes p -> Notes p -> Either AnnConvergeError (Notes p)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes p
pN Notes p
Notes p
pM Either AnnConvergeError (Notes q -> Notes ('TOr p q))
-> Either AnnConvergeError (Notes q)
-> Either AnnConvergeError (Notes ('TOr p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes q -> Notes q -> Either AnnConvergeError (Notes q)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes q
qN Notes q
Notes q
qM
  (NTLambda a :: TypeAnn
a pN :: Notes p
pN qN :: Notes q
qN, NTLambda b :: TypeAnn
b pM :: Notes p
pM qM :: Notes q
qM) ->
    TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
forall (p :: T) (q :: T).
TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
NTLambda (TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q))
-> Either AnnConvergeError TypeAnn
-> Either
     AnnConvergeError (Notes p -> Notes q -> Notes ('TLambda p q))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b Either
  AnnConvergeError (Notes p -> Notes q -> Notes ('TLambda p q))
-> Either AnnConvergeError (Notes p)
-> Either AnnConvergeError (Notes q -> Notes ('TLambda p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes p -> Notes p -> Either AnnConvergeError (Notes p)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes p
pN Notes p
Notes p
pM Either AnnConvergeError (Notes q -> Notes ('TLambda p q))
-> Either AnnConvergeError (Notes q)
-> Either AnnConvergeError (Notes ('TLambda p q))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes q -> Notes q -> Either AnnConvergeError (Notes q)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes q
qN Notes q
Notes q
qM
  (NTMap a :: TypeAnn
a kN :: Notes k
kN vN :: Notes v
vN, NTMap b :: TypeAnn
b kM :: Notes k
kM vM :: Notes v
vM) ->
    TypeAnn -> Notes k -> Notes v -> Notes ('TMap k v)
forall (q :: T) (k :: T).
TypeAnn -> Notes q -> Notes k -> Notes ('TMap q k)
NTMap (TypeAnn -> Notes k -> Notes v -> Notes ('TMap k v))
-> Either AnnConvergeError TypeAnn
-> Either
     AnnConvergeError (Notes k -> Notes v -> Notes ('TMap k v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b Either AnnConvergeError (Notes k -> Notes v -> Notes ('TMap k v))
-> Either AnnConvergeError (Notes k)
-> Either AnnConvergeError (Notes v -> Notes ('TMap k v))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes k -> Notes k -> Either AnnConvergeError (Notes k)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes k
kN Notes k
Notes k
kM Either AnnConvergeError (Notes v -> Notes ('TMap k v))
-> Either AnnConvergeError (Notes v)
-> Either AnnConvergeError (Notes ('TMap k v))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes v -> Notes v -> Either AnnConvergeError (Notes v)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes v
vN Notes v
Notes v
vM
  (NTBigMap a :: TypeAnn
a kN :: Notes k
kN vN :: Notes v
vN, NTBigMap b :: TypeAnn
b kM :: Notes k
kM vM :: Notes v
vM) ->
    TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
forall (k :: T) (v :: T).
TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
NTBigMap (TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v))
-> Either AnnConvergeError TypeAnn
-> Either
     AnnConvergeError (Notes k -> Notes v -> Notes ('TBigMap k v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeAnn -> TypeAnn -> Either AnnConvergeError TypeAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns TypeAnn
a TypeAnn
b Either
  AnnConvergeError (Notes k -> Notes v -> Notes ('TBigMap k v))
-> Either AnnConvergeError (Notes k)
-> Either AnnConvergeError (Notes v -> Notes ('TBigMap k v))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes k -> Notes k -> Either AnnConvergeError (Notes k)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes k
kN Notes k
Notes k
kM Either AnnConvergeError (Notes v -> Notes ('TBigMap k v))
-> Either AnnConvergeError (Notes v)
-> Either AnnConvergeError (Notes ('TBigMap k v))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Notes v -> Notes v -> Either AnnConvergeError (Notes v)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes v
vN Notes v
Notes v
vM

-- | Insert the provided type annotation into the provided notes.
insertTypeAnn :: forall (b :: T). TypeAnn -> Notes b -> Notes b
insertTypeAnn :: TypeAnn -> Notes b -> Notes b
insertTypeAnn nt :: TypeAnn
nt s :: Notes b
s = case Notes b
s of
  NTInt _ -> TypeAnn -> Notes 'TInt
NTInt TypeAnn
nt
  NTNat _ -> TypeAnn -> Notes 'TNat
NTNat TypeAnn
nt
  NTString _ -> TypeAnn -> Notes 'TString
NTString TypeAnn
nt
  NTBytes _ -> TypeAnn -> Notes 'TBytes
NTBytes TypeAnn
nt
  NTMutez _ -> TypeAnn -> Notes 'TMutez
NTMutez TypeAnn
nt
  NTBool _ -> TypeAnn -> Notes 'TBool
NTBool TypeAnn
nt
  NTKeyHash _ -> TypeAnn -> Notes 'TKeyHash
NTKeyHash TypeAnn
nt
  NTBls12381Fr _ -> TypeAnn -> Notes 'TBls12381Fr
NTBls12381Fr TypeAnn
nt
  NTBls12381G1 _ -> TypeAnn -> Notes 'TBls12381G1
NTBls12381G1 TypeAnn
nt
  NTBls12381G2 _ -> TypeAnn -> Notes 'TBls12381G2
NTBls12381G2 TypeAnn
nt
  NTTimestamp _ -> TypeAnn -> Notes 'TTimestamp
NTTimestamp TypeAnn
nt
  NTAddress _ -> TypeAnn -> Notes 'TAddress
NTAddress TypeAnn
nt
  NTKey _ -> TypeAnn -> Notes 'TKey
NTKey TypeAnn
nt
  NTUnit _ -> TypeAnn -> Notes 'TUnit
NTUnit TypeAnn
nt
  NTSignature _ -> TypeAnn -> Notes 'TSignature
NTSignature TypeAnn
nt
  NTOption _ n1 :: 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 _ n1 :: 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 _ n1 :: 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 -> Notes 'TOperation
NTOperation TypeAnn
nt
  NTContract _ n1 :: Notes t
n1 -> TypeAnn -> Notes t -> Notes ('TContract t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TContract t)
NTContract TypeAnn
nt Notes t
n1
  NTPair _ n1 :: FieldAnn
n1 n2 :: FieldAnn
n2 n3 :: VarAnn
n3 n4 :: VarAnn
n4 n5 :: Notes p
n5 n6 :: Notes q
n6 -> TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes q
-> Notes ('TPair p q)
forall (p :: T) (p :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes p
-> Notes ('TPair p p)
NTPair TypeAnn
nt FieldAnn
n1 FieldAnn
n2 VarAnn
n3 VarAnn
n4 Notes p
n5 Notes q
n6
  NTOr _ n1 :: FieldAnn
n1 n2 :: FieldAnn
n2 n3 :: Notes p
n3 n4 :: Notes q
n4 -> TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q)
forall (p :: T) (p :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes p -> Notes ('TOr p p)
NTOr TypeAnn
nt FieldAnn
n1 FieldAnn
n2 Notes p
n3 Notes q
n4
  NTLambda _ n1 :: Notes p
n1 n2 :: Notes q
n2 -> TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
forall (p :: T) (q :: T).
TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
NTLambda TypeAnn
nt Notes p
n1 Notes q
n2
  NTMap _ n1 :: Notes k
n1 n2 :: Notes v
n2 -> TypeAnn -> Notes k -> Notes v -> Notes ('TMap k v)
forall (q :: T) (k :: T).
TypeAnn -> Notes q -> Notes k -> Notes ('TMap q k)
NTMap TypeAnn
nt Notes k
n1 Notes v
n2
  NTBigMap _ n1 :: Notes k
n1 n2 :: Notes v
n2 -> TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
forall (k :: T) (v :: T).
TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
NTBigMap TypeAnn
nt Notes k
n1 Notes v
n2
  NTChainId _ -> TypeAnn -> Notes 'TChainId
NTChainId TypeAnn
nt
  NTNever _ -> TypeAnn -> Notes 'TNever
NTNever TypeAnn
nt

data AnnConvergeError where
  AnnConvergeError
    :: forall (tag :: Kind.Type).
       (Buildable (Annotation tag), Show (Annotation tag), Typeable tag)
    => Annotation tag -> Annotation tag -> AnnConvergeError

deriving stock instance Show AnnConvergeError

instance Eq AnnConvergeError where
  AnnConvergeError ann1 :: Annotation tag
ann1 ann2 :: Annotation tag
ann2 == :: AnnConvergeError -> AnnConvergeError -> Bool
== AnnConvergeError ann1' :: Annotation tag
ann1' ann2' :: Annotation tag
ann2' =
    (Annotation tag
ann1 Annotation tag -> Annotation tag -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(Typeable a1, Typeable a2, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParam1` Annotation tag
ann1') Bool -> Bool -> Bool
&& (Annotation tag
ann2 Annotation tag -> Annotation tag -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(Typeable a1, Typeable a2, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParam1` Annotation tag
ann2')

instance Buildable AnnConvergeError where
  build :: AnnConvergeError -> Builder
build (AnnConvergeError ann1 :: Annotation tag
ann1 ann2 :: Annotation tag
ann2) =
    "Annotations do not converge: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Annotation tag
ann1 Annotation tag -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ " /= " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Annotation tag
ann2 Annotation tag -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ ""

convergeAnnsImpl
  :: forall (tag :: Kind.Type).
     (Buildable (Annotation tag), Show (Annotation tag), Typeable tag)
  => (Annotation tag -> Annotation tag -> Maybe (Annotation tag))
  -> Annotation tag -> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnnsImpl :: (Annotation tag -> Annotation tag -> Maybe (Annotation tag))
-> Annotation tag
-> Annotation tag
-> Either AnnConvergeError (Annotation tag)
convergeAnnsImpl unify :: Annotation tag -> Annotation tag -> Maybe (Annotation tag)
unify a :: Annotation tag
a b :: Annotation tag
b = Either AnnConvergeError (Annotation tag)
-> (Annotation tag -> Either AnnConvergeError (Annotation tag))
-> Maybe (Annotation tag)
-> Either AnnConvergeError (Annotation tag)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (AnnConvergeError -> Either AnnConvergeError (Annotation tag)
forall a b. a -> Either a b
Left (AnnConvergeError -> Either AnnConvergeError (Annotation tag))
-> AnnConvergeError -> Either AnnConvergeError (Annotation tag)
forall a b. (a -> b) -> a -> b
$ Annotation tag -> Annotation tag -> AnnConvergeError
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
Annotation tag -> Annotation tag -> AnnConvergeError
AnnConvergeError Annotation tag
a Annotation tag
b) Annotation tag -> Either AnnConvergeError (Annotation tag)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Annotation tag)
 -> Either AnnConvergeError (Annotation tag))
-> Maybe (Annotation tag)
-> Either AnnConvergeError (Annotation tag)
forall a b. (a -> b) -> a -> b
$ Annotation tag -> Annotation tag -> Maybe (Annotation tag)
unify Annotation tag
a Annotation tag
b

-- | Converge two type or field notes (which may be wildcards).
convergeAnns
  :: forall (tag :: Kind.Type).
     (Buildable (Annotation tag), Show (Annotation tag), Typeable tag)
  => Annotation tag -> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns :: Annotation tag
-> Annotation tag -> Either AnnConvergeError (Annotation tag)
convergeAnns = (Annotation tag -> Annotation tag -> Maybe (Annotation tag))
-> Annotation tag
-> Annotation tag
-> Either AnnConvergeError (Annotation tag)
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
(Annotation tag -> Annotation tag -> Maybe (Annotation tag))
-> Annotation tag
-> Annotation tag
-> Either AnnConvergeError (Annotation tag)
convergeAnnsImpl Annotation tag -> Annotation tag -> Maybe (Annotation tag)
forall k (tag :: k).
Annotation tag -> Annotation tag -> Maybe (Annotation tag)
unifyAnn

-- | Converge two field notes in CAR or CDR, given that one of them may be a
-- special annotation.
convergeDestrAnns :: FieldAnn -> FieldAnn -> Either AnnConvergeError FieldAnn
convergeDestrAnns :: FieldAnn -> FieldAnn -> Either AnnConvergeError FieldAnn
convergeDestrAnns = (FieldAnn -> FieldAnn -> Maybe FieldAnn)
-> FieldAnn -> FieldAnn -> Either AnnConvergeError FieldAnn
forall tag.
(Buildable (Annotation tag), Show (Annotation tag),
 Typeable tag) =>
(Annotation tag -> Annotation tag -> Maybe (Annotation tag))
-> Annotation tag
-> Annotation tag
-> Either AnnConvergeError (Annotation tag)
convergeAnnsImpl FieldAnn -> FieldAnn -> Maybe FieldAnn
unifyPairFieldAnn

$(deriveGADTNFData ''AnnConvergeError)