{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE FlexibleContexts #-}
module Codec.Candid.Coerce
  ( coerceSeqDesc
  , SeqCoercion
  , coerce
  , Coercion
  )
  where

import Data.Text.Prettyprint.Doc
import qualified Data.Vector as V
import qualified Data.ByteString.Lazy as BS
import qualified Data.Map as M
import Data.Bifunctor
import Data.List
import Data.Tuple
import Control.Monad.State.Lazy
import Control.Monad.Except

import Codec.Candid.FieldName
import Codec.Candid.Types
import Codec.Candid.TypTable

type SeqCoercion = [Value] -> Either String [Value]
type Coercion = Value -> Either String Value

coerceSeqDesc :: SeqDesc -> SeqDesc -> Either String SeqCoercion
coerceSeqDesc :: SeqDesc -> SeqDesc -> Either String SeqCoercion
coerceSeqDesc SeqDesc
sd1 SeqDesc
sd2 =
    SeqDesc
-> (forall k.
    (Pretty k, Ord k) =>
    [Type (Ref k Type)] -> Either String SeqCoercion)
-> Either String SeqCoercion
forall r.
SeqDesc
-> (forall k. (Pretty k, Ord k) => [Type (Ref k Type)] -> r) -> r
unrollTypeTable SeqDesc
sd1 ((forall k.
  (Pretty k, Ord k) =>
  [Type (Ref k Type)] -> Either String SeqCoercion)
 -> Either String SeqCoercion)
-> (forall k.
    (Pretty k, Ord k) =>
    [Type (Ref k Type)] -> Either String SeqCoercion)
-> Either String SeqCoercion
forall a b. (a -> b) -> a -> b
$ \[Type (Ref k Type)]
ts1 ->
    SeqDesc
-> (forall k.
    (Pretty k, Ord k) =>
    [Type (Ref k Type)] -> Either String SeqCoercion)
-> Either String SeqCoercion
forall r.
SeqDesc
-> (forall k. (Pretty k, Ord k) => [Type (Ref k Type)] -> r) -> r
unrollTypeTable SeqDesc
sd2 ((forall k.
  (Pretty k, Ord k) =>
  [Type (Ref k Type)] -> Either String SeqCoercion)
 -> Either String SeqCoercion)
-> (forall k.
    (Pretty k, Ord k) =>
    [Type (Ref k Type)] -> Either String SeqCoercion)
-> Either String SeqCoercion
forall a b. (a -> b) -> a -> b
$ \[Type (Ref k Type)]
ts2 ->
    [Type (Ref k Type)]
-> [Type (Ref k Type)] -> Either String SeqCoercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)]
-> [Type (Ref k2 Type)] -> Either String SeqCoercion
coerceSeq [Type (Ref k Type)]
ts1 [Type (Ref k Type)]
ts2

coerceSeq ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    [Type (Ref k1 Type)] ->
    [Type (Ref k2 Type)] ->
    Either String SeqCoercion
coerceSeq :: [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)] -> Either String SeqCoercion
coerceSeq [Type (Ref k1 Type)]
t1 [Type (Ref k2 Type)]
t2 = M k1 k2 SeqCoercion -> Either String SeqCoercion
forall k1 k2 a. (Ord k1, Ord k2) => M k1 k2 a -> Either String a
runM (M k1 k2 SeqCoercion -> Either String SeqCoercion)
-> M k1 k2 SeqCoercion -> Either String SeqCoercion
forall a b. (a -> b) -> a -> b
$ [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
t1 [Type (Ref k2 Type)]
t2

-- | This function implements the `C[<t> <: <t>]` coercion function from the
-- spec. It returns `Left` if no subtyping relation holds, or `Right c` if it
-- holds, together with a coercion function.
--
-- The coercion function itself is not total because the intput value isn’t
-- typed, so we have to cater for errors there. It should not fail if the
-- passed value really is inherently of the input type.
--
-- In a dependently typed language we’d maybe have something like
-- `coerce :: foreach t1 -> foreach t2 -> Either String (t1 -> t2)`
-- instead, and thus return a total function
coerce ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    Type (Ref k1 Type) ->
    Type (Ref k2 Type) ->
    Either String Coercion
coerce :: Type (Ref k1 Type) -> Type (Ref k2 Type) -> Either String Coercion
coerce Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = M k1 k2 Coercion -> Either String Coercion
forall k1 k2 a. (Ord k1, Ord k2) => M k1 k2 a -> Either String a
runM (M k1 k2 Coercion -> Either String Coercion)
-> M k1 k2 Coercion -> Either String Coercion
forall a b. (a -> b) -> a -> b
$ Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2

type Memo k1 k2 =
    (M.Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
     M.Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion)
type M k1 k2 = ExceptT String (State (Memo k1 k2))

runM :: (Ord k1, Ord k2) => M k1 k2 a -> Either String a
runM :: M k1 k2 a -> Either String a
runM M k1 k2 a
act = State (Memo k1 k2) (Either String a)
-> Memo k1 k2 -> Either String a
forall s a. State s a -> s -> a
evalState (M k1 k2 a -> State (Memo k1 k2) (Either String a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT M k1 k2 a
act) (Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion
forall a. Monoid a => a
mempty, Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion
forall a. Monoid a => a
mempty)

flipM :: M k1 k2 a -> M k2 k1 a
flipM :: M k1 k2 a -> M k2 k1 a
flipM (ExceptT (StateT Memo k1 k2 -> Identity (Either String a, Memo k1 k2)
f)) = StateT
  (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
   Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)
  Identity
  (Either String a)
-> M k2 k1 a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (((Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
  Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)
 -> Identity
      (Either String a,
       (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
        Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)))
-> StateT
     (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
      Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)
     Identity
     (Either String a)
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
 Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)
-> Identity
     (Either String a,
      (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
       Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion))
f')
  where
    f' :: (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
 Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)
-> Identity
     (Either String a,
      (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
       Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion))
f' (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion
m1,Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion
m2) = (Memo k1 k2
 -> (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
     Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion))
