-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

-- | Identity transformations between different Haskell types.
module Lorentz.Coercions
  ( -- * Safe coercions
    CanCastTo (..)
  , castDummyG
  , checkedCoerce
  , Castable_
  , Coercible_
  , checkedCoerce_
  , checkedCoercing_
  , allowCheckedCoerceTo
  , allowCheckedCoerce
  , coerceUnwrap
  , unsafeCoerceWrap
  , coerceWrap
  , toNamed
  , fromNamed

    -- * Unsafe coercions
  , MichelsonCoercible
  , forcedCoerce
  , forcedCoerce_
  , gForcedCoerce_
  , fakeCoerce
  , fakeCoercing

    -- * Re-exports
  , Unwrappable (..)
  , Wrappable
  ) where

import Data.Coerce qualified as Coerce
import Data.Constraint ((\\))
import GHC.Generics qualified as G
import Unsafe.Coerce (unsafeCoerce)

import Lorentz.Address
import Lorentz.Base
import Lorentz.Bytes
import Lorentz.Lambda
import Lorentz.Value
import Lorentz.Wrappable
import Lorentz.Zip
import Morley.Michelson.Typed
import Morley.Util.Named


----------------------------------------------------------------------------
-- Unsafe coercions
----------------------------------------------------------------------------

-- | Coercion for Haskell world.
--
-- We discourage using this function on Lorentz types, consider using 'Data.Coerce.coerce'
-- instead.
-- One of the reasons for that is that in Lorentz it's common to declare types as
-- newtypes consisting of existing primitives, and @forcedCoerce@ tends to ignore
-- all phantom type variables of newtypes thus violating their invariants.
forcedCoerce :: Coerce.Coercible a b => a -> b
forcedCoerce :: forall a b. Coercible a b => a -> b
forcedCoerce = a -> b
Coerce.coerce

-- | Whether two types have the same Michelson representation.
type MichelsonCoercible a b = ToT a ~ ToT b

-- | Convert between values of types that have the same representation.
--
-- This function is not safe in a sense that this allows
-- * breaking invariants of casted type
--   (example: @UStore@ from morley-upgradeable), or
-- * may stop compile on code changes
--   (example: coercion of pair to a datatype with two fields
--    will break if new field is added).
-- Still, produced Michelson code will always be valid.
--
-- Prefer using one of more specific functions from this module.
forcedCoerce_ :: MichelsonCoercible a b => a : s :-> b : s
forcedCoerce_ :: forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ = Instr (ToTs (a : s)) (ToTs (b : s)) -> (a : s) :-> (b : s)
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (a : s)) (ToTs (b : s))
forall (inp :: [T]). Instr inp inp
Nop

