{-# 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`

-- | The type of singletonized Haskell kinds representing Plutus kinds.
-- Indexing by a Haskell kind allows us to avoid an 'error' call in the 'ToKind' instance of
-- 'DefaultUni' and not worry about proxies in the type of 'knownKind'.
data SingKind k where
    SingType      :: SingKind GHC.Type
    SingKindArrow :: SingKind k -> SingKind l -> SingKind (k -> l)

-- | Feed the 'SingKind' version of the given 'Kind' to the given continuation.
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

-- | For reifying Haskell kinds representing Plutus kinds at the term level.
class KnownKind k where
    knownKind :: SingKind k

-- | Plutus only supports lifted types, hence the equality constraint.
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)

-- | Satisfy the 'KnownKind' constraint of a continuation using the given 'SingKind'.
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

-- We need this for type checking Plutus, however we get Plutus types/terms/programs by either
-- producing them directly or by parsing/decoding them and in both the cases we have access to the
-- @Typeable@ information for the Haskell kind of a type and so we could just keep it around
-- (instead of throwing it away like we do now) and compute the Plutus kind directly from that.
-- That might be less efficient and probably requires updating the Plutus Tx compiler, so we went
-- with the simplest option for now and it's to have a class. Providing an instance per universe is
-- no big deal.
-- | For computing the Plutus kind of a built-in type. See 'kindOfBuiltinType'.
class ToKind (uni :: GHC.Type -> GHC.Type) where
    -- | Reify the kind of a type from the universe at the term level.
    toSingKind :: uni (Esc (a :: k)) -> SingKind k

-- | Convert a reified Haskell kind to a Plutus kind.
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)

-- | Compute the kind of a type from a universe.
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