{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module PlutusCore.Builtin.KnownTypeAst ( TyNameRep (..) , TyVarRep , TyAppRep , TyForallRep , Hole , RepHole , TypeHole , KnownBuiltinTypeAst , KnownTypeAst (..) , Merge ) where import PlutusCore.Builtin.Emitter import PlutusCore.Builtin.KnownKind import PlutusCore.Builtin.Polymorphism import PlutusCore.Core import PlutusCore.Evaluation.Result import PlutusCore.MkPlc hiding (error) import PlutusCore.Name import Data.Kind qualified as GHC (Constraint, Type) import Data.Proxy import Data.Some.GADT qualified as GADT import Data.Text qualified as Text import GHC.TypeLits import Universe {- Note [Rep vs Type context] Say you define an @Id@ built-in function and specify its Haskell type signature: id :: forall a. a -> a This gets picked up by the 'TypeScheme' inference machinery, which detects @a@ and instantiates it to @Opaque val Var0@ where @Var0@ is some concrete type (the exact details don't matter here) representing a Plutus type variable of kind @*@ with the @0@ unique, so @id@ elaborates to id :: Opaque val Var0 -> Opaque val Var0 But consider also the case where you want to define @id@ only over lists. The signature of the built-in function then is idList :: forall a. Opaque val [a] -> Opaque val [a] Now the 'Opaque' is explicit and the 'TypeScheme' inference machinery needs to go under it in order to instantiate @a@. Which now does not get instantiated to an 'Opaque' as before, since we're already inside an 'Opaque' and can just use @Var0@ directly. So @idList@ elaborates to idList :: Opaque val [Var0] -> Opaque val [Var0] Now let's make up some syntax for annotating contexts so that it's clear what's going on: idList @Type | :: (@Type | Opaque val (@Rep | [Var0])) -> (@Type | Opaque val (@Rep | [Var0])) '@ann |' annotates everything to the right of it. The whole thing then reads as 1. a builtin is always defined in the Type context 2. @->@ preserves the Type context, i.e. it accepts it and passes it down to the domain and codomain 3. @Opaque val@ switches the context from Type to Rep, i.e. it accepts the Type context, but creates the Rep context for its argument that represents a Plutus type So why the distinction? The difference between the Rep and the Type contexts that we've seen so far is that in the Rep context we don't need any @Opaque@, but this is a very superficial reason to keep the distinction between contexts, since everything that is legal in the Type context is legal in the Rep context as well. For example we could've elaborated @idList@ into a bit more verbose idList :: Opaque val [Opaque val Var0] -> Opaque val [Opaque val Var0] and the world wouldn't end because of that, everything would work correctly. The opposite however is not true: certain types that are legal in the Rep context are not legal in the Type one and this is the reason why the distinction exists. The simplest example is id :: Var0 -> Var0 @Var0@ represents a Plutus type variable and it's a data family with no inhabitants, so it does not make sense to try to unlift a value of that type. Now let's say we added a @term@ argument to @Var0@ and said that when @Var0 term@ is a @GHC.Type@, it has a @term@ inside, just like 'Opaque'. Then we would be able to unlift it, but we also have things like @TyAppRep@, @TyForallRep@ and that set is open, any Plutus type can be represented using such combinators and we can even name particular types, e.g. we could have @PlcListRep@, so we'd have to special-case @GHC.Type@ for each of them and it would be a huge mess. So instead of mixing up types whose values are actually unliftable with types that are only used for type checking, we keep the distinction explicit. The barrier between Haskell and Plutus is the barrier between the Type and the Rep contexts and that barrier must always be some explicit type constructor that switches the context from Type to Rep. We've only considered 'Opaque' as an example of such type constructor, but we also have 'SomeConstant' as another example. Some type constructors turn any context into the Type one, for example 'EvaluationResult' and 'Emitter', although they are useless inside the Rep context, given that it's only for type checking Plutus and they don't exist in the type language of Plutus. These @*Rep@ data families like 'TyVarRep', 'TyAppRep' etc all require the Rep context and preserve it, since they're only for representing Plutus types for type checking purposes. We call a thing in a Rep or 'Type' context a 'RepHole' or 'TypeHole' respectively. The reason for the name is that the inference machinery looks at the thing and tries to instantiate it, like fill a hole. We could also have a third type of hole/context, Name, because binders bind names rather than variables and so it makes sense to infer names sometimes, like for 'TyForallRep' for example. We don't do that currently, because we don't have such builtins anyway. And there could be even fancier kinds of holes like "infer anything" for cases where the hole is determined by some other part of the signature. We don't have that either, for the same reason. For the user defining a builtin this all is pretty much invisible. -} -- See Note [Rep vs Type context]. -- | The kind of holes. data Hole -- See Note [Rep vs Type context]. -- | A hole in the Rep context. type RepHole :: forall a hole. a -> hole data family RepHole x -- See Note [Rep vs Type context]. -- | A hole in the Type context. type TypeHole :: forall hole. GHC.Type -> hole data family TypeHole a -- | For annotating an uninstantiated built-in type, so that it gets handled by the right instance -- or type family. type BuiltinHead :: forall k. k -> k data family BuiltinHead f -- | Take an iterated application of a built-in type and elaborate every function application -- inside of it to 'TypeAppRep', plus annotate the head with 'BuiltinHead'. -- The idea is that we don't need to process built-in types manually if we simply add some -- annotations for instance resolution to look for. Think what we'd have to do manually for, say, -- 'ToHoles': traverse the spine of the application and collect all the holes into a list, which is -- troubling, because type applications are left-nested and lists are right-nested, so we'd have to -- use accumulators or an explicit 'Reverse' type family. And then we also have 'KnownTypeAst' and -- 'ToBinds', so handling built-in types in a special way for each of those would be a hassle, -- especially given the fact that type-level Haskell is not exactly good at computing things. -- With the 'ElaborateBuiltin' approach we get 'KnownTypeAst', 'ToHoles' and 'ToBinds' for free. type ElaborateBuiltin :: forall k. k -> k type family ElaborateBuiltin a where ElaborateBuiltin (f x) = ElaborateBuiltin f `TyAppRep` x ElaborateBuiltin f = BuiltinHead f -- | A constraint for \"@a@ is a 'KnownTypeAst' by means of being included in @uni@\". type KnownBuiltinTypeAst uni a = KnownTypeAst uni (ElaborateBuiltin a) type KnownTypeAst :: forall a. (GHC.Type -> GHC.Type) -> a -> GHC.Constraint class KnownTypeAst uni x where -- | Return every part of the type that can be a to-be-instantiated type variable. -- For example, in @Integer@ there's no such types and in @(a, b)@ it's the two arguments -- (@a@ and @b@) and the same applies to @a -> b@ (to mention a type that is not built-in). type ToHoles x :: [Hole] type ToHoles x = ToHoles (ElaborateBuiltin x) -- | Collect all unique variables (a variable consists of a textual name, a unique and a kind) -- in an @a@. type ToBinds x :: [GADT.Some TyNameRep] type ToBinds x = ToBinds (ElaborateBuiltin x) -- | The type representing @a@ used on the PLC side. toTypeAst :: proxy x -> Type TyName uni () default toTypeAst :: KnownBuiltinTypeAst uni x => proxy x -> Type TyName uni () toTypeAst proxy x _ = Proxy (ElaborateBuiltin x) -> Type TyName uni () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst (Proxy (ElaborateBuiltin x) -> Type TyName uni ()) -> Proxy (ElaborateBuiltin x) -> Type TyName uni () forall a b. (a -> b) -> a -> b $ Proxy (ElaborateBuiltin x) forall k (t :: k). Proxy t Proxy @(ElaborateBuiltin x) {-# INLINE toTypeAst #-} instance KnownTypeAst uni a => KnownTypeAst uni (EvaluationResult a) where type ToHoles (EvaluationResult a) = '[TypeHole a] type ToBinds (EvaluationResult a) = ToBinds a toTypeAst :: proxy (EvaluationResult a) -> Type TyName uni () toTypeAst proxy (EvaluationResult a) _ = Proxy a -> Type TyName uni () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst (Proxy a -> Type TyName uni ()) -> Proxy a -> Type TyName uni () forall a b. (a -> b) -> a -> b $ Proxy a forall k (t :: k). Proxy t Proxy @a {-# INLINE toTypeAst #-} instance KnownTypeAst uni a => KnownTypeAst uni (Emitter a) where type ToHoles (Emitter a) = '[TypeHole a] type ToBinds (Emitter a) = ToBinds a toTypeAst :: proxy (Emitter a) -> Type TyName uni () toTypeAst proxy (Emitter a) _ = Proxy a -> Type TyName uni () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst (Proxy a -> Type TyName uni ()) -> Proxy a -> Type TyName uni () forall a b. (a -> b) -> a -> b $ Proxy a forall k (t :: k). Proxy t Proxy @a {-# INLINE toTypeAst #-} instance KnownTypeAst uni rep => KnownTypeAst uni (SomeConstant uni rep) where type ToHoles (SomeConstant _ rep) = '[RepHole rep] type ToBinds (SomeConstant _ rep) = ToBinds rep toTypeAst :: proxy (SomeConstant uni rep) -> Type TyName uni () toTypeAst proxy (SomeConstant uni rep) _ = Proxy rep -> Type TyName uni () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst (Proxy rep -> Type TyName uni ()) -> Proxy rep -> Type TyName uni () forall a b. (a -> b) -> a -> b $ Proxy rep forall k (t :: k). Proxy t Proxy @rep {-# INLINE toTypeAst #-} instance KnownTypeAst uni rep => KnownTypeAst uni (Opaque val rep) where type ToHoles (Opaque _ rep) = '[RepHole rep] type ToBinds (Opaque _ rep) = ToBinds rep toTypeAst :: proxy (Opaque val rep) -> Type TyName uni () toTypeAst proxy (Opaque val rep) _ = Proxy rep -> Type TyName uni () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst (Proxy rep -> Type TyName uni ()) -> Proxy rep -> Type TyName uni () forall a b. (a -> b) -> a -> b $ Proxy rep forall k (t :: k). Proxy t Proxy @rep {-# INLINE toTypeAst #-} toTyNameAst :: forall text uniq. (KnownSymbol text, KnownNat uniq) => Proxy ('TyNameRep text uniq) -> TyName toTyNameAst :: Proxy ('TyNameRep text uniq) -> TyName toTyNameAst Proxy ('TyNameRep text uniq) _ = Name -> TyName TyName (Name -> TyName) -> Name -> TyName forall a b. (a -> b) -> a -> b $ Text -> Unique -> Name Name (String -> Text Text.pack (String -> Text) -> String -> Text forall a b. (a -> b) -> a -> b $ Proxy text -> String forall (n :: Symbol) (proxy :: Symbol -> *). KnownSymbol n => proxy n -> String symbolVal @text Proxy text forall k (t :: k). Proxy t Proxy) (Int -> Unique Unique (Int -> Unique) -> (Integer -> Int) -> Integer -> Unique forall b c a. (b -> c) -> (a -> b) -> a -> c . Integer -> Int forall a b. (Integral a, Num b) => a -> b fromIntegral (Integer -> Unique) -> Integer -> Unique forall a b. (a -> b) -> a -> b $ Proxy uniq -> Integer forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Integer natVal @uniq Proxy uniq forall k (t :: k). Proxy t Proxy) {-# INLINE toTyNameAst #-} instance uni `Contains` f => KnownTypeAst uni (BuiltinHead f) where type ToHoles (BuiltinHead f) = '[] type ToBinds (BuiltinHead f) = '[] toTypeAst :: proxy (BuiltinHead f) -> Type TyName uni () toTypeAst proxy (BuiltinHead f) _ = () -> Type TyName uni () forall k (a :: k) (uni :: * -> *) tyname ann. Contains uni a => ann -> Type tyname uni ann mkTyBuiltin @_ @f () {-# INLINE toTypeAst #-} instance (KnownTypeAst uni a, KnownTypeAst uni b) => KnownTypeAst uni (a -> b) where type ToHoles (a -> b) = '[TypeHole a, TypeHole b] type ToBinds (a -> b) = Merge (ToBinds a) (ToBinds b) toTypeAst :: proxy (a -> b) -> Type TyName uni () toTypeAst proxy (a -> b) _ = () -> Type TyName uni () -> Type TyName uni () -> Type TyName uni () forall tyname (uni :: * -> *) ann. ann -> Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann TyFun () (Proxy a -> Type TyName uni () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst (Proxy a -> Type TyName uni ()) -> Proxy a -> Type TyName uni () forall a b. (a -> b) -> a -> b $ Proxy a forall k (t :: k). Proxy t Proxy @a) (Proxy b -> Type TyName uni () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst (Proxy b -> Type TyName uni ()) -> Proxy b -> Type TyName uni () forall a b. (a -> b) -> a -> b $ Proxy b forall k (t :: k). Proxy t Proxy @b) {-# INLINE toTypeAst #-} instance (name ~ 'TyNameRep text uniq, KnownSymbol text, KnownNat uniq) => KnownTypeAst uni (TyVarRep name) where type ToHoles (TyVarRep name) = '[] type ToBinds (TyVarRep name) = '[ 'GADT.Some name ] toTypeAst :: proxy (TyVarRep name) -> Type TyName uni () toTypeAst proxy (TyVarRep name) _ = () -> TyName -> Type TyName uni () forall tyname (uni :: * -> *) ann. ann -> tyname -> Type tyname uni ann TyVar () (TyName -> Type TyName uni ()) -> (Proxy ('TyNameRep text uniq) -> TyName) -> Proxy ('TyNameRep text uniq) -> Type TyName uni () forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy ('TyNameRep text uniq) -> TyName forall kind (text :: Symbol) (uniq :: Nat). (KnownSymbol text, KnownNat uniq) => Proxy ('TyNameRep text uniq) -> TyName toTyNameAst (Proxy ('TyNameRep text uniq) -> Type TyName uni ()) -> Proxy ('TyNameRep text uniq) -> Type TyName uni () forall a b. (a -> b) -> a -> b $ Proxy ('TyNameRep text uniq) forall k (t :: k). Proxy t Proxy @('TyNameRep text uniq) {-# INLINE toTypeAst #-} instance (KnownTypeAst uni fun, KnownTypeAst uni arg) => KnownTypeAst uni (TyAppRep fun arg) where type ToHoles (TyAppRep fun arg) = '[RepHole fun, RepHole arg] type ToBinds (TyAppRep fun arg) = Merge (ToBinds fun) (ToBinds arg) toTypeAst :: proxy (TyAppRep fun arg) -> Type TyName uni () toTypeAst proxy (TyAppRep fun arg) _ = () -> Type TyName uni () -> Type TyName uni () -> Type TyName uni () forall tyname (uni :: * -> *) ann. ann -> Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann TyApp () (Proxy fun -> Type TyName uni () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst (Proxy fun -> Type TyName uni ()) -> Proxy fun -> Type TyName uni () forall a b. (a -> b) -> a -> b $ Proxy fun forall k (t :: k). Proxy t Proxy @fun) (Proxy arg -> Type TyName uni () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst (Proxy arg -> Type TyName uni ()) -> Proxy arg -> Type TyName uni () forall a b. (a -> b) -> a -> b $ Proxy arg forall k (t :: k). Proxy t Proxy @arg) {-# INLINE toTypeAst #-} instance ( name ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq , KnownKind kind, KnownTypeAst uni a ) => KnownTypeAst uni (TyForallRep name a) where type ToHoles (TyForallRep name a) = '[RepHole a] type ToBinds (TyForallRep name a) = Delete ('GADT.Some name) (ToBinds a) toTypeAst :: proxy (TyForallRep name a) -> Type TyName uni () toTypeAst proxy (TyForallRep name a) _ = () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni () forall tyname (uni :: * -> *) ann. ann -> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann TyForall () (Proxy ('TyNameRep text uniq) -> TyName forall kind (text :: Symbol) (uniq :: Nat). (KnownSymbol text, KnownNat uniq) => Proxy ('TyNameRep text uniq) -> TyName toTyNameAst (Proxy ('TyNameRep text uniq) -> TyName) -> Proxy ('TyNameRep text uniq) -> TyName forall a b. (a -> b) -> a -> b $ Proxy ('TyNameRep text uniq) forall k (t :: k). Proxy t Proxy @('TyNameRep text uniq)) (SingKind kind -> Kind () forall k. SingKind k -> Kind () demoteKind (SingKind kind -> Kind ()) -> SingKind kind -> Kind () forall a b. (a -> b) -> a -> b $ KnownKind kind => SingKind kind forall k. KnownKind k => SingKind k knownKind @kind) (Proxy a -> Type TyName uni () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst (Proxy a -> Type TyName uni ()) -> Proxy a -> Type TyName uni () forall a b. (a -> b) -> a -> b $ Proxy a forall k (t :: k). Proxy t Proxy @a) {-# INLINE toTypeAst #-} -- Utils -- | Delete all @x@s from a list. type family Delete x xs :: [a] where Delete _ '[] = '[] Delete x (x ': xs) = Delete x xs Delete x (y ': xs) = y ': Delete x xs -- | Delete all elements appearing in the first list from the second one and concatenate the lists. type family Merge xs ys :: [a] where Merge '[] ys = ys Merge (x ': xs) ys = x ': Delete x (Merge xs ys)