-> (Either String a, Memo k1 k2)
-> (Either String a,
    (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
     Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion))
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Memo k1 k2
-> (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
    Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)
forall a b. (a, b) -> (b, a)
swap ((Either String a, Memo k1 k2)
 -> (Either String a,
     (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
      Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)))
-> Identity (Either String a, Memo k1 k2)
-> Identity
     (Either String a,
      (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
       Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Memo k1 k2 -> Identity (Either String a, Memo k1 k2)
f (Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion
m2,Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion
m1) -- f (m2,m1) >>= \case (r, (m2',m1')) -> pure (r, (m1', m2'))

memo, go ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    Type (Ref k1 Type) ->
    Type (Ref k2 Type) ->
    M k1 k2 Coercion

goSeq ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    [Type (Ref k1 Type)] ->
    [Type (Ref k2 Type)] ->
    M k1 k2 SeqCoercion


-- Memoization uses lazyiness: When we see a pair for the first time,
-- we optimistically put the resulting coercion into the map.
-- Either the following recursive call will fail (but then this optimistic
-- value was never used), or it will succeed, but then the guess was correct.
memo :: Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = do
  ((Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
  Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion)
 -> Maybe Coercion)
-> ExceptT
     String
     (State
        (Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
         Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion))
     (Maybe Coercion)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((Type (Ref k1 Type), Type (Ref k2 Type))
-> Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion
-> Maybe Coercion
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Type (Ref k1 Type)
t1,Type (Ref k2 Type)
t2) (Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion
 -> Maybe Coercion)
-> ((Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
     Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion)
    -> Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)
-> (Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
    Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion)
-> Maybe Coercion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
 Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion)
-> Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion
forall a b. (a, b) -> a
fst) ExceptT
  String
  (State
     (Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
      Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion))
  (Maybe Coercion)
-> (Maybe Coercion -> M k1 k2 Coercion) -> M k1 k2 Coercion
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Coercion
c -> Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
c
    Maybe Coercion
Nothing -> mdo
        ((Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
  Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion)
 -> (Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
     Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion))
-> ExceptT
     String
     (State
        (Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
         Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion
 -> Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)
-> (Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
    Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion)
-> (Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
    Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Type (Ref k1 Type), Type (Ref k2 Type))
-> Coercion
-> Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion
-> Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Type (Ref k1 Type)
t1,Type (Ref k2 Type)
t2) Coercion
c))
        Coercion
c <- Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
go Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
        Coercion -> M k1 k2 Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
c

-- Look through refs
go :: Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
go (RefT (Ref k1
_ Type (Ref k1 Type)
t1)) Type (Ref k2 Type)
t2 = Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
go Type (Ref k1 Type)
t1 (RefT (Ref k2
_ Type (Ref k2 Type)
t2)) = Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2

-- Identity coercion for primitive values
go Type (Ref k1 Type)
NatT Type (Ref k2 Type)
NatT = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Nat8T Type (Ref k2 Type)
Nat8T = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Nat16T Type (Ref k2 Type)
Nat16T = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Nat32T Type (Ref k2 Type)
Nat32T = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Nat64T Type (Ref k2 Type)
Nat64T = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
IntT Type (Ref k2 Type)
IntT = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Int8T Type (Ref k2 Type)
Int8T = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Int16T Type (Ref k2 Type)
Int16T = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Int32T Type (Ref k2 Type)
Int32T = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Int64T Type (Ref k2 Type)
Int64T = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Float32T Type (Ref k2 Type)
Float32T = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Float64T Type (Ref k2 Type)
Float64T = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
BoolT Type (Ref k2 Type)
BoolT = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
TextT Type (Ref k2 Type)
TextT = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
NullT Type (Ref k2 Type)
NullT = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
PrincipalT Type (Ref k2 Type)
PrincipalT = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- Nat <: Int
go Type (Ref k1 Type)
NatT Type (Ref k2 Type)
IntT = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Coercion -> M k1 k2 Coercion) -> Coercion -> M k1 k2 Coercion
forall a b. (a -> b) -> a -> b
$ \case
    NatV Natural
