{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleContexts #-}
module Codec.Candid.Subtype
  ( isSubtypeOf
  , SubTypeM
  , runSubTypeM
  , isSubtypeOfM
  )
  where

import Prettyprinter
import qualified Data.Map as M
import Data.Bifunctor
import Data.Tuple
import Control.Monad
import Control.Monad.State.Lazy
import Control.Monad.Except
import Control.Monad.Trans.Except

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

type Memo k1 k2 =
    (M.Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()),
     M.Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()))

type SubTypeM k1 k2 = ExceptT String (State (Memo k1 k2))

runSubTypeM :: (Ord k1, Ord k2) => SubTypeM k1 k2 a -> Either String a
runSubTypeM :: forall k1 k2 a.
(Ord k1, Ord k2) =>
SubTypeM k1 k2 a -> Either String a
runSubTypeM SubTypeM k1 k2 a
act = forall s a. State s a -> s -> a
evalState (forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT SubTypeM k1 k2 a
act) (forall a. Monoid a => a
mempty, forall a. Monoid a => a
mempty)

-- | Returns 'Right' if the first argument is a subtype of the second, or
-- returns 'Left' with an explanation if not
isSubtypeOf ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    Type (Ref k1 Type) ->
    Type (Ref k2 Type) ->
    Either String ()
isSubtypeOf :: forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> Either String ()
isSubtypeOf Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = forall k1 k2 a.
(Ord k1, Ord k2) =>
SubTypeM k1 k2 a -> Either String a
runSubTypeM forall a b. (a -> b) -> a -> b
$ forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
isSubtypeOfM Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2

isSubtypeOfM ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    Type (Ref k1 Type) ->
    Type (Ref k2 Type) ->
    SubTypeM k1 k2 ()
isSubtypeOfM :: forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
isSubtypeOfM Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2

flipM :: SubTypeM k1 k2 a -> SubTypeM k2 k1 a
flipM :: forall k1 k2 a. SubTypeM k1 k2 a -> SubTypeM k2 k1 a
flipM (ExceptT (StateT Memo k1 k2 -> Identity (Either String a, Memo k1 k2)
f)) = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
 Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()))
-> Identity
     (Either String a,
      (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
       Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())))
f')
  where
    f' :: (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
 Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()))
-> Identity
     (Either String a,
      (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
       Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())))
f' (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ())
m1,Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())
m2) = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a b. (a, b) -> (b, a)
swap 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)) (Either String ())
m2,Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ())
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) ->
    SubTypeM k1 k2 ()

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

-- Memoization: When we see a pair for the first time,
-- we optimistically put 'True' into the map.
-- Either the following recursive call will fail (but then this optimistic
-- value wasn't a problem), or it will succeed, but then the guess was correct.
-- If it fails we put 'False' into it, to as a caching optimization
memo :: forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = do
  forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Type (Ref k1 Type)
t1,Type (Ref k2 Type)
t2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Either String ()
r -> forall (m :: * -> *) e a. Monad m => Either e a -> ExceptT e m a
except Either String ()
r
    Maybe (Either String ())
Nothing -> SubTypeM k1 k2 ()
assume_ok forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
go Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 forall (m :: * -> *) e a e'.
Monad m =>
ExceptT e m a -> (e -> ExceptT e' m a) -> ExceptT e' m a
`catchE` forall {m :: * -> *} {p :: * -> * -> *} {e} {b} {c} {b}.
(MonadState
   (p (Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either e b)) c)
   m,
 Bifunctor p, MonadError e m) =>
e -> m b
remember_failure)
  where
    remember :: a -> m ()
remember a
r         = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (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) a
r))
    assume_ok :: SubTypeM k1 k2 ()
assume_ok          = forall {p :: * -> * -> *} {a} {c} {m :: * -> *}.
(MonadState
   (p (Map (Type (Ref k1 Type), Type (Ref k2 Type)) a) c) m,
 Bifunctor p) =>
a -> m ()
remember (forall a b. b -> Either a b
Right ())
    remember_failure :: e -> m b
remember_failure e
e = forall {p :: * -> * -> *} {a} {c} {m :: * -> *}.
(MonadState
   (p (Map (Type (Ref k1 Type), Type (Ref k2 Type)) a) c) m,
 Bifunctor p) =>
a -> m ()
remember (forall a b. a -> Either a b
Left e
e) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e

-- Look through refs
go :: forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
go (RefT (Ref k1
_ Type (Ref k1 Type)
t1)) Type (Ref k2 Type)
t2 = forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
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)) = forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Nat8T Type (Ref k2 Type)
Nat8T = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Nat16T Type (Ref k2 Type)
Nat16T = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Nat32T Type (Ref k2 Type)
Nat32T = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Nat64T Type (Ref k2 Type)
Nat64T = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
IntT Type (Ref k2 Type)
IntT = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Int8T Type (Ref k2 Type)
Int8T = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Int16T Type (Ref k2 Type)
Int16T = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Int32T Type (Ref k2 Type)
Int32T = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Int64T Type (Ref k2 Type)
Int64T = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Float32T Type (Ref k2 Type)
Float32T = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Float64T Type (Ref k2 Type)
Float64T = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
BoolT Type (Ref k2 Type)
BoolT = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
TextT Type (Ref k2 Type)
TextT = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
NullT Type (Ref k2 Type)
NullT = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
PrincipalT Type (Ref k2 Type)
PrincipalT = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- Nat <: Int
go Type (Ref k1 Type)
NatT Type (Ref k2 Type)
IntT = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- t <: reserved
go Type (Ref k1 Type)
_ Type (Ref k2 Type)
ReservedT = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- empty <: t
go Type (Ref k1 Type)
EmptyT Type (Ref k2 Type)
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- vec t1 <: vec t2
go (VecT Type (Ref k1 Type)
t1) (VecT Type (Ref k2 Type)
t2) = forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2

