-- editorconfig-checker-disable-file {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module PlutusCore.Builtin.KnownTypeAst ( TyNameRep (..) , TyVarRep , TyAppRep , TyForallRep , Hole , RepHole , HasTermLevel , HasTypeLevel , HasTypeAndTermLevel , mkTyBuiltin , TypeHole , KnownBuiltinTypeAst , KnownTypeAst (..) , toTypeAst , Insert , Delete ) where import PlutusCore.Builtin.KnownKind import PlutusCore.Builtin.Polymorphism import PlutusCore.Builtin.Result import PlutusCore.Core import PlutusCore.Evaluation.Result import PlutusCore.Name.Unique import PlutusCore.Subst (typeMapNames) 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 Data.Type.Bool import Data.Void 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 {- Note [Name generality of KnownTypeAst] The 'KnownTypeAst' class takes a @tyname@ argument. The reason for this is that we want to be able to define 'mkTyBuiltin' such that it's generic over the type of names, because in addition to 'TyName' we also have 'TyDeBruijn' and it's convenient to seemlessly embed built-in types into a 'Type' regardless of which kind of names it expects. However we don't want that @tyname@ to proliferate through the entire code base. For example, 'HasTypeLevel' propagates up to PlutusTx and it doesn't make sense to mention implementation details such as 'TyName' there. For this reason we instantiate @tyname@ as soon as possible. When we want and can have full generality, we instantiate @tyname@ with 'Void', because anything can be recovered from 'Void' via 'absurd' while allowing us not to thread the @tyname@ parameter through half the codebase. And when we don't want or can't have generality, we instantiate @tyname@ with 'TyName'. -} -- | Specifies that the given type is a built-in one and can be embedded into a 'Type'. type HasTypeLevel :: forall a. (GHC.Type -> GHC.Type) -> a -> GHC.Constraint type HasTypeLevel uni x = KnownTypeAst Void uni (ElaborateBuiltin uni x) -- | The product of 'HasTypeLevel' and 'HasTermLevel'. type HasTypeAndTermLevel :: forall a. (GHC.Type -> GHC.Type) -> a -> GHC.Constraint type HasTypeAndTermLevel uni x = (uni `HasTypeLevel` x, uni `HasTermLevel` x) -- See Note [Name generality of KnownTypeAst]. -- TODO: make it @forall {a}@ once we have that. -- (see https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0099-explicit-specificity.rst) -- | Convert a Haskell representation of a possibly 0-ary application of a built-in type to -- arbitrary types implementing 'KnownTypeAst'. mkTyBuiltin :: forall a (x :: a) uni ann tyname. uni `HasTypeLevel` x => ann -> Type tyname uni ann mkTyBuiltin :: forall a (x :: a) (uni :: * -> *) ann tyname. HasTypeLevel uni x => ann -> Type tyname uni ann mkTyBuiltin ann ann = ann ann ann -> Type tyname uni () -> Type tyname uni ann forall a b. a -> Type tyname uni b -> Type tyname uni a forall (f :: * -> *) a b. Functor f => a -> f b -> f a <$ (Void -> tyname) -> Type Void uni () -> Type tyname uni () forall tyname tyname' (uni :: * -> *) ann. (tyname -> tyname') -> Type tyname uni ann -> Type tyname' uni ann typeMapNames Void -> tyname forall a. Void -> a absurd (Proxy (ElaborateBuiltin uni x) -> Type Void uni () forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname uni x => proxy x -> Type tyname uni () toTypeAst (Proxy (ElaborateBuiltin uni x) -> Type Void uni ()) -> Proxy (ElaborateBuiltin uni x) -> Type Void uni () forall a b. (a -> b) -> a -> b $ forall (t :: a). Proxy t forall {k} (t :: k). Proxy t Proxy @(ElaborateBuiltin uni x)) {-# INLINE mkTyBuiltin #-} -- | A constraint for \"@a@ is a 'KnownTypeAst' by means of being included in @uni@\". type KnownBuiltinTypeAst :: forall a. GHC.Type -> (GHC.Type -> GHC.Type) -> a -> GHC.Constraint type KnownBuiltinTypeAst tyname uni x = AllBuiltinArgs uni (KnownTypeAst tyname uni) x -- See Note [Name generality of KnownTypeAst]. -- | This class allows one to convert the type-level Haskell representation of a Plutus type into -- the corresponding Plutus type. Associated type families are needed to help elaboration. -- -- Depending on the universe converting a Haskell type to a Plutus team can give different results -- (e.g. 'Int' can be a built-in type instead of being encoded via built-in 'Integer'), hence this -- class takes a @uni@ argument. Plus, elaboration is universe-specific too. type KnownTypeAst :: forall a. GHC.Type -> (GHC.Type -> GHC.Type) -> a -> GHC.Constraint class KnownTypeAst tyname uni x where -- | Whether @x@ is a built-in type. type IsBuiltin uni x :: Bool type IsBuiltin uni x = IsBuiltin uni (ElaborateBuiltin uni x) -- | 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 uni x :: [Hole] type ToHoles uni x = ToHoles uni (ElaborateBuiltin uni x) -- | Collect all unique variables (a variable consists of a textual name, a unique and a kind) -- in an accumulator and return the accumulator once a leaf is reached. type ToBinds uni (acc :: [GADT.Some TyNameRep]) x :: [GADT.Some TyNameRep] type ToBinds uni acc x = ToBinds uni acc (ElaborateBuiltin uni x) -- Doesn't take a @proxy@, so that newtype- and via-deriving are available. -- | The Plutus counterpart of the @x@ type. typeAst :: Type tyname uni () default typeAst :: KnownTypeAst tyname uni (ElaborateBuiltin uni x) => Type tyname uni () typeAst = Proxy (ElaborateBuiltin uni x) -> Type tyname uni () forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname uni x => proxy x -> Type tyname uni () toTypeAst (Proxy (ElaborateBuiltin uni x) -> Type tyname uni ()) -> Proxy (ElaborateBuiltin uni x) -> Type tyname uni () forall a b. (a -> b) -> a -> b $ forall (t :: a). Proxy t forall {k} (t :: k). Proxy t Proxy @(ElaborateBuiltin uni x) {-# INLINE typeAst #-} instance KnownTypeAst tyname uni a => KnownTypeAst tyname uni (EvaluationResult a) where type IsBuiltin _ (EvaluationResult a) = 'False type ToHoles _ (EvaluationResult a) = '[TypeHole a] type ToBinds uni acc (EvaluationResult a) = ToBinds uni acc a typeAst :: Type tyname uni () typeAst = Proxy a -> Type tyname uni () forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname 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 $ forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @a {-# INLINE typeAst #-} instance KnownTypeAst tyname uni a => KnownTypeAst tyname uni (BuiltinResult a) where type IsBuiltin _ (BuiltinResult a) = 'False type ToHoles _ (BuiltinResult a) = '[TypeHole a] type ToBinds uni acc (BuiltinResult a) = ToBinds uni acc a typeAst :: Type tyname uni () typeAst = Proxy a -> Type tyname uni () forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname 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 $ forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @a {-# INLINE typeAst #-} instance KnownTypeAst tyname uni rep => KnownTypeAst tyname uni (SomeConstant uni rep) where type IsBuiltin _ (SomeConstant uni rep) = 'False type ToHoles _ (SomeConstant _ rep) = '[RepHole rep] type ToBinds uni acc (SomeConstant _ rep) = ToBinds uni acc rep typeAst :: Type tyname uni () typeAst = Proxy rep -> Type tyname uni () forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname 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 $ forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @rep {-# INLINE typeAst #-} instance KnownTypeAst tyname uni rep => KnownTypeAst tyname uni (Opaque val rep) where type IsBuiltin _ (Opaque val rep) = 'False type ToHoles _ (Opaque _ rep) = '[RepHole rep] type ToBinds uni acc (Opaque _ rep) = ToBinds uni acc rep typeAst :: Type tyname uni () typeAst = Proxy rep -> Type tyname uni () forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname 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 $ forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @rep {-# INLINE typeAst #-} -- | Return the Plutus counterpart of the @x@ type. toTypeAst :: forall a tyname uni (x :: a) proxy. KnownTypeAst tyname uni x => proxy x -> Type tyname uni () toTypeAst :: forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname uni x => proxy x -> Type tyname uni () toTypeAst proxy x _ = forall a tyname (uni :: * -> *) (x :: a). KnownTypeAst tyname uni x => Type tyname uni () typeAst @_ @tyname @uni @x {-# INLINE toTypeAst #-} toTyNameAst :: forall text uniq. (KnownSymbol text, KnownNat uniq) => Proxy ('TyNameRep text uniq) -> TyName toTyNameAst :: forall {kind} (text :: Symbol) (uniq :: Nat). (KnownSymbol text, KnownNat uniq) => 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 $ 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 $ 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 tyname uni (BuiltinHead f) where type IsBuiltin _ (BuiltinHead f) = 'True type ToHoles _ (BuiltinHead f) = '[] type ToBinds _ acc (BuiltinHead f) = acc typeAst :: Type tyname uni () typeAst = () -> SomeTypeIn uni -> Type tyname uni () forall tyname (uni :: * -> *) ann. ann -> SomeTypeIn uni -> Type tyname uni ann TyBuiltin () (SomeTypeIn uni -> Type tyname uni ()) -> SomeTypeIn uni -> Type tyname uni () forall a b. (a -> b) -> a -> b $ forall k (a :: k) (uni :: * -> *). Contains uni a => SomeTypeIn uni someType @_ @f {-# INLINE typeAst #-} instance (KnownTypeAst tyname uni a, KnownTypeAst tyname uni b) => KnownTypeAst tyname uni (a -> b) where type IsBuiltin _ (a -> b) = 'False type ToHoles _ (a -> b) = '[TypeHole a, TypeHole b] type ToBinds uni acc (a -> b) = ToBinds uni (ToBinds uni acc a) b typeAst :: Type tyname uni () typeAst = () -> 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 tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname 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 $ forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @a) (Proxy b -> Type tyname uni () forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname 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 $ forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @b) {-# INLINE typeAst #-} instance (tyname ~ TyName, name ~ 'TyNameRep text uniq, KnownSymbol text, KnownNat uniq) => KnownTypeAst tyname uni (TyVarRep name) where type IsBuiltin _ (TyVarRep name) = 'False type ToHoles _ (TyVarRep name) = '[] type ToBinds _ acc (TyVarRep name) = Insert ('GADT.Some name) acc typeAst :: Type tyname uni () typeAst = () -> 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 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 $ forall {k} (t :: k). Proxy t forall (t :: TyNameRep Any). Proxy t Proxy @('TyNameRep text uniq) {-# INLINE typeAst #-} instance (KnownTypeAst tyname uni fun, KnownTypeAst tyname uni arg) => KnownTypeAst tyname uni (TyAppRep fun arg) where type IsBuiltin uni (TyAppRep fun arg) = IsBuiltin uni fun && IsBuiltin uni arg type ToHoles _ (TyAppRep fun arg) = '[RepHole fun, RepHole arg] type ToBinds uni acc (TyAppRep fun arg) = ToBinds uni (ToBinds uni acc fun) arg typeAst :: Type tyname uni () typeAst = () -> 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 tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname 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 $ forall {k} (t :: k). Proxy t forall (t :: dom -> a). Proxy t Proxy @fun) (Proxy arg -> Type tyname uni () forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname 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 $ forall (t :: dom). Proxy t forall {k} (t :: k). Proxy t Proxy @arg) {-# INLINE typeAst #-} instance ( tyname ~ TyName, name ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq , KnownKind kind, KnownTypeAst tyname uni a ) => KnownTypeAst tyname uni (TyForallRep name a) where type IsBuiltin _ (TyForallRep name a) = 'False type ToHoles _ (TyForallRep name a) = '[RepHole a] type ToBinds uni acc (TyForallRep name a) = Delete ('GADT.Some name) (ToBinds uni acc a) typeAst :: Type tyname uni () typeAst = () -> 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 $ forall {k} (t :: k). Proxy t forall (t :: TyNameRep Any). 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 $ forall k. KnownKind k => SingKind k knownKind @kind) (Proxy a -> Type tyname uni () forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst tyname 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 $ forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @a) {-# INLINE typeAst #-} -- Utils -- | Insert @x@ into @xs@ unless it's already there. type Insert :: forall a. a -> [a] -> [a] type family Insert x xs where Insert x '[] = '[x] Insert x (x : xs) = x ': xs Insert x (y : xs) = y ': Insert x xs -- | Delete the first @x@ from a list. Which is okay since we only ever put things in once. type Delete :: forall a. a -> [a] -> [a] type family Delete x xs where Delete _ '[] = '[] Delete x (x ': xs) = xs Delete x (y ': xs) = y ': Delete x xs