Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Builtins] Bake inference into 'KnownTypeAst' #4220

Closed
wants to merge 8 commits into from
Closed

[Builtins] Bake inference into 'KnownTypeAst' #4220

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
b6282b9
[Builtins] Bake inference into 'KnownTypeAst' via 'AsSpineRev'
effectfully Nov 14, 2021
c763f59
Add 'IsBuiltin'
effectfully Nov 14, 2021
686d1cc
Merge branch 'master' of https://github.com/input-output-hk/plutus in…
effectfully Nov 14, 2021
793f3a2
Add 'RepInfer' and friends
effectfully Nov 15, 2021
2625f97
Some cleanup
effectfully Nov 15, 2021
5f013d2
A bit more cleanup
effectfully Nov 15, 2021
92cedf8
Drop junk
effectfully Nov 15, 2021
1731d86
A tiny test bug
effectfully Nov 15, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
A bit more cleanup
  • Loading branch information
@effectfully
effectfully committed Nov 15, 2021
commit 5f013d2f3d4b9fa5db118e666dc91c571f80b0cd
148 changes: 6 additions & 142 deletions plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@ import PlutusCore.Core
import PlutusCore.Default.Universe
import PlutusCore.Name

-- Just not to depend on any set of builtins, 'cause they might be broken when there's a need for
-- debugging.
data FunDebug
type TermDebug = Term TyName Name DefaultUni FunDebug ()