n -> Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Integer -> Value
IntV (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n)
    Value
v -> String -> Either String Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String Value) -> String -> Either String Value
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing nat <: int"

-- t <: reserved
go Type (Ref k1 Type)
_ Type (Ref k2 Type)
ReservedT = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String Value -> Coercion
forall a b. a -> b -> a
const (Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
ReservedV))

-- empty <: t
go Type (Ref k1 Type)
EmptyT Type (Ref k2 Type)
_ = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Coercion -> M k1 k2 Coercion) -> Coercion -> M k1 k2 Coercion
forall a b. (a -> b) -> a -> b
$ \Value
v ->
    String -> Either String Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String Value) -> String -> Either String Value
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing empty"

-- vec t1 <: vec t2
go (VecT Type (Ref k1 Type)
t1) (VecT Type (Ref k2 Type)
t2) = do
    Coercion
c <- Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
    Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Coercion -> M k1 k2 Coercion) -> Coercion -> M k1 k2 Coercion
forall a b. (a -> b) -> a -> b
$ \case
        VecV Vector Value
vs -> Vector Value -> Value
VecV (Vector Value -> Value)
-> Either String (Vector Value) -> Either String Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Vector Value -> Either String (Vector Value)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Coercion
c Vector Value
vs
        Value
v -> String -> Either String Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String Value) -> String -> Either String Value
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing vector"

-- Option: The normal rule
go (OptT Type (Ref k1 Type)
t1) (OptT Type (Ref k2 Type)
t2) = State (Memo k1 k2) (Either String Coercion)
-> ExceptT String (State (Memo k1 k2)) (Either String Coercion)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (M k1 k2 Coercion -> State (Memo k1 k2) (Either String Coercion)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2)) ExceptT String (State (Memo k1 k2)) (Either String Coercion)
-> (Either String Coercion -> M k1 k2 Coercion) -> M k1 k2 Coercion
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Right Coercion
c -> Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Coercion -> M k1 k2 Coercion) -> Coercion -> M k1 k2 Coercion
forall a b. (a -> b) -> a -> b
$ \case
        OptV Maybe Value
Nothing -> Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV Maybe Value
forall a. Maybe a
Nothing)
        OptV (Just Value
v) -> Maybe Value -> Value
OptV (Maybe Value -> Value) -> (Value -> Maybe Value) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Maybe Value
forall a. a -> Maybe a
Just (Value -> Value) -> Either String Value -> Either String Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion
c Value
v
        Value
v -> String -> Either String Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String Value) -> String -> Either String Value
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing option"
    Left String
_ -> Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String Value -> Coercion
forall a b. a -> b -> a
const (Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV Maybe Value
forall a. Maybe a
Nothing)))

-- Option: The constituent rule
go Type (Ref k1 Type)
t (OptT Type (Ref k2 Type)
t2) | Bool -> Bool
not (Type (Ref k2 Type) -> Bool
forall a. Type (Ref a Type) -> Bool
isOptLike Type (Ref k2 Type)
t2) = State (Memo k1 k2) (Either String Coercion)
-> ExceptT String (State (Memo k1 k2)) (Either String Coercion)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (M k1 k2 Coercion -> State (Memo k1 k2) (Either String Coercion)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t Type (Ref k2 Type)
t2)) ExceptT String (State (Memo k1 k2)) (Either String Coercion)
-> (Either String Coercion -> M k1 k2 Coercion) -> M k1 k2 Coercion
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Right Coercion
c -> Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Coercion -> M k1 k2 Coercion) -> Coercion -> M k1 k2 Coercion
forall a b. (a -> b) -> a -> b
$ \Value
v -> Maybe Value -> Value
OptV (Maybe Value -> Value) -> (Value -> Maybe Value) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Maybe Value
forall a. a -> Maybe a
Just (Value -> Value) -> Either String Value -> Either String Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion
c Value
v
    Left String
_ -> Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String Value -> Coercion
forall a b. a -> b -> a
const (Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV Maybe Value
forall a. Maybe a
Nothing)))
-- Option: The fallback rule
go Type (Ref k1 Type)
_ (OptT Type (Ref k2 Type)
_) = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String Value -> Coercion
forall a b. a -> b -> a
const (Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV Maybe Value
forall a. Maybe a
Nothing)))

-- Records
go (RecT Fields (Ref k1 Type)
fs1) (RecT Fields (Ref k2 Type)
fs2) = do
    let m1 :: Map FieldName (Type (Ref k1 Type))
m1 = Fields (Ref k1 Type) -> Map FieldName (Type (Ref k1 Type))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k1 Type)
fs1
    let m2 :: Map FieldName (Type (Ref k2 Type))
