-- 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
  , insertTypeAnn
  , orAnn
  , isStar
  , starNotes
  , notesSing
  , notesT
  ) where

import Data.Default (Default(..))
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, fullAnnSet, noAnn, singleAnnSet, unifyAnn)
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 corrspoding 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
              -> 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
  NTTimestamp :: TypeAnn -> Notes 'TTimestamp
  NTAddress   :: TypeAnn -> Notes 'TAddress

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
    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
    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 np :: Notes p
np nq :: Notes q
nq -> "NTPair" 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
    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] []

-- | 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
  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
  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 -> Notes a -> Notes b -> Notes ('TPair a b)
forall (p :: T) (p :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> 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 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)

orAnn :: Annotation t -> Annotation t -> Annotation t
orAnn :: Annotation t -> Annotation t -> Annotation t
orAnn a :: Annotation t
a b :: Annotation t
b = Annotation t -> Annotation t -> Bool -> Annotation t
forall a. a -> a -> Bool -> a
bool Annotation t
a Annotation t
b (Annotation t
a Annotation t -> Annotation t -> Bool
forall a. Eq a => a -> a -> Bool
== Annotation t
forall a. Default a => a
def)

-- | 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
  (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
  (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 pN :: Notes p
pN qN :: Notes q
qN, NTPair 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 ('TPair p q)
forall (p :: T) (p :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes p -> Notes ('TPair p p)
NTPair (TypeAnn
 -> FieldAnn
 -> FieldAnn
 -> Notes p
 -> Notes q
 -> Notes ('TPair p q))
-> Either AnnConvergeError TypeAnn
-> Either
     AnnConvergeError
     (FieldAnn -> FieldAnn -> 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 -> Notes p -> Notes q -> Notes ('TPair p q))
-> Either AnnConvergeError FieldAnn
-> Either
     AnnConvergeError
     (FieldAnn -> 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 -> Notes p -> Notes q -> Notes ('TPair p q))
-> Either AnnConvergeError FieldAnn
-> Either
     AnnConvergeError (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 (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
  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 :: Notes p
n3 n4 :: Notes q
n4 -> TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TPair p q)
forall (p :: T) (p :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes p -> Notes ('TPair p p)
NTPair TypeAnn
nt FieldAnn
n1 FieldAnn
n2 Notes p
n3 Notes q
n4
  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

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
|+ ""

-- | 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 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)
forall k (tag :: k).
Annotation tag -> Annotation tag -> Maybe (Annotation tag)
unifyAnn Annotation tag
a Annotation tag
b

$(deriveGADTNFData ''AnnConvergeError)