morley 1.19.2 → 1.20.0

raw patch · 49 files changed

+839/−720 lines, 49 filesdep −show-typePVP ok

version bump matches the API change (PVP)

Dependencies removed: show-type

API changes (from Hackage documentation)

Files

• CHANGES.md +14/−0
• README.md +2/−2
• app/Main.hs +22/−22
• morley.cabal +4/−5
• src/Morley/App/REPL.hs +1/−1
• src/Morley/AsRPC.hs +4/−3
• src/Morley/Micheline/Binary/Internal.hs +1/−1
• src/Morley/Michelson/Internal/ViewName.hs +6/−5
• src/Morley/Michelson/Interpret.hs +25/−24
• src/Morley/Michelson/Macro.hs +19/−19
• src/Morley/Michelson/Optimizer/Internal/Rules.hs +0/−6
• src/Morley/Michelson/Printer.hs +0/−2
• src/Morley/Michelson/Printer/Util.hs +0/−54
• src/Morley/Michelson/Runtime/GState.hs +1/−1
• src/Morley/Michelson/Typed/Arith.hs +19/−3
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/Classifiers/NumChildren.hs +1/−1
• src/Morley/Michelson/Typed/Convert.hs +1/−1
• src/Morley/Michelson/Typed/Doc.hs +4/−4
• src/Morley/Michelson/Typed/Haskell/Doc.hs +121/−37
• src/Morley/Michelson/Typed/Haskell/Instr/Product.hs +142/−29
• src/Morley/Michelson/Typed/Haskell/Instr/Sum.hs +86/−30
• src/Morley/Michelson/Typed/Haskell/LooseSum.hs +42/−5
• src/Morley/Michelson/Typed/Haskell/ValidateDescription.hs +19/−6
• src/Morley/Michelson/Typed/Haskell/Value.hs +25/−9
• src/Morley/Michelson/Typed/Instr.hs +1/−1
• src/Morley/Michelson/Typed/Instr/Internal/Proofs.hs +1/−1
• src/Morley/Michelson/Typed/Polymorphic.hs +1/−1
• src/Morley/Michelson/Typed/Scope.hs +1/−47
• src/Morley/Michelson/Typed/Scope/Internal/Deprecated.hs +0/−299
• src/Morley/Michelson/Typed/Scope/Internal/ForbidT.hs +15/−5
• src/Morley/Michelson/Typed/Scope/Internal/Scopes.hs +8/−8
• src/Morley/Michelson/Typed/Value.hs +1/−2
• src/Morley/Michelson/Typed/View.hs +1/−6
• src/Morley/Michelson/Untyped/Annotation.hs +3/−1
• src/Morley/Michelson/Untyped/Instr.hs +2/−2
• src/Morley/Michelson/Untyped/View.hs +1/−6
• src/Morley/Tezos/Core.hs +3/−1
• src/Morley/Util/CustomGeneric.hs +4/−3
• src/Morley/Util/Generic.hs +40/−1
• src/Morley/Util/Interpolate/Internal.hs +3/−3
• src/Morley/Util/Lens.hs +1/−1
• src/Morley/Util/MultiReader.hs +1/−1
• src/Morley/Util/Named.hs +1/−1
• src/Morley/Util/Peano.hs +1/−0
• src/Morley/Util/PeanoNatural.hs +1/−1
• src/Morley/Util/ShowType.hs +172/−0
• src/Morley/Util/SizedList.hs +12/−5
• src/Morley/Util/TH.hs +1/−1
• src/Morley/Util/Type.hs +5/−53