m2 = Fields (Ref k2 Type) -> Map FieldName (Type (Ref k2 Type))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k2 Type)
fs2
    [(FieldName, Value)]
new_fields <- [ExceptT String (State (Memo k1 k2)) (FieldName, Value)]
-> ExceptT String (State (Memo k1 k2)) [(FieldName, Value)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
            [ case Type (Ref k2 Type) -> Type (Ref k2 Type)
forall a. Type (Ref a Type) -> Type (Ref a Type)
unRef Type (Ref k2 Type)
t of
                OptT Type (Ref k2 Type)
_ -> (FieldName, Value)
-> ExceptT String (State (Memo k1 k2)) (FieldName, Value)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FieldName
fn, Maybe Value -> Value
OptV Maybe Value
forall a. Maybe a
Nothing)
                Type (Ref k2 Type)
ReservedT -> (FieldName, Value)
-> ExceptT String (State (Memo k1 k2)) (FieldName, Value)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FieldName
fn, Value
ReservedV)
                Type (Ref k2 Type)
t -> String -> ExceptT String (State (Memo k1 k2)) (FieldName, Value)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String (State (Memo k1 k2)) (FieldName, Value))
-> String -> ExceptT String (State (Memo k1 k2)) (FieldName, Value)
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Missing record field" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FieldName -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type (Ref k2 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k2 Type)
t
            | (FieldName
fn, Type (Ref k2 Type)
t) <- Map FieldName (Type (Ref k2 Type)) -> Fields (Ref k2 Type)
forall k a. Map k a -> [(k, a)]
M.toList (Map FieldName (Type (Ref k2 Type)) -> Fields (Ref k2 Type))
-> Map FieldName (Type (Ref k2 Type)) -> Fields (Ref k2 Type)
forall a b. (a -> b) -> a -> b
$ Map FieldName (Type (Ref k2 Type))
m2 Map FieldName (Type (Ref k2 Type))
-> Map FieldName (Type (Ref k1 Type))
-> Map FieldName (Type (Ref k2 Type))
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.\\ Map FieldName (Type (Ref k1 Type))
m1
            ]
    [Map FieldName Value -> Either String (FieldName, Value)]
field_coercions <- [ExceptT
   String
   (State (Memo k1 k2))
   (Map FieldName Value -> Either String (FieldName, Value))]
-> ExceptT
     String
     (State (Memo k1 k2))
     [Map FieldName Value -> Either String (FieldName, Value)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
            [ do Coercion
c <- Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
                 (Map FieldName Value -> Either String (FieldName, Value))
-> ExceptT
     String
     (State (Memo k1 k2))
     (Map FieldName Value -> Either String (FieldName, Value))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Map FieldName Value -> Either String (FieldName, Value))
 -> ExceptT
      String
      (State (Memo k1 k2))
      (Map FieldName Value -> Either String (FieldName, Value)))
-> (Map FieldName Value -> Either String (FieldName, Value))
-> ExceptT
     String
     (State (Memo k1 k2))
     (Map FieldName Value -> Either String (FieldName, Value))
forall a b. (a -> b) -> a -> b
$ \Map FieldName Value
vm -> case FieldName -> Map FieldName Value -> Maybe Value
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FieldName
fn Map FieldName Value
vm of
                    Maybe Value
Nothing -> String -> Either String (FieldName, Value)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String (FieldName, Value))
-> String -> Either String (FieldName, Value)
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Record value lacks field" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FieldName -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type (Ref k1 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1
                    Just Value
v -> (FieldName
fn, ) (Value -> (FieldName, Value))
-> Either String Value -> Either String (FieldName, Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion
c Value
v
            | (FieldName
fn, (Type (Ref k1 Type)
t1, Type (Ref k2 Type)
t2)) <- Map FieldName (Type (Ref k1 Type), Type (Ref k2 Type))
-> [(FieldName, (Type (Ref k1 Type), Type (Ref k2 Type)))]
forall k a. Map k a -> [(k, a)]
M.toList (Map FieldName (Type (Ref k1 Type), Type (Ref k2 Type))
 -> [(FieldName, (Type (Ref k1 Type), Type (Ref k2 Type)))])
-> Map FieldName (Type (Ref k1 Type), Type (Ref k2 Type))
-> [(FieldName, (Type (Ref k1 Type), Type (Ref k2 Type)))]
forall a b. (a -> b) -> a -> b
$ (Type (Ref k1 Type)
 -> Type (Ref k2 Type) -> (Type (Ref k1 Type), Type (Ref k2 Type)))
-> Map FieldName (Type (Ref k1 Type))
-> Map FieldName (Type (Ref k2 Type))
-> Map FieldName (Type (Ref k1 Type), Type (Ref k2 Type))
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map FieldName (Type (Ref k1 Type))
m1 Map FieldName (Type (Ref k2 Type))
m2
            ]
    Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Coercion -> M k1 k2 Coercion) -> Coercion -> M k1 k2 Coercion
