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 @forcedCoerce@ 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: @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_
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` 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@.
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 @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

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 oldStore@ to @MigrationScript oldStore newStore@.

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