diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,19 @@ +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 ====== diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -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"] diff --git a/morley.cabal b/morley.cabal --- a/morley.cabal +++ b/morley.cabal @@ -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 diff --git a/src/Morley/App/REPL.hs b/src/Morley/App/REPL.hs --- a/src/Morley/App/REPL.hs +++ b/src/Morley/App/REPL.hs @@ -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 diff --git a/src/Morley/AsRPC.hs b/src/Morley/AsRPC.hs --- a/src/Morley/AsRPC.hs +++ b/src/Morley/AsRPC.hs @@ -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 diff --git a/src/Morley/Micheline/Binary/Internal.hs b/src/Morley/Micheline/Binary/Internal.hs --- a/src/Morley/Micheline/Binary/Internal.hs +++ b/src/Morley/Micheline/Binary/Internal.hs @@ -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' diff --git a/src/Morley/Michelson/Internal/ViewName.hs b/src/Morley/Michelson/Internal/ViewName.hs --- a/src/Morley/Michelson/Internal/ViewName.hs +++ b/src/Morley/Michelson/Internal/ViewName.hs @@ -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. diff --git a/src/Morley/Michelson/Interpret.hs b/src/Morley/Michelson/Interpret.hs --- a/src/Morley/Michelson/Interpret.hs +++ b/src/Morley/Michelson/Interpret.hs @@ -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) diff --git a/src/Morley/Michelson/Macro.hs b/src/Morley/Michelson/Macro.hs --- a/src/Morley/Michelson/Macro.hs +++ b/src/Morley/Michelson/Macro.hs @@ -84,9 +84,9 @@ instance Buildable ParsedOp where build = \case - Prim parseInstr _ -> "" - Mac macro _ -> "" - Seq parsedOps _ -> "" + Prim parseInstr _ -> "" + Mac macro _ -> "" + Seq parsedOps _ -> "" instance NFData ParsedOp @@ -139,28 +139,28 @@ instance Buildable Macro where build = \case - CMP parsedInstr -> "" - IFX parsedInstr parsedOps1 parsedOps2 -> "" - IFCMP parsedInstr parsedOps1 parsedOps2 -> "" + CMP parsedInstr -> "" + IFX parsedInstr parsedOps1 parsedOps2 -> "" + IFCMP parsedInstr parsedOps1 parsedOps2 -> "" FAIL -> "FAIL" - PAPAIR pairStruct typeAnn varAnn -> "" - UNPAPAIR pairStruct -> "" - CADR cadrStructs varAnn fieldAnn -> "" - CARN varAnn idx -> "" - CDRN varAnn idx -> "" - SET_CADR cadrStructs varAnn fieldAnn -> "" - MAP_CADR cadrStructs varAnn fieldAnn parsedOps -> "" - DIIP integer parsedOps -> "" - DUUP integer varAnn -> "" + PAPAIR pairStruct typeAnn varAnn -> "" + UNPAPAIR pairStruct -> "" + CADR cadrStructs varAnn fieldAnn -> "" + CARN varAnn idx -> "" + CDRN varAnn idx -> "" + SET_CADR cadrStructs varAnn fieldAnn -> "" + MAP_CADR cadrStructs varAnn fieldAnn parsedOps -> "" + DIIP integer parsedOps -> "" + DUUP integer varAnn -> "" ASSERT -> "ASSERT" - ASSERTX parsedInstr -> "" - ASSERT_CMP parsedInstr -> "" + ASSERTX 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_RIGHT parsedOps1 parsedOps2 -> "" + IF_SOME parsedOps1 parsedOps2 -> "" + IF_RIGHT parsedOps1 parsedOps2 -> "" instance NFData Macro diff --git a/src/Morley/Michelson/Optimizer/Internal/Rules.hs b/src/Morley/Michelson/Optimizer/Internal/Rules.hs --- a/src/Morley/Michelson/Optimizer/Internal/Rules.hs +++ b/src/Morley/Michelson/Optimizer/Internal/Rules.hs @@ -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 diff --git a/src/Morley/Michelson/Printer.hs b/src/Morley/Michelson/Printer.hs --- a/src/Morley/Michelson/Printer.hs +++ b/src/Morley/Michelson/Printer.hs @@ -3,8 +3,6 @@ module Morley.Michelson.Printer ( RenderDoc(..) - , renderAnyBuildable - , printDoc , printUntypedContract , printTypedContractCode , printTypedContract diff --git a/src/Morley/Michelson/Printer/Util.hs b/src/Morley/Michelson/Printer/Util.hs --- a/src/Morley/Michelson/Printer/Util.hs +++ b/src/Morley/Michelson/Printer/Util.hs @@ -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 diff --git a/src/Morley/Michelson/Runtime/GState.hs b/src/Morley/Michelson/Runtime/GState.hs --- a/src/Morley/Michelson/Runtime/GState.hs +++ b/src/Morley/Michelson/Runtime/GState.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Arith.hs b/src/Morley/Michelson/Typed/Arith.hs --- a/src/Morley/Michelson/Typed/Arith.hs +++ b/src/Morley/Michelson/Typed/Arith.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/ClassifiedInstr/Internal/Classifiers/NumChildren.hs b/src/Morley/Michelson/Typed/ClassifiedInstr/Internal/Classifiers/NumChildren.hs --- a/src/Morley/Michelson/Typed/ClassifiedInstr/Internal/Classifiers/NumChildren.hs +++ b/src/Morley/Michelson/Typed/ClassifiedInstr/Internal/Classifiers/NumChildren.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Convert.hs b/src/Morley/Michelson/Typed/Convert.hs --- a/src/Morley/Michelson/Typed/Convert.hs +++ b/src/Morley/Michelson/Typed/Convert.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Doc.hs b/src/Morley/Michelson/Typed/Doc.hs --- a/src/Morley/Michelson/Typed/Doc.hs +++ b/src/Morley/Michelson/Typed/Doc.hs @@ -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 () diff --git a/src/Morley/Michelson/Typed/Haskell/Doc.hs b/src/Morley/Michelson/Typed/Haskell/Doc.hs --- a/src/Morley/Michelson/Typed/Haskell/Doc.hs +++ b/src/Morley/Michelson/Typed/Haskell/Doc.hs @@ -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. diff --git a/src/Morley/Michelson/Typed/Haskell/Instr/Product.hs b/src/Morley/Michelson/Typed/Haskell/Instr/Product.hs --- a/src/Morley/Michelson/Typed/Haskell/Instr/Product.hs +++ b/src/Morley/Michelson/Typed/Haskell/Instr/Product.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Haskell/Instr/Sum.hs b/src/Morley/Michelson/Typed/Haskell/Instr/Sum.hs --- a/src/Morley/Michelson/Typed/Haskell/Instr/Sum.hs +++ b/src/Morley/Michelson/Typed/Haskell/Instr/Sum.hs @@ -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. diff --git a/src/Morley/Michelson/Typed/Haskell/LooseSum.hs b/src/Morley/Michelson/Typed/Haskell/LooseSum.hs --- a/src/Morley/Michelson/Typed/Haskell/LooseSum.hs +++ b/src/Morley/Michelson/Typed/Haskell/LooseSum.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Haskell/ValidateDescription.hs b/src/Morley/Michelson/Typed/Haskell/ValidateDescription.hs --- a/src/Morley/Michelson/Typed/Haskell/ValidateDescription.hs +++ b/src/Morley/Michelson/Typed/Haskell/ValidateDescription.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Haskell/Value.hs b/src/Morley/Michelson/Typed/Haskell/Value.hs --- a/src/Morley/Michelson/Typed/Haskell/Value.hs +++ b/src/Morley/Michelson/Typed/Haskell/Value.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Instr.hs b/src/Morley/Michelson/Typed/Instr.hs --- a/src/Morley/Michelson/Typed/Instr.hs +++ b/src/Morley/Michelson/Typed/Instr.hs @@ -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) diff --git a/src/Morley/Michelson/Typed/Instr/Internal/Proofs.hs b/src/Morley/Michelson/Typed/Instr/Internal/Proofs.hs --- a/src/Morley/Michelson/Typed/Instr/Internal/Proofs.hs +++ b/src/Morley/Michelson/Typed/Instr/Internal/Proofs.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Polymorphic.hs b/src/Morley/Michelson/Typed/Polymorphic.hs --- a/src/Morley/Michelson/Typed/Polymorphic.hs +++ b/src/Morley/Michelson/Typed/Polymorphic.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Scope.hs b/src/Morley/Michelson/Typed/Scope.hs --- a/src/Morley/Michelson/Typed/Scope.hs +++ b/src/Morley/Michelson/Typed/Scope.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Scope/Internal/Deprecated.hs b/src/Morley/Michelson/Typed/Scope/Internal/Deprecated.hs deleted file mode 100644 --- a/src/Morley/Michelson/Typed/Scope/Internal/Deprecated.hs +++ /dev/null @@ -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" #-} diff --git a/src/Morley/Michelson/Typed/Scope/Internal/ForbidT.hs b/src/Morley/Michelson/Typed/Scope/Internal/ForbidT.hs --- a/src/Morley/Michelson/Typed/Scope/Internal/ForbidT.hs +++ b/src/Morley/Michelson/Typed/Scope/Internal/ForbidT.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/Scope/Internal/Scopes.hs b/src/Morley/Michelson/Typed/Scope/Internal/Scopes.hs --- a/src/Morley/Michelson/Typed/Scope/Internal/Scopes.hs +++ b/src/Morley/Michelson/Typed/Scope/Internal/Scopes.hs @@ -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 => () diff --git a/src/Morley/Michelson/Typed/Value.hs b/src/Morley/Michelson/Typed/Value.hs --- a/src/Morley/Michelson/Typed/Value.hs +++ b/src/Morley/Michelson/Typed/Value.hs @@ -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 diff --git a/src/Morley/Michelson/Typed/View.hs b/src/Morley/Michelson/Typed/View.hs --- a/src/Morley/Michelson/Typed/View.hs +++ b/src/Morley/Michelson/Typed/View.hs @@ -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)) => diff --git a/src/Morley/Michelson/Untyped/Annotation.hs b/src/Morley/Michelson/Untyped/Annotation.hs --- a/src/Morley/Michelson/Untyped/Annotation.hs +++ b/src/Morley/Michelson/Untyped/Annotation.hs @@ -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) diff --git a/src/Morley/Michelson/Untyped/Instr.hs b/src/Morley/Michelson/Untyped/Instr.hs --- a/src/Morley/Michelson/Untyped/Instr.hs +++ b/src/Morley/Michelson/Untyped/Instr.hs @@ -59,8 +59,8 @@ instance Buildable ExpandedOp where build (WithSrcEx _ op) = build op - build (PrimEx expandedInstr) = "" - build (SeqEx expandedOps) = "" + build (PrimEx expandedInstr) = "" + build (SeqEx expandedOps) = "" -- | Flatten all 'SeqEx' in 'ExpandedOp'. This function is mostly for -- testing. It returns instructions with the same logic, but they are diff --git a/src/Morley/Michelson/Untyped/View.hs b/src/Morley/Michelson/Untyped/View.hs --- a/src/Morley/Michelson/Untyped/View.hs +++ b/src/Morley/Michelson/Untyped/View.hs @@ -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 diff --git a/src/Morley/Tezos/Core.hs b/src/Morley/Tezos/Core.hs --- a/src/Morley/Tezos/Core.hs +++ b/src/Morley/Tezos/Core.hs @@ -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 diff --git a/src/Morley/Util/CustomGeneric.hs b/src/Morley/Util/CustomGeneric.hs --- a/src/Morley/Util/CustomGeneric.hs +++ b/src/Morley/Util/CustomGeneric.hs @@ -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 diff --git a/src/Morley/Util/Generic.hs b/src/Morley/Util/Generic.hs --- a/src/Morley/Util/Generic.hs +++ b/src/Morley/Util/Generic.hs @@ -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) diff --git a/src/Morley/Util/Interpolate/Internal.hs b/src/Morley/Util/Interpolate/Internal.hs --- a/src/Morley/Util/Interpolate/Internal.hs +++ b/src/Morley/Util/Interpolate/Internal.hs @@ -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] ~~~~~~~~~~~~~~~~~~~~ diff --git a/src/Morley/Util/Lens.hs b/src/Morley/Util/Lens.hs --- a/src/Morley/Util/Lens.hs +++ b/src/Morley/Util/Lens.hs @@ -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"]) diff --git a/src/Morley/Util/MultiReader.hs b/src/Morley/Util/MultiReader.hs --- a/src/Morley/Util/MultiReader.hs +++ b/src/Morley/Util/MultiReader.hs @@ -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' diff --git a/src/Morley/Util/Named.hs b/src/Morley/Util/Named.hs --- a/src/Morley/Util/Named.hs +++ b/src/Morley/Util/Named.hs @@ -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 (:!) diff --git a/src/Morley/Util/Peano.hs b/src/Morley/Util/Peano.hs --- a/src/Morley/Util/Peano.hs +++ b/src/Morley/Util/Peano.hs @@ -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 diff --git a/src/Morley/Util/PeanoNatural.hs b/src/Morley/Util/PeanoNatural.hs --- a/src/Morley/Util/PeanoNatural.hs +++ b/src/Morley/Util/PeanoNatural.hs @@ -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. diff --git a/src/Morley/Util/ShowType.hs b/src/Morley/Util/ShowType.hs new file mode 100644 --- /dev/null +++ b/src/Morley/Util/ShowType.hs @@ -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 , +-- , +-- +-- 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 diff --git a/src/Morley/Util/SizedList.hs b/src/Morley/Util/SizedList.hs --- a/src/Morley/Util/SizedList.hs +++ b/src/Morley/Util/SizedList.hs @@ -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: diff --git a/src/Morley/Util/TH.hs b/src/Morley/Util/TH.hs --- a/src/Morley/Util/TH.hs +++ b/src/Morley/Util/TH.hs @@ -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)) [] ) diff --git a/src/Morley/Util/Type.hs b/src/Morley/Util/Type.hs --- a/src/Morley/Util/Type.hs +++ b/src/Morley/Util/Type.hs @@ -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