{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module PlutusCore.Builtin.KnownKind where
import PlutusCore.Core
import Data.Kind as GHC
import Data.Proxy
import GHC.Types
import Universe
infixr 5 `SingKindArrow`
data SingKind k where
SingType :: SingKind GHC.Type
SingKindArrow :: SingKind k -> SingKind l -> SingKind (k -> l)
withSingKind :: Kind ann -> (forall k. SingKind k -> r) -> r
withSingKind :: forall ann r. Kind ann -> (forall k. SingKind k -> r) -> r
withSingKind (Type ann
_) forall k. SingKind k -> r
k = SingKind (*) -> r
forall k. SingKind k -> r
k SingKind (*)
SingType
withSingKind (KindArrow ann
_ Kind ann
dom Kind ann
cod) forall k. SingKind k -> r
k =
Kind ann -> (forall k. SingKind k -> r) -> r
forall ann r. Kind ann -> (forall k. SingKind k -> r) -> r
withSingKind Kind ann
dom ((forall k. SingKind k -> r) -> r)
-> (forall k. SingKind k -> r) -> r
forall a b. (a -> b) -> a -> b
$ \SingKind k
domS ->
Kind ann -> (forall k. SingKind k -> r) -> r
forall ann r. Kind ann -> (forall k. SingKind k -> r) -> r
withSingKind Kind ann
cod ((forall k. SingKind k -> r) -> r)
-> (forall k. SingKind k -> r) -> r
forall a b. (a -> b) -> a -> b
$ \SingKind k
codS ->
SingKind (k -> k) -> r
forall k. SingKind k -> r
k (SingKind (k -> k) -> r) -> SingKind (k -> k) -> r
forall a b. (a -> b) -> a -> b
$ SingKind k -> SingKind k -> SingKind (k -> k)
forall k l. SingKind k -> SingKind l -> SingKind (k -> l)
SingKindArrow SingKind k
domS SingKind k
codS
class KnownKind k where
knownKind :: SingKind k
instance rep ~ LiftedRep => KnownKind (TYPE rep) where
knownKind :: SingKind (TYPE rep)
knownKind = SingKind (TYPE rep)
SingKind (*)
SingType
instance (KnownKind dom, KnownKind cod) => KnownKind (dom -> cod) where
knownKind :: SingKind (dom -> cod)
knownKind = SingKind dom -> SingKind cod -> SingKind (dom -> cod)
forall k l. SingKind k -> SingKind l -> SingKind (k -> l)
SingKindArrow (forall k. KnownKind k => SingKind k
knownKind @dom) (forall k. KnownKind k => SingKind k
knownKind @cod)
bringKnownKind :: SingKind k -> (KnownKind k => r) -> r
bringKnownKind :: forall k r. SingKind k -> (KnownKind k => r) -> r
bringKnownKind SingKind k
SingType KnownKind k => r
r = r
KnownKind k => r
r
bringKnownKind (SingKindArrow SingKind k
dom SingKind l
cod) KnownKind k => r
r = SingKind k -> (KnownKind k => r) -> r
forall k r. SingKind k -> (KnownKind k => r) -> r
bringKnownKind SingKind k
dom ((KnownKind k => r) -> r) -> (KnownKind k => r) -> r
forall a b. (a -> b) -> a -> b
$ SingKind l -> (KnownKind l => r) -> r
forall k r. SingKind k -> (KnownKind k => r) -> r
bringKnownKind SingKind l
cod r
KnownKind k => r
KnownKind l => r
r
withKnownKind :: Kind ann -> (forall k. KnownKind k => Proxy k -> r) -> r
withKnownKind :: forall ann r.
Kind ann -> (forall k. KnownKind k => Proxy k -> r) -> r
withKnownKind Kind ann
kind forall k. KnownKind k => Proxy k -> r
k =
Kind ann -> (forall {k}. SingKind k -> r) -> r
forall ann r. Kind ann -> (forall k. SingKind k -> r) -> r
withSingKind Kind ann
kind ((forall {k}. SingKind k -> r) -> r)
-> (forall {k}. SingKind k -> r) -> r
forall a b. (a -> b) -> a -> b
$ \(SingKind k
kindS :: SingKind kind) ->
SingKind k -> (KnownKind k => r) -> r
forall k r. SingKind k -> (KnownKind k => r) -> r
bringKnownKind SingKind k
kindS ((KnownKind k => r) -> r) -> (KnownKind k => r) -> r
forall a b. (a -> b) -> a -> b
$ Proxy k -> r
forall k. KnownKind k => Proxy k -> r
k (Proxy k -> r) -> Proxy k -> r
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @kind
class ToKind (uni :: GHC.Type -> GHC.Type) where
toSingKind :: uni (Esc (a :: k)) -> SingKind k
demoteKind :: SingKind k -> Kind ()
demoteKind :: forall k. SingKind k -> Kind ()
demoteKind SingKind k
SingType = () -> Kind ()
forall ann. ann -> Kind ann
Type ()
demoteKind (SingKindArrow SingKind k
dom SingKind l
cod) = () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (SingKind k -> Kind ()
forall k. SingKind k -> Kind ()
demoteKind SingKind k
dom) (SingKind l -> Kind ()
forall k. SingKind k -> Kind ()
demoteKind SingKind l
cod)
kindOfBuiltinType :: ToKind uni => uni (Esc a) -> Kind ()
kindOfBuiltinType :: forall {k} (uni :: * -> *) (a :: k).
ToKind uni =>
uni (Esc a) -> Kind ()
kindOfBuiltinType = SingKind k -> Kind ()
forall k. SingKind k -> Kind ()
demoteKind (SingKind k -> Kind ())
-> (uni (Esc a) -> SingKind k) -> uni (Esc a) -> Kind ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. uni (Esc a) -> SingKind k
forall k (a :: k). uni (Esc a) -> SingKind k
forall (uni :: * -> *) k (a :: k).
ToKind uni =>
uni (Esc a) -> SingKind k
toSingKind