forall a b. (a -> b) -> a -> b
$ \case
        TupV [Value]
ts -> do
            let vm :: Map FieldName Value
vm = [(FieldName, Value)] -> Map FieldName Value
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(FieldName, Value)] -> Map FieldName Value)
-> [(FieldName, Value)] -> Map FieldName Value
forall a b. (a -> b) -> a -> b
$ [FieldName] -> [Value] -> [(FieldName, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Word32 -> FieldName
hashedField Word32
n | Word32
n <- [Word32
0..]] [Value]
ts
            [(FieldName, Value)]
coerced_fields <- ((Map FieldName Value -> Either String (FieldName, Value))
 -> Either String (FieldName, Value))
-> [Map FieldName Value -> Either String (FieldName, Value)]
-> Either String [(FieldName, Value)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Map FieldName Value -> Either String (FieldName, Value))
-> Map FieldName Value -> Either String (FieldName, Value)
forall a b. (a -> b) -> a -> b
$ Map FieldName Value
vm) [Map FieldName Value -> Either String (FieldName, Value)]
field_coercions
            Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ [(FieldName, Value)] -> Value
RecV ([(FieldName, Value)] -> Value) -> [(FieldName, Value)] -> Value
forall a b. (a -> b) -> a -> b
$ ((FieldName, Value) -> FieldName)
-> [(FieldName, Value)] -> [(FieldName, Value)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (FieldName, Value) -> FieldName
forall a b. (a, b) -> a
fst ([(FieldName, Value)] -> [(FieldName, Value)])
-> [(FieldName, Value)] -> [(FieldName, Value)]
forall a b. (a -> b) -> a -> b
$ [(FieldName, Value)]
coerced_fields [(FieldName, Value)]
-> [(FieldName, Value)] -> [(FieldName, Value)]
forall a. Semigroup a => a -> a -> a
<> [(FieldName, Value)]
new_fields
        RecV [(FieldName, Value)]
fvs -> do
            let vm :: Map FieldName Value
vm = [(FieldName, Value)] -> Map FieldName Value
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(FieldName, Value)]
fvs
            [(FieldName, Value)]
coerced_fields <- ((Map FieldName Value -> Either String (FieldName, Value))
 -> Either String (FieldName, Value))
-> [Map FieldName Value -> Either String (FieldName, Value)]
-> Either String [(FieldName, Value)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Map FieldName Value -> Either String (FieldName, Value))
-> Map FieldName Value -> Either String (FieldName, Value)
forall a b. (a -> b) -> a -> b
$ Map FieldName Value
vm) [Map FieldName Value -> Either String (FieldName, Value)]
field_coercions
            Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ [(FieldName, Value)] -> Value
RecV ([(FieldName, Value)] -> Value) -> [(FieldName, Value)] -> Value
forall a b. (a -> b) -> a -> b
$ ((FieldName, Value) -> FieldName)
-> [(FieldName, Value)] -> [(FieldName, Value)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (FieldName, Value) -> FieldName
forall a b. (a, b) -> a
fst ([(FieldName, Value)] -> [(FieldName, Value)])
-> [(FieldName, Value)] -> [(FieldName, Value)]
forall a b. (a -> b) -> a -> b
$ [(FieldName, Value)]
coerced_fields [(FieldName, Value)]
-> [(FieldName, Value)] -> [(FieldName, Value)]
forall a. Semigroup a => a -> a -> a
<> [(FieldName, Value)]
new_fields
        Value
v -> String -> Either String Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String Value) -> String -> Either String Value
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing record"

-- Variants
go (VariantT Fields (Ref k1 Type)
fs1) (VariantT Fields (Ref k2 Type)
fs2) = do
    let m1 :: Map FieldName (Type (Ref k1 Type))
m1 = Fields (Ref k1 Type) -> Map FieldName (Type (Ref k1 Type))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k1 Type)
fs1
    let m2 :: Map FieldName (Type (Ref k2 Type))
m2 = Fields (Ref k2 Type) -> Map FieldName (Type (Ref k2 Type))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k2 Type)
fs2
    Map FieldName Coercion
cm <- (FieldName -> Type (Ref k1 Type) -> M k1 k2 Coercion)
-> Map FieldName (Type (Ref k1 Type))
-> ExceptT String (State (Memo k1 k2)) (Map FieldName Coercion)
forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
M.traverseWithKey (\FieldName
fn Type (Ref k1 Type)
t1 ->
        case FieldName
-> Map FieldName (Type (Ref k2 Type)) -> Maybe (Type (Ref k2 Type))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FieldName
fn Map FieldName (Type (Ref k2 Type))
m2 of
            Just Type (Ref k2 Type)
t2 -> Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
            Maybe (Type (Ref k2 Type))
Nothing -> String -> M k1 k2 Coercion
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> M k1 k2 Coercion) -> String -> M k1 k2 Coercion
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Missing variant field" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FieldName -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type (Ref k1 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1
        ) Map FieldName (Type (Ref k1 Type))
