[Builtins] Use 'Data.Some.Newtype' instead of 'data Some' (#3318)

* [Builtins] Use 'Data.Some.Newtype' instead of 'data Some'

* Fixed 'nix'

plutus-core/plutus-core.cabal

@@ -255,8 +255,7 @@ library
         cryptonite -any,
         data-default-class -any,
         deepseq -any,
-        dependent-map -any,
-        dependent-sum <0.7,
+        dependent-map >=0.4.0.0,
         dependent-sum-template -any,
         deriving-aeson >= 0.2.3,
         deriving-compat -any,
@@ -273,6 +272,7 @@ library
         megaparsec -any,
         memory -any,
         mmorph -any,
+        mono-traversable -any,
         monoidal-containers,
         mtl -any,
         nonempty-containers -any,
@@ -285,6 +285,7 @@ library
         semigroups -any,
         serialise -any,
         size-based -any,
+        some -any,
         sop-core -any,
         tasty -any,
         tasty-golden -any,

plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs

@@ -32,10 +32,10 @@ import           Data.Array
 import qualified Data.ByteString                         as BS
 import qualified Data.Kind                               as GHC
 import           Data.Proxy
+import           Data.Some.GADT
 import           Data.Type.Bool
 import           Data.Type.Equality
 import           GHC.TypeLits
-import           Universe
 
 -- | The meaning of a built-in function consists of its type represented as a 'TypeScheme',
 -- its Haskell denotation and a costing function (both in uninstantiated form).

plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE LambdaCase               #-}
 -- | This module assigns types to built-ins.
 -- See the @plutus/plutus-core/docs/Constant application.md@
 -- article for how this emerged.
@@ -92,7 +93,7 @@ data TypeScheme term (args :: [GHC.Type]) res where
                Proxy ot -> TypeScheme term args res)
         -> TypeScheme term args res
 
--- | Turn a list of Haskell types @as@ into a functional type ending in @r@.
+-- | Turn a list of Haskell types @args@ into a functional type ending in @res@.
 --
 -- >>> :set -XDataKinds
 -- >>> :kind! FoldArgs [Char, Bool] Integer
@@ -440,18 +441,18 @@ class KnownTypeAst (UniOf term) a => KnownType term a where
            , KnownBuiltinType term a
            )
         => term -> m a
-    readKnown term = do
-        Some (ValueOf uniAct x) <- asConstant term
-        let uniExp = knownUni @_ @(UniOf term) @a
-        case uniAct `geq` uniExp of
-            Just Refl -> pure x
-            Nothing   -> do
-                let err = fromString $ concat
-                        [ "Type mismatch: "
-                        , "expected: " ++ gshow uniExp
-                        , "; actual: " ++ gshow uniAct
-                        ]
-                throwingWithCause _UnliftingError err $ Just term
+    readKnown term = asConstant term >>= \case
+        Some (ValueOf uniAct x) -> do
+            let uniExp = knownUni @_ @(UniOf term) @a
+            case uniAct `geq` uniExp of
+                Just Refl -> pure x
+                Nothing   -> do
+                    let err = fromString $ concat
+                            [ "Type mismatch: "
+                            , "expected: " ++ gshow uniExp
+                            , "; actual: " ++ gshow uniAct
+                            ]
+                    throwingWithCause _UnliftingError err $ Just term
 
 makeKnownNoEmit :: (KnownType term a, MonadError err m, AsEvaluationFailure err) => a -> m term
 makeKnownNoEmit = unNoEmitterT . makeKnown
