-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

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

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

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

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

import Lorentz.Address
import Lorentz.Base
import Lorentz.Instr
import Lorentz.Value
import Lorentz.Zip
import Michelson.Typed
import Lorentz.Wrappable (Wrappable(..))
----------------------------------------------------------------------------
-- Unsafe coercions
----------------------------------------------------------------------------

-- | Coercion for Haskell world.
--
-- We discourage using this function on Lorentz types, consider using 'coerce'
-- instead.
-- One of the reasons forthat 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 :: a -> b
forcedCoerce = a -> b
forall a b. Coercible a b => 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@) 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_ :: (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_ :: (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 :: s1 :-> s2
fakeCoerce = s1 :-> (() & s1)
forall (s :: [*]). s :-> (() & s)
unit (s1 :-> (() & s1)) -> ((() & s1) :-> s2) -> s1 :-> s2
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Instr (ToTs (() & s1)) (ToTs s2) -> (() & s1) :-> s2
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs (() & s1)) (ToTs s2)
forall (a :: T) (s :: [T]) (out :: [T]).
KnownT a =>
Instr (a : s) out
FAILWITH

fakeCoercing :: (s1 :-> s2) -> s1' :-> s2'
fakeCoercing :: (s1 :-> s2) -> s1' :-> s2'
fakeCoercing i :: 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 'coerce_' to wrap into a haskell newtype.
coerceWrap
  :: forall a s. Wrappable a
  => Unwrappable a : s :-> a : s
coerceWrap :: (Unwrappable a : s) :-> (a : s)
coerceWrap = (Unwrappable a : s) :-> (a : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a & s) :-> (b & s)
forcedCoerce_

-- | Specialized version of 'coerce_' to unwrap a haskell newtype.
coerceUnwrap
  :: forall a s. Wrappable a
  => a : s :-> Unwrappable a : s
coerceUnwrap :: (a : s) :-> (Unwrappable a : s)
coerceUnwrap = (a : s) :-> (Unwrappable 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 :-> NamedF Identity a name : s
toNamed :: Label name -> (a : s) :-> (NamedF Identity a name : s)
toNamed _ = (a : s) :-> (NamedF Identity a name : s)
forall a (s :: [*]). Wrappable a => (Unwrappable a : s) :-> (a : s)
coerceWrap

-- | Unpack named value.
fromNamed :: Label name -> NamedF Identity a name : s :-> a : s
fromNamed :: Label name -> (NamedF Identity a name : s) :-> (a : s)
fromNamed _ = (NamedF Identity a name : s) :-> (a : s)
forall a (s :: [*]). Wrappable a => (a : s) :-> (Unwrappable 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 _ _ = ()

-- | Coercion in Haskell world which respects 'CanCastTo'.
checkedCoerce :: forall a b. (CanCastTo a b, Coerce.Coercible a b) => a -> b
checkedCoerce :: a -> b
checkedCoerce = a -> b
forall a b. Coercible a b => a -> b
Coerce.coerce
  where _useCast :: Proxy a -> Proxy b -> ()
_useCast = 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_ :: (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_ :: ((b : s) :-> (b : s)) -> (a : s) :-> (a : s)
checkedCoercing_ f :: (b : s) :-> (b : s)
f = forall (s :: [*]). Castable_ a b => (a : s) :-> (b : s)
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 (s :: [*]). Castable_ b a => (b : s) :-> (a : s)
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 :: Dict (CanCastTo a b)
allowCheckedCoerceTo =
  (Dict $ CanCastTo () ()) -> Dict (CanCastTo a b)
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 :: 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
\\ Dict (CanCastTo b a)
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
\\ 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 a b, f ~ g) => 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 :: 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 = (Generic a, Generic b, GCanCastTo (Rep a) (Rep b)) =>
Dict (Generic a, Generic b, GCanCastTo (Rep a) (Rep b))
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

{- 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 `CanCastTo` Address
instance Address `CanCastTo` TAddress p

instance FutureContract p `CanCastTo` EpAddress