m1
    Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Coercion -> M k1 k2 Coercion) -> Coercion -> M k1 k2 Coercion
forall a b. (a -> b) -> a -> b
$ \case
        VariantV FieldName
fn Value
v | Just Coercion
c <- FieldName -> Map FieldName Coercion -> Maybe Coercion
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FieldName
fn Map FieldName Coercion
cm -> FieldName -> Value -> Value
VariantV FieldName
fn (Value -> Value) -> Either String Value -> Either String Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion
c Value
v
                      | Bool
otherwise -> String -> Either String Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String Value) -> String -> Either String Value
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected variant field" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FieldName -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn
        Value
v -> String -> Either String Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String Value) -> String -> Either String Value
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing variant"

-- Reference types
go (FuncT MethodType (Ref k1 Type)
mt1) (FuncT MethodType (Ref k2 Type)
mt2) = MethodType (Ref k1 Type) -> MethodType (Ref k2 Type) -> M k1 k2 ()
forall k2 k1.
(Pretty k2, Pretty k1, Ord k2, Ord k1) =>
MethodType (Ref k1 Type) -> MethodType (Ref k2 Type) -> M k1 k2 ()
goMethodType MethodType (Ref k1 Type)
mt1 MethodType (Ref k2 Type)
mt2 M k1 k2 () -> M k1 k2 Coercion -> M k1 k2 Coercion
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go (ServiceT [(Text, MethodType (Ref k1 Type))]
meths1) (ServiceT [(Text, MethodType (Ref k2 Type))]
meths2) = do
    let m1 :: Map Text (MethodType (Ref k1 Type))
m1 = [(Text, MethodType (Ref k1 Type))]
-> Map Text (MethodType (Ref k1 Type))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Text, MethodType (Ref k1 Type))]
meths1
    [(Text, MethodType (Ref k2 Type))]
-> ((Text, MethodType (Ref k2 Type)) -> M k1 k2 ()) -> M k1 k2 ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Text, MethodType (Ref k2 Type))]
meths2 (((Text, MethodType (Ref k2 Type)) -> M k1 k2 ()) -> M k1 k2 ())
-> ((Text, MethodType (Ref k2 Type)) -> M k1 k2 ()) -> M k1 k2 ()
forall a b. (a -> b) -> a -> b
$ \(Text
m, MethodType (Ref k2 Type)
mt2) -> case Text
-> Map Text (MethodType (Ref k1 Type))
-> Maybe (MethodType (Ref k1 Type))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
m Map Text (MethodType (Ref k1 Type))
m1 of
        Just MethodType (Ref k1 Type)
mt1 -> MethodType (Ref k1 Type) -> MethodType (Ref k2 Type) -> M k1 k2 ()
forall k2 k1.
(Pretty k2, Pretty k1, Ord k2, Ord k1) =>
MethodType (Ref k1 Type) -> MethodType (Ref k2 Type) -> M k1 k2 ()
goMethodType MethodType (Ref k1 Type)
mt1 MethodType (Ref k2 Type)
mt2
        Maybe (MethodType (Ref k1 Type))
Nothing -> String -> M k1 k2 ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> M k1 k2 ()) -> String -> M k1 k2 ()
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Missing service method" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Text
m Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> MethodType (Ref k2 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty MethodType (Ref k2 Type)
mt2
    Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- BlobT
go Type (Ref k1 Type)
BlobT Type (Ref k2 Type)
BlobT = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure
go (VecT Type (Ref k1 Type)
t) Type (Ref k2 Type)
BlobT | Type (Ref k1 Type) -> Bool
forall a. Type (Ref a Type) -> Bool
isNat8 Type (Ref k1 Type)
t = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Coercion -> M k1 k2 Coercion) -> Coercion -> M k1 k2 Coercion
forall a b. (a -> b) -> a -> b
$ \case
    VecV Vector Value
vs ->  ByteString -> Value
BlobV (ByteString -> Value)
-> (Vector Word8 -> ByteString) -> Vector Word8 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
BS.pack ([Word8] -> ByteString)
-> (Vector Word8 -> [Word8]) -> Vector Word8 -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Word8 -> [Word8]
forall a. Vector a -> [a]
V.toList (Vector Word8 -> Value)
-> Either String (Vector Word8) -> Either String Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Either String Word8)
-> Vector Value -> Either String (Vector Word8)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Value -> Either String Word8
forall (f :: * -> *). MonadError String f => Value -> f Word8
goNat8 Vector Value
vs
    Value
v -> String -> Either String Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String Value) -> String -> Either String Value
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing vec nat8 to blob"
   where
    goNat8 :: Value -> f Word8
goNat8 (Nat8V Word8
n) = Word8 -> f Word8
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word8
n
    goNat8 Value