Expand All @@ -26,14 +28,14 @@ type TermDebug = Term TyName Name DefaultUni FunDebug ()
-- >>> :t enumerateDebug $ Just 'a'
-- <interactive>:1:1-25: error:
-- • Ambiguous type variable ‘j0’ arising from a use of ‘enumerateDebug’
-- prevents the constraint ‘(HandleSpecialCasesEnter
-- prevents the constraint ‘(HandleSpecialCasesGo
-- 0
-- j0
-- (PlutusCore.Constant.Typed.ReverseGo
-- '[] (AsSpineRev (Maybe Char))))’ from being solved.
-- (Term TyName Name DefaultUni FunDebug ())
-- (AsSpine (Maybe Char)))’ from being solved.
-- Probable fix: use a type annotation to specify what ‘j0’ should be.
-- These potential instances exist:
-- four instances involving out-of-scope types
-- two instances involving out-of-scope types
-- (use -fprint-potential-instances to see them all)
-- • In the expression: enumerateDebug $ Just 'a'
-- >>> :t enumerateDebug $ \_ -> ()
Expand All @@ -51,144 +53,6 @@ type TermDebug = Term TyName Name DefaultUni FunDebug ()
enumerateDebug :: forall a j. EnumerateFromTo 0 j TermDebug a => a -> a
enumerateDebug = id

-- >>> :t enumerateDebug (undefined :: Opaque term (a, b))
-- enumerateDebug (undefined :: Opaque term (a, b))
-- :: Opaque
-- term (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-- >>> :t enumerateDebug (undefined :: Opaque term a)
-- enumerateDebug (undefined :: Opaque term a)
-- :: Opaque
-- (Term TyName Name DefaultUni FunDebug ())
-- (TyVarRep ('TyNameRep "a" 0))
-- >>> :t enumerateDebug (undefined :: SomeConstant uni a)
-- enumerateDebug (undefined :: SomeConstant uni a)
-- :: SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-- >>> :t enumerateDebug (undefined :: SomeConstant uni a -> SomeConstant uni b)
-- enumerateDebug (undefined :: SomeConstant uni a -> SomeConstant uni b)
-- :: SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-- -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))

-- >>> import PlutusCore.Evaluation.Result
-- >>> :t enumerateDebug (undefined :: SomeConstant uni a -> EvaluationResult b)
-- enumerateDebug (undefined :: SomeConstant uni a -> EvaluationResult b)
-- :: HandleSpecialCasesEnter
-- 1 j (PlutusCore.Constant.Typed.ReverseGo '[] (AsSpineRev b)) =>
-- SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-- -> EvaluationResult b


-- fstPlc :: Opaque term (a, b) -> EvaluationResult (Opaque term a)

-- >>> enumerateDebug (undefined :: Opaque term (a, b)) `seq` ()
-- <interactive>:331:2-49: error:
-- • '(Opaque term0 (a0, b0), '[AnyRep (a0, b0)])
-- • In the first argument of ‘seq’, namely
-- ‘enumerateDebug (undefined :: Opaque term (a, b))’
-- In the expression:
-- enumerateDebug (undefined :: Opaque term (a, b)) `seq` ()
-- In an equation for ‘it’:
-- it = enumerateDebug (undefined :: Opaque term (a, b)) `seq` ()

-- >>> :t inferDebug (undefined :: SomeConstant uni a)
-- inferDebug (undefined :: SomeConstant uni a)
-- :: SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0))

-- >>> import Data.Proxy
-- >>> :set -XDataKinds
-- >>> :t toTypeAst @_ @DefaultUni $ Proxy @(RepInfer (TyVarRep ('TyNameRep "a" 0)))
-- <interactive>:1:1-74: error:
-- • Ambiguous type variable ‘a0’ arising from a use of ‘toTypeAst’
-- prevents the constraint ‘(KnownTypeAst
-- DefaultUni
-- (RepInfer (TyVarRep ('TyNameRep "a" 0))))’ from being solved.
-- Probable fix: use a type annotation to specify what ‘a0’ should be.
-- These potential instance exist:
-- one instance involving out-of-scope types
-- (use -fprint-potential-instances to see them all)
-- • In the expression:
-- toTypeAst @_ @DefaultUni
-- $ Proxy @(RepInfer (TyVarRep ('TyNameRep "a" 0)))

-- >>> import Data.Proxy
-- >>> :set -XDataKinds
-- >>> toTypeAst $ Proxy @(SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0)))
-- TyVar () (TyName {unTyName = Name {nameString = "a", nameUnique = Unique {unUnique = 0}}})

-- >>> :t inferDebug (Prelude.id :: Opaque term (TyAppRep a Integer) -> Opaque term (TyAppRep a Integer))
-- <interactive>:1:1-95: error:
-- • No instance for (KnownTypeAst
-- DefaultUni (RepInfer (TyVarRep ('TyNameRep "a" 0))))
-- arising from a use of ‘inferDebug’
-- • In the expression:
-- inferDebug
-- (id ::
-- Opaque term (TyAppRep a Integer)
-- -> Opaque term (TyAppRep a Integer))


-- >>> :set -XTypeApplications
-- >>> :t (Proxy @(AsSpine (a, b)))
-- <interactive>:1:19: error: Not in scope: type variable ‘a’
-- <interactive>:1:22: error: Not in scope: type variable ‘b’

-- Opaque (SomeValueOf uni) (a, b) ?

-- >>> :t inferDebug (undefined :: Opaque term (a, b))
-- <interactive>:1:1-44: error:
-- • No instance for (Contains DefaultUni TyVarRep)
-- arising from a use of ‘inferDebug’
-- • In the expression: inferDebug (undefined :: Opaque term (a, b))
-- >>> :t inferDebug (undefined :: Opaque term a)
-- inferDebug (undefined :: Opaque term a)
-- :: Opaque
-- (Term TyName Name DefaultUni FunDebug ())
-- (TyVarRep ('TyNameRep "a" 0))
-- >>> :t inferDebug (undefined :: SomeConstant uni a)
-- inferDebug (undefined :: SomeConstant uni a)
-- :: (KnownPolytype
-- (Merge (ToBinds f) (ListToBinds args))
-- TermDebug
-- '[]
-- (SomeConstant DefaultUni a)
-- (SomeConstant DefaultUni a),
-- HandleSpecialCasesEnter
-- 0 j (PlutusCore.Constant.Typed.ReverseGo '[] (AsSpineRev a)),
-- KnownTypeAst DefaultUni f,
-- Data.SOP.Constraint.All (KnownTypeAst DefaultUni) args,
-- PlutusCore.Constant.Typed.ReverseGo '[] (AsSpineRev a)
-- ~ (f : args),
-- ListToBinds
-- (PlutusCore.Constant.Typed.ReverseGo '[] (AsSpineRev a))
-- ~ Merge (ToBinds f) (ListToBinds args)) =>
-- SomeConstant DefaultUni a
-- >>> :t inferDebug (undefined :: SomeConstant uni a -> SomeConstant uni b)
-- inferDebug (undefined :: SomeConstant uni a -> SomeConstant uni b)
-- :: (KnownPolytype
-- (Merge
-- (Merge
-- (ListToBinds
-- (PlutusCore.Constant.Typed.ReverseGo '[] (AsSpineRev a)))
-- '[])
-- (ListToBinds
-- (PlutusCore.Constant.Typed.ReverseGo '[] (AsSpineRev b))))
-- TermDebug
-- '[SomeConstant DefaultUni a]
-- (SomeConstant DefaultUni b)
-- (SomeConstant DefaultUni a -> SomeConstant DefaultUni b),
-- HandleSpecialCasesEnter
-- k j (PlutusCore.Constant.Typed.ReverseGo '[] (AsSpineRev b)),
-- HandleSpecialCasesEnter
-- 0 k (PlutusCore.Constant.Typed.ReverseGo '[] (AsSpineRev a)),
-- KnownTypeAst DefaultUni f1, KnownTypeAst DefaultUni f2,
-- Data.SOP.Constraint.All (KnownTypeAst DefaultUni) args1,
-- Data.SOP.Constraint.All (KnownTypeAst DefaultUni) args2,
-- PlutusCore.Constant.Typed.ReverseGo '[] (AsSpineRev b)
-- ~ (f2 : args2),
-- PlutusCore.Constant.Typed.ReverseGo '[] (AsSpineRev a)
-- ~ (f1 : args1)) =>
-- SomeConstant DefaultUni a -> SomeConstant DefaultUni b


-- | Instantiate type variables in the type of a value using 'EnumerateFromTo' and check that it's
-- possibe to construct a 'TypeScheme' out of the resulting type. Example usages:
--
Expand Down
12 changes: 7 additions & 5 deletions plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -479,15 +479,19 @@ type KnownBuiltinTypeAst = Contains
-- type IsBuiltin :: forall a. Bool -> a -> GHC.Type
-- data IsBuiltin b x

-- | Requires a rep context and turns it into a type context.
type BuiltinDone :: forall a. a -> GHC.Type
data BuiltinDone x

-- | Requires a type context and preserves it.
type TypeInfer :: GHC.Type -> GHC.Type
data TypeInfer a

-- | Requires a rep context and turns it into a type context.
type RepInfer :: forall a. a -> GHC.Type
data RepInfer x

-- | Requires a rep context and preserves it.
type RepDone :: forall a. a -> GHC.Type
data RepDone x

Expand Down Expand Up @@ -712,8 +716,7 @@ newtype SomeConstant uni (rep :: GHC.Type) = SomeConstant
{ unSomeConstant :: Some (ValueOf uni)
}

instance (uni ~ uni', AsSpine rep ~ spine, spine ~ (f ': args), All (KnownTypeAst uni) spine) =>
KnownTypeAst uni (SomeConstant uni' rep) where
instance KnownTypeAst uni (RepInfer rep) => KnownTypeAst uni (SomeConstant uni' rep) where
type ToBinds (SomeConstant _ rep) = ListToBinds (AsSpine rep)
type AsSpine (SomeConstant _ rep) = '[ RepInfer rep ]
toTypeAst _ = toTypeAst $ Proxy @(RepInfer rep)
Expand Down Expand Up @@ -754,11 +757,10 @@ instance
(runSingKind $ knownKind @kind)
(toTypeAst $ Proxy @a)

instance (uni ~ uni', AsSpine rep ~ spine, spine ~ (f ': args), All (KnownTypeAst uni) spine) =>
KnownTypeAst uni (Opaque term rep) where
instance KnownTypeAst uni (RepInfer rep) => KnownTypeAst uni (Opaque term rep) where
type ToBinds (Opaque _ rep) = ListToBinds (AsSpine rep)
type AsSpine (Opaque _ rep) = '[ RepInfer rep ]
toTypeAst _ = toTypeAst $ Proxy @(SomeConstant uni rep)
toTypeAst _ = toTypeAst $ Proxy @(RepInfer rep)

instance (term ~ term', uni ~ UniOf term, KnownTypeAst uni (Opaque term' rep)) =>
KnownTypeIn uni term (Opaque term' rep) where
Expand Down
2 changes: 1 addition & 1 deletion plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -292,7 +292,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
pure $ case xs of
[] -> a
_ : _ -> b
toBuiltinMeaning MkCons = undefined
toBuiltinMeaning MkCons =
makeBuiltinMeaning
consPlc
(runCostingFunTwoArguments . paramMkCons)
Expand Down