@@ -1,5 +1,19 @@ <!-- Unreleased: append new entries here --> +1.20.0+======+* [!1364](https://gitlab.com/morley-framework/morley/-/merge_requests/1364)+  Update to LTS-21.4 (GHC 9.4.5)+* [!1358](https://gitlab.com/morley-framework/morley/-/merge_requests/1358)+  Make missing `Generic` errors more readable+* [!1356](https://gitlab.com/morley-framework/morley/-/merge_requests/1356)+  Optimize `SizedList` `Monad` instance+  + Avoid unnecessary traversals+  + Make `SizedList` lazy in both head and tail+* [!1367](https://gitlab.com/morley-framework/morley/-/merge_requests/1367)+  Replace `HaveCommonTypeCtor` class with a type family+* [!1368](https://gitlab.com/morley-framework/morley/-/merge_requests/1368)+  Remove deprecated types and functions  1.19.2 ======

@@ -1,6 +1,6 @@-> :warning: **Note: this project is being deprecated.**+> :warning: **Note: this project is deprecated.** >-> It will no longer be maintained after the activation of protocol "N" on the Tezos mainnet.+> It is no longer maintained since the activation of protocol "Nairobi" on the Tezos mainnet (June 24th, 2023).  # Morley: Developer tools for the Michelson Language 

@@ -8,7 +8,7 @@ import Data.Version (showVersion) import Options.Applicative   (execParser, footerDoc, fullDesc, header, help, helper, info, infoOption, long, progDesc)-import Options.Applicative.Help.Pretty (Doc, linebreak)+import Options.Applicative.Help.Pretty (Doc, line) import Paths_morley (version)  import Morley.App.CLI@@ -30,25 +30,25 @@  usageDoc :: Maybe Doc usageDoc = Just $ mconcat-   [ "You can use help for specific COMMAND", linebreak-   , "EXAMPLE:", linebreak-   , "  morley emulate run --help", linebreak-   , linebreak-   , "Documentation for morley tools can be found at the following links:", linebreak-   , "  https://gitlab.com/morley-framework/morley/blob/master/README.md", linebreak-   , "  https://gitlab.com/morley-framework/morley/tree/master/docs", linebreak-   , linebreak-   , "Sample contracts for running can be found at the following link:", linebreak-   , "  https://gitlab.com/morley-framework/morley/tree/master/contracts", linebreak-   , linebreak-   , "USAGE EXAMPLE:", linebreak-   , "  morley parse --contract add1.tz", linebreak-   , linebreak-   , "  This command will parse contract stored in add1.tz", linebreak-   , "  and return its representation in haskell types", linebreak-   , linebreak-   , "  morley emulate originate --contract add1.tz --storage 1 --verbose", linebreak-   , linebreak-   , "  This command will originate contract with code stored in add1.tz", linebreak-   , "  with initial storage value set to 1 and return info about", linebreak+   [ "You can use help for specific COMMAND", line+   , "EXAMPLE:", line+   , "  morley emulate run --help", line+   , line+   , "Documentation for morley tools can be found at the following links:", line+   , "  https://gitlab.com/morley-framework/morley/blob/master/README.md", line+   , "  https://gitlab.com/morley-framework/morley/tree/master/docs", line+   , line+   , "Sample contracts for running can be found at the following link:", line+   , "  https://gitlab.com/morley-framework/morley/tree/master/contracts", line+   , line+   , "USAGE EXAMPLE:", line+   , "  morley parse --contract add1.tz", line+   , line+   , "  This command will parse contract stored in add1.tz", line+   , "  and return its representation in haskell types", line+   , line+   , "  morley emulate originate --contract add1.tz --storage 1 --verbose", line+   , line+   , "  This command will originate contract with code stored in add1.tz", line+   , "  with initial storage value set to 1 and return info about", line    , "  originated contract: its balance, storage and contract code"]

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           morley-version:        1.19.2+version:        1.20.0 synopsis:       Developer tools for the Michelson Language description:    A library to make writing smart contracts in Michelson — the smart contract language of the Tezos blockchain — pleasant and effective. category:       Language@@ -131,7 +131,6 @@       Morley.Michelson.Typed.Scope       Morley.Michelson.Typed.Scope.Internal.CheckScope       Morley.Michelson.Typed.Scope.Internal.Comparable-      Morley.Michelson.Typed.Scope.Internal.Deprecated       Morley.Michelson.Typed.Scope.Internal.ForbidT       Morley.Michelson.Typed.Scope.Internal.Presence       Morley.Michelson.Typed.Scope.Internal.Scopes@@ -191,6 +190,7 @@       Morley.Util.Named       Morley.Util.Peano       Morley.Util.PeanoNatural+      Morley.Util.ShowType       Morley.Util.Sing       Morley.Util.SizedList       Morley.Util.SizedList.Types@@ -259,7 +259,7 @@       UndecidableInstances       UndecidableSuperClasses       ViewPatterns-  ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode+  ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode -Wno-missing-kind-signatures -Wno-implicit-lift -Wno-unticked-promoted-constructors   build-depends:       Diff     , MonadRandom@@ -298,7 +298,6 @@     , prettyprinter     , scientific     , semigroups >=0.19.1-    , show-type     , singletons     , singletons-base     , some@@ -377,7 +376,7 @@       UndecidableInstances       UndecidableSuperClasses       ViewPatterns-  ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode+  ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode -Wno-missing-kind-signatures -Wno-implicit-lift -Wno-unticked-promoted-constructors   build-depends:       base-noprelude >=4.7 && <5     , morley

@@ -105,7 +105,7 @@            printResult "Public Key" (formatPublicKey pk)            printResult "Public Key hash" (formatHash pkh)         (stripPrefixNonEmpty ":" -> Just cmd) ->-          printErr $ "Unknown command or argument missing in `:"<> (toText cmd) <> "`. Use :help to see a list of commands"+          printErr $ "Unknown command or argument missing in `:" <> (toText cmd) <> "`. Use :help to see a list of commands"         _ -> flip catch (\Interrupt -> putTextLn "Cancelled") $ withInterrupt $ runCode (toText input)       repl_   where

@@ -456,8 +456,8 @@  >>> :i AsRPC ...-type instance AsRPC B = BRPC ... type instance AsRPC A = ARPC ...+type instance AsRPC B = BRPC ... ...  This check isn't very smart, so it might miss some corner cases.@@ -689,7 +689,8 @@             -> ConT x `AppT` (convertFieldType $ replaceVars fieldType)           x `AppT` y -> go x `AppT` go y           x -> replaceVars x-        replaceVars = \case+        replaceVars = everywhere (mkT doReplace)+        doReplace = \case           VarT v -> VarT $ fromMaybe v $ Map.lookup v varMap           x -> x @@ -846,7 +847,7 @@ replaceBigMapIds findBigMapById = go   where     go :: forall t1. Sing t1 -> Value (TAsRPC t1) -> m (Value t1)-    go s v = case (s, v) of+    go s !v = case (s, v) of       (STKey {}, _) -> pure v       (STUnit {}, _) -> pure v       (STSignature {}, _) -> pure v

@@ -82,7 +82,7 @@ readZ :: forall a. (Integral a, Bits a) => Int -> a -> Bi.Get a readZ offset n = do   b <- Bi.getWord8-  if (b == 0) && (offset > 0) then fail "trailing zero" else pure ()+  when ((b == 0) && (offset > 0)) $ fail "trailing zero"   let n' = (Unsafe.fromIntegral @Word8 @a (b .&. 0x7f) `shift` offset) .|. n   if b `testBit` 7 then readZ (offset + 7) n' else pure n' 

@@ -12,6 +12,7 @@ import Data.Aeson (FromJSONKey(..), ToJSONKey(..)) import Data.Aeson.TH (deriveJSON) import Data.Aeson.Types qualified as AesonTypes+import Data.Char (isAsciiLower, isAsciiUpper, isDigit) import Data.Data (Data) import Data.Text qualified as Text import Fmt (Buildable(..), Doc, pretty, (+|), (|+))@@ -48,11 +49,11 @@  -- | Whether the given character is valid for a view. isValidViewNameChar :: Char -> Bool-isValidViewNameChar c = or-  [ 'A' <= c && c <= 'Z'-  , 'a' <= c && c <= 'z'-  , '0' <= c && c <= '9'-  , c `elem` ['_', '.', '%', '@']+isValidViewNameChar = or+  [ isAsciiUpper+  , isAsciiLower+  , isDigit+  , (`elem` ['_', '.', '%', '@'])   ]  -- | Maximum allowed name length for a view.

@@ -651,19 +651,19 @@       go n r <&> \case         (a :& resTail) -> a :& b :& resTail runInstrImpl _ SWAP (a :& b :& r) = pure $ b :& a :& r-runInstrImpl _ (DIG s) input0 =+runInstrImpl _ (DIG @_ @_ @_ @a s) input0 =   pure $ go s input0   where-    go :: forall (n :: Peano) inp out a. ConstraintDIG n inp out a+    go :: forall (n :: Peano) inp out. ConstraintDIG n inp out a        => PeanoNatural n -> Rec (StkEl meta) inp -> Rec (StkEl meta) out     go Zero stack = stack     go (Succ n') (b :& r) =       case go n' r of         a :& resTail -> a :& b :& resTail-runInstrImpl _ (DUG s) input0 =+runInstrImpl _ (DUG @_ @_ @_ @a s) input0 =   pure $ go s input0   where-    go :: forall (n :: Peano) inp out a. ConstraintDUG n inp out a+    go :: forall (n :: Peano) inp out. ConstraintDUG n inp out a        => PeanoNatural n -> Rec (StkEl meta) inp -> Rec (StkEl meta) out     go Zero stack = stack     go (Succ n') (a :& b :& r) = b :& go n' (a :& r)@@ -899,27 +899,28 @@       mkStkEl (VContract (MkAddress ceSelf) sepc) <:&> r runInstrImpl _ (AnnCONTRACT (Anns2' _ (_ :: Notes a)) instrEpName) (StkEl (VAddress epAddr) :& r) = do   ContractEnv{..} <- ask-  EpAddress' (Constrained addr) addrEpName <- pure epAddr-  let mepName =-        case (instrEpName, addrEpName) of-          (DefEpName, DefEpName) -> Just DefEpName-          (DefEpName, en) -> Just en-          (en, DefEpName) -> Just en-          _ -> Nothing+  case epAddr of+    EpAddress' (Constrained addr) addrEpName -> do+      let mepName =+            case (instrEpName, addrEpName) of+              (DefEpName, DefEpName) -> Just DefEpName+              (DefEpName, en) -> Just en+              (en, DefEpName) -> Just en+              _ -> Nothing -  let withNotes v = mkStkEl v <:&> r-  withNotes . VOption =<< case mepName of-    Nothing -> pure Nothing-    Just epName -> case addr of-      ImplicitAddress{} -> pure $ case sing @a of-        STTicket{} -> castContract addr epName $ starParamNotes @a-        STUnit -> castContract addr epName $ starParamNotes @a-        _ -> Nothing-      ContractAddress{} -> runMaybeT do-        ContractState{csContract} <- MaybeT $ ceContracts addr-        hoistMaybe $ castContract addr epName (cParamNotes csContract)-      SmartRollupAddress{} ->-        throwMichelson $ MichelsonUnsupported "sr1 addresses with CONTRACT"+      let withNotes v = mkStkEl v <:&> r+      withNotes . VOption =<< case mepName of+        Nothing -> pure Nothing+        Just epName -> case addr of+          ImplicitAddress{} -> pure $ case sing @a of+            STTicket{} -> castContract addr epName $ starParamNotes @a+            STUnit -> castContract addr epName $ starParamNotes @a+            _ -> Nothing+          ContractAddress{} -> runMaybeT do+            ContractState{csContract} <- MaybeT $ ceContracts addr+            hoistMaybe $ castContract addr epName (cParamNotes csContract)+          SmartRollupAddress{} ->+            throwMichelson $ MichelsonUnsupported "sr1 addresses with CONTRACT"   where     castContract       :: forall p kind. (ParameterScope p)

@@ -84,9 +84,9 @@  instance Buildable ParsedOp where   build = \case-    Prim parseInstr _ -> "<Prim: "+|parseInstr|+">"-    Mac macro _       -> "<Mac: "+|macro|+">"-    Seq parsedOps _   -> "<Seq: "+|parsedOps|+">"+    Prim parseInstr _ -> "<Prim: " +| parseInstr |+ ">"+    Mac macro _       -> "<Mac: " +| macro |+ ">"+    Seq parsedOps _   -> "<Seq: " +| parsedOps |+ ">"  instance NFData ParsedOp @@ -139,28 +139,28 @@  instance Buildable Macro where   build = \case-    CMP parsedInstr -> "<CMP: "+|parsedInstr|+">"-    IFX parsedInstr parsedOps1 parsedOps2 -> "<IFX: "+|parsedInstr|+", "+|parsedOps1|+", "+|parsedOps2|+">"-    IFCMP parsedInstr parsedOps1 parsedOps2 -> "<IFCMP: "+|parsedInstr|+", "+|parsedOps1|+", "+|parsedOps2|+">"+    CMP parsedInstr -> "<CMP: " +| parsedInstr |+ ">"+    IFX parsedInstr parsedOps1 parsedOps2 -> "<IFX: " +| parsedInstr |+ ", " +| parsedOps1 |+ ", " +| parsedOps2 |+ ">"+    IFCMP parsedInstr parsedOps1 parsedOps2 -> "<IFCMP: " +| parsedInstr |+ ", " +| parsedOps1 |+ ", " +| parsedOps2 |+ ">"     FAIL -> "FAIL"-    PAPAIR pairStruct typeAnn varAnn -> "<PAPAIR: "+|pairStruct|+", "+|typeAnn|+", "+|varAnn|+">"-    UNPAPAIR pairStruct -> "<UNPAPAIR: "+|pairStruct|+">"-    CADR cadrStructs varAnn fieldAnn -> "<CADR: "+|cadrStructs|+", "+|varAnn|+", "+|fieldAnn|+">"-    CARN varAnn idx -> "<CAR: #"+|idx|+","+|varAnn|+">"-    CDRN varAnn idx -> "<CDR: #"+|idx|+","+|varAnn|+">"-    SET_CADR cadrStructs varAnn fieldAnn -> "<SET_CADR: "+|cadrStructs|+", "+|varAnn|+", "+|fieldAnn|+">"-    MAP_CADR cadrStructs varAnn fieldAnn parsedOps -> "<MAP_CADR: "+|cadrStructs|+", "+|varAnn|+", "+|fieldAnn|+", "+|parsedOps|+">"-    DIIP integer parsedOps -> "<DIIP: "+|integer|+", "+|parsedOps|+">"-    DUUP integer varAnn -> "<DUUP: "+|integer|+", "+|varAnn|+">"+    PAPAIR pairStruct typeAnn varAnn -> "<PAPAIR: " +| pairStruct |+ ", " +| typeAnn |+ ", " +| varAnn |+ ">"+    UNPAPAIR pairStruct -> "<UNPAPAIR: " +| pairStruct |+ ">"+    CADR cadrStructs varAnn fieldAnn -> "<CADR: " +| cadrStructs |+ ", " +| varAnn |+ ", " +| fieldAnn |+ ">"+    CARN varAnn idx -> "<CAR: #" +| idx |+ "," +| varAnn |+ ">"+    CDRN varAnn idx -> "<CDR: #" +| idx |+ "," +| varAnn |+ ">"+    SET_CADR cadrStructs varAnn fieldAnn -> "<SET_CADR: " +| cadrStructs |+ ", " +| varAnn |+ ", " +| fieldAnn |+ ">"+    MAP_CADR cadrStructs varAnn fieldAnn parsedOps -> "<MAP_CADR: " +| cadrStructs |+ ", " +| varAnn |+ ", " +| fieldAnn |+ ", " +| parsedOps |+ ">"+    DIIP integer parsedOps -> "<DIIP: " +| integer |+ ", " +| parsedOps |+ ">"+    DUUP integer varAnn -> "<DUUP: " +| integer |+ ", " +| varAnn |+ ">"     ASSERT -> "ASSERT"-    ASSERTX parsedInstr -> "<ASSERTX: "+|parsedInstr|+">"-    ASSERT_CMP parsedInstr -> "<ASSERT_CMP: "+|parsedInstr|+">"+    ASSERTX parsedInstr -> "<ASSERTX: " +| parsedInstr |+ ">"+    ASSERT_CMP parsedInstr -> "<ASSERT_CMP: " +| parsedInstr |+ ">"     ASSERT_NONE  -> "ASSERT_NONE"     ASSERT_SOME  -> "ASSERT_SOME"     ASSERT_LEFT  -> "ASSERT_LEFT"     ASSERT_RIGHT -> "ASSERT_RIGHT"-    IF_SOME parsedOps1 parsedOps2 -> "<IF_SOME: "+|parsedOps1|+", "+|parsedOps2|+">"-    IF_RIGHT parsedOps1 parsedOps2 -> "<IF_RIGHT: "+|parsedOps1|+", "+|parsedOps2|+">"+    IF_SOME parsedOps1 parsedOps2 -> "<IF_SOME: " +| parsedOps1 |+ ", " +| parsedOps2 |+ ">"+    IF_RIGHT parsedOps1 parsedOps2 -> "<IF_RIGHT: " +| parsedOps1 |+ ", " +| parsedOps2 |+ ">"  instance NFData Macro 

@@ -3,12 +3,6 @@  {-# OPTIONS_HADDOCK not-home #-} --- NOTE this pragmas.--- We disable some warnings for the sake of speed up.--- Write code with care.-{-# OPTIONS_GHC -Wno-incomplete-patterns #-}-{-# OPTIONS_GHC -Wno-overlapping-patterns #-}- -- | Optimizer rewrite rules module Morley.Michelson.Optimizer.Internal.Rules   ( module Morley.Michelson.Optimizer.Internal.Rules

@@ -3,8 +3,6 @@  module Morley.Michelson.Printer   ( RenderDoc(..)-  , renderAnyBuildable-  , printDoc   , printUntypedContract   , printTypedContractCode   , printTypedContract

@@ -7,18 +7,10 @@ -- Octez software (e.g @octez-client@) module Morley.Michelson.Printer.Util   ( RenderDoc(..)-  , Prettier(..)-  , printDoc-  , printDocB-  , printDocS   , printRenderDoc-  , renderOps   , renderOpsList   , renderOpsListNoBraces-  , renderAnyBuildable   , wrapInParens-  , buildRenderDoc-  , buildRenderDocExtended   , renderDocList      -- * Smart parentheses@@ -34,7 +26,6 @@  import Control.Exception (assert) import Data.Foldable qualified as Foldable-import Data.Text.Lazy.Builder (Builder) import Fmt (Buildable(build), FromSimpleDoc(..)) import Fmt.Operators ((<+>), (<//>)) import Fmt.Utils (Doc, SimpleDoc, isEmpty, mkLayoutOptions, renderOneLine)@@ -77,44 +68,10 @@ renderDocList :: RenderDoc a => RenderContext -> [a] -> Doc renderDocList context = align . encloseSep lbracket rbracket ", " . fmap (renderDoc context) -renderAnyBuildable :: Buildable a => a -> Doc-renderAnyBuildable = build-{-# DEPRECATED renderAnyBuildable "Use build instead" #-}---- | A new type that can wrap values so that the RenderDoc--- instances of the combined value can have a different--- behavior for the pretty printer.-newtype Prettier a = Prettier a-  deriving stock Functor-{-# DEPRECATED Prettier "This has no actual effect nowadays" #-}--instance RenderDoc a => RenderDoc (Prettier a) where-  renderDoc ctx (Prettier a) = renderDoc ctx a- -- | Convert anything renderable to some text format with line width of 80. printRenderDoc :: (RenderDoc a, FromSimpleDoc b) => Bool -> a -> b printRenderDoc oneLine = fmtSimple . doRender oneLine . renderDoc doesntNeedParens --- | Convert 'Doc' to 'LText' with a line width of 80.-printDoc :: Bool -> Doc -> LText-printDoc = printRenderDoc---- | Convert 'Doc' to 'Builder' in the same manner as 'printDoc'.-printDocB :: Bool -> Doc -> Builder-printDocB = printRenderDoc---- | Convert 'Doc' to 'String' in the same manner as 'printDoc'.-printDocS :: Bool -> Doc -> String-printDocS = printRenderDoc--{-# DEPRECATED printDoc, printDocB, printDocS "Use printRenderDoc instead" #-}---- | Generic way to render the different op types that get passed--- to a contract.-renderOps :: (RenderDoc op) => Bool -> NonEmpty op -> Doc-renderOps = renderOpsList-{-# DEPRECATED renderOps "Use renderOpsList instead" #-}- -- | Render a comma-separated list of items in braces renderOpsList :: (RenderDoc op, Foldable f) => Bool -> f op -> Doc renderOpsList oneLine ops =@@ -132,17 +89,6 @@   let moreThanOne = length (filter (not . isEmpty) (toList ds)) > 1   in  addParens (RenderContext (pn && moreThanOne)) $         foldr (<+>) mempty ds---- | 'renderDoc', then 'group' and 'align'. Generally, this is the same as--- 'build'.-buildRenderDoc :: RenderDoc a => a -> Doc-buildRenderDoc = align . group . renderDoc doesntNeedParens---- | Works as 'buildRenderDoc' above, but doesn't 'group'.-buildRenderDocExtended :: RenderDoc a => a -> Doc-buildRenderDocExtended = align . renderDoc doesntNeedParens-{-# DEPRECATED buildRenderDoc, buildRenderDocExtended-  "`RenderDoc` already implies `Buildable`, use `build` if you can" #-}  instance {-# overlappable #-} RenderDoc a => Buildable a where   build = align . group . renderDoc doesntNeedParens

@@ -453,7 +453,7 @@     GSSetStorageValue addr newValue ->       setStorageValue addr newValue     GSSetBalance addr newBalance -> addr `setBalance` newBalance-    GSIncrementCounter -> Right . over gsCounterL (+1)+    GSIncrementCounter -> Right . over gsCounterL (+ 1)     GSUpdateCounter newCounter -> Right . set gsCounterL newCounter     GSSetBigMapCounter bmCounter -> Right . set gsBigMapCounterL bmCounter     GSSetDelegate addr key -> setDelegate addr key

@@ -342,15 +342,31 @@   :: (Int -> Int -> Int) -- ^ Length comparator   -> (Word8 -> Word8 -> Word8) -- ^ Zipper   -> ByteString -> ByteString -> ByteString-bitwiseWithByteStringsEnd comp op i j = BS.pack $ BS.zipWith op i' j'-  -- TODO [#919]: use packZipWith and takeEnd+bitwiseWithByteStringsEnd comp op i j = BS.packZipWith op i' j'   where     resultLen = comp lenI lenJ     lenI = length i     lenJ = length j-    normalize len = (BS.replicate (resultLen - len) 0 <>) . BS.drop (len - resultLen)+    normalize len = -- see Note [resultLen and normalize]+      (BS.replicate (resultLen - len) 0 <>) . BS.takeEnd resultLen     i' = normalize lenI i     j' = normalize lenJ j++{-+Note [resultLen and normalize]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~++The idea with 'normalize' is to take exactly 'resultLen' bytes and left-pad with+zero bytes to the same length, so that 'packZipWith' is aligned correctly.++Note that depending on whether 'comp' is 'min' or 'max', either 'replicate' or+'takeEnd' is a no-op, respectively.++'takeEnd' is O(1), and replicate is O(1) for arguments <= 0, hence we do both+instead of making two functions or checking some condition.++-- @lierdakil+-}  instance ArithOp Or 'TNat 'TNat where   type ArithRes Or 'TNat 'TNat = 'TNat

@@ -36,7 +36,7 @@     go !n = \case       [] -> n       (x:xs)-        | isInstr x -> go (n+1) xs+        | isInstr x -> go (n + 1) xs         | otherwise -> go n xs  isExtInstr :: Type -> Bool

@@ -169,7 +169,7 @@ -- -- For full isomorphism type of the given t'Morley.Michelson.Typed.Aliases.Value' should not contain -- 'TOperation' - a compile error will be raised otherwise.--- You can analyse its presence with 'checkOpPresence' function.+-- You can analyse its presence with 'checkTPresence' function. untypeValueImpl   :: ForbidOp t   => UntypingOptions

@@ -21,14 +21,14 @@ import Morley.Michelson.Typed.Util  someDefinitionDocItemToContractDoc :: SomeDocDefinitionItem -> State ContractDoc ()-someDefinitionDocItemToContractDoc sdi@(SomeDocDefinitionItem di) =-  modify $ flip mappend+someDefinitionDocItemToContractDoc sdi@(SomeDocDefinitionItem di)+  | DocItemRef docItemId <- docItemRef di+  = modify $ flip mappend     mempty     { cdContents = mempty     , cdDefinitions = docItemToBlock di     , cdDefinitionsSet = one sdi-    , cdDefinitionIds = one $ case docItemRef di of-        DocItemRef docItemId -> docItemId+    , cdDefinitionIds = one docItemId     }  someDocItemToContractDoc :: SomeDocItem -> State ContractDoc ()

@@ -62,7 +62,7 @@ import GHC.Generics ((:*:)(..), (:+:)(..)) import GHC.Generics qualified as G import GHC.TypeLits (ErrorMessage(..), KnownSymbol, TypeError, symbolVal)-import Type.Showtype (Showtype(..))+import Morley.Util.ShowType (Showtype(..))  import Morley.Michelson.Doc import Morley.Michelson.Text@@ -210,7 +210,28 @@ instance TypeHasFieldNamingStrategy FieldSnakeCase where   typeFieldNamingStrategy = toSnake . dropPrefix --- | Description for a Haskell type appearing in documentation.+{- | Description for a Haskell type appearing in documentation.++Generic-deriving instance produces a custom error when 'Generic' is missing:++>>> data Foo = Foo () deriving TypeHasDoc+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = Foo () deriving Generic+>>> instance TypeHasDoc Foo where typeDocMdDescription = "Foo"+...+... No instance for (IsoValue Foo)+...++>>> data Foo = Foo () deriving (Generic, IsoValue)+>>> instance TypeHasDoc Foo where typeDocMdDescription = "Foo"++-} class ( Typeable a       , SingI (TypeDocFieldDescriptions a)       , FieldDescriptionsValid (TypeDocFieldDescriptions a) a@@ -260,7 +281,7 @@   -- Used in automatic types discovery.   typeDocDependencies :: Proxy a -> [SomeDocDefinitionItem]   default typeDocDependencies-    :: (Generic a, GTypeHasDoc (G.Rep a))+    :: (Generic a, GTypeHasDoc (GRep a))     => Proxy a -> [SomeDocDefinitionItem]   typeDocDependencies = genericTypeDocDependencies @@ -282,7 +303,7 @@   -- lorentz, for better naming consistency.   typeDocHaskellRep :: TypeDocHaskellRep a   default typeDocHaskellRep-    :: (Generic a, GTypeHasDoc (G.Rep a), IsHomomorphic a, TypeHasFieldNamingStrategy a)+    :: (Generic a, GTypeHasDoc (GRep a), IsHomomorphic a, TypeHasFieldNamingStrategy a)     => TypeDocHaskellRep a   typeDocHaskellRep = haskellRepMap (typeFieldNamingStrategy @a) homomorphicTypeDocHaskellRep @@ -473,10 +494,11 @@ -- | Require two types to be built from the same type constructor. -- -- E.g. @HaveCommonTypeCtor (Maybe Integer) (Maybe Natural)@ is defined,--- while @HaveCmmonTypeCtor (Maybe Integer) [Integer]@ is not.-class HaveCommonTypeCtor a b-instance HaveCommonTypeCtor ac bc => HaveCommonTypeCtor (ac a) (bc b)-instance HaveCommonTypeCtor a a+-- while @HaveCommonTypeCtor (Maybe Integer) [Integer]@ is not.+type HaveCommonTypeCtor :: forall {k}. k -> k -> Constraint+type family HaveCommonTypeCtor a b where+  HaveCommonTypeCtor (ac _) (bc _) = HaveCommonTypeCtor ac bc+  HaveCommonTypeCtor a a = ()  -- | Require this type to be homomorphic. class IsHomomorphic a where@@ -549,64 +571,126 @@     , DType (Proxy @b)     ] --- | Implement 'typeDocDependencies' via getting all immediate fields--- of a datatype.------ Note: this will not include phantom types, I'm not sure yet how this--- scenario should be handled (@martoon).+{- | Implement 'typeDocDependencies' via getting all immediate fields+of a datatype.++Produces a custom error message for missing 'Generic' instances:++>>> data Foo = Foo ()+>>> length $ genericTypeDocDependencies $ Proxy @Foo+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = Foo () deriving Generic+>>> length $ genericTypeDocDependencies $ Proxy @Foo+1++Note: this will not include phantom types, I'm not sure yet how this+scenario should be handled (@martoon).+-} genericTypeDocDependencies-  :: forall a.-      (Generic a, GTypeHasDoc (G.Rep a))+  :: forall a. (Generic a, GTypeHasDoc (GRep a))   => Proxy a -> [SomeDocDefinitionItem] genericTypeDocDependencies _ = do-  ConstructorRep{..} <- toList $ gTypeDocHaskellRep @(G.Rep a) []+  ConstructorRep{..} <- toList $ gTypeDocHaskellRep @(GRep a) []   FieldRep{..} <- crFields   SomeTypeWithDoc ty <- pure frTypeRep   return (dTypeDepP ty) --- | Implement 'typeDocHaskellRep' for a homomorphic type.------ Note that it does not require your type to be of 'IsHomomorphic' instance,--- which can be useful for some polymorphic types which, for documentation--- purposes, we want to consider homomorphic.------ Example: 'Operation' is in fact polymorphic, but we don't want this fact to--- be reflected in the documentation.+{- | Implement 'typeDocHaskellRep' for a homomorphic type.++Note that it does not require your type to be of 'IsHomomorphic' instance,+which can be useful for some polymorphic types which, for documentation+purposes, we want to consider homomorphic.++Example: 'Operation' is in fact polymorphic, but we don't want this fact to+be reflected in the documentation.++Produces a custom error message for missing 'Generic' instances:++>>> data Foo = Foo ()+>>> isJust $ homomorphicTypeDocHaskellRep (Proxy @Foo) []+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = Foo () deriving Generic+>>> isJust $ homomorphicTypeDocHaskellRep (Proxy @Foo) []+True+-} homomorphicTypeDocHaskellRep   :: forall a.-     (Generic a, GTypeHasDoc (G.Rep a))+     (Generic a, GTypeHasDoc (GRep a))   => TypeDocHaskellRep a homomorphicTypeDocHaskellRep _ descr = Just   ( Nothing-  , gTypeDocHaskellRep @(G.Rep a) descr+  , gTypeDocHaskellRep @(GRep a) descr   ) --- | Implement 'typeDocHaskellRep' on example of given concrete type.------ This is a best effort attempt to implement 'typeDocHaskellRep' for polymorphic--- types, as soon as there is no simple way to preserve type variables when--- automatically deriving Haskell representation of a type.+{- | Implement 'typeDocHaskellRep' on example of given concrete type.++This is a best effort attempt to implement 'typeDocHaskellRep' for polymorphic+types, as soon as there is no simple way to preserve type variables when+automatically deriving Haskell representation of a type.++Produces a custom error message for missing 'Generic' instances:++>>> data Foo a = Foo a+>>> isJust $ concreteTypeDocHaskellRep @(Foo Integer) @(Foo ()) Proxy []+...+... GHC.Generics.Rep (Foo Integer)+... is stuck. Likely+... Generic (Foo Integer)+... instance is missing or out of scope.+...++>>> data Foo a = Foo a deriving (Generic, IsoValue)+>>> isJust $ concreteTypeDocHaskellRep @(Foo Integer) @(Foo ()) Proxy []+True+-} concreteTypeDocHaskellRep   :: forall a b.-     ( Typeable a, GenericIsoValue a, GTypeHasDoc (G.Rep a)+     ( Typeable a, GenericIsoValue a, GTypeHasDoc (GRep a)      , HaveCommonTypeCtor b a      )   => TypeDocHaskellRep b concreteTypeDocHaskellRep = unsafeConcreteTypeDocHaskellRep @a --- | Version of 'concreteTypeDocHaskellRep' which does not ensure--- whether the type for which representation is built is any similar to--- the original type which you implement a 'TypeHasDoc' instance for.+{- | Version of 'concreteTypeDocHaskellRep' which does not ensure+whether the type for which representation is built is any similar to+the original type which you implement a 'TypeHasDoc' instance for.++>>> data Foo = Foo ()+>>> isJust $ unsafeConcreteTypeDocHaskellRep @Foo @() Proxy []+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = Foo () deriving (Generic, IsoValue)+>>> isJust $ unsafeConcreteTypeDocHaskellRep @Foo @() Proxy []+True++-} unsafeConcreteTypeDocHaskellRep   :: forall a b.-     ( Typeable a, GenericIsoValue a, GTypeHasDoc (G.Rep a)+     ( Typeable a, GenericIsoValue a, GTypeHasDoc (GRep a)      )   => TypeDocHaskellRep b unsafeConcreteTypeDocHaskellRep _ descr = Just   ( Just (DocTypeRepLHS . toText . showtype $ Proxy @a)     -- ↑ this also shows kinds when poly-kinded type arguments are present,     -- but there seems to be no simple way to deal with this.-  , gTypeDocHaskellRep @(G.Rep a) descr+  , gTypeDocHaskellRep @(GRep a) descr   )  -- | Erase fields from Haskell datatype representation.

@@ -41,10 +41,17 @@ import Morley.Michelson.Typed.Instr import Morley.Michelson.Typed.Scope import Morley.Michelson.Typed.T (T)+import Morley.Util.Generic import Morley.Util.Label (Label) import Morley.Util.Named import Morley.Util.Type +{- $setup+>>> import Morley.Util.Named+>>> import Morley.Michelson.Typed+>>> import Fmt (pretty)+-}+ -- Fields lookup (helper) ---------------------------------------------------------------------------- @@ -61,7 +68,7 @@ -- -- Name might be either field record name, or one in 'NamedF' if -- field is wrapped using 'Named.(:!)' or 'Named.(:?)'.-type GetNamed name a = LNRequireFound name a (GLookupNamed name (G.Rep a))+type GetNamed name a = LNRequireFound name a (GLookupNamed name (GRep a))  -- | Force result of 'GLookupNamed' to be 'Just' type family LNRequireFound@@ -108,33 +115,86 @@   LNMergeFound name ('Just _) ('Just _) = TypeError     ('Text "Ambiguous reference to datatype field: " ':<>: 'ShowType name) --- | Get type of field by datatype it is contained in and field name.+{- | Get type of field by datatype it is contained in and field name.++>>> () :: GetFieldType ("foo" :! Bool, "bar" :! ()) "bar"+()++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () }+>>> () :: GetFieldType Foo "fooField2"+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () } deriving Generic+>>> () :: GetFieldType Foo "fooField2"+()++-} type GetFieldType dt name = LnrFieldType (GetNamed name dt)  ---------------------------------------------------------------------------- -- Value accessing instruction ---------------------------------------------------------------------------- --- | Make an instruction which accesses given field of the given datatype.+{- | Make an instruction which accesses given field of the given datatype.++>>> pretty $ instrToField @("foo" :! Bool, "bar" :! ()) #foo+[CAR]++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () }+>>> pretty $ instrToField @Foo #fooField1+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () } deriving (Generic, IsoValue)+>>> pretty $ instrToField @Foo #fooField1+[CAR]+-} instrToField   :: forall dt name st.      InstrGetFieldC dt name   => Label name -> Instr (ToT dt ': st) (ToT (GetFieldType dt name) ': st) instrToField _ =-  gInstrToField @name @(G.Rep dt) @(LnrBranch (GetNamed name dt))+  gInstrToField @name @(GRep dt) @(LnrBranch (GetNamed name dt))     @(GetFieldType dt name) --- | Make an instruction which copies given field of the given datatype.------ This behaves exactly as @Seq DUP (instrToField #name)@, but does not require--- the entire datatype to be dupable (the field ofc still must be dupable).------ If we follow the path from the root to the copied field in the pairs tree,--- the more nodes contain non-dupable elements in the subtree, the less--- efficient this function becomes.--- Assuming that all fields are accessed equally often, the most optimal--- representation would be to put all dupable elements to one subtree--- of the root, and all non-dupable elements in the second subtree of the root.+{- | Make an instruction which copies given field of the given datatype.++This behaves exactly as @Seq DUP (instrToField #name)@, but does not require+the entire datatype to be dupable (the field ofc still must be dupable).++If we follow the path from the root to the copied field in the pairs tree,+the more nodes contain non-dupable elements in the subtree, the less+efficient this function becomes.+Assuming that all fields are accessed equally often, the most optimal+representation would be to put all dupable elements to one subtree+of the root, and all non-dupable elements in the second subtree of the root.++>>> pretty $ instrGetField @("foo" :! Bool, "bar" :! ()) #foo+[DUP, CAR]++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () }+>>> pretty $ instrGetField @Foo #fooField1+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () } deriving (Generic, IsoValue)+>>> pretty $ instrGetField @Foo #fooField1+[DUP, CAR]++-} instrGetField   :: forall dt name st.      (InstrGetFieldC dt name, DupableScope (ToT (GetFieldType dt name)))@@ -165,13 +225,13 @@   -> Label name   -> Instr (ToT dt ': st) (res ': ToT dt ': st) instrGetFieldOpen contWDup contWoDup _ =-  gInstrGetFieldOpen @name @(G.Rep dt) @(LnrBranch (GetNamed name dt))+  gInstrGetFieldOpen @name @(GRep dt) @(LnrBranch (GetNamed name dt))     @(GetFieldType dt name) contWDup contWoDup  -- | Constraint for 'instrGetField'. type InstrGetFieldC dt name =   ( GenericIsoValue dt-  , GInstrGet name (G.Rep dt)+  , GInstrGet name (GRep dt)       (LnrBranch (GetNamed name dt))       (LnrFieldType (GetNamed name dt))   )@@ -270,7 +330,24 @@ -- Value modification instruction ---------------------------------------------------------------------------- --- | For given complex type @dt@ and its field @fieldTy@ update the field value.+{- | For given complex type @dt@ and its field @fieldTy@ update the field value.++>>> pretty $ instrSetField @("foo" :! Bool, "bar" :! ()) #foo+[DIP { UNPAIR }, DIP { DROP }, PAIR]++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () }+>>> pretty $ instrSetField @Foo #fooField1+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () } deriving (Generic, IsoValue)+>>> pretty $ instrSetField @Foo #fooField1+[DIP { UNPAIR }, DIP { DROP }, PAIR]+-} instrSetField   :: forall dt name st.      InstrSetFieldC dt name@@ -290,13 +367,13 @@   -> Label name   -> Instr (new ': ToT dt ': st) (ToT dt ': st) instrSetFieldOpen cont _ =-  gInstrSetFieldOpen @name @(G.Rep dt) @(LnrBranch (GetNamed name dt))+  gInstrSetFieldOpen @name @(GRep dt) @(LnrBranch (GetNamed name dt))     @(GetFieldType dt name) cont  -- | Constraint for 'instrSetField'. type InstrSetFieldC dt name =   ( GenericIsoValue dt-  , GInstrSetField name (G.Rep dt)+  , GInstrSetField name (GRep dt)       (LnrBranch (GetNamed name dt))       (LnrFieldType (GetNamed name dt))   )@@ -363,24 +440,42 @@   :: forall dt st. InstrConstructC dt   => Rec (FieldConstructor st) (ConstructorFieldTypes dt)   -> Instr st (ToT dt ': st)-instrConstruct = fst . gInstrConstruct @(G.Rep dt) @'[]+instrConstruct = fst . gInstrConstruct @(GRep dt) @'[] +{- | Construct a complex datatype from values on stack++>>> pretty $ instrConstructStack @("foo" :! Bool, "bar" :! ())+[DIP {  }, PAIR]++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () }+>>> pretty $ instrConstructStack @Foo+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () } deriving (Generic, IsoValue)+>>> pretty $ instrConstructStack @Foo+[DIP {  }, PAIR]+-} instrConstructStack   :: forall dt stack st .   ( InstrConstructC dt   , stack ~ ToTs (ConstructorFieldTypes dt)   )   => Instr (stack ++ st) (ToT dt ': st)-instrConstructStack = gInstrConstructStack @(G.Rep dt) @'[] (proxy# @st)+instrConstructStack = gInstrConstructStack @(GRep dt) @'[] (proxy# @st)  -- | Types of all fields in a datatype.-type ConstructorFieldTypes dt = GFieldTypes (G.Rep dt) '[]+type ConstructorFieldTypes dt = GFieldTypes (GRep dt) '[]  -- | Names of all fields in a datatype.-type ConstructorFieldNames dt = GFieldNames (G.Rep dt)+type ConstructorFieldNames dt = GFieldNames (GRep dt)  -- | Constraint for 'instrConstruct' and 'gInstrConstructStack'.-type InstrConstructC dt = (GenericIsoValue dt, GInstrConstruct (G.Rep dt) '[])+type InstrConstructC dt = (GenericIsoValue dt, GInstrConstruct (GRep dt) '[])  -- | Retrieve field names of a constructor. type family GFieldNames x :: [Symbol] where@@ -475,16 +570,34 @@ ----------------------------------------------------------------------------  -- | Constraint for 'instrConstruct'.-type InstrDeconstructC dt st = ( GenericIsoValue dt, GInstrDeconstruct (G.Rep dt) '[] st)+type InstrDeconstructC dt st = ( GenericIsoValue dt, GInstrDeconstruct (GRep dt) '[] st) --- | For given complex type @dt@ deconstruct it to its field types.+{- | For given complex type @dt@ deconstruct it to its field types.++>>> pretty $ instrDeconstruct @("foo" :! Bool, "bar" :! ())+[UNPAIR, DIP {  }]++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () }+>>> pretty $ instrDeconstruct @Foo+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = Foo { fooField1 :: Bool, fooField2 :: () } deriving (Generic, IsoValue)+>>> pretty $ instrDeconstruct @Foo+[UNPAIR, DIP {  }]++-} instrDeconstruct   :: forall dt stack (st :: [T]) .   (InstrDeconstructC dt st-  , stack ~ ToTs (GFieldTypes (G.Rep dt) '[])+  , stack ~ ToTs (GFieldTypes (GRep dt) '[])   )   => Instr (ToT dt ': st) (stack ++ st)-instrDeconstruct = gInstrDeconstruct @(G.Rep dt) @'[] @st+instrDeconstruct = gInstrDeconstruct @(GRep dt) @'[] @st  -- | Generic traversal for 'instrDeconstruct'. class GInstrDeconstruct (x :: Type -> Type) (rest :: [Type]) (st :: [T]) where

@@ -59,11 +59,18 @@ import Morley.Tezos.Address (Address) import Morley.Tezos.Core (ChainId, Mutez, Timestamp) import Morley.Tezos.Crypto (KeyHash, PublicKey, Signature)+import Morley.Util.Generic import Morley.Util.Label (Label) import Morley.Util.Named import Morley.Util.Type import Morley.Util.TypeTuple +{- $setup+>>> import Morley.Util.Named+>>> import Morley.Michelson.Typed+>>> import Fmt (pretty)+-}+ -- Constructors lookup (helper) ---------------------------------------------------------------------------- @@ -121,7 +128,7 @@ -- -- Transitivity means that if sum type consists of other sum types, -- they will be searched recursively.-type GetNamed name a = LNRequireFound name a (GLookupNamed name (G.Rep a))+type GetNamed name a = LNRequireFound name a (GLookupNamed name (GRep a))  -- | Force result of 'GLookupNamed' to be 'Just' type family LNRequireFound@@ -215,11 +222,11 @@ type CanGoDeeper (x :: Type) =   If (IsPrimitiveValue x)      'False-     (GCanGoDeeper (G.Rep x))+     (GCanGoDeeper (GRep x))  type family GLookupNamedDeeper (name :: Symbol) (x :: Type -> Type)           :: Maybe LookupNamedResult where-  GLookupNamedDeeper name (G.S1 _ (G.Rec0 y))  = GLookupNamed name (G.Rep y)+  GLookupNamedDeeper name (G.S1 _ (G.Rec0 y))  = GLookupNamed name (GRep y)   GLookupNamedDeeper name _ = TypeError     ('Text "Attempt to go deeper failed while looking for sum type constructor"      ':<>: 'ShowType name@@ -250,8 +257,23 @@     --- ^ @martoon: Probably we will have no use cases for such scenario     --- anyway, tuples seem to be not worse than separate fields in most cases. --- | Get type of constructor fields (one or zero) referred by given datatype--- and name.+{- | Get type of constructor fields (one or zero) referred by given datatype and+name.++>>> data Foo = Foo1 Bool | Foo2 ()+>>> () :: CtorOnlyField "Foo2" Foo+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = Foo1 Bool | Foo2 () deriving Generic+>>> :kind! GetCtorField Foo "Foo2"+...+= 'OneField ()+-} type GetCtorField dt ctor =   LnrFieldType (GetNamed ctor dt) @@ -275,13 +297,28 @@ -- Constructor wrapping instruction ---------------------------------------------------------------------------- --- | Wrap given element into a constructor with the given name.------ Mentioned constructor must have only one field.------ Since labels interpretable by @OverloadedLabels@ extension cannot--- start with capital latter, prepend constructor name with letter--- "c" (see examples below).+{- | Wrap given element into a constructor with the given name.++Mentioned constructor must have only one field.++Since labels interpretable by @OverloadedLabels@ extension cannot start with+capital latter, prepend constructor name with letter "c" (see examples below).++>>> data Foo = FooCtor () | FooCtor2 Bool+>>> instrWrap @Foo #cFooCtor+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = FooCtor | FooCtor2 Bool deriving (Generic, IsoValue)+>>> pretty $ instrWrap @Foo #cFooCtor2+[RIGHT unit]+>>> pretty $ instrWrap @Foo #cFooCtor+[PUSH unit Unit, LEFT bool]+-} instrWrap   :: forall dt name st.      InstrWrapC dt name@@ -289,23 +326,42 @@   -> Instr (AppendCtorField (GetCtorField dt name) st)            (ToT dt ': st) instrWrap _ =-  gInstrWrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))+  gInstrWrap @(GRep dt) @(LnrBranch (GetNamed name dt))                          @(LnrFieldType (GetNamed name dt)) --- | Like 'instrWrap' but only works for contructors with a single field.--- Results in a type error if a constructor with no field is used instead.+{- | Like 'instrWrap' but only works for contructors with a single field.+Results in a type error if a constructor with no field is used instead.++>>> data Foo = FooCtor | FooCtor2 Bool+>>> instrWrapOne @Foo #cFooCtor+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...++>>> data Foo = FooCtor | FooCtor2 Bool deriving (Generic, IsoValue)+>>> pretty $ instrWrapOne @Foo #cFooCtor2+[RIGHT unit]+>>> pretty $ instrWrapOne @Foo #cFooCtor+...+... Expected exactly one field+... In constructor "cFooCtor"+...+-} instrWrapOne   :: forall dt name st.      InstrWrapOneC dt name   => Label name   -> Instr (ToT (CtorOnlyField name dt) ': st) (ToT dt ': st) instrWrapOne _ =-  gInstrWrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))+  gInstrWrap @(GRep dt) @(LnrBranch (GetNamed name dt))                          @(LnrFieldType (GetNamed name dt))  type InstrWrapC dt name =   ( GenericIsoValue dt-  , GInstrWrap (G.Rep dt)+  , GInstrWrap (GRep dt)       (LnrBranch (GetNamed name dt))       (LnrFieldType (GetNamed name dt))   )@@ -325,7 +381,7 @@   -> ExtractCtorField (GetCtorField dt name)   -> dt hsWrap _ =-  G.to . gHsWrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))+  G.to . gHsWrap @(GRep dt) @(LnrBranch (GetNamed name dt))                              @(LnrFieldType (GetNamed name dt))  -- | Generic traversal for 'instrWrap'.@@ -360,12 +416,12 @@ -- This is the case when a sum type is part of another sum type. -- Here 'sub' is intermediate sum type. instance ( path ~ (x ': xs)-         , GInstrWrap (G.Rep sub) path e+         , GInstrWrap (GRep sub) path e          , GenericIsoValue sub          ) =>          GInstrWrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where-  gInstrWrap = gInstrWrap @(G.Rep sub) @path @e-  gHsWrap = G.M1 . G.M1 . G.K1 . G.to . gHsWrap @(G.Rep sub) @path @e+  gInstrWrap = gInstrWrap @(GRep sub) @path @e+  gHsWrap = G.M1 . G.M1 . G.K1 . G.to . gHsWrap @(GRep sub) @path @e  instance GInstrWrap (G.C1 c G.U1) '[ 'S] 'NoFields where   gInstrWrap = PUSH VUnit@@ -485,9 +541,9 @@   :: forall dt out inp.      InstrCaseC dt   => Rec (CaseClause inp out) (CaseClauses dt) -> RemFail Instr (ToT dt ': inp) out-instrCase = fst . gInstrCase @(G.Rep dt) @'[]+instrCase = fst . gInstrCase @(GRep dt) @'[] -type InstrCaseC dt = (GenericIsoValue dt, GInstrCase (G.Rep dt) '[])+type InstrCaseC dt = (GenericIsoValue dt, GInstrCase (GRep dt) '[])  -- | In what different case branches differ - related constructor name and -- input stack type which the branch starts with.@@ -515,7 +571,7 @@ infixr 8 //->  -- | List of 'CaseClauseParam's required to pattern match on the given type.-type CaseClauses a = GCaseClauses (G.Rep a) '[]+type CaseClauses a = GCaseClauses (GRep a) '[]   -- | Generic traversal for 'instrWrap'.@@ -621,12 +677,12 @@   -> Instr (ToT dt ': st)            (ToT (CtorOnlyField name dt) ': st) unsafeInstrUnwrap _ =-  unsafeGInstrUnwrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))+  unsafeGInstrUnwrap @(GRep dt) @(LnrBranch (GetNamed name dt))                                  @(CtorOnlyField name dt)  type InstrUnwrapC dt name =   ( GenericIsoValue dt-  , GInstrUnwrap (G.Rep dt)+  , GInstrUnwrap (GRep dt)       (LnrBranch (GetNamed name dt))       (CtorOnlyField name dt)   )@@ -639,7 +695,7 @@   -> dt   -> Maybe (CtorOnlyField name dt) hsUnwrap _ =-  gHsUnwrap @(G.Rep dt) @(LnrBranch (GetNamed name dt))+  gHsUnwrap @(GRep dt) @(LnrBranch (GetNamed name dt))             @(CtorOnlyField name dt) .   G.from @@ -678,12 +734,12 @@ -- This is the case when a sum type is part of another sum type. -- Here 'sub' is intermediate sum type. instance ( path ~ (x ': xs)-         , GInstrUnwrap (G.Rep sub) path e+         , GInstrUnwrap (GRep sub) path e          , GenericIsoValue sub          ) =>          GInstrUnwrap (G.C1 c (G.S1 i (G.Rec0 sub))) ('S ': x ': xs) e where-  unsafeGInstrUnwrap = unsafeGInstrUnwrap @(G.Rep sub) @path @e-  gHsUnwrap = gHsUnwrap @(G.Rep sub) @path @e . G.from . G.unK1 . G.unM1 . G.unM1+  unsafeGInstrUnwrap = unsafeGInstrUnwrap @(GRep sub) @path @e+  gHsUnwrap = gHsUnwrap @(GRep sub) @path @e . G.from . G.unK1 . G.unM1 . G.unM1  -- | Failure indicating that we expected value created with one constructor, -- but got value with different one.

@@ -27,6 +27,7 @@ import Morley.Michelson.Typed.Existential import Morley.Michelson.Typed.Haskell.Value import Morley.Michelson.Typed.T+import Morley.Util.Generic import Morley.Util.Sing (castSing) import Morley.Util.TypeLits @@ -40,7 +41,7 @@   | ComposeFieldTypeMismatch T T     -- ^ Found required constructor, but type of data does not correspond     -- to provided one.-  deriving stock (Functor)+  deriving stock (Show, Functor)  instance Semigroup (ComposeResult a) where   r@(ComposeOk _) <> _ = r@@ -55,15 +56,51 @@  -- | Constraint for 'toTaggedVal' and 'fromTaggedVal'. type LooseSumC dt =-  ( Generic dt, GLooseSum (G.Rep dt)+  ( NiceGeneric dt, GLooseSum (GRep dt)   ) --- | Decompose Haskell type into constructor name and--- data it carries, converting the latter into Michelson 'Value'.+{- | Decompose Haskell type into constructor name and+data it carries, converting the latter into Michelson 'Value'.++>>> toTaggedVal $ Just ()+("Just",Constrained VUnit)++A custom TypeError is generated if a type doesn't have a 'Generic' instance++>>> data Foo = Foo ()+>>> toTaggedVal $ Foo ()+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...+>>> data Foo = Foo () deriving Generic+>>> toTaggedVal $ Foo ()+("Foo",Constrained VUnit)+-} toTaggedVal :: LooseSumC dt => dt -> (Text, SomeValue) toTaggedVal = gToTaggedVal . G.from --- | Inverse to 'toTaggedVal'.+{- | Inverse to 'toTaggedVal'.++>>> import Morley.Michelson.Typed++>>> fromTaggedVal @(Maybe ()) ("Just", SomeValue VUnit)+ComposeOk (Just ())++>>> data Foo = Foo () deriving Show+>>> fromTaggedVal @Foo ("Foo", SomeValue VUnit)+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...+>>> data Foo = Foo () deriving (Show, Generic)+>>> fromTaggedVal @Foo ("Foo", SomeValue VUnit)+ComposeOk (Foo ())+-} fromTaggedVal :: LooseSumC dt => (Text, SomeValue) -> ComposeResult dt fromTaggedVal = fmap G.to . gFromTaggedVal 

@@ -51,12 +51,23 @@ -- | Value-level counterpart to 'FieldDescriptions'. type FieldDescriptionsV = Demote FieldDescriptions --- | This type family checks that field descriptions mention only existing constructors and fields.------ When @descr@ is empty this family does nothing, to avoid breaking for built-in, non-ADT types.------ When @descr@ is not empty, this family will demand 'G.Generic' instance for @typ@ and fail with a--- @TypeError@ if there none.+{- | This type family checks that field descriptions mention only existing constructors and fields.++When @descr@ is empty this family does nothing, to avoid breaking for built-in, non-ADT types.++When @descr@ is not empty, this family will demand 'G.Generic' instance for @typ@ and fail with a+@TypeError@ if there none.++>>> data Foo = Foo { fooField :: () } -- no Generic instance+>>> () :: FieldDescriptionsValid '[ '("Foo", '(Nothing, '[ '("fooField", "")]))] Foo => ()+...+... No Generic instance for Foo.+... Generic is needed to validate TypeDocFieldDescriptions.+...+>>> data Foo = Foo { fooField :: () } deriving Generic+>>> () :: FieldDescriptionsValid '[ '("Foo", '(Nothing, '[ '("fooField", "")]))] Foo => ()+()+-} type FieldDescriptionsValid :: FieldDescriptions -> Type -> Constraint type family FieldDescriptionsValid descr typ where   FieldDescriptionsValid '[] _ = ()@@ -67,6 +78,8 @@          'Text "Generic is needed to validate TypeDocFieldDescriptions.")       )       (Fcf.Pure (FieldDescriptionsValidImpl descr typ))++-- Note: This module doesn't use 'Morley.Util.Generic.GRep' because it's already guarded.  -- | Actual recursive implementation for 'FieldDescriptionsValid'. type FieldDescriptionsValidImpl :: FieldDescriptions -> Type -> Constraint

@@ -59,6 +59,7 @@ import Morley.Tezos.Core (ChainId, Mutez, Timestamp) import Morley.Tezos.Crypto   (Bls12381Fr, Bls12381G1, Bls12381G2, Chest, ChestKey, KeyHash, PublicKey, Signature)+import Morley.Util.Generic import Morley.Util.Named import Morley.Util.SizedList.Types import Morley.Util.Type@@ -69,26 +70,41 @@  type KnownIsoT a = (IsoValue a, SingI (ToT a)) --- | Isomorphism between Michelson values and plain Haskell types.------ Default implementation of this typeclass converts ADTs to Michelson--- "pair"s and "or"s.+{- | Isomorphism between Michelson values and plain Haskell types.++Default implementation of this typeclass converts ADTs to Michelson+"pair"s and "or"s.++Can be derived generically. If the type is missing the 'Generic' instance, a+custom error is generated.++>>> data Foo = Foo+>>> instance IsoValue Foo+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...+>>> data Foo = Foo deriving Generic+>>> instance IsoValue Foo -- ok+-} class (WellTypedToT a) => IsoValue a where   -- | Type function that converts a regular Haskell type into a @T@ type.   type ToT a :: T-  type ToT a = GValueType (G.Rep a)+  type ToT a = GValueType (GRep a)    -- | Converts a Haskell structure into @Value@ representation.   toVal :: a -> Value (ToT a)   default toVal-    :: (Generic a, GIsoValue (G.Rep a), ToT a ~ GValueType (G.Rep a))+    :: (NiceGeneric a, GIsoValue (GRep a), ToT a ~ GValueType (GRep a))     => a -> Value (ToT a)   toVal = gToValue . G.from    -- | Converts a @Value@ into Haskell type.   fromVal :: Value (ToT a) -> a   default fromVal-    :: (Generic a, GIsoValue (G.Rep a), ToT a ~ GValueType (G.Rep a))+    :: (NiceGeneric a, GIsoValue (GRep a), ToT a ~ GValueType (GRep a))     => Value (ToT a) -> a   fromVal = G.to . gFromValue @@ -441,14 +457,14 @@   gToValue = \case   gFromValue = \case -instance IsoValue a => GIsoValue (G.Rec0 a) where+instance (IsoValue a, SingI (ToT a)) => GIsoValue (G.Rec0 a) where   type GValueType (G.Rec0 a) = ToT a   gToValue = toVal . G.unK1   gFromValue = G.K1 . fromVal  -- | Whether Michelson representation of the type is derived via Generics. type GenericIsoValue t =-  (IsoValue t, Generic t, ToT t ~ GValueType (G.Rep t))+  (IsoValue t, NiceGeneric t, ToT t ~ GValueType (GRep t))  ---------------------------------------------------------------------------- -- Stacks conversion

@@ -980,7 +980,7 @@                 inpV <- newName "inp"                 outV <- newName "out"                 let pat = PatSynD baseName (PrefixPatSyn args) (ExplBidir [cl])-                      (ConP nm $ WildP:(VarP <$> args))+                      (ConP nm [] $ WildP : (VarP <$> args))                     baseName = mkName base                     cl = Clause (VarP <$> args) (NormalB body) []                     body = foldl' AppE (ConE nm) $ (VarE $ 'def):(VarE <$> args)

@@ -108,7 +108,7 @@   \\ isLongerOrSameLengthExtThm @a @s n  dupNExtensionThm-  :: forall s a b n x. (b ~ x : a, ConstraintDUPN n a b x)+  :: forall s a b n x. (ConstraintDUPN n a b x)   => PeanoNatural n   -> Dict (ConstraintDUPN n (a ++ s) (b ++ s) x) dupNExtensionThm n@(Succ m) = Dict

@@ -70,7 +70,7 @@   type MapOpInp ('TOption e) = e   type MapOpRes ('TOption e) = 'TOption   mapOpToList (VOption l) = maybe [] pure l-  mapOpFromList (VOption _) l' = VOption $ listToMaybe l'+  mapOpFromList (VOption _) l' = VOption $ safeHead l'   mapOpNotes (NTOption _ n) = n -- If you find it difficult to implement 'MapOp' for your datatype -- because of order of type arguments in it, consider wrapping it

@@ -51,7 +51,6 @@      -- * Implementation internals   , ContainsT-  , IsComparable    , ForbidT   , ForbidOp@@ -61,14 +60,7 @@   , ForbidNestedBigMaps   , ForbidNonComparable -  , TPresence(..-      , OpPresent, OpAbsent-      , ContractPresent, ContractAbsent-      , TicketPresent, TicketAbsent-      , BigMapPresent, BigMapAbsent-      , NestedBigMapsPresent, NestedBigMapsAbsent-      , SaplingStatePresent, SaplingStateAbsent-      )+  , TPresence(..)   , TPredicateSym(..)   , SingTPredicateSym(..)   , checkTPresence@@ -85,43 +77,6 @@   , withDict   , SingI (..)   , (:-)(..)-    -- * Deprecated-  , OpPresence-  , ContractPresence-  , TicketPresence-  , BigMapPresence-  , NestedBigMapsPresence-  , ProperParameterBetterErrors-  , ProperStorageBetterErrors-  , ProperConstantBetterErrors-  , ProperDupableBetterErrors-  , ProperPackedValBetterErrors-  , ProperUnpackedValBetterErrors-  , ProperUntypedValBetterErrors-  , ProperViewableBetterErrors-  , ProperNonComparableValBetterErrors-  , opAbsense-  , contractTypeAbsense-  , bigMapAbsense-  , nestedBigMapsAbsense-  , checkOpPresence-  , checkContractTypePresence-  , checkTicketPresence-  , checkBigMapPresence-  , checkNestedBigMapsPresence-  , HasNoBigMap-  , HasNoNestedBigMaps-  , HasNoOp-  , HasNoContract-  , HasNoTicket-  , ContainsBigMap-  , ContainsContract-  , ContainsNestedBigMaps-  , ContainsOp-  , ContainsTicket-  , comparabilityImpliesNoNestedBigMaps-  , comparabilityImpliesNoOp-  , getComparableProofS   ) where  import Data.Constraint (withDict, (:-)(..))@@ -129,7 +84,6 @@  import Morley.Michelson.Typed.Scope.Internal.CheckScope import Morley.Michelson.Typed.Scope.Internal.Comparable-import Morley.Michelson.Typed.Scope.Internal.Deprecated import Morley.Michelson.Typed.Scope.Internal.ForbidT import Morley.Michelson.Typed.Scope.Internal.Presence import Morley.Michelson.Typed.Scope.Internal.Scopes

@@ -1,299 +0,0 @@--- SPDX-FileCopyrightText: 2023 Oxhead Alpha--- SPDX-License-Identifier: LicenseRef-MIT-OA--{-# OPTIONS_HADDOCK not-home #-}--module Morley.Michelson.Typed.Scope.Internal.Deprecated-  ( module Morley.Michelson.Typed.Scope.Internal.Deprecated-  ) where--import Data.Constraint (Dict(..), (\\))-import Data.Singletons (Sing, SingI(..))-import Data.Type.Bool (Not)-import Data.Type.Equality ((:~:)(..))--import Morley.Michelson.Typed.Scope.Internal.Comparable-import Morley.Michelson.Typed.Scope.Internal.ForbidT-import Morley.Michelson.Typed.Scope.Internal.Presence-import Morley.Michelson.Typed.Scope.Internal.WellTyped-import Morley.Michelson.Typed.Sing (SingT(..))-import Morley.Michelson.Typed.T (T(..))-import Morley.Util.StubbedProof (stubProof)---- | Whether a value of this type _may_ contain an operation.------ In some scopes (constants, parameters, storage) appearing for operation type--- is prohibited.--- Operations in input/output of lambdas are allowed without limits though.-type ContainsOp t = ContainsT 'PSOp t---- | Whether a value of this type _may_ contain a @contract@ value.------ In some scopes (constants, storage) appearing for contract type--- is prohibited.--- Contracts in input/output of lambdas are allowed without limits though.-type ContainsContract t = ContainsT 'PSContract t---- | Whether a value of this type _may_ contain a @ticket@ value.-type ContainsTicket t = ContainsT 'PSTicket t---- | Whether a value of this type _may_ contain a @big_map@ value.-type ContainsBigMap t = ContainsT 'PSBigMap t---- | Whether a value of this type _may_ contain nested @big_map@s.------ Nested big_maps (i.e. big_map which contains another big_map inside of it's value type) are--- prohibited in all contexts. Some context such as PUSH, APPLY, PACK/UNPACK instructions are more--- strict because they don't work with big_map at all.-type ContainsNestedBigMaps t = ContainsT 'PSNestedBigMaps t---- | Whether a value of this type _may_ contain a @samping_state@ value.-type ContainsSaplingState t = ContainsT 'PSSaplingState t--{-# DEPRECATED-  ContainsOp-  , ContainsContract-  , ContainsTicket-  , ContainsBigMap-  , ContainsNestedBigMaps-  , ContainsSaplingState-  "Use 'ContainsT' with the corresponding type marker, e.g. \-  \'ContainsT PSOp', 'ContainsT PSTicket', etc"-  #-}----- | Constraint which ensures that a value of type @t@ does not contain operations.------ Not just a type alias in order to be able to partially apply it--- (e.g. in 'Each').-class (ContainsOp t ~ 'False) => HasNoOp t-instance (ContainsOp t ~ 'False) => HasNoOp t---- | Constraint which ensures that a value of type @t@ does not contain @contract@ values.-class (ContainsContract t ~ 'False) => HasNoContract t-instance (ContainsContract t ~ 'False) => HasNoContract t---- | Constraint which ensures that a value of type @t@ does not contain @ticket@ values.-class (ContainsTicket t ~ 'False) => HasNoTicket t-instance (ContainsTicket t ~ 'False) => HasNoTicket t---- | Constraint which ensures that a value of type @t@ does not contain @big_map@ values.-class (ContainsBigMap t ~ 'False) => HasNoBigMap t-instance (ContainsBigMap t ~ 'False) => HasNoBigMap t---- | Constraint which ensures that a value of type @t@ does not contain @sapling_state@ values.-class (ContainsSaplingState t ~ 'False) => HasNoSaplingState t-instance (ContainsSaplingState t ~ 'False) => HasNoSaplingState t---- | Constraint which ensures that there are no nested bigmaps.-class (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t-instance (ContainsNestedBigMaps t ~ 'False) => HasNoNestedBigMaps t--{-# DEPRECATED HasNoOp, HasNoContract, HasNoTicket, HasNoBigMap, HasNoSaplingState, HasNoNestedBigMaps-  "Use Forbid* instead" #-}----- | Whether a value of this type _may_ contain an operation.-type OpPresence (t :: T) = TPresence 'PSOp t-pattern OpPresent :: () => ContainsOp t ~ 'True => OpPresence t-pattern OpPresent = TPresent-pattern OpAbsent :: () => ContainsOp t ~ 'False => OpPresence t-pattern OpAbsent = TAbsent-{-# COMPLETE OpPresent, OpAbsent #-}---- | Whether a value of this type _may_ contain a @contract@ value.-type ContractPresence (t :: T) = TPresence 'PSContract t-pattern ContractPresent :: () => ContainsContract t ~ 'True => ContractPresence t-pattern ContractPresent = TPresent-pattern ContractAbsent :: () => ContainsContract t ~ 'False => ContractPresence t-pattern ContractAbsent = TAbsent-{-# COMPLETE ContractPresent, ContractAbsent #-}---- | Whether a value of this type _may_ contain a @ticket@ value.-type TicketPresence (t :: T) = TPresence 'PSTicket t-pattern TicketPresent :: () => ContainsTicket t ~ 'True => TicketPresence t-pattern TicketPresent = TPresent-pattern TicketAbsent :: () => ContainsTicket t ~ 'False => TicketPresence t-pattern TicketAbsent = TAbsent-{-# COMPLETE TicketPresent, TicketAbsent #-}---- | Whether a value of this type _may_ contain a @big_map@ value.-type BigMapPresence (t :: T) = TPresence 'PSBigMap t-pattern BigMapPresent :: () => ContainsBigMap t ~ 'True => BigMapPresence t-pattern BigMapPresent = TPresent-pattern BigMapAbsent :: () => ContainsBigMap t ~ 'False => BigMapPresence t-pattern BigMapAbsent = TAbsent-{-# COMPLETE BigMapPresent, BigMapAbsent #-}---- | Whether a value of this type _may_ contain nested @big_map@s.-type NestedBigMapsPresence (t :: T) = TPresence 'PSNestedBigMaps t-pattern NestedBigMapsPresent :: () => ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresence t-pattern NestedBigMapsPresent = TPresent-pattern NestedBigMapsAbsent :: () => ContainsNestedBigMaps t ~ 'False => NestedBigMapsPresence t-pattern NestedBigMapsAbsent = TAbsent-{-# COMPLETE NestedBigMapsPresent, NestedBigMapsAbsent #-}---- | Whether a value of this type _may_ contain a @sapling_state@ value.-type SaplingStatePresence (t :: T) = TPresence 'PSSaplingState t-pattern SaplingStatePresent :: () => ContainsSaplingState t ~ 'True => SaplingStatePresence t-pattern SaplingStatePresent = TPresent-pattern SaplingStateAbsent :: () => ContainsSaplingState t ~ 'False => SaplingStatePresence t-pattern SaplingStateAbsent = TAbsent-{-# COMPLETE SaplingStatePresent, SaplingStateAbsent #-}--{-# DEPRECATED-  OpPresence, OpPresent, OpAbsent-  , ContractPresence, ContractPresent, ContractAbsent-  , TicketPresence, TicketPresent, TicketAbsent-  , BigMapPresence, BigMapPresent, BigMapAbsent-  , NestedBigMapsPresence, NestedBigMapsPresent, NestedBigMapsAbsent-  , SaplingStatePresence, SaplingStatePresent, SaplingStateAbsent-  "Use TPresence instead" #-}--type ProperParameterBetterErrors t =-  (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t)--type ProperStorageBetterErrors t =-  (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t)--type ProperConstantBetterErrors t =-  (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidContract t, ForbidTicket t, ForbidSaplingState t)--type ProperDupableBetterErrors t =-  (SingI t, ForbidTicket t)--type ProperPackedValBetterErrors t =-  (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidTicket t, ForbidSaplingState t)--type ProperUnpackedValBetterErrors t =-  (ProperPackedValBetterErrors t, ProperConstantBetterErrors t)--type ProperViewableBetterErrors t =-  (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t)--type ProperUntypedValBetterErrors t =-  (SingI t, ForbidOp t)--type ProperNonComparableValBetterErrors t =-  (SingI t, ForbidNonComparable t)--{-# DEPRECATED ProperParameterBetterErrors-  , ProperStorageBetterErrors-  , ProperConstantBetterErrors-  , ProperDupableBetterErrors-  , ProperPackedValBetterErrors-  , ProperUnpackedValBetterErrors-  , ProperViewableBetterErrors-  , ProperUntypedValBetterErrors-  , ProperNonComparableValBetterErrors-  "Use *Scope instead"-  #-}---- | Check at runtime whether a value of the given type _may_ contain an operation.-checkOpPresence :: Sing (ty :: T) -> TPresence 'PSOp ty-checkOpPresence = checkTPresence SPSOp---- | Check at runtime whether a value of the given type _may_ contain a @contract@ value.-checkContractTypePresence :: Sing (ty :: T) -> TPresence 'PSContract ty-checkContractTypePresence = checkTPresence SPSContract---- | Check at runtime whether a value of the given type _may_ contain a @ticket@ value.-checkTicketPresence :: Sing (ty :: T) -> TPresence 'PSTicket ty-checkTicketPresence = checkTPresence SPSTicket---- | Check at runtime whether a value of the given type _may_ contain a @big_map@ value.-checkBigMapPresence :: Sing (ty :: T) -> TPresence 'PSBigMap ty-checkBigMapPresence = checkTPresence SPSBigMap---- | Check at runtime whether a value of the given type _may_ contain nested @big_map@s.-checkNestedBigMapsPresence :: Sing (ty :: T) -> TPresence 'PSNestedBigMaps ty-checkNestedBigMapsPresence = checkTPresence SPSNestedBigMaps--{-# DEPRECATED checkOpPresence, checkContractTypePresence, checkTicketPresence, checkBigMapPresence, checkNestedBigMapsPresence-  "Use checkTPresence instead" #-}---- | Check at runtime that a value of the given type cannot contain operations.-opAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidOp t)-opAbsense = fmap (\Refl -> Dict) . tAbsence SPSOp---- | Check at runtime that a value of the given type cannot contain @contract@ values.-contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidContract t)-contractTypeAbsense = fmap (\Refl -> Dict) . tAbsence SPSContract---- | Check at runtime that a value of the given type cannot containt @big_map@ values-bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidBigMap t)-bigMapAbsense = fmap (\Refl -> Dict) . tAbsence SPSBigMap---- | Check at runtime that a value of the given type cannot contain nested @big_map@s.-nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ ForbidNestedBigMaps t)-nestedBigMapsAbsense = fmap (\Refl -> Dict) . tAbsence SPSNestedBigMaps--{-# DEPRECATED opAbsense, contractTypeAbsense, bigMapAbsense, nestedBigMapsAbsense-  "Use tAbsence instead"- #-}---- | Inductive proof that 'Comparable' implies 'HasNoNestedBigMaps'. This is--- stubbed with an @unsafeCoerce Refl@ at runtime to avoid runtime traversals.-comparabilityImpliesNoNestedBigMaps-  :: forall t. (SingI t, IsComparable t ~ 'True) => ContainsNestedBigMaps t :~: 'False-comparabilityImpliesNoNestedBigMaps = stubProof $ go (sing @t)-  where-    go :: IsComparable a ~ 'True => Sing a -> ContainsNestedBigMaps a :~: 'False-    go = \case-      STPair (a :: Sing a) (b :: Sing b) -> case (checkComparability a, checkComparability b) of-        (CanBeCompared, CanBeCompared) -> Refl \\ go a \\ go b-      STOr a b -> case (checkComparability a, checkComparability b) of-        (CanBeCompared, CanBeCompared) -> Refl \\ go a \\ go b-      STOption t -> Refl \\ go t-      STNever -> Refl-      STUnit -> Refl-      STInt -> Refl-      STNat -> Refl-      STString -> Refl-      STBytes -> Refl-      STMutez -> Refl-      STBool -> Refl-      STKeyHash -> Refl-      STTimestamp -> Refl-      STAddress -> Refl-      STKey -> Refl-      STSignature -> Refl-      STChainId -> Refl---- | Inductive proof that 'Comparable' implies 'HasNoOp'. This is--- stubbed with an @unsafeCoerce Refl@ at runtime to avoid runtime traversals.-comparabilityImpliesNoOp-  :: forall t. (SingI t, IsComparable t ~ 'True) => ContainsOp t :~: 'False-comparabilityImpliesNoOp = stubProof $ go (sing @t)-  where-    go :: IsComparable a ~ 'True => Sing a -> ContainsOp a :~: 'False-    go = \case-      STPair (a :: Sing a) (b :: Sing b) -> case (checkComparability a, checkComparability b) of-        (CanBeCompared, CanBeCompared) -> Refl \\ go a \\ go b-      STOr a b -> case (checkComparability a, checkComparability b) of-        (CanBeCompared, CanBeCompared) -> Refl \\ go a \\ go b-      STOption t -> Refl \\ go t-      STNever -> Refl-      STUnit -> Refl-      STInt -> Refl-      STNat -> Refl-      STString -> Refl-      STBytes -> Refl-      STMutez -> Refl-      STBool -> Refl-      STKeyHash -> Refl-      STTimestamp -> Refl-      STAddress -> Refl-      STKey -> Refl-      STSignature -> Refl-      STChainId -> Refl--{-# DEPRECATED comparabilityImpliesNoNestedBigMaps, comparabilityImpliesNoOp-  "Already implied by Comparable constraint" #-}--getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a))-getComparableProofS = comparabilityPresence-{-# DEPRECATED getComparableProofS "Use comparabilityPresence" #-}--type IsComparable t = Not (ContainsT 'PSNonComparable t)-{-# DEPRECATED IsComparable "Use 'Not (ContainsT PSNonComparable t)' instead" #-}

@@ -8,9 +8,8 @@   ) where  import Data.Type.Bool (type (||))-import Fcf (Pure)-import GHC.TypeLits (Symbol)-import Type.Errors (DelayError, ErrorMessage(..), IfStuck)+import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError)+import Type.Errors (WhenStuck)  import Morley.Michelson.Typed.T (T(..)) import Morley.Util.Sing@@ -184,8 +183,8 @@ instance ForbidManyT' c ps' '[] t where   type ForbidManySuperC '[] _ = () instance-  ( IfStuck (ContainsT p t) (DelayError (ForbidManyTStuckErr c ps' t)) (Pure (ForbidManyT' c ps' ps t))-  , FailWhen (ContainsT p t) (ForbidTErrorMsg p t)+  ( ForbidManyT' c ps' ps t+  , DelayedContainsTCheck c ps' p t (ContainsT p t)   ) => ForbidManyT' c ps' (p : ps) t where     type ForbidManySuperC (p : ps) t =       -- NB: WhenStuck isn't in the superclass constraints by design, as@@ -193,6 +192,17 @@       ( ContainsT p t ~ 'False       , ForbidManySuperC ps t       )++-- | This is a horrible hack designed to delay GHC's test for equality of+-- ContainsT ... with False. Unfortunately, due to the use of incoherence, more+-- type signatures will be required downstream. But the impact seems somewhat+-- minimal in practice.+class a ~ 'False => DelayedContainsTCheck c ps' p t a+instance DelayedContainsTCheck c ps' p t 'False+instance {-# incoherent #-}+  ( WhenStuck t (TypeError (ForbidManyTStuckErr c ps' t))+  , FailWhen a (ForbidTErrorMsg p t)+  ) => DelayedContainsTCheck c ps' p t a  {- | Abstracts multiple 'ForbidT' constraints. Accepts a constraint that will be suggested in an error message in case 'ContainsT' gets stuck. This is used with

@@ -46,14 +46,14 @@  >>> () :: ParameterScope (TBigMap TUnit (TBigMap TUnit TOperation)) => () ...-... Nested `big_map`s found in-... 'TBigMap 'TUnit ('TBigMap 'TUnit 'TOperation)-... are not allowed-... ... Type `operation` found in ... 'TBigMap 'TUnit ('TBigMap 'TUnit 'TOperation) ... is not allowed in this scope ...+... Nested `big_map`s found in+... 'TBigMap 'TUnit ('TBigMap 'TUnit 'TOperation)+... are not allowed+... >>> () :: ParameterScope (TBigMap TInt TNat) => () () @@ -80,12 +80,12 @@  >>> () :: StorageScope (TContract TOperation) => () ...-... Type `contract` found in-... 'TContract 'TOperation-... is not allowed in this scope-... ... Type `operation` found in ... 'TOperation+... is not allowed in this scope+...+... Type `contract` found in+... 'TContract 'TOperation ... is not allowed in this scope ... >>> () :: StorageScope TUnit => ()

@@ -22,7 +22,6 @@   , buildVContract   , checkComparability   , compileEpLiftSequence-  , getComparableProofS   , liftCallArg   , valueTypeSanity   , withValueTypeSanity@@ -460,4 +459,4 @@ type instance IxValue (Value' _ ('TSet _)) = () instance Ixed (Value' instr ('TSet a)) instance At (Value' instr ('TSet a)) where-  at key handler (VSet vset) = VSet<$> at key handler vset+  at key handler (VSet vset) = VSet <$> at key handler vset

@@ -18,7 +18,7 @@   , someViewName      -- * Views set-  , ViewsSet' (.., ViewsList, UnsafeViewsSet)+  , ViewsSet' (.., ViewsList)   , VS.ViewsSetError (..)   , mkViewsSet   , emptyViewsSet@@ -82,11 +82,6 @@ -- | Views that belong to one contract. newtype ViewsSet' instr st = ViewsSet { unViewsSet :: Map ViewName (SomeView' instr st) }   deriving newtype (Default, Container)--pattern UnsafeViewsSet :: Map ViewName (SomeView' instr st) -> ViewsSet' instr st-pattern UnsafeViewsSet x = ViewsSet x-{-# COMPLETE UnsafeViewsSet #-}-{-# DEPRECATED UnsafeViewsSet "Use ViewsSet instead" #-}  deriving stock instance   (forall i o. Show (instr i o)) =>

@@ -48,6 +48,8 @@   , renderAnyAnns   ) where +import Prelude hiding (lift)+ import Data.Aeson.TH (deriveJSON) import Data.Char (isAlpha, isAscii, isDigit, isNumber) import Data.Data (Data(..))@@ -58,7 +60,7 @@ import Instances.TH.Lift () import Language.Haskell.TH qualified as TH import Language.Haskell.TH.Quote qualified as TH-import Language.Haskell.TH.Syntax (Lift)+import Language.Haskell.TH.Syntax (Lift(..)) import Prettyprinter (hsep) import Text.Show qualified as T import Type.Reflection (tyConName, typeRep, typeRepTyCon)

@@ -59,8 +59,8 @@  instance Buildable ExpandedOp where   build (WithSrcEx _ op) = build op-  build (PrimEx expandedInstr) = "<PrimEx: "+|expandedInstr|+">"-  build (SeqEx expandedOps)    = "<SeqEx: "+|expandedOps|+">"+  build (PrimEx expandedInstr) = "<PrimEx: " +| expandedInstr |+ ">"+  build (SeqEx expandedOps)    = "<SeqEx: " +| expandedOps |+ ">"  -- | Flatten all 'SeqEx' in 'ExpandedOp'. This function is mostly for -- testing. It returns instructions with the same logic, but they are

@@ -12,7 +12,7 @@   , viewNameToMText    , View' (..)-  , ViewsSet (.., UnsafeViewsSet)+  , ViewsSet (..)   , mkViewsSet   , VS.ViewsSetError (..) @@ -53,11 +53,6 @@ newtype ViewsSet instr = ViewsSet { unViewsSet :: Map ViewName (View' instr) }   deriving newtype (FromJSON, ToJSON, Default, NFData, Container)   deriving stock (Eq, Show, Data, Functor)--pattern UnsafeViewsSet :: Map ViewName (View' instr) -> ViewsSet instr-pattern UnsafeViewsSet x = ViewsSet x-{-# COMPLETE UnsafeViewsSet #-}-{-# DEPRECATED UnsafeViewsSet "Use ViewsSet instead" #-}  mkViewsSet :: [View' instr] -> Either VS.ViewsSetError (ViewsSet instr) mkViewsSet = coerce ... VS.mkViewsSet viewName

@@ -46,6 +46,8 @@   , chainIdLength   ) where +import Prelude hiding (lift)+ import Data.Aeson (FromJSON(..), ToJSON(..)) import Data.Aeson qualified as Aeson import Data.Aeson.TH (deriveJSON)@@ -196,7 +198,7 @@   where     parseTez :: forall t m. (CheckIntSubType Word63 t, Integral t, MonadFail m) => String -> m t     parseTez inp = fromIntegral <$>-      case readP_to_S (skipSpaces *> parser) $ filter (/='_') inp of+      case readP_to_S (skipSpaces *> parser) $ filter (/= '_') inp of         [(val, "")] -> unsafeM . maybeToRight (oobErr val) $ toBoundedInteger @Word63 val         _ -> fail "no parse"     parser = (*) <$> (scientificP <* skipSpaces) <*> (unit <* skipSpaces) <* eof

@@ -39,15 +39,16 @@   ) where  import Prelude hiding (Type)+import Unsafe qualified (fromIntegral)  import Control.Lens (traversed) import Fmt (pretty)-import GHC.Generics qualified as G import Generics.Deriving.TH (makeRep0Inline)+import GHC.Generics qualified as G import Language.Haskell.TH+ import Morley.Util.Generic (mkGenericTree) import Morley.Util.TH (lookupTypeNameOrFail)-import Unsafe qualified (fromIntegral)  {-# ANN module ("HLint: ignore Language.Haskell.TH should be imported post-qualified or with an explicit import list" :: Text) #-} @@ -526,7 +527,7 @@       return (fDepth, fExpr)     -- make pattern for this constructor     fPatts <- mapM varP wOrigFields-    let cPatt = ConP cName fPatts+    let cPatt = ConP cName [] fPatts     -- make expression to assemble its fields as an isolated Generic Constructor     cExp <- appE [| G.M1 |] $ case fDepthExp of       [] -> conE 'G.U1

@@ -7,12 +7,16 @@   , mkGenericTreeVec    , GenericTypeName++  , GRep+  , NiceGeneric   ) where  import Control.Exception (assert) import Data.Vector qualified as V import GHC.Generics qualified as G import GHC.TypeLits (Symbol)+import Type.Errors (ErrorMessage(..), IfStuck, Pure, TypeError) import Unsafe qualified (fromIntegral)  -- | Rebuild a list into a binary tree of exactly the same form which@@ -42,7 +46,42 @@ -- | Extract datatype name via its Generic representation. -- -- For polymorphic types this throws away all type arguments.-type GenericTypeName a = GTypeName (G.Rep a)+type GenericTypeName a = GTypeName (GRep a)  type family GTypeName (x :: Type -> Type) :: Symbol where   GTypeName (G.D1 ('G.MetaData tyName _ _ _) _) = tyName++-- | Avoid too eagerly reducing 'GRep'.+data ThisTypeShallNotBeExported++{- | Like 'G.Rep', but has better error messages when stuck.++Trying to use something requiring generics without the 'Generic' instance should+trigger a custom error message:++>>> data Foo = Foo+>>> (from . to :: GRep a ~ GRep () => a -> ()) Foo+...+... GHC.Generics.Rep Foo+... is stuck. Likely+... Generic Foo+... instance is missing or out of scope.+...+>>> data Foo = Foo deriving Generic+>>> (from . to :: GRep a ~ GRep () => a -> ()) Foo+...+... Couldn't match type ‘"Foo"’ with ‘"()"’+...+-}+type family GRep t where+  GRep ThisTypeShallNotBeExported = TypeError ('Text "impossible")+  GRep t = IfStuck (G.Rep t) (TypeError (GRepErrorMsg t)) (Pure (G.Rep t))++type GRepErrorMsg t = 'ShowType (G.Rep t)+  ':$$: 'Text "is stuck. Likely"+  ':$$: 'ShowType (Generic t)+  ':$$: 'Text "instance is missing or out of scope."++-- | Similar to 'Generic', but also asserts that 'GRep' is the same as 'G.Rep'.+-- Useful in place of 'Generic' when 'GRep' is used.+type NiceGeneric t = (Generic t, GRep t ~ G.Rep t)

@@ -74,7 +74,7 @@   where     go tacc ('\\':'#':xs) = go (tacc <> "#") xs     go tacc ('#':'{':xs)-      | (expr, '}':ys) <- List.span (/='}') xs+      | (expr, '}':ys) <- List.span (/= '}') xs       = lookupValueName expr >>= \case           Just valueName ->             let txt = fmt tacc :: Text@@ -102,7 +102,7 @@       in intercalate "\n" $ drop minIndent <$> ls     Nothing -> s   where-    ls = split (=='\n') s+    ls = split (== '\n') s     indentOf = length . takeWhile (== ' ')  -- See Note [lines/unlines] below about the use of this function@@ -114,7 +114,7 @@ trim :: String -> String trim = intercalate "\n" . List.dropWhileEnd (all (== ' '))      -- See Note [lines/unlines] below about the use of 'intercalate'-     . dropWhile (all (== ' ')) . split (=='\n')+     . dropWhile (all (== ' ')) . split (== '\n')  {- Note [lines/unlines]    ~~~~~~~~~~~~~~~~~~~~

@@ -12,4 +12,4 @@  -- | For datatype with "myNyan" field it will create "myNyanL" lens. postfixLFields :: LensRules-postfixLFields = lensRules & lensField .~ mappingNamer (\s -> [s++"L"])+postfixLFields = lensRules & lensField .~ mappingNamer (\s -> [s ++ "L"])

@@ -71,7 +71,7 @@   local' = local  instance-  ( MultiReader n r m, Monad m, 'S n ~ MultiReaderDepth r (x ': MultiReaderIso m) )+  ( MultiReader n r m, 'S n ~ MultiReaderDepth r (x ': MultiReaderIso m) )   => MultiReader ('S n) r (ReaderT x m) where   ask' = lift ask'   local' = mapReaderT . local'

@@ -106,7 +106,7 @@ instance (Show a, KnownSymbol name) => Show (NamedF Identity a name) where   showsPrec d (ArgF (Identity a)) = T.showParen (d > app_prec) $     T.showString "fromLabel @" . T.shows (symbolVal (Proxy @name)) .-    T.showString " :! " . T.showsPrec (bang_prec+1) a+    T.showString " :! " . T.showsPrec (bang_prec + 1) a     where       app_prec = 10       -- precedence of (:!)

@@ -498,6 +498,7 @@ transitivity x y z = stubProof $ case (x, y, z) of   (SS _, SS _, SZ) -> Refl   (SS x', SS y', SS z') -> Refl \\ transitivity x' y' z'+  (SZ, y', _) -> case y' of  ---------------------------------------------------------------------------- -- Helpers

@@ -62,7 +62,7 @@  pattern Succ :: () => (n ~ 'S m) => PeanoNatural m -> PeanoNatural n pattern Succ s <- (matchPS -> PS_Match s) where-  Succ (PN n k) = PN (SS n) (k+1)+  Succ (PN n k) = PN (SS n) (k + 1) {-# COMPLETE Zero, Succ #-}  -- | The following patterns are introduced for convenience.

@@ -0,0 +1,172 @@+-- SPDX-FileCopyrightText: 2015 Yusuke Matsushita+-- SPDX-FileCopyrightText: 2023 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-BSD3-Yusuke-Matsushita+-- SPDX-License-Identifier: LicenseRef-MIT-OA++-- | This is essentially [show-type](https://hackage.haskell.org/package/show-type) adapted to work+-- with GHC 9.4. The unfortunate thing is, GHC 9.4 conflates @Type@ and @Constraint@ for the purpose+-- of instance overlap, but not instance resolution, hence we have to use an overlappable+-- kind-polymorphic "catch-all" instance instead of the more specific @Constraint@-kinded one.+--+-- See <https://gitlab.haskell.org/ghc/ghc/-/issues/23446>,+-- <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0032-constraint-vs-type.rst>,+-- <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0518-type-vs-constraint.rst>+-- for more information.+--+-- There is an argument for eventually upstreaming this, but it's small enough to bundle in-tree,+-- and time constraints on our side are pretty tight at the time of writing.+module Morley.Util.ShowType (+    -- * Showtype+    Showtype(showtype, showtypesPrec), printtype+  ) where++import Data.Foldable (foldr1)+import Prelude hiding (foldr1, show)+import Text.Show (Show(..), showParen, showString)++import Data.Typeable (typeRep)+import GHC.TypeLits (KnownSymbol, Nat, Symbol, symbolVal)++-- | Conversion of types to readable 'String's. Analogous to 'Show'.+class Showtype (a :: k) where+  {-# MINIMAL showtype | showtypesPrec #-}+  -- | Convert a type @a@ to a readable 'String'. Analogous to 'show' in 'Show'.+  showtype :: proxy a -> String+  -- | Convert a type @a@ to a readable 'String' with additional arguments. Analogous to 'showsPrec' in 'Show'.+  showtypesPrec :: Int -> proxy a -> String -> String+  showtype p = showtypesPrec 0 p ""+  showtypesPrec _ p s = showtype p ++ s++printtype :: Showtype a => proxy a -> IO ()+printtype = putStrLn . showtype++instance Showtype False where+  showtype _ = "False"+instance Showtype True where+  showtype _ = "True"++instance Showtype LT where+  showtype _ = "LT"+instance Showtype EQ where+  showtype _ = "EQ"+instance Showtype GT where+  showtype _ = "GT"++instance KnownNat n => Showtype (n :: Nat) where+  showtype = show . natVal++instance KnownSymbol s => Showtype (s :: Symbol) where+  showtype = show . symbolVal++instance Showtype Nothing where+  showtype _ = "Nothing"+instance Showtype a => Showtype (Just a) where+  showtypesPrec p _ = showParen (p > 10) $+    showString "Just " .+    showtypesPrec 11 (Proxy :: Proxy a)++instance Showtype a => Showtype (Left a) where+  showtypesPrec p _ = showParen (p > 10) $+    showString "Left " .+    showtypesPrec 11 (Proxy :: Proxy a)+instance Showtype a => Showtype (Right a) where+  showtypesPrec p _ = showParen (p > 10) $+    showString "Right " .+    showtypesPrec 11 (Proxy :: Proxy a)++instance Showtype '[] where+  showtype _ = "[]"+instance (Showtype a, Showlisttype as) => Showtype (a ': as :: [k]) where+  showtype _ = "[" ++ showtype (Proxy :: Proxy a) ++ showlisttype (Proxy :: Proxy as)+class Showlisttype (as :: [k]) where+  showlisttype :: Proxy as -> String+instance Showlisttype '[] where+  showlisttype _ = "]"+instance (Showtype a, Showlisttype as) => Showlisttype (a ': as) where+  showlisttype _ = "," ++ showtype (Proxy :: Proxy a) ++ showlisttype (Proxy :: Proxy as)++showtuple, showtuple' :: [String] -> String+showtuple ss = "(" ++ foldr1 (\s t -> s ++ "," ++ t) ss ++ ")"+showtuple' ss = "'" ++ showtuple ss++instance Showtype '() where+  showtype _ = "'()"+instance (Showtype a, Showtype b) => Showtype '(a,b) where+  showtype _ = showtuple' [+    showtype (Proxy :: Proxy a),+    showtype (Proxy :: Proxy b)]+instance (Showtype a, Showtype b, Showtype c) => Showtype '(a,b,c) where+  showtype _ = showtuple' [+    showtype (Proxy :: Proxy a),+    showtype (Proxy :: Proxy b),+    showtype (Proxy :: Proxy c)]+instance (Showtype a, Showtype b, Showtype c, Showtype d) => Showtype '(a,b,c,d) where+  showtype _ = showtuple' [+    showtype (Proxy :: Proxy a),+    showtype (Proxy :: Proxy b),+    showtype (Proxy :: Proxy c),+    showtype (Proxy :: Proxy d)]+instance (Showtype a, Showtype b, Showtype c, Showtype d, Showtype e) => Showtype '(a,b,c,d,e) where+  showtype _ = showtuple' [+    showtype (Proxy :: Proxy a),+    showtype (Proxy :: Proxy b),+    showtype (Proxy :: Proxy c),+    showtype (Proxy :: Proxy d),+    showtype (Proxy :: Proxy e)]+instance (Showtype a, Showtype b, Showtype c, Showtype d, Showtype e, Showtype f) => Showtype '(a,b,c,d,e,f) where+  showtype _ = showtuple' [+    showtype (Proxy :: Proxy a),+    showtype (Proxy :: Proxy b),+    showtype (Proxy :: Proxy c),+    showtype (Proxy :: Proxy d),+    showtype (Proxy :: Proxy e),+    showtype (Proxy :: Proxy f)]+instance (Showtype a, Showtype b, Showtype c, Showtype d, Showtype e, Showtype f, Showtype g) => Showtype '(a,b,c,d,e,f,g) where+  showtype _ = showtuple' [+    showtype (Proxy :: Proxy a),+    showtype (Proxy :: Proxy b),+    showtype (Proxy :: Proxy c),+    showtype (Proxy :: Proxy d),+    showtype (Proxy :: Proxy e),+    showtype (Proxy :: Proxy f),+    showtype (Proxy :: Proxy g)]+instance (Showtype a, Showtype b, Showtype c, Showtype d, Showtype e, Showtype f, Showtype g, Showtype h) => Showtype '(a,b,c,d,e,f,g,h) where+  showtype _ = showtuple' [+    showtype (Proxy :: Proxy a),+    showtype (Proxy :: Proxy b),+    showtype (Proxy :: Proxy c),+    showtype (Proxy :: Proxy d),+    showtype (Proxy :: Proxy e),+    showtype (Proxy :: Proxy f),+    showtype (Proxy :: Proxy g),+    showtype (Proxy :: Proxy h)]+instance (Showtype a, Showtype b, Showtype c, Showtype d, Showtype e, Showtype f, Showtype g, Showtype h, Showtype i) => Showtype '(a,b,c,d,e,f,g,h,i) where+  showtype _ = showtuple' [+    showtype (Proxy :: Proxy a),+    showtype (Proxy :: Proxy b),+    showtype (Proxy :: Proxy c),+    showtype (Proxy :: Proxy d),+    showtype (Proxy :: Proxy e),+    showtype (Proxy :: Proxy f),+    showtype (Proxy :: Proxy g),+    showtype (Proxy :: Proxy h),+    showtype (Proxy :: Proxy i)]+instance (Showtype a, Showtype b, Showtype c, Showtype d, Showtype e, Showtype f, Showtype g, Showtype h, Showtype i, Showtype j) => Showtype '(a,b,c,d,e,f,g,h,i,j) where+  showtype _ = showtuple' [+    showtype (Proxy :: Proxy a),+    showtype (Proxy :: Proxy b),+    showtype (Proxy :: Proxy c),+    showtype (Proxy :: Proxy d),+    showtype (Proxy :: Proxy e),+    showtype (Proxy :: Proxy f),+    showtype (Proxy :: Proxy g),+    showtype (Proxy :: Proxy h),+    showtype (Proxy :: Proxy i),+    showtype (Proxy :: Proxy j)]++showtypesPrecAuto :: Typeable a => Int -> proxy a -> String -> String+showtypesPrecAuto n p s = showsPrec n (typeRep p) s+{-# INLINE showtypesPrecAuto #-}++instance {-# overlappable #-} Typeable a => Showtype (a :: k) where+  showtypesPrec = showtypesPrecAuto

@@ -87,7 +87,7 @@ -- @zipWith ($) f x@ data SizedList' (n :: Peano) a where   Nil :: SizedList' 'Z a -- ^ Empty list-  (:<) :: a -> SizedList' n a -> SizedList' ('S n) a -- ^ Cons+  (:<) :: ~a -> ~(SizedList' n a) -> SizedList' ('S n) a -- ^ Cons infixr 5 :<  -- | Sized list cons pattern. Unlike ':<' this pattern can be used to auto-deduce the type of@@ -113,7 +113,7 @@ deriving stock instance Functor (SizedList' n) instance Show a => Show (SizedList' n a) where   showsPrec d (x :< xs) = showParen (d > prec) $-    showsPrec (prec+1) x . showString " :< " . showsPrec prec xs+    showsPrec (prec + 1) x . showString " :< " . showsPrec prec xs     where prec = 5   showsPrec _ Nil = showString "Nil" deriving stock instance Ord a => Ord (SizedList' n a)@@ -128,7 +128,14 @@   (<*>) = zipWith ($) \\ minIdempotency (sing @n)  instance SingI n => Monad (SizedList' n) where-  f >>= k = generate' (sing @n) $ \(r, _) -> index' r $ k (index' r f)+  f >>= (k :: a -> SizedList' n b) = go SZ f+    where+      go :: forall k m. (AddPeano k m ~ n)+         => SingNat k -> SizedList' m a -> SizedList' m b+      go _ Nil = Nil+      go i (el :< (rest :: SizedList' m' a)) =+        index' i (k el) :< go (SS i) rest+        \\ associativity @m' i \\ additivity @k @m' @n i  -- | Existential capturing a fixed-size list whose length is only known at runtime. --@@ -275,7 +282,7 @@ -- -- >>> generate @3 (+1) -- 1 :< 2 :< 3 :< Nil-generate :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => (Natural -> a) -> SizedList n a+generate :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => (Natural -> a) -> SizedList' n' a generate f = generate' (sing @n') (f . snd)  -- | Same as 'generate', but accepts an explicit 'Peano' singleton, and passes an explicit@@ -339,7 +346,7 @@ -- >>> let someList = 'a' :< 'b' :< 'c' :< Nil -- >>> generate' @_ @Char (peanoSing @2) $ \(sg, _) -> index' sg someList -- ...---     • Could not deduce: ('S ('S ('S 'Z)) > m) ~ 'True+-- ... Could not deduce (('S ('S ('S 'Z)) > m) ~ 'True) -- ... -- -- To make this work, use 'transitivity' proof:

@@ -48,7 +48,7 @@         let infixSeq e1 e2 = InfixE (Just e1) seqQ (Just e2)         return $           (Clause-            [ConP conName $ map VarP varNames]+            [ConP conName [] $ map VarP varNames]             (NormalB $ foldl' infixSeq unit (map rnfExp varNames))             []           )

@@ -159,58 +159,8 @@ type FailWhenElse :: Bool -> ErrorMessage -> Constraint -> Constraint type FailWhenElse cond msg els = FailUnlessEqualElse cond 'False msg els -{- | Fail with given error if the condition does not hold. Otherwise, return the-third argument.--There is a subtle difference between @FailWhenElsePoly@ and the following type-definition:-->>> :{-type FailWhenElsePolyAlternative cond msg els =-  If cond-    (DelayError msg)-    els-:}--If @cond@ cannot be fully reduced (e.g., it's a stuck type family-application or an ambiguous type) then:--* @FailWhenElsePoly@ will state that the constraint cannot be deduced (and this-error message will be suppressed if there are also custom type errors).--* @FailWhenElsePolyAlternative@ will fail with the given error message, @err@.--For example:-->>> :{--- Partial function-type family IsZero (n :: Peano) :: Bool where-  IsZero ('S _) = 'False----f1 :: ( IsZero n ~ 'True-      , FailWhenElsePoly (IsZero n) ('Text "Expected zero") (() :: Constraint))-   => ()-f1 = ()----f2 :: ( IsZero n ~ 'True-      , FailWhenElsePolyAlternative (IsZero n) ('Text "Expected zero") (() :: Constraint))-   => ()-f2 = ()-:}-->>> f1 @'Z-...-... • Couldn't match type ‘IsZero 'Z’ with ‘'True’-...-->>> f2 @'Z-...-... • Expected zero-...--As you can see, the error message in @f2res@ is misleading (because the type argument-actually _is_ zero), so it's preferable to fail with the standard GHC error message.--}+-- | Fail with given error if the condition does not hold. Otherwise, return the+-- third argument. type FailWhenElsePoly :: forall k. Bool -> ErrorMessage -> k -> k type family FailWhenElsePoly cond msg els where   FailWhenElsePoly 'True msg _els = TypeError msg@@ -224,7 +174,9 @@ -- | Fail with given error if the condition does not hold. Otherwise, -- return the third argument. type FailUnlessElsePoly :: forall k. Bool -> ErrorMessage -> k -> k-type FailUnlessElsePoly b e k = FailWhenElsePoly (Not b) e k+type family FailUnlessElsePoly b e k where+  FailUnlessElsePoly 'False msg _els = TypeError msg+  FailUnlessElsePoly 'True _ els = els  -- | Fail with given error if the condition does not hold. type FailUnless :: Bool -> ErrorMessage -> Constraint