@@ -559,33 +560,33 @@ instance (KnownBuiltinTypeIn uni term f, All (KnownTypeAst uni) reps, HasUniAppl
             KnownType term (SomeConstantOf uni f reps) where
     makeKnown = pure . fromConstant . runSomeConstantOf
 
-    readKnown term = do
-        Some (ValueOf uni xs) <- asConstant term
-        let uniF = knownUni @_ @_ @f
-            err = fromString $ concat
-                [ "Type mismatch: "
-                , "expected an application of: " ++ gshow uniF
-                , "; but got the following type: " ++ gshow uni
-                ]
-            wrongType :: (MonadError (ErrorWithCause err term) m, AsUnliftingError err) => m a
-            wrongType = throwingWithCause _UnliftingError err $ Just term
-        -- In order to prove that the type of @xs@ is an application of @f@ we need to
-        -- peel all type applications off in the type of @xs@ until we get to the head and then
-        -- check that the head is indeed @f@. Each peeled type application becomes a
-        -- 'SomeConstantOfArg' in the final result.
-        ReadSomeConstantOf res uniHead <-
-            cparaM_SList @_ @(KnownTypeAst uni) @reps
-                Proxy
-                (ReadSomeConstantOf (SomeConstantOfRes uni xs) uni)
-                (\(ReadSomeConstantOf acc uniApp) ->
-                    matchUniApply
-                        uniApp
-                        wrongType
-                        (\uniApp' uniA ->
-                            pure $ ReadSomeConstantOf (SomeConstantOfArg uniA acc) uniApp'))
-        case uniHead `geq` uniF of
-            Nothing   -> wrongType
-            Just Refl -> pure res
+    readKnown term = asConstant term >>= \case
+        Some (ValueOf uni xs) -> do
+            let uniF = knownUni @_ @_ @f
+                err = fromString $ concat
+                    [ "Type mismatch: "
+                    , "expected an application of: " ++ gshow uniF
+                    , "; but got the following type: " ++ gshow uni
+                    ]
+                wrongType :: (MonadError (ErrorWithCause err term) m, AsUnliftingError err) => m a
+                wrongType = throwingWithCause _UnliftingError err $ Just term
+            -- In order to prove that the type of @xs@ is an application of @f@ we need to
+            -- peel all type applications off in the type of @xs@ until we get to the head and then
+            -- check that the head is indeed @f@. Each peeled type application becomes a
+            -- 'SomeConstantOfArg' in the final result.
+            ReadSomeConstantOf res uniHead <-
+                cparaM_SList @_ @(KnownTypeAst uni) @reps
+                    Proxy
+                    (ReadSomeConstantOf (SomeConstantOfRes uni xs) uni)
+                    (\(ReadSomeConstantOf acc uniApp) ->
+                        matchUniApply
+                            uniApp
+                            wrongType
+                            (\uniApp' uniA ->
+                                pure $ ReadSomeConstantOf (SomeConstantOfArg uniA acc) uniApp'))
+            case uniHead `geq` uniF of
+                Nothing   -> wrongType
+                Just Refl -> pure res
 
 toTyNameAst
     :: forall text uniq. (KnownSymbol text, KnownNat uniq)

plutus-core/plutus-core/src/Universe/Core.hs

@@ -49,10 +49,12 @@ import           Control.Monad
 import           Control.Monad.Trans.State.Strict
 import           Data.GADT.Compare
 import           Data.GADT.Compare.TH
+import           Data.GADT.DeepSeq
 import           Data.GADT.Show
 import           Data.Hashable
 import           Data.Kind
 import           Data.Proxy
+import           Data.Some.Newtype
 import           Data.Type.Equality
 import           Text.Show.Deriving
 import           Type.Reflection
@@ -323,10 +325,6 @@ even though that required reworking all the infrastructure in a backwards-incomp
 type Esc :: forall k. k -> Type
 data Esc a
 
--- | Existential quantification as a data type.
-type Some :: forall a. (a -> Type) -> Type
-data Some f = forall x. Some !(f x)
-
 -- | A particular type from a universe.
 type SomeTypeIn :: (Type -> Type) -> Type
 data SomeTypeIn uni = forall k (a :: k). SomeTypeIn !(uni (Esc a))
@@ -705,9 +703,6 @@ $(return [])  -- Stage restriction, see https://gitlab.haskell.org/ghc/ghc/issue
 instance GShow f => Show (AG f a) where
     showsPrec pr (AG a) = gshowsPrec pr a
 
-instance GShow f => Show (Some f) where
-    showsPrec pr (Some a) = ($(makeShowsPrec ''Some)) pr (Some (AG a))
-
 instance GShow uni => Show (SomeTypeIn uni) where
     showsPrec pr (SomeTypeIn uni) = ($(makeShowsPrec ''SomeTypeIn)) pr (SomeTypeIn (AG uni))
 
@@ -724,9 +719,6 @@ instance (GShow uni, Closed uni, uni `Everywhere` Show) => Show (ValueOf uni a)
 
 -------------------- 'Eq' / 'GEq'
 
-instance GEq f => Eq (Some f) where
-    Some a1 == Some a2 = a1 `defaultEq` a2
-
 instance (GEq uni, Closed uni, uni `Everywhere` Eq) => GEq (ValueOf uni) where
     ValueOf uni1 x1 `geq` ValueOf uni2 x2 = do
         Refl <- uni1 `geq` uni2
@@ -741,14 +733,14 @@ instance (GEq uni, Closed uni, uni `Everywhere` Eq) => Eq (ValueOf uni a) where
 
 -------------------- 'NFData'
 
+instance (Closed uni, uni `Everywhere` NFData) => GNFData (ValueOf uni) where
+    grnf (ValueOf uni x) = bring (Proxy @NFData) uni $ rnf x
+
 instance Closed uni => NFData (SomeTypeIn uni) where
     rnf (SomeTypeIn uni) = rnf $ encodeUni uni
 
 instance (Closed uni, uni `Everywhere` NFData) => NFData (ValueOf uni a) where
-    rnf (ValueOf uni x) = bring (Proxy @NFData) uni $ rnf x
-
-instance (Closed uni, uni `Everywhere` NFData) => NFData (Some (ValueOf uni)) where
-    rnf (Some s) = rnf s
+    rnf = grnf
 
 -------------------- 'Hashable'
 

stack.yaml

@@ -42,7 +42,7 @@ extra-deps:
 - composition-prelude-3.0.0.2
 - constraints-extras-0.3.0.2
 - dependent-map-0.4.0.0
-- dependent-sum-0.6.2.0
+- dependent-sum-0.7.1.0
 - dependent-sum-template-0.1.0.3
 - eventful-memory-0.2.0
 - barbies-2.0.2.0