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

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

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

import Control.Lens (Wrapped(..))
import qualified Data.Coerce as Coerce
import Data.Constraint (Dict(..), (\\))
import Data.Vinyl.Derived (Label)
import Named (NamedF)
import Unsafe.Coerce (unsafeCoerce)

import Lorentz.Base
import Lorentz.Instr
import Lorentz.Value
import Michelson.Typed

----------------------------------------------------------------------------
-- 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 = 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_ = I Nop

gForcedCoerce_ :: MichelsonCoercible (t a) (t b) => t a : s :-> t b : s
gForcedCoerce_ = forcedCoerce_

-- | Convert between two stacks via failing.
fakeCoerce :: s1 :-> s2
fakeCoerce = unit # I FAILWITH

fakeCoercing :: (s1 :-> s2) -> s1' :-> s2'
fakeCoercing i = fakeCoerce # iForceNotFail i # fakeCoerce

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

-- | Specialized version of 'coerce_' to wrap into a haskell newtype.
coerceWrap
  :: forall newtyp inner s.
     (inner ~ Unwrapped newtyp, MichelsonCoercible newtyp (Unwrapped newtyp))
  => inner : s :-> newtyp : s
coerceWrap = forcedCoerce_

-- | Specialized version of 'coerce_' to unwrap a haskell newtype.
coerceUnwrap
  :: forall newtyp inner s.
     (inner ~ Unwrapped newtyp, MichelsonCoercible newtyp (Unwrapped newtyp))
  => newtyp : s :-> inner : s
coerceUnwrap = forcedCoerce_

-- | Lift given value to a named value.
toNamed :: Label name -> a : s :-> NamedF Identity a name : s
toNamed _ = coerceWrap

-- | Unpack named value.
fromNamed :: Label name -> NamedF Identity a name : s :-> a : s
fromNamed _ = coerceUnwrap

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

-- | Explicitly allowed coercions.
class a `CanCastTo` b where
  -- | An optional method which helps passing -Wredundant-constraints check.
  castDummy :: ()
  castDummy = ()

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

-- Incoherent instance 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
  castDummy = castDummy @a @a

instance CanCastTo a b => CanCastTo [a] [b] where
  castDummy = castDummy @a @b

instance (CanCastTo a1 a2, CanCastTo b1 b2) =>
         CanCastTo (a1, b1) (a2, b2) where
  castDummy = castDummy @a1 @a2 `seq` castDummy @b1 @b2

instance (CanCastTo i1 i2, CanCastTo o1 o2) =>
         CanCastTo (Lambda i1 o1) (Lambda i2 o2)
  -- That's magic, having default impl for 'castDummy' disables
  -- -Wredundant-constraints automatically

instance CanCastTo a b => CanCastTo (Maybe a) (Maybe 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_ = 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_ f = checkedCoerce_ @a @b # f # checkedCoerce_ @b @a

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

-- | Locally provide bidirectional 'CanCastTo' instance.
allowCheckedCoerce :: forall a b. Dict (CanCastTo a b, CanCastTo b a)
allowCheckedCoerce =
  Dict \\ allowCheckedCoerceTo @a @b \\ allowCheckedCoerceTo @b @a

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