Coercions.hs 8.84 KB
Newer Older
Kirill Elagin's avatar
Kirill Elagin committed
1 2 3 4
-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

5 6
-- | Identity transformations between different Haskell types.
module Lorentz.Coercions
7 8
  ( -- * Safe coercions
    CanCastTo (..)
9
  , castDummyG
10 11 12 13 14 15
  , checkedCoerce
  , Coercible_
  , checkedCoerce_
  , checkedCoercing_
  , allowCheckedCoerceTo
  , allowCheckedCoerce
16 17 18 19
  , coerceUnwrap
  , coerceWrap
  , toNamed
  , fromNamed
20

21 22 23 24 25 26
    -- * Unsafe coercions
  , MichelsonCoercible
  , forcedCoerce
  , forcedCoerce_
  , gForcedCoerce_
  , fakeCoerce
27
  , fakeCoercing
28

29
    -- * Re-exports
30
  , Wrappable (..)
31 32
  ) where

33
import qualified Data.Coerce as Coerce
34
import Data.Constraint ((\\))
35
import qualified GHC.Generics as G
36
import Named (NamedF)
37
import Unsafe.Coerce (unsafeCoerce)
38

39
import Lorentz.Address
40
import Lorentz.Base
41
import Lorentz.Instr
42
import Lorentz.Value
43
import Lorentz.Zip
44
import Michelson.Typed
45
import Lorentz.Wrappable (Wrappable(..))
46 47 48 49 50 51 52 53 54 55 56 57 58 59
----------------------------------------------------------------------------
-- 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 @[email protected] tends to ignore
-- all phantom type variables of newtypes thus violating their invariants.
forcedCoerce :: Coerce.Coercible a b => a -> b
forcedCoerce = Coerce.coerce

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

-- | Convert between values of types that have the same representation.
64 65 66 67 68 69 70 71 72 73 74 75 76
--
-- This function is not safe in a sense that this allows breaking invariants of
-- casted type (example: @[email protected]) 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_
77

78 79
-- | Convert between two stacks via failing.
fakeCoerce :: s1 :-> s2
Konstantin Ivanov's avatar
Konstantin Ivanov committed
80
fakeCoerce = unit # I FAILWITH
81

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

85 86 87 88
----------------------------------------------------------------------------
-- Safe coercions
----------------------------------------------------------------------------

89 90
-- | Specialized version of 'coerce_' to wrap into a haskell newtype.
coerceWrap
91 92
  :: forall a s. Wrappable a
  => Unwrappable a : s :-> a : s
93
coerceWrap = forcedCoerce_
94 95 96

-- | Specialized version of 'coerce_' to unwrap a haskell newtype.
coerceUnwrap
97 98
  :: forall a s. Wrappable a
  => a : s :-> Unwrappable a : s
99
coerceUnwrap = forcedCoerce_
100 101 102 103 104 105 106 107

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

109 110 111 112
-- Arbitrary coercions
----------------------------------------------------------------------------

-- | Explicitly allowed coercions.
113 114 115 116 117 118 119 120 121 122 123 124
--
-- @a `CanCastTo` [email protected] proclaims that @[email protected] can be casted to @[email protected] without violating
-- any invariants of @[email protected]
--
-- 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 @[email protected] to @[email protected] requires some validation, consider
-- rather making a dedicated function which performs the necessary checks and
-- then calls @[email protected]
125 126
class a `CanCastTo` b where
  -- | An optional method which helps passing -Wredundant-constraints check.
127 128 129
  -- Also, you can set specific implementation for it with specific sanity checks.
  castDummy :: Proxy a -> Proxy b -> ()
  castDummy _ _ = ()
130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165

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

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

-- | Coercions between @[email protected] to @[email protected] 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

166 167 168
-- 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.
169
instance {-# INCOHERENT #-} CanCastTo a a where
170 171 172 173 174 175 176 177 178 179 180 181 182

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)
183 184 185 186
instance ( CanCastTo (ZippedStack i1) (ZippedStack i2)
         , CanCastTo (ZippedStack o1) (ZippedStack o2)
         ) =>
         CanCastTo (i1 :-> o1) (i2 :-> o2)
187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
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)

205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221
-- | 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) = ()
  where _dummy = 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

222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241
{- 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 [email protected] to @MigrationScript oldStore [email protected]

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

-}

242 243 244 245
----------------------------------------------------------------------------
-- Coercions for some basic types
----------------------------------------------------------------------------

246 247 248
instance TAddress p `CanCastTo` Address
instance Address `CanCastTo` TAddress p

249
instance FutureContract p `CanCastTo` EpAddress