gForcedCoerce_ :: MichelsonCoercible (t a) (t b) => t a : s :-> t b : s
gForcedCoerce_ :: forall {k} (t :: k -> *) (a :: k) (b :: k) (s :: [*]).
MichelsonCoercible (t a) (t b) =>
(t a : s) :-> (t b : s)
gForcedCoerce_ = (t a : s) :-> (t b : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_

-- | Convert between two stacks via failing.
fakeCoerce :: s1 :-> s2
fakeCoerce :: forall (s1 :: [*]) (s2 :: [*]). s1 :-> s2
fakeCoerce = Instr (ToTs s1) (ToTs s2) -> s1 :-> s2
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs s1) ('TUnit : ToTs s1)
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT Instr (ToTs s1) ('TUnit : ToTs s1)
-> Instr ('TUnit : ToTs s1) (ToTs s2) -> Instr (ToTs s1) (ToTs s2)
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
`Seq` Instr ('TUnit : ToTs s1) (ToTs s2)
forall (a :: T) (s :: [T]) (out :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : s) out
FAILWITH)

fakeCoercing :: (s1 :-> s2) -> s1' :-> s2'
fakeCoercing :: forall (s1 :: [*]) (s2 :: [*]) (s1' :: [*]) (s2' :: [*]).
(s1 :-> s2) -> s1' :-> s2'
fakeCoercing s1 :-> s2
i = s1' :-> s1
forall (s1 :: [*]) (s2 :: [*]). s1 :-> s2
fakeCoerce (s1' :-> s1) -> (s1 :-> s2) -> s1' :-> s2
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s1 :-> s2) -> s1 :-> s2
forall (i :: [*]) (o :: [*]). (i :-> o) -> i :-> o
iForceNotFail s1 :-> s2
i (s1' :-> s2) -> (s2 :-> s2') -> s1' :-> s2'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# s2 :-> s2'
forall (s1 :: [*]) (s2 :: [*]). s1 :-> s2
fakeCoerce

----------------------------------------------------------------------------
-- Safe coercions
----------------------------------------------------------------------------

-- | Specialized version of 'forcedCoerce_' to unwrap a haskell newtype.
coerceUnwrap
  :: forall a s. Unwrappable a
  => a : s :-> Unwrappabled a : s
coerceUnwrap :: forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap = (a : s) :-> (Unwrappabled a : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_

-- | Specialized version of 'forcedCoerce_' to wrap a haskell newtype.
--
-- Works under 'Unwrappable' constraint, thus is not safe.
unsafeCoerceWrap
  :: forall a s. Unwrappable a
  => Unwrappabled a : s :-> a : s
unsafeCoerceWrap :: forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap = (Unwrappabled a : s) :-> (a : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_

-- | Specialized version of 'forcedCoerce_' to wrap into a haskell newtype.
--
-- Requires 'Wrappable' constraint.
coerceWrap
  :: forall a s. Wrappable a
  => Unwrappabled a : s :-> a : s
coerceWrap :: forall a (s :: [*]).
Wrappable a =>
(Unwrappabled a : s) :-> (a : s)
coerceWrap = (Unwrappabled a : s) :-> (a : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_

-- | Lift given value to a named value.
toNamed :: Label name -> a : s :-> (name :! a) : s
toNamed :: forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label name
_ = (a : s) :-> ((name :! a) : s)
forall a (s :: [*]).
Wrappable a =>
(Unwrappabled a : s) :-> (a : s)
coerceWrap

-- | Unpack named value.
fromNamed :: Label name -> (name :! a) : s :-> a : s
fromNamed :: forall (name :: Symbol) a (s :: [*]).
Label name -> ((name :! a) : s) :-> (a : s)
fromNamed Label name
_ = ((name :! a) : s) :-> (a : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap

-- Arbitrary coercions
----------------------------------------------------------------------------

-- | Explicitly allowed coercions.
--
-- @a `CanCastTo` b@ proclaims that @a@ can be casted to @b@ without violating
-- any invariants of @b@.
--
-- This relation is reflexive; it /may/ be symmetric or not.
-- It tends to be composable: casting complex types usually requires permission
-- to cast their respective parts; for such types consider using 'castDummyG'
-- as implementation of the method of this typeclass.
--
-- For cases when a cast from @a@ to @b@ requires some validation, consider
-- rather making a dedicated function which performs the necessary checks and
-- then calls 'forcedCoerce'.
class a `CanCastTo` b where
  -- | An optional method which helps passing -Wredundant-constraints check.
  -- Also, you can set specific implementation for it with specific sanity checks.
  castDummy :: Proxy a -> Proxy b -> ()
  castDummy Proxy a
_ Proxy b
_ = ()

-- | Coercion in Haskell world which respects 'CanCastTo'.
checkedCoerce :: forall a b. (CanCastTo a b, Coerce.Coercible a b) => a -> b
checkedCoerce :: forall a b. (CanCastTo a b, Coercible a b) => a -> b
checkedCoerce = a -> b
Coerce.coerce
  where _useCast :: Proxy a -> Proxy b -> ()
_useCast = forall a b. CanCastTo a b => Proxy a -> Proxy b -> ()
forall {k} {k} (a :: k) (b :: k).
CanCastTo a b =>
Proxy a -> Proxy b -> ()
castDummy @a @b

-- | Coercion from @a@ to @b@ is permitted and safe.
type Castable_ a b = (MichelsonCoercible a b, CanCastTo a b)

-- | Coercions between @a@ to @b@ are permitted and safe.
type Coercible_ a b = (MichelsonCoercible a b, CanCastTo a b, CanCastTo b a)

-- | Coerce between types which have an explicit permission for that in the
-- face of 'CanCastTo' constraint.
checkedCoerce_ :: forall a b s. (Castable_ a b) => a : s :-> b : s
checkedCoerce_ :: forall a b (s :: [*]). Castable_ a b => (a : s) :-> (b : s)
checkedCoerce_ = (a : s) :-> (b : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_

-- | Pretends that the top item of the stack was coerced.
checkedCoercing_
  :: forall a b s. (Coercible_ a b)
  => (b ': s :-> b ': s) -> (a ': s :-> a ': s)
checkedCoercing_ :: forall a b (s :: [*]).
Coercible_ a b =>
((b : s) :-> (b : s)) -> (a : s) :-> (a : s)
checkedCoercing_ (b : s) :-> (b : s)
f = forall a b (s :: [*]). Castable_ a b => (a : s) :-> (b : s)
checkedCoerce_ @a @b ((a : s) :-> (b : s))
-> ((b : s) :-> (b : s)) -> (a : s) :-> (b : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b : s) :-> (b : s)
f ((a : s) :-> (b : s))
-> ((b : s) :-> (a : s)) -> (a : s) :-> (a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a b (s :: [*]). Castable_ a b => (a : s) :-> (b : s)
checkedCoerce_ @b @a

-- | Locally provide given 'CanCastTo' instance.
allowCheckedCoerceTo :: forall b a. Dict (CanCastTo a b)
allowCheckedCoerceTo :: forall {k} {k} (b :: k) (a :: k). Dict (CanCastTo a b)
allowCheckedCoerceTo =
  forall a b. a -> b
unsafeCoerce
    @(Dict $ CanCastTo () ())
    @(Dict $ CanCastTo a b)
    Dict (CanCastTo () ())
forall (a :: Constraint). a => Dict a
Dict

-- | Locally provide bidirectional 'CanCastTo' instance.
allowCheckedCoerce :: forall a b. Dict (CanCastTo a b, CanCastTo b a)
allowCheckedCoerce :: forall {k} {k} (a :: k) (b :: k).
Dict (CanCastTo a b, CanCastTo b a)
allowCheckedCoerce =
  CanCastTo b a => Dict (CanCastTo a b, CanCastTo b a)
forall (a :: Constraint). a => Dict a
Dict (CanCastTo b a => Dict (CanCastTo a b, CanCastTo b a))
-> Dict (CanCastTo b a) -> Dict (CanCastTo a b, CanCastTo b a)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (b :: k) (a :: k). Dict (CanCastTo a b)
forall {k} {k} (b :: k) (a :: k). Dict (CanCastTo a b)
allowCheckedCoerceTo @a @b (CanCastTo a b => Dict (CanCastTo a b, CanCastTo b a))
-> Dict (CanCastTo a b) -> Dict (CanCastTo a b, CanCastTo b a)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (b :: k) (a :: k). Dict (CanCastTo a b)
forall {k} {k} (b :: k) (a :: k). Dict (CanCastTo a b)
allowCheckedCoerceTo @b @a

-- Incoherent instances are generally evil because arbitrary instance can be
-- picked, but in our case this is exactly what we want: permit cast if
-- /any/ instance matches.
instance {-# INCOHERENT #-} CanCastTo a a where

instance CanCastTo a b =>
         CanCastTo [a] [b]
instance CanCastTo a b =>
         CanCastTo (Maybe a) (Maybe b)
instance (CanCastTo l1 l2, CanCastTo r1 r2) =>
         CanCastTo (Either l1 r1) (Either l2 r2)
instance CanCastTo k1 k2 =>
         CanCastTo (Set k1) (Set k2)
instance (CanCastTo k1 k2, CanCastTo v1 v2) =>
         CanCastTo (Map k1 v1) (Map k2 v2)
instance (CanCastTo k1 k2, CanCastTo v1 v2) =>
         CanCastTo (BigMap k1 v1) (BigMap k2 v2)
instance ( CanCastTo (ZippedStack i1) (ZippedStack i2)
         , CanCastTo (ZippedStack o1) (ZippedStack o2)
         ) =>
         CanCastTo (i1 :-> o1) (i2 :-> o2)
instance (CanCastTo a1 a2) =>
         CanCastTo (ContractRef a1) (ContractRef a2)

instance CanCastTo (f a) (g b) => CanCastTo (NamedF f a n) (NamedF g b m)

instance (CanCastTo a1 a2, CanCastTo b1 b2) =>
         CanCastTo (a1, b1) (a2, b2)
instance (CanCastTo a1 a2, CanCastTo b1 b2, CanCastTo c1 c2) =>
         CanCastTo (a1, b1, c1) (a2, b2, c2)
instance (CanCastTo a1 a2, CanCastTo b1 b2, CanCastTo c1 c2, CanCastTo d1 d2) =>
         CanCastTo (a1, b1, c1, d1) (a2, b2, c2, d2)
instance ( CanCastTo a1 a2, CanCastTo b1 b2, CanCastTo c1 c2, CanCastTo d1 d2
         , CanCastTo e1 e2 ) =>
         CanCastTo (a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2)
instance ( CanCastTo a1 a2, CanCastTo b1 b2, CanCastTo c1 c2, CanCastTo d1 d2
         , CanCastTo e1 e2, CanCastTo f1 f2 ) =>
         CanCastTo (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2)

-- | Implementation of 'castDummy' for types composed from smaller types.
-- It helps to ensure that all necessary constraints are requested in instance
-- head.
castDummyG
  :: (Generic a, Generic b, GCanCastTo (G.Rep a) (G.Rep b))
  => Proxy a -> Proxy b -> ()
castDummyG :: forall a b.
(Generic a, Generic b, GCanCastTo (Rep a) (Rep b)) =>
Proxy a -> Proxy b -> ()
castDummyG (Proxy a
_ :: Proxy a) (Proxy b
_ :: Proxy b) = ()
  where _dummy :: Dict (Generic a, Generic b, GCanCastTo (Rep a) (Rep b))
_dummy = forall (a :: Constraint). a => Dict a
Dict @(Generic a, Generic b, GCanCastTo (G.Rep a) (G.Rep b))

type family GCanCastTo x y :: Constraint where
  GCanCastTo (G.M1 _ _ x) (G.M1 _ _ y) = GCanCastTo x y
  GCanCastTo (xl G.:+: xr) (yl G.:+: yr) = (GCanCastTo xl yl, GCanCastTo xr yr)
  GCanCastTo (xl G.:*: xr) (yl G.:*: yr) = (GCanCastTo xl yl, GCanCastTo xr yr)
  GCanCastTo G.U1 G.U1 = ()
  GCanCastTo G.V1 G.V1 = ()
  GCanCastTo (G.Rec0 a) (G.Rec0 b) = CanCastTo a b

instance (CanCastTo a1 a2, CanCastTo b1 b2)
  => CanCastTo (ZippedStackRepr a1 b1) (ZippedStackRepr a2 b2) where
  castDummy :: Proxy (ZippedStackRepr a1 b1)
-> Proxy (ZippedStackRepr a2 b2) -> ()
castDummy = Proxy (ZippedStackRepr a1 b1)
-> Proxy (ZippedStackRepr a2 b2) -> ()
forall a b.
(Generic a, Generic b, GCanCastTo (Rep a) (Rep b)) =>
Proxy a -> Proxy b -> ()
castDummyG

instance ( CanCastTo (ZippedStack inp1) (ZippedStack inp2)
         , CanCastTo (ZippedStack out1) (ZippedStack out2) )
  => WrappedLambda inp1 out1 `CanCastTo` WrappedLambda inp2 out2 where
  castDummy :: Proxy (WrappedLambda inp1 out1)
-> Proxy (WrappedLambda inp2 out2) -> ()
castDummy = Proxy (WrappedLambda inp1 out1)
-> Proxy (WrappedLambda inp2 out2) -> ()
forall a b.
(Generic a, Generic b, GCanCastTo (Rep a) (Rep b)) =>
Proxy a -> Proxy b -> ()
castDummyG

{- Note about potential use of 'Coercible'.

Alternative to 'CanCastTo' would be using 'Coercible' constraint.

Pros:
* Reflexivity, symmetry and transitivity properties hold automatically.
* Complex structures are handled automatically.

Cons:
* When declaring a datatype type, one should always care to set the corresponding
type role (in most cases it will nominal or representational). Newtypes are
even more difficult to control as they are always coercible if constructor is
in scope.
* Where are some cases where going with 'Coercible' does not work, e.g.
allow @MigrationScriptFrom oldStore@ to @MigrationScript oldStore newStore@.

Despite the mentioned cons, described 'coerce_' may be useful someday.

-}

----------------------------------------------------------------------------
-- Coercions for some basic types
----------------------------------------------------------------------------

instance TAddress p vd `CanCastTo` Address
instance Address `CanCastTo` TAddress p vd

instance FutureContract p `CanCastTo` EpAddress

instance Packed a `CanCastTo` ByteString
instance TSignature a `CanCastTo` ByteString
instance Hash alg a `CanCastTo` ByteString

instance CanCastTo a b => Packed a `CanCastTo` Packed b
instance CanCastTo a b => TSignature a `CanCastTo` TSignature b
instance (CanCastTo alg1 alg2, CanCastTo a1 a2) =>
         Hash alg1 a1 `CanCastTo` Hash alg2 a2