[Builtins] Drop a couple more 'Proxy's from 'TypeScheme'

plutus-core/executables/Common.hs

@@ -616,9 +616,9 @@ typeSchemeToSignature = toSig []
     where toSig :: [QVarOrType] -> PLC.TypeScheme PlcTerm args res -> Signature
           toSig acc =
               \case
-               PLC.TypeSchemeResult pR -> Signature acc (PLC.toTypeAst pR)
-               PLC.TypeSchemeArrow pA schB ->
-                   toSig (acc ++ [Type $ PLC.toTypeAst pA]) schB
+               pR@PLC.TypeSchemeResult -> Signature acc (PLC.toTypeAst pR)
+               arr@(PLC.TypeSchemeArrow schB) ->
+                   toSig (acc ++ [Type $ PLC.toTypeAst $ PLC.argOf arr]) schB
                PLC.TypeSchemeAll proxy schK ->
                    case proxy of
                      (_ :: Proxy '(text, uniq, kind)) ->

plutus-core/generators/PlutusCore/Generators/Internal/Denotation.hs

@@ -25,7 +25,6 @@ import PlutusCore.Name
 import Data.Dependent.Map (DMap)
 import Data.Dependent.Map qualified as DMap
 import Data.Functor.Compose
-import Data.Proxy
 
 -- | Haskell denotation of a PLC object. An object can be a 'Builtin' or a variable for example.
 data Denotation term object res = forall args. Denotation
@@ -62,15 +61,15 @@ newtype DenotationContext term = DenotationContext
 
 -- | The resulting type of a 'TypeScheme'.
 typeSchemeResult :: TypeScheme term args res -> AsKnownType term res
-typeSchemeResult (TypeSchemeResult _)     = AsKnownType
-typeSchemeResult (TypeSchemeArrow _ schB) = typeSchemeResult schB
-typeSchemeResult (TypeSchemeAll _ schK)   = typeSchemeResult schK
+typeSchemeResult TypeSchemeResult       = AsKnownType
+typeSchemeResult (TypeSchemeArrow schB) = typeSchemeResult schB
+typeSchemeResult (TypeSchemeAll _ schK) = typeSchemeResult schK
 
 -- | Get the 'Denotation' of a variable.
 denoteVariable
     :: KnownType (Term TyName Name uni fun ()) res
     => Name -> res -> Denotation (Term TyName Name uni fun ()) Name res
-denoteVariable name meta = Denotation name (Var ()) meta (TypeSchemeResult Proxy)
+denoteVariable name meta = Denotation name (Var ()) meta TypeSchemeResult
 
 -- | Insert the 'Denotation' of an object into a 'DenotationContext'.
 insertDenotation

plutus-core/generators/PlutusCore/Generators/Internal/Entity.hs

@@ -153,17 +153,17 @@ genIterAppValue (Denotation object embed meta scheme) = result where
         -> ([Plain Term uni fun] -> [Plain Term uni fun])
         -> FoldArgs args res
         -> PlcGenT uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
-    go (TypeSchemeResult _)     term args y = do  -- Computed the result.
+    go TypeSchemeResult       term args y = do  -- Computed the result.
         let pia = IterApp object $ args []
         return $ IterAppValue term pia y
-    go (TypeSchemeArrow _ schB) term args f = do  -- Another argument is required.
+    go (TypeSchemeArrow schB) term args f = do  -- Another argument is required.
         BuiltinGensT genTb <- ask
         TermOf v x <- liftT $ genTb AsKnownType  -- Get a Haskell and the correspoding PLC values.
         let term' = Apply () term v              -- Apply the term to the PLC value.
             args' = args . (v :)                 -- Append the PLC value to the spine.
             y     = f x                          -- Apply the Haskell function to the generated argument.
         go schB term' args' y
-    go (TypeSchemeAll _ schK)   term args f =
+    go (TypeSchemeAll _ schK) term args f =
         go schK term args f
 
 -- | Generate a PLC 'Term' of the specified type and the corresponding Haskell value.

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

@@ -18,8 +18,9 @@ import GHC.TypeLits
 -- | Convert a 'TypeScheme' to the corresponding 'Type'.
 -- Basically, a map from the PHOAS representation to the FOAS one.
 typeSchemeToType :: TypeScheme term args res -> Type TyName (UniOf term) ()
-typeSchemeToType (TypeSchemeResult pR)      = toTypeAst pR
-typeSchemeToType (TypeSchemeArrow pA schB)  = TyFun () (toTypeAst pA) $ typeSchemeToType schB
+typeSchemeToType sch@TypeSchemeResult       = toTypeAst sch
+typeSchemeToType sch@(TypeSchemeArrow schB) =
+    TyFun () (toTypeAst $ argOf sch) $ typeSchemeToType schB
 typeSchemeToType (TypeSchemeAll proxy schK) = case proxy of
     (_ :: Proxy '(text, uniq, kind)) ->
         let text = Text.pack $ symbolVal @text Proxy

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

@@ -184,12 +184,12 @@ class KnownMonotype term args res a | args res -> a, a -> res where
 
 -- | Once we've run out of term-level arguments, we return a 'TypeSchemeResult'.
 instance (res ~ res', KnownType term res) => KnownMonotype term '[] res res' where
-    knownMonotype = TypeSchemeResult Proxy
+    knownMonotype = TypeSchemeResult
 
 -- | Every term-level argument becomes as 'TypeSchemeArrow'.
 instance (KnownType term arg, KnownMonotype term args res a) =>
             KnownMonotype term (arg ': args) res (arg -> a) where
-    knownMonotype = Proxy `TypeSchemeArrow` knownMonotype
+    knownMonotype = TypeSchemeArrow knownMonotype
 
 -- | A class that allows us to derive a polytype for a builtin.
 class KnownPolytype (binds :: [Some TyNameRep]) term args res a | args res -> a, a -> res where

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

@@ -25,6 +25,7 @@
 
 module PlutusCore.Constant.Typed
     ( TypeScheme (..)
+    , argOf
     , FoldArgs
     , FoldArgsEx
     , TyNameRep (..)
@@ -87,10 +88,10 @@ infixr 9 `TypeSchemeArrow`
 data TypeScheme term (args :: [GHC.Type]) res where
     TypeSchemeResult
         :: KnownType term res
-        => Proxy res -> TypeScheme term '[] res
+        => TypeScheme term '[] res
     TypeSchemeArrow
         :: KnownType term arg
-        => Proxy arg -> TypeScheme term args res -> TypeScheme term (arg ': args) res
+        => TypeScheme term args res -> TypeScheme term (arg ': args) res
     TypeSchemeAll
         :: (KnownSymbol text, KnownNat uniq, KnownKind kind)
            -- Here we require the user to manually provide the unique of a type variable.
@@ -99,6 +100,9 @@ data TypeScheme term (args :: [GHC.Type]) res where
         -> TypeScheme term args res
         -> TypeScheme term args res
 
+argOf :: TypeScheme term (arg ': args) res -> Proxy arg
+argOf _ = Proxy
+
 -- | Turn a list of Haskell types @args@ into a functional type ending in @res@.
 --
 -- >>> :set -XDataKinds

plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs

@@ -67,8 +67,8 @@ evalBuiltinApp
     -> BuiltinRuntime (CkValue uni fun)
     -> CkM uni fun s (CkValue uni fun)
 evalBuiltinApp term runtime@(BuiltinRuntime sch x _) = case sch of
-    TypeSchemeResult _ -> makeKnown emitCkM (Just term) x
-    _                  -> pure $ VBuiltin term runtime
+    TypeSchemeResult -> makeKnown emitCkM (Just term) x
+    _                -> pure $ VBuiltin term runtime
 
 ckValueToTerm :: CkValue uni fun -> Term TyName Name uni fun ()
 ckValueToTerm = \case
@@ -300,7 +300,7 @@ applyEvaluate stack (VBuiltin term (BuiltinRuntime sch f _)) arg = do
     case sch of
         -- It's only possible to apply a builtin application if the builtin expects a term
         -- argument next.
-        TypeSchemeArrow _ schB -> do
+        TypeSchemeArrow schB -> do
             x <- liftEither $ readKnown (Just argTerm) arg
             let noCosting = error "The CK machine does not support costing"
                 runtime' = BuiltinRuntime schB (f x) noCosting

plutus-core/plutus-ir/src/PlutusIR/Purity.hs

@@ -18,16 +18,16 @@ data BuiltinApp tyname name uni fun a = BuiltinApp fun [Arg tyname name uni fun
 
 saturatesScheme ::  [Arg tyname name uni fun a] -> TypeScheme term args res -> Maybe Bool
 -- We've passed enough arguments that the builtin will reduce. Note that this also accepts over-applied builtins.
-saturatesScheme _ TypeSchemeResult{}                       = Just True
+saturatesScheme _ TypeSchemeResult{}                     = Just True
 -- Consume one argument
-saturatesScheme (TermArg _ : args) (TypeSchemeArrow _ sch) = saturatesScheme args sch
-saturatesScheme (TypeArg _ : args) (TypeSchemeAll _ sch)   = saturatesScheme args sch
+saturatesScheme (TermArg _ : args) (TypeSchemeArrow sch) = saturatesScheme args sch
+saturatesScheme (TypeArg _ : args) (TypeSchemeAll _ sch) = saturatesScheme args sch
 -- Under-applied, not saturated
-saturatesScheme [] TypeSchemeArrow{}                       = Just False
-saturatesScheme [] TypeSchemeAll{}                         = Just False
+saturatesScheme [] TypeSchemeArrow{}                     = Just False
+saturatesScheme [] TypeSchemeAll{}                       = Just False
 -- These cases are only possible in case we have an ill-typed builtin application, so we can't give an answer.
-saturatesScheme (TypeArg _ : _) TypeSchemeArrow{}          = Nothing
-saturatesScheme (TermArg _ : _) TypeSchemeAll{}            = Nothing
+saturatesScheme (TypeArg _ : _) TypeSchemeArrow{}        = Nothing
+saturatesScheme (TermArg _ : _) TypeSchemeAll{}          = Nothing
 
 -- | Is the given 'BuiltinApp' saturated? Returns 'Nothing' if something is badly wrong and we can't tell.
 isSaturated

plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs

@@ -539,7 +539,7 @@ evalBuiltinApp
     -> BuiltinRuntime (CekValue uni fun)
     -> CekM uni fun s (CekValue uni fun)
 evalBuiltinApp fun term env runtime@(BuiltinRuntime sch x cost) = case sch of
-    TypeSchemeResult _ -> do
+    TypeSchemeResult -> do
         spendBudgetCek (BBuiltinApp fun) cost
         makeKnown ?cekEmitter (Just term) x
     _ -> pure $ VBuiltin fun term env runtime
@@ -681,7 +681,7 @@ enterComputeCek = computeCek (toWordArray 0) where
         case sch of
             -- It's only possible to apply a builtin application if the builtin expects a term
             -- argument next.
-            TypeSchemeArrow _ schB -> do
+            TypeSchemeArrow schB -> do
                 x <- liftEither $ readKnown (Just argTerm) arg
                 -- TODO: should we bother computing that 'ExMemory' eagerly? We may not need it.
                 -- We pattern match on @arg@ twice: in 'readKnown' and in 'toExMemory'.