-- Option: very simple
go Type (Ref k1 Type)
_ (OptT Type (Ref k2 Type)
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- Records
go (RecT Fields (Ref k1 Type)
fs1) (RecT Fields (Ref k2 Type)
fs2) = do
    let m1 :: Map FieldName (Type (Ref k1 Type))
m1 = 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 = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k2 Type)
fs2
    -- Check missing fields
    forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_
      [ case forall a. Type (Ref a Type) -> Type (Ref a Type)
unRef Type (Ref k2 Type)
t of
          OptT Type (Ref k2 Type)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Type (Ref k2 Type)
ReservedT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Type (Ref k2 Type)
t -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Missing record field" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k2 Type)
t
      | (FieldName
fn, Type (Ref k2 Type)
t) <- forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ Map FieldName (Type (Ref k2 Type))
m2 forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.\\ Map FieldName (Type (Ref k1 Type))
m1
      ]
    -- Check existing fields
    forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 | (FieldName
_fn, (Type (Ref k1 Type)
t1, Type (Ref k2 Type)
t2)) <- forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ 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 ]

-- Variants
go (VariantT Fields (Ref k1 Type)
fs1) (VariantT Fields (Ref k2 Type)
fs2) = do
    let m1 :: Map FieldName (Type (Ref k1 Type))
m1 = 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 = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k2 Type)
fs2
    forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_
      [ case 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 -> forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
            Maybe (Type (Ref k2 Type))
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Missing variant field" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1
      | (FieldName
fn, Type (Ref k1 Type)
t1) <- forall k a. Map k a -> [(k, a)]
M.toList Map FieldName (Type (Ref k1 Type))
m1
      ]

-- Reference types
go (FuncT MethodType (Ref k1 Type)
mt1) (FuncT MethodType (Ref k2 Type)
mt2) = forall k2 k1.
(Pretty k2, Pretty k1, Ord k2, Ord k1) =>
MethodType (Ref k1 Type)
-> MethodType (Ref k2 Type) -> SubTypeM k1 k2 ()
goMethodType MethodType (Ref k1 Type)
mt1 MethodType (Ref k2 Type)
mt2
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 = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Text, MethodType (Ref k1 Type))]
meths1
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Text, MethodType (Ref k2 Type))]
meths2 forall a b. (a -> b) -> a -> b
$ \(Text
m, MethodType (Ref k2 Type)
mt2) -> case 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 -> forall k2 k1.
(Pretty k2, Pretty k1, Ord k2, Ord k1) =>
MethodType (Ref k1 Type)
-> MethodType (Ref k2 Type) -> SubTypeM k1 k2 ()
goMethodType MethodType (Ref k1 Type)
mt1 MethodType (Ref k2 Type)
mt2
        Maybe (MethodType (Ref k1 Type))
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Missing service method" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Text
m forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty MethodType (Ref k2 Type)
mt2

-- BlobT
go Type (Ref k1 Type)
BlobT Type (Ref k2 Type)
BlobT = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go (VecT Type (Ref k1 Type)
t) Type (Ref k2 Type)
BlobT | forall a. Type (Ref a Type) -> Bool
isNat8 Type (Ref k1 Type)
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
BlobT (VecT Type (Ref k2 Type)
t) | forall a. Type (Ref a Type) -> Bool
isNat8 Type (Ref k2 Type)
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- Final catch-all
go Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1 forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"is not a subtype of" forall ann. Doc ann -> Doc ann -> Doc ann
<+> 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) ->
    SubTypeM k1 k2 ()
goMethodType :: forall k2 k1.
(Pretty k2, Pretty k1, Ord k2, Ord k1) =>
MethodType (Ref k1 Type)
-> MethodType (Ref k2 Type) -> SubTypeM 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
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
q1 forall a. Eq a => a -> a -> Bool
== Bool
q2) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"Methods differ in query annotation"
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
o1 forall a. Eq a => a -> a -> Bool
== Bool
o2) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"Methods differ in oneway annotation"
    forall k1 k2 a. SubTypeM k1 k2 a -> SubTypeM k2 k1 a
flipM forall a b. (a -> b) -> a -> b
$ forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k2 Type)]
ta2 [Type (Ref k1 Type)]
ta1
    forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
tr1 [Type (Ref k2 Type)]
tr2

goSeq :: forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
_ []  = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
goSeq [Type (Ref k1 Type)]
ts1 (RefT (Ref k2
_ Type (Ref k2 Type)
t) : [Type (Ref k2 Type)]
ts) = forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
ts1 (Type (Ref k2 Type)
tforall a. a -> [a] -> [a]
:[Type (Ref k2 Type)]
ts)
-- Missing optional arguments are ok
goSeq ts1 :: [Type (Ref k1 Type)]
ts1@[] (OptT Type (Ref k2 Type)
_ : [Type (Ref k2 Type)]
ts) = forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
goSeq ts1 :: [Type (Ref k1 Type)]
ts1@[] (Type (Ref k2 Type)
ReservedT : [Type (Ref k2 Type)]
ts) = forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
goSeq [] [Type (Ref k2 Type)]
ts = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Argument type list too short, expecting types" forall ann. Doc ann -> Doc ann -> Doc ann
<+> 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) = forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts2

unRef :: Type (Ref a Type) -> Type (Ref a Type)
unRef :: forall a. Type (Ref a Type) -> Type (Ref a Type)
unRef (RefT (Ref a
_ Type (Ref a Type)
t)) = 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 :: forall a. Type (Ref a Type) -> Bool
isNat8 (RefT (Ref a
_ Type (Ref a Type)
t)) = 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