v = String -> f Word8
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> f Word8) -> String -> f Word8
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing vec nat8 to blob"
go Type (Ref k1 Type)
BlobT (VecT Type (Ref k2 Type)
t) | Type (Ref k2 Type) -> Bool
forall a. Type (Ref a Type) -> Bool
isNat8 Type (Ref k2 Type)
t = Coercion -> M k1 k2 Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Coercion -> M k1 k2 Coercion) -> Coercion -> M k1 k2 Coercion
forall a b. (a -> b) -> a -> b
$ \case
    BlobV ByteString
b -> Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Vector Value -> Value
VecV (Vector Value -> Value) -> Vector Value -> Value
forall a b. (a -> b) -> a -> b
$ [Value] -> Vector Value
forall a. [a] -> Vector a
V.fromList ([Value] -> Vector Value) -> [Value] -> Vector Value
forall a b. (a -> b) -> a -> b
$ (Word8 -> Value) -> [Word8] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map (Word8 -> Value
Nat8V (Word8 -> Value) -> (Word8 -> Word8) -> Word8 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral) ([Word8] -> [Value]) -> [Word8] -> [Value]
forall a b. (a -> b) -> a -> b
$ ByteString -> [Word8]
BS.unpack ByteString
b
    Value
v -> String -> Either String Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String Value) -> String -> Either String Value
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing blob to vec nat8"

go Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = String -> M k1 k2 Coercion
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> M k1 k2 Coercion) -> String -> M k1 k2 Coercion
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Type" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type (Ref k1 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1 Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"is not a subtype of" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type (Ref k2 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k2 Type)
t2

goMethodType ::
    (Pretty k2, Pretty k1, Ord k2, Ord k1) =>
    MethodType (Ref k1 Type) ->
    MethodType (Ref k2 Type) ->
    M k1 k2 ()
goMethodType :: MethodType (Ref k1 Type) -> MethodType (Ref k2 Type) -> M k1 k2 ()
goMethodType (MethodType [Type (Ref k1 Type)]
ta1 [Type (Ref k1 Type)]
tr1 Bool
q1 Bool
o1) (MethodType [Type (Ref k2 Type)]
ta2 [Type (Ref k2 Type)]
tr2 Bool
q2 Bool
o2) = do
    Bool -> M k1 k2 () -> M k1 k2 ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
q1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
q2) (M k1 k2 () -> M k1 k2 ()) -> M k1 k2 () -> M k1 k2 ()
forall a b. (a -> b) -> a -> b
$ String -> M k1 k2 ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"Methods differ in query annotation"
    Bool -> M k1 k2 () -> M k1 k2 ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
o1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
o2) (M k1 k2 () -> M k1 k2 ()) -> M k1 k2 () -> M k1 k2 ()
forall a b. (a -> b) -> a -> b
$ String -> M k1 k2 ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"Methods differ in oneway annotation"
    ExceptT String (State (Memo k1 k2)) SeqCoercion -> M k1 k2 ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ExceptT String (State (Memo k1 k2)) SeqCoercion -> M k1 k2 ())
-> ExceptT String (State (Memo k1 k2)) SeqCoercion -> M k1 k2 ()
forall a b. (a -> b) -> a -> b
$ M k2 k1 SeqCoercion
-> ExceptT String (State (Memo k1 k2)) SeqCoercion
forall k1 k2 a. M k1 k2 a -> M k2 k1 a
flipM (M k2 k1 SeqCoercion
 -> ExceptT String (State (Memo k1 k2)) SeqCoercion)
-> M k2 k1 SeqCoercion
-> ExceptT String (State (Memo k1 k2)) SeqCoercion
forall a b. (a -> b) -> a -> b
$ [Type (Ref k2 Type)] -> [Type (Ref k1 Type)] -> M k2 k1 SeqCoercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k2 Type)]
ta2 [Type (Ref k1 Type)]
ta1
    ExceptT String (State (Memo k1 k2)) SeqCoercion -> M k1 k2 ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ExceptT String (State (Memo k1 k2)) SeqCoercion -> M k1 k2 ())
