{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

module PlutusCore.Builtin.Polymorphism
    ( Opaque (..)
    , SomeConstant (..)
    , TyNameRep (..)
    , TyVarRep
    , TyAppRep
    , TyForallRep
    ) where

import PlutusCore.Builtin.HasConstant
import PlutusCore.Core
import PlutusCore.Pretty

import Data.Kind qualified as GHC (Type)
import GHC.Ix
import GHC.TypeLits
import Universe

{- Note [Motivation for polymorphic built-in functions]
We need to support polymorphism for built-in functions for these reasons:

1. @ifThenElse@ for 'Bool' (being a built-in type rather than a Scott-encoded one) has to be
   polymorphic as its type signature is

       ifThenElse : all a. Bool -> a -> a -> a

   Previously we had 'Bool' as a Scott-encoded type, but this required plenty of supporting machinery,
   because unlifting (aka Scott-decoding) a PLC 'Bool' into a Haskell 'Bool' is quite a non-trivial
   thing, see https://github.com/input-output-hk/plutus/blob/e222466e6d46bbca9f76243bb496b3c88ed02ca1/language-plutus-core/src/PlutusCore.Builtin/Typed.hs#L165-L252

   Now that we got rid of all this complexity we have to pay for that by supporting polymorphic
   built-in functions (but we added that support long ago anyway, 'cause it was easy to do).

2. we may want to add efficient polymorphic built-in types like @IntMap@ or @Vector@ and most functions
   defined over them are polymorphic as well
-}

-- See Note [Motivation for polymorphic built-in functions].
-- See Note [Implementation of polymorphic built-in functions].
-- See Note [Pattern matching on built-in types].
-- | The denotation of a term whose PLC type is encoded in @rep@ (for example a type variable or
-- an application of a type variable). I.e. the denotation of such a term is the term itself.
-- This is because we have parametricity in Haskell, so we can't inspect a value whose
-- type is, say, a bound variable, so we never need to convert such a term from Plutus Core to
-- Haskell and back and instead can keep it intact.
newtype Opaque val (rep :: GHC.Type) = Opaque
    { Opaque val rep -> val
unOpaque :: val
    } deriving newtype ([Opaque val rep] -> Doc ann
Opaque val rep -> Doc ann
(forall ann. Opaque val rep -> Doc ann)
-> (forall ann. [Opaque val rep] -> Doc ann)
-> Pretty (Opaque val rep)
forall ann. [Opaque val rep] -> Doc ann
forall ann. Opaque val rep -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
forall val rep ann. Pretty val => [Opaque val rep] -> Doc ann
forall val rep ann. Pretty val => Opaque val rep -> Doc ann
prettyList :: [Opaque val rep] -> Doc ann
$cprettyList :: forall val rep ann. Pretty val => [Opaque val rep] -> Doc ann
pretty :: Opaque val rep -> Doc ann
$cpretty :: forall val rep ann. Pretty val => Opaque val rep -> Doc ann
Pretty, Maybe cause
-> Opaque val rep -> m (Some (ValueOf (UniOf (Opaque val rep))))
(forall err cause (m :: * -> *).
 (MonadError (ErrorWithCause err cause) m, AsUnliftingError err) =>
 Maybe cause
 -> Opaque val rep -> m (Some (ValueOf (UniOf (Opaque val rep)))))
-> AsConstant (Opaque val rep)
forall term.
(forall err cause (m :: * -> *).
 (MonadError (ErrorWithCause err cause) m, AsUnliftingError err) =>
 Maybe cause -> term -> m (Some (ValueOf (UniOf term))))
-> AsConstant term
forall val rep err cause (m :: * -> *).
(AsConstant val, MonadError (ErrorWithCause err cause) m,
 AsUnliftingError err) =>
Maybe cause
-> Opaque val rep -> m (Some (ValueOf (UniOf (Opaque val rep))))
forall err cause (m :: * -> *).
(MonadError (ErrorWithCause err cause) m, AsUnliftingError err) =>
Maybe cause
-> Opaque val rep -> m (Some (ValueOf (UniOf (Opaque val rep))))
asConstant :: Maybe cause
-> Opaque val rep -> m (Some (ValueOf (UniOf (Opaque val rep))))
$casConstant :: forall val rep err cause (m :: * -> *).
(AsConstant val, MonadError (ErrorWithCause err cause) m,
 AsUnliftingError err) =>
Maybe cause
-> Opaque val rep -> m (Some (ValueOf (UniOf (Opaque val rep))))
AsConstant, Some (ValueOf (UniOf (Opaque val rep))) -> Opaque val rep
(Some (ValueOf (UniOf (Opaque val rep))) -> Opaque val rep)
-> FromConstant (Opaque val rep)
forall term.
(Some (ValueOf (UniOf term)) -> term) -> FromConstant term
forall val rep.
FromConstant val =>
Some (ValueOf (UniOf (Opaque val rep))) -> Opaque val rep
fromConstant :: Some (ValueOf (UniOf (Opaque val rep))) -> Opaque val rep
$cfromConstant :: forall val rep.
FromConstant val =>
Some (ValueOf (UniOf (Opaque val rep))) -> Opaque val rep
FromConstant)

type instance UniOf (Opaque val rep) = UniOf val

-- | For unlifting from the 'Constant' constructor when the stored value is of a monomorphic
-- built-in type
--
-- The @rep@ parameter specifies how the type looks on the PLC side (i.e. just like with
-- @Opaque val rep@).
newtype SomeConstant uni (rep :: GHC.Type) = SomeConstant
    { SomeConstant uni rep -> Some (ValueOf uni)
unSomeConstant :: Some (ValueOf uni)
    }

{- Note [Implementation of polymorphic built-in functions]
Encoding polymorphism in an AST in an intrinsically-typed manner is not a pleasant thing to do in Haskell.
It's not impossible, see "Embedding F", Sam Lindley: http://homepages.inf.ed.ac.uk/slindley/papers/embedding-f.pdf
But we'd rather avoid such heavy techniques.

Fortunately, there is a simple trick: we have parametricity in Haskell, so a function that is
polymorphic in its argument can't inspect that argument in any way and so we never actually need to
convert such an argument from PLC to Haskell just to convert it back later without ever inspecting
the value. Instead we can keep the argument intact and apply the Haskell function directly to
the PLC AST representing some value.

E.g. Having a built-in function with the following signature:
(TODO: we can't have that, figure out a way to make this example actually work while being as
clear as it currently is)

    reverse : all a. [a] -> [a]

that maps to Haskell's

    reverse :: forall a. [a] -> [a]

evaluation of

    PLC.reverse {bool} (cons true (cons false nil))

proceeds as follows:

      PLC.reverse {bool} (cons true (cons false nil))
    ~ makeKnown (Haskell.reverse (readKnown (cons true (cons false nil))))
    ~ makeKnown (Haskell.reverse [Opaque true, Opaque false])
    ~ makeKnown [Opaque false, Opaque true]
    ~ EvaluationSuccess (cons false (cons true nil))

Note how we use the 'Opaque' wrapper in order to unlift a PLC term as an opaque Haskell value
using 'readKnown' and then lift the term back using 'makeKnown' without ever inspecting the term.

An opaque PLC @term@ whose type is a PLC type variable `a_0` has the following type on the Haskell
side:

    Opaque val (TyVarRep ('TyNameRep "a" 0))

where that last argument is a direct counterpart of the term-level

    TyVar () (TyName (Name "a" 0))

@Opaque val rep@ can be used for passing any @term@ through the builtin application machinery,
not just one whose type is a bound variable. For example, you can define a new data type

    data NatRep

provide a 'KnownTypeAst' instance for it (mapping a @Proxy NatRep@ to the actual type of natural
numbers in PLC) and define a (rather pointless) builtin like @idNat : nat -> nat@.

It's also possible to bind a type variable of a higher-kind, say, @f :: * -> *@ and make a builtin
with the following signature:

    idFInteger : all (f :: * -> *). f integer -> f integer

where the type application is handled with 'TyAppRep'. Note that the latter is defined as a
@data family@:

    data family TyAppRep (fun :: dom -> cod) (arg :: dom) :: cod

We do that because a @data family@ can return a poly-kinded argument, which allows us to get an
intrinsically-kinded representation of PLC types. For example, an opaque @term@ whose type is an
application of a type variable @f@ to a type variable @a@ is represented like this:

    Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "a" 1 :: TyNameRep *)))

Note the @TyNameRep *@ kind annotation. It tells us three things:

1. a type-level name has a kind associated with it. The reason for that is that we use names in
binders (for example, in the universal quantifier) and as variables and kinds are important in
both these cases due to us having an intrinsically-kinded representation of types, so it's
convenient to annotate type-level names with kinds. Another reason is that we do not attempt to do
any kind of static analysis on reflected type variables and associating kinds with them allows us
to catch errors like "two variables with equal names and uniques, but different kinds" earlier
2. the kind is not stored as an argument to the @TyNameRep@ constructor. Instead it's stored as
an index of the data type. The point of this is that if we stored the kind as an argument, we'd
have to provide it manually, but since the representation is intrinsically-kinded there's no point
in doing so as GHC can infer all the kinds itself
3. ... apart from cases where they're inherently ambiguous, like in the case above. If we don't
specify the kind of the @a_1@ type variable, then there's no way GHC could infer it as the variable
is passed as an argument to another variable with an unspecified kind (@f_0@)
4. finally, an opaque term can only be of a type of kind @*@. You can't construct a term whose type
is of some other kind. That's why we don't need to annotate the @f_0@ type variable: the domain is
inferred from the kind of the argument (where it's explicitly specified via @TyNameRep *@) and the
codomain is inferred from the fact that the whole type is passed to 'Opaque' and so it has to be
of kind @*@

It would be nice if we didn't need to define that @*Rep@ stuff at the type level just to demote it
to the term level via a type class, but this hasn't been investigated yet. A plausible way would be
to ditch 'KnownTypeAst' (but keep 'KnownType') and provide PLC types manually. But that doesn't seem
to give rise to a terribly nice API. And we'd lose all the static guarantees, which is not a big
deal, but losing the automatic inference of type schemes would suck, given that it's quite handy.

Representing contructors as poly-kinded data families and handling those with open type families
and/or type classes is a way of solving the expression problem for indexed data types at the type
level, if you are into these things.
-}

-- | Representation of a type variable: its name and unique and an implicit kind.
data TyNameRep (kind :: GHC.Type) = TyNameRep Symbol Nat

-- | Representation of an intrinsically-kinded type variable: a name.
data family TyVarRep (name :: TyNameRep kind) :: kind

-- | Representation of an intrinsically-kinded type application: a function and an argument.
data family TyAppRep (fun :: dom -> cod) (arg :: dom) :: cod

-- | Representation of of an intrinsically-kinded universal quantifier: a bound name and a body.
data family TyForallRep (name :: TyNameRep kind) (a :: GHC.Type) :: GHC.Type

-- Custom type errors to guide the programmer adding a new built-in function.
-- We cover a lot of cases here, but some are missing, for example we do not attempt to detect
-- higher-kinded type variables, which means that if your function returns an @m a@ we can neither
-- instantiate @m@ (which is impossible anyway: it could be 'EvaluationResult' or 'Emitter'
-- or else), nor report that higher-kinded type variables are not allowed and suggest
-- to instantiate such variables manually. In general, we do not attempt to look inside type
-- applications (as it's a rather hard thing to do) and so a type variable inside, say, a list
-- does not get instantiated, hence the custom type error does not get triggered (as it's only
-- triggered for instantiated type variables) and the user gets a standard unhelpful GHC error.

-- We don't have @Unsatisfiable@ yet (https://github.com/ghc-proposals/ghc-proposals/pull/433).
-- | To be used when there's a 'TypeError' in the context. The condition is not checked as there's
-- no way we could do that.
underTypeError :: void
underTypeError :: void
underTypeError = [Char] -> void
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: a 'TypeError' was bypassed"

type NoStandalonePolymorphicDataErrMsg =
    'Text "Plutus type variables can't directly appear inside built-in types" ':$$:
    'Text "Are you trying to define a polymorphic built-in function over a polymorphic type?" ':$$:
    'Text "In that case you need to wrap all polymorphic built-in types having type variables" ':<>:
    'Text " in them with either ‘SomeConstant’ or ‘Opaque’ depending on whether its the type" ':<>:
    'Text " of an argument or the type of the result, respectively"

instance TypeError NoStandalonePolymorphicDataErrMsg => uni `Contains` TyVarRep where
    knownUni :: uni (Esc TyVarRep)
knownUni = uni (Esc TyVarRep)
forall void. void
underTypeError

type NoConstraintsErrMsg =
    'Text "Built-in functions are not allowed to have constraints" ':$$:
    'Text "To fix this error instantiate all constrained type variables"

instance TypeError NoConstraintsErrMsg => Eq (Opaque val rep) where
    == :: Opaque val rep -> Opaque val rep -> Bool
(==) = Opaque val rep -> Opaque val rep -> Bool
forall void. void
underTypeError

instance TypeError NoConstraintsErrMsg => Ord (Opaque val rep) where
    compare :: Opaque val rep -> Opaque val rep -> Ordering
compare = Opaque val rep -> Opaque val rep -> Ordering
forall void. void
underTypeError

instance TypeError NoConstraintsErrMsg => Num (Opaque val rep) where
    + :: Opaque val rep -> Opaque val rep -> Opaque val rep
(+)         = Opaque val rep -> Opaque val rep -> Opaque val rep
forall void. void
underTypeError
    * :: Opaque val rep -> Opaque val rep -> Opaque val rep
(*)         = Opaque val rep -> Opaque val rep -> Opaque val rep
forall void. void
underTypeError
    abs :: Opaque val rep -> Opaque val rep
abs         = Opaque val rep -> Opaque val rep
forall void. void
underTypeError
    signum :: Opaque val rep -> Opaque val rep
signum      = Opaque val rep -> Opaque val rep
forall void. void
underTypeError
    fromInteger :: Integer -> Opaque val rep
fromInteger = Integer -> Opaque val rep
forall void. void
underTypeError
    negate :: Opaque val rep -> Opaque val rep
negate      = Opaque val rep -> Opaque val rep
forall void. void
underTypeError

instance TypeError NoConstraintsErrMsg => Enum (Opaque val rep) where
    toEnum :: Int -> Opaque val rep
toEnum   = Int -> Opaque val rep
forall void. void
underTypeError
    fromEnum :: Opaque val rep -> Int
fromEnum = Opaque val rep -> Int
forall void. void
underTypeError

instance TypeError NoConstraintsErrMsg => Real (Opaque val rep) where
    toRational :: Opaque val rep -> Rational
toRational = Opaque val rep -> Rational
forall void. void
underTypeError

instance TypeError NoConstraintsErrMsg => Integral (Opaque val rep) where
    quotRem :: Opaque val rep
-> Opaque val rep -> (Opaque val rep, Opaque val rep)
quotRem   = Opaque val rep
-> Opaque val rep -> (Opaque val rep, Opaque val rep)
forall void. void
underTypeError
    divMod :: Opaque val rep
-> Opaque val rep -> (Opaque val rep, Opaque val rep)
divMod    = Opaque val rep
-> Opaque val rep -> (Opaque val rep, Opaque val rep)
forall void. void
underTypeError
    toInteger :: Opaque val rep -> Integer
toInteger = Opaque val rep -> Integer
forall void. void
underTypeError

instance TypeError NoConstraintsErrMsg => Bounded (Opaque val rep) where
    minBound :: Opaque val rep
minBound = Opaque val rep
forall void. void
underTypeError
    maxBound :: Opaque val rep
maxBound = Opaque val rep
forall void. void
underTypeError

instance TypeError NoConstraintsErrMsg => Ix (Opaque val rep) where
    range :: (Opaque val rep, Opaque val rep) -> [Opaque val rep]
range   = (Opaque val rep, Opaque val rep) -> [Opaque val rep]
forall void. void
underTypeError
    index :: (Opaque val rep, Opaque val rep) -> Opaque val rep -> Int
index   = (Opaque val rep, Opaque val rep) -> Opaque val rep -> Int
forall void. void
underTypeError
    inRange :: (Opaque val rep, Opaque val rep) -> Opaque val rep -> Bool
inRange = (Opaque val rep, Opaque val rep) -> Opaque val rep -> Bool
forall void. void
underTypeError

instance TypeError NoConstraintsErrMsg => Semigroup (Opaque val rep) where
    <> :: Opaque val rep -> Opaque val rep -> Opaque val rep
(<>) = Opaque val rep -> Opaque val rep -> Opaque val rep
forall void. void
underTypeError

instance TypeError NoConstraintsErrMsg => Monoid (Opaque val rep) where
    mempty :: Opaque val rep
mempty = Opaque val rep
forall void. void
underTypeError