content: -- editorconfig-checker-disable-file
  -- GHC doesn't like the definition of 'TrySpecializeAsVar'.
  {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
  
  {-# LANGUAGE ConstraintKinds          #-}
  {-# LANGUAGE DataKinds                #-}
  {-# LANGUAGE FlexibleInstances        #-}
  {-# LANGUAGE FunctionalDependencies   #-}
  {-# LANGUAGE PolyKinds                #-}
  {-# LANGUAGE StandaloneKindSignatures #-}
  {-# LANGUAGE TypeApplications         #-}
  {-# LANGUAGE TypeFamilies             #-}
  {-# LANGUAGE TypeOperators            #-}
  {-# LANGUAGE UndecidableInstances     #-}
  
  module PlutusCore.Builtin.Elaborate
    ( ElaborateFromTo
    ) where
  
  import PlutusCore.Builtin.KnownTypeAst
  import PlutusCore.Builtin.Polymorphism
  import PlutusCore.Core.Type
  
  import Data.Kind qualified as GHC
  import Data.Type.Bool
  import Data.Type.Equality
  import GHC.TypeLits
  
  -- | Check if two values of different kinds are in fact the same value (with the same kind).
  -- A heterogeneous version of @Type.Equality.(==)@.
  type (===) :: forall a b. a -> b -> Bool
  type family x === y where
      x === x = 'True
      x === y = 'False
  
  -- Explained in detail in https://github.com/effectfully-ou/sketches/tree/cbf3ee9d11e0e3d4fc397ce7bf419418224122e2/poly-type-of-saga/part1-try-unify
  -- | Unify two values if possible, otherwise leave them alone. Useful for instantiating type
  -- variables.
  type TryUnify :: forall a b. Bool -> a -> b -> GHC.Constraint
  class same ~ (x === y) => TryUnify same x y
  instance (x === y) ~ 'False => TryUnify 'False x y
  instance {-# INCOHERENT #-} (x ~~ y, same ~ 'True) => TryUnify same x y
  
  -- | Unify two values unless they're obviously distinct (in which case do nothing).
  -- Allows us to detect and specialize type variables, since a type variable is not obviously
  -- distinct from anything else and so the INCOHERENT instance of 'TryUnify' gets triggered and the
  -- variable gets unified with whatever we want it to.
  type (~?~) :: forall a b. a -> b -> GHC.Constraint
  type x ~?~ y = TryUnify (x === y) x y
  
  -- | Get the element at an @i@th position in a list.
  type Lookup :: forall a. Nat -> [a] -> a
  type family Lookup n xs where
      Lookup _ '[]       = TypeError ('Text "Not enough elements")
      Lookup 0 (x ': xs) = x
      Lookup n (_ ': xs) = Lookup (n - 1) xs
  
  -- | Get the name at the @i@th position in the list of default names. We could use @a_0@, @a_1@,
  -- @a_2@ etc instead, but @a@, @b@, @c@ etc are nicer.
  type GetName :: GHC.Type -> Nat -> Symbol
  type family GetName k i where
      GetName GHC.Type i = Lookup i '["a", "b", "c", "d", "e", "i", "j", "k", "l"]
      GetName _        i = Lookup i '["f", "g", "h", "m", "n"]  -- For higher-kinded types.
  
  -- | Apply the function stored in the provided 'Maybe' if there's one.
  type MaybeApply :: forall k. Maybe (k -> k) -> k -> k
  type family MaybeApply mayVal x where
      MaybeApply 'Nothing  a = a
      MaybeApply ('Just f) a = f a
  
  -- | Try to specialize @a@ as a type representing a PLC type variable.
  -- @i@ is a fresh id and @j@ is a final one (either @i + 1@ or @i@ depending on whether
  -- specialization attempt is successful or not).
  -- @mw@ is for wrapping 'TyVarRep', if there's a wrapper inside (see 'HandleHole' for how it's
  -- used).
  type TrySpecializeAsVar :: forall k. Nat -> Nat -> Maybe (k -> k) -> k -> GHC.Constraint
  class TrySpecializeAsVar i j mw a | i mw a -> j
  instance
      ( var ~ MaybeApply mw (TyVarRep @k ('TyNameRep (GetName k i) i))
      -- Try to unify @a@ with a freshly created @var@.
      , a ~?~ var
      -- If @a@ is equal to @var@ then unification was successful and we just used the fresh id and
      -- so we need to bump it up. Otherwise @var@ was discarded and so the fresh id is still fresh.
      -- Replacing @(===)@ with @(==)@ causes errors at use site, for whatever reason.
      , j ~ If (a === var) (i + 1) i
      ) => TrySpecializeAsVar i j mw (a :: k)
  
  type NoAppliedVarsHeader =
      'Text "A built-in function is not allowed to have applied type variables in its type"
  
  -- See Note [Rep vs Type context].
  -- | Throw an error telling the user not to apply type variables to anything.
  type ThrowNoAppliedVars :: (GHC.Type -> GHC.Type) -> GHC.Constraint
  type family ThrowNoAppliedVars hole where
      -- In the Rep context higher-kinded type variables are allowed, but need to be applied via
      -- 'TyAppRep', hence the error message.
      ThrowNoAppliedVars RepHole = TypeError
          ( NoAppliedVarsHeader
          ':$$: 'Text "To fix this error apply type variables via explicit ‘TyAppRep’"
          )
      -- In the Type context no higher-kinded type variables are allowed.
      ThrowNoAppliedVars TypeHole = TypeError
          ( NoAppliedVarsHeader
          ':$$: 'Text "To fix this error specialize all higher-kinded type variables"
          )
      -- In case we add more contexts.
      ThrowNoAppliedVars _ = TypeError
          ( NoAppliedVarsHeader
          ':$$: 'Text "Internal error: the context is not recognized. Please report"
          )
  
  -- | Check that the higher-kinded type does not represent a PLC type variable and if it does.
  type CheckNotAppliedVar :: forall k. (GHC.Type -> GHC.Type) -> k -> GHC.Constraint
  type family CheckNotAppliedVar hole a where
      CheckNotAppliedVar hole (TyVarRep _) = ThrowNoAppliedVars hole
      CheckNotAppliedVar _    _            = ()
  
  -- | Try to specialize the head of a (possibly nullary) type application to a type representing a
  -- PLC variable and throw if that succeeds or if it already was one.
  type TrySpecializeHeadAsVar
      :: forall a b. Nat -> Nat -> (GHC.Type -> GHC.Type) -> (a -> b) -> GHC.Constraint
  class TrySpecializeHeadAsVar i j hole f | i f -> j
  -- | Recurse to reach the head.
  instance {-# OVERLAPPABLE #-}
      TrySpecializeHeadAsVar i j hole f => TrySpecializeHeadAsVar i j hole (f x)
  -- | Reached the head, it's a 'TyVarRep', throwing. Mostly to ensure that a 'TyVarRep' doesn't slip
  -- in via user input, but also out of pure paranoia (GHC seems to occasionally solve constraints
  -- for the same type multiple times by racing through different routes in the presence of
  -- @INCOHERENT@ pragmas, but this is not confirmed. It wouldn't be unreasonable, though).
  instance {-# OVERLAPPING #-}
      (ThrowNoAppliedVars hole, i ~ j) => TrySpecializeHeadAsVar i j hole (TyVarRep name)
  -- | Reached the head, try to specialize it as a variable and throw if that succeeds.
  instance {-# INCOHERENT #-}
      ( TrySpecializeAsVar i j 'Nothing f
      , CheckNotAppliedVar hole f
      ) => TrySpecializeHeadAsVar i j hole f
  
  {- | Try to specialize @a@ as a type representing a PLC type variable.
  Same as 'TrySpecializeAsVar' (in particular, the parameters are the same), except this one also
  checks if the given type is a type application, in which case it tries to specialize the head of the
  application to a type representing a PLC type variable and throws if that succeeds.
  
  We need this because blindly specializing an @f A@ (where @f@ is a type variable and @A@ is an
  arbitrary type) in the Type context would give us @Opaque val A@ (by @f ~ Opaque val@) instead of
  @Opaque val (f' A)@, which would be very confusing to the user: the only reasonable way to elaborate
  an application of a type variable in Haskell is to make an application of a type variable in PLC,
  not to randomly drop the type variable.
  
  There's no way we could elaborate an applied type variable without surprising the user, because no
  instantiation of @f@ could turn @f A@ into @Opaque val (f' A)@, hence we simply forbid applied type
  variables and throw upon encountering one. It would be a pain to handle an iterated application of a
  type representing a PLC type variable anyway.
  
  It's not possible to determine if @Opaque val A@ is a specialization of @f a@ or @a@ (for a type
  variable @a@), hence we have to make this whole check during elaboration and not any later.
  
  Regardless of whether the given argument is a type application or not, it's attempted to be
  specialized as a type representing a PLC type variable, because such a type is a type application
  itself. Unifying an already known type variable with a fresh one is useful when the name part
  of the former is unknown.
  -}
  type TrySpecializeAsUnappliedVar
      :: forall k. Nat -> Nat -> (GHC.Type -> GHC.Type) -> Maybe (k -> k) -> k -> GHC.Constraint
  class TrySpecializeAsUnappliedVar i j hole mw a | i mw a -> j
  instance
      ( TrySpecializeHeadAsVar i j hole f
      , TrySpecializeAsVar j k mw (f x)
      ) => TrySpecializeAsUnappliedVar i k hole mw (f x)
  instance {-# INCOHERENT #-} TrySpecializeAsVar i j mw a => TrySpecializeAsUnappliedVar i j hole mw a
  
  -- See Note [Rep vs Type context]
  -- | First try to specialize the hole using 'TrySpecializeAsVar' and then recurse on the result of
  -- that using 'HandleHoles'.
  -- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since 'HandleHole' can
  -- specialize multiple variables, @j@ can be equal to @i + n@ for any @n@ (including @0@).
  type HandleHole :: (GHC.Type -> GHC.Type) -> Nat -> Nat -> GHC.Type -> Hole -> GHC.Constraint
  class HandleHole uni i j val hole | uni i val hole -> j
  -- In the Rep context @x@ is attempted to be specialized as a 'TyVarRep'.
  instance
      ( TrySpecializeAsUnappliedVar i j RepHole 'Nothing x
      , HandleHoles uni j k val RepHole x
      ) => HandleHole uni i k val (RepHole x)
  -- In the Type context @a@ is attempted to be specialized as a 'TyVarRep' wrapped in @Opaque val@.
  instance
      ( TrySpecializeAsUnappliedVar i j TypeHole ('Just (Opaque val)) a
      , HandleHoles uni j k val TypeHole a
      ) => HandleHole uni i k val (TypeHole a)
  
  -- | Call 'HandleHole' over each hole from the list, threading the state (the fresh unique) through
  -- the calls.
  type HandleHolesGo :: (GHC.Type -> GHC.Type) -> Nat -> Nat -> GHC.Type -> [Hole] -> GHC.Constraint
  class HandleHolesGo uni i j val holes | uni i val holes -> j
  instance i ~ j => HandleHolesGo uni i j val '[]
  instance
      ( HandleHole uni i j val hole
      , HandleHolesGo uni j k val holes
      ) => HandleHolesGo uni i k val (hole ': holes)
  
  -- | If the outermost constructor of the second argument is known and happens to be one of the
  -- constructors of the list data type, then the second argument is returned back. Otherwise the
  -- first one is returned, which is meant to be a custom type error.
  type ThrowOnStuckList :: forall a. [a] -> [a] -> [a]
  type family ThrowOnStuckList err xs where
      ThrowOnStuckList _   '[]       = '[]
      ThrowOnStuckList _   (x ': xs) = x ': xs
      ThrowOnStuckList err _         = err
  
  type UnknownTypeError :: forall a any. GHC.Type -> a -> any
  type family UnknownTypeError val x where
      UnknownTypeError val x = TypeError
          (         'Text "No instance for ‘KnownTypeAst "
              ':<>: 'ShowType (UniOf val)
              ':<>: 'Text " ("
              ':<>: 'ShowType x
              ':<>: 'Text ")’"
          ':$$: 'Text "Which means"
          ':$$: 'Text "  ‘" ':<>: 'ShowType x ':<>: 'Text "’"
          ':$$: 'Text "is neither a built-in type, nor one of the control types."
          ':$$: 'Text "If it can be represented in terms of one of the built-in types"
          ':$$: 'Text "  then go add the instance (you may need a few others too)"
          ':$$: 'Text "  alongside the instance for the built-in type."
          ':$$: 'Text "Otherwise you may need to add a new built-in type"
          ':$$: 'Text "  (provided you're doing something that can be supported in principle)"
          )
  
  -- | Get the holes of @x@ and recurse into them.
  type HandleHoles
      :: forall a. (GHC.Type -> GHC.Type) -> Nat -> Nat -> GHC.Type -> (GHC.Type -> GHC.Type) -> a -> GHC.Constraint
  type HandleHoles uni i j val hole x =
      -- Here we detect a stuck application of 'ToHoles' and throw 'UnknownTypeError' on it.
      -- See https://blog.csongor.co.uk/report-stuck-families for a detailed description of how
      -- detection of stuck type families works.
      HandleHolesGo uni i j val (ThrowOnStuckList (UnknownTypeError val x) (ToHoles uni hole x))
  
  -- Check out the following for a detailed explanation of the idea (after learning about 'TryUnify'):
  -- https://github.com/effectfully-ou/sketches/tree/cbf3ee9d11e0e3d4fc397ce7bf419418224122e2/poly-type-of-saga/part2-enumerate-type-vars
  -- | Specialize each Haskell type variable in @a@ as a type representing a PLC type variable.
  -- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since 'HandleHole' can
  -- specialize multiple variables, @j@ can be equal to @i + n@ for any @n@ (including @0@).
  type ElaborateFromTo
      :: (GHC.Type -> GHC.Type) -> Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint
  type ElaborateFromTo uni i j val a = HandleHole uni i j val (TypeHole a)
  