-> ExceptT String (State (Memo k1 k2)) SeqCoercion -> M k1 k2 ()
forall a b. (a -> b) -> a -> b
$ [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> ExceptT String (State (Memo k1 k2)) SeqCoercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
tr1 [Type (Ref k2 Type)]
tr2

goSeq :: [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
_ []  = SeqCoercion -> M k1 k2 SeqCoercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String [Value] -> SeqCoercion
forall a b. a -> b -> a
const (SeqCoercion
forall (m :: * -> *) a. Monad m => a -> m a
return []))
goSeq [Type (Ref k1 Type)]
ts1 (RefT (Ref k2
_ Type (Ref k2 Type)
t) : [Type (Ref k2 Type)]
ts) = [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
ts1 (Type (Ref k2 Type)
tType (Ref k2 Type) -> [Type (Ref k2 Type)] -> [Type (Ref k2 Type)]
forall a. a -> [a] -> [a]
:[Type (Ref k2 Type)]
ts)
goSeq ts1 :: [Type (Ref k1 Type)]
ts1@[] (Type (Ref k2 Type)
NullT  : [Type (Ref k2 Type)]
ts) = do
    SeqCoercion
cs2 <- [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
    SeqCoercion -> M k1 k2 SeqCoercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SeqCoercion -> M k1 k2 SeqCoercion)
-> SeqCoercion -> M k1 k2 SeqCoercion
forall a b. (a -> b) -> a -> b
$ \[Value]
_vs -> (Value
NullV Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:) ([Value] -> [Value])
-> Either String [Value] -> Either String [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqCoercion
cs2 []
goSeq ts1 :: [Type (Ref k1 Type)]
ts1@[] (OptT Type (Ref k2 Type)
_ : [Type (Ref k2 Type)]
ts) = do
    SeqCoercion
cs2 <- [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
    SeqCoercion -> M k1 k2 SeqCoercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SeqCoercion -> M k1 k2 SeqCoercion)
-> SeqCoercion -> M k1 k2 SeqCoercion
forall a b. (a -> b) -> a -> b
$ \[Value]
_vs -> (Maybe Value -> Value
OptV Maybe Value
forall a. Maybe a
Nothing Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:) ([Value] -> [Value])
-> Either String [Value] -> Either String [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqCoercion
cs2 []
goSeq ts1 :: [Type (Ref k1 Type)]
ts1@[] (Type (Ref k2 Type)
ReservedT : [Type (Ref k2 Type)]
ts) = do
    SeqCoercion
cs2 <- [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
    SeqCoercion -> M k1 k2 SeqCoercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SeqCoercion -> M k1 k2 SeqCoercion)
-> SeqCoercion -> M k1 k2 SeqCoercion
forall a b. (a -> b) -> a -> b
$ \[Value]
_vs -> (Value
ReservedV Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:) ([Value] -> [Value])
-> Either String [Value] -> Either String [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqCoercion
cs2 []
goSeq [] [Type (Ref k2 Type)]
ts =
    String -> M k1 k2 SeqCoercion
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> M k1 k2 SeqCoercion) -> String -> M k1 k2 SeqCoercion
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Argument type list too short, expecting types" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Type (Ref k2 Type)] -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty [Type (Ref k2 Type)]
ts
goSeq (Type (Ref k1 Type)
t1:[Type (Ref k1 Type)]
ts1) (Type (Ref k2 Type)
t2:[Type (Ref k2 Type)]
ts2) = do
    Coercion
c1 <- Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
    SeqCoercion
cs2 <- [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts2
    SeqCoercion -> M k1 k2 SeqCoercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SeqCoercion -> M k1 k2 SeqCoercion)
-> SeqCoercion -> M k1 k2 SeqCoercion
forall a b. (a -> b) -> a -> b
$ \case
        [] -> String -> Either String [Value]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String [Value])
-> String -> Either String [Value]
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Expecting value of type:" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type (Ref k1 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1
        (Value
v:[Value]
vs) -> do
            Value
v' <- Coercion
c1 Value
v
            [Value]
vs' <- SeqCoercion
cs2 [Value]
vs
            SeqCoercion
forall (m :: * -> *) a. Monad m => a -> m a
return (Value
v'Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:[Value]
vs')

unRef :: Type (Ref a Type) -> Type (Ref a Type)
unRef :: Type (Ref a Type) -> Type (Ref a Type)
unRef (RefT (Ref a
_ Type (Ref a Type)
t)) = Type (Ref a Type) -> Type (Ref a Type)
forall a. Type (Ref a Type) -> Type (Ref a Type)
unRef Type (Ref a Type)
t
unRef Type (Ref a Type)
t = Type (Ref a Type)
t

isNat8 :: Type (Ref a Type) -> Bool
isNat8 :: Type (Ref a Type) -> Bool
isNat8 (RefT (Ref a
_ Type (Ref a Type)
t)) = Type (Ref a Type) -> Bool
forall a. Type (Ref a Type) -> Bool
isNat8 Type (Ref a Type)
t
isNat8 Type (Ref a Type)
Nat8T = Bool
True
isNat8 Type (Ref a Type)
_ = Bool
False

-- | `null <: t`?
isOptLike :: Type (Ref a Type) -> Bool
isOptLike :: Type (Ref a Type) -> Bool
isOptLike (RefT (Ref a
_ Type (Ref a Type)
t)) = Type (Ref a Type) -> Bool
forall a. Type (Ref a Type) -> Bool
isOptLike Type (Ref a Type)
t
isOptLike Type (Ref a Type)
NullT = Bool
True
isOptLike (OptT Type (Ref a Type)
_) = Bool
True
isOptLike Type (Ref a Type)
ReservedT = Bool
True
isOptLike Type (Ref a Type)
_ = Bool
False