    {-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleInstances, PatternGuards, RankNTypes, FlexibleContexts #-}

    module Language.Javascript.JMacro.TypeCheck where

    import Language.Javascript.JMacro.Base
    import Language.Javascript.JMacro.Types

    import Control.Applicative
    import Control.Monad
    import Control.Monad.Identity
    import Control.Monad.State
    import Control.Monad.Reader
    import Control.Monad.Writer
    import Control.Monad.Except
    import Data.Either
    import Data.Map (Map)
    import Data.Maybe(catMaybes)
    import Data.List(intercalate, nub, transpose)
    import qualified Data.Traversable as T
    import qualified Data.Foldable as F
    import qualified Data.Map as M
    import qualified Data.Text.Lazy as T
    import Data.Set(Set)
    import qualified Data.Set as S

    import Text.PrettyPrint.Leijen.Text hiding ((<$>))

    -- Utility

    eitherIsLeft :: Either a b -> Bool
    eitherIsLeft :: forall a b. Either a b -> Bool
    eitherIsLeft (Left a
    _) = Bool
    True
    eitherIsLeft Either a b
    _ = Bool
    False

    partitionOut :: (a -> Maybe b) -> [a] -> ([b],[a])
    partitionOut :: forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
    partitionOut a -> Maybe b
    f [a]
    xs' = (a -> ([b], [a]) -> ([b], [a])) -> ([b], [a]) -> [a] -> ([b], [a])
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr a -> ([b], [a]) -> ([b], [a])
    go ([],[]) [a]
    xs'
        where go :: a -> ([b], [a]) -> ([b], [a])
    go a
    x ~([b]
    bs,[a]
    as)
                 | Just b
    b <- a -> Maybe b
    f a
    x = (b
    bb -> [b] -> [b]
    forall a. a -> [a] -> [a]
    :[b]
    bs,[a]
    as)
                 | Bool
    otherwise = ([b]
    bs,a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    as)

    zipWithOrChange :: (a -> a -> b) -> (a -> b) -> [a] -> [a] -> [b]
    zipWithOrChange :: forall a b. (a -> a -> b) -> (a -> b) -> [a] -> [a] -> [b]
    zipWithOrChange a -> a -> b
    f a -> b
    g [a]
    xss [a]
    yss = [a] -> [a] -> [b]
    go [a]
    xss [a]
    yss
        where go :: [a] -> [a] -> [b]
    go (a
    x:[a]
    xs) (a
    y:[a]
    ys) = a -> a -> b
    f a
    x a
    y b -> [b] -> [b]
    forall a. a -> [a] -> [a]
    : [a] -> [a] -> [b]
    go [a]
    xs [a]
    ys
              go xs :: [a]
    xs@(a
    _:[a]
    _) [a]
    _ = (a -> b) -> [a] -> [b]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> b
    g [a]
    xs
              go [a]
    _ [a]
    ys = (a -> b) -> [a] -> [b]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> b
    g [a]
    ys

    zipWithOrIdM :: Monad m => (a -> a -> m a) -> [a] -> [a] -> m [a]
    zipWithOrIdM :: forall (m :: * -> *) a.
    Monad m =>
    (a -> a -> m a) -> [a] -> [a] -> m [a]
    zipWithOrIdM a -> a -> m a
    f [a]
    xs [a]
    ys = [m a] -> m [a]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence ([m a] -> m [a]) -> [m a] -> m [a]
    forall a b. (a -> b) -> a -> b
    $ (a -> a -> m a) -> (a -> m a) -> [a] -> [a] -> [m a]
    forall a b. (a -> a -> b) -> (a -> b) -> [a] -> [a] -> [b]
    zipWithOrChange a -> a -> m a
    f a -> m a
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [a]
    xs [a]
    ys

    unionWithM :: (Monad m, Ord key) => (val -> val -> m val) -> Map key val -> Map key val -> m (Map key val)
    unionWithM :: forall (m :: * -> *) key val.
    (Monad m, Ord key) =>
    (val -> val -> m val)
    -> Map key val -> Map key val -> m (Map key val)
    unionWithM val -> val -> m val
    f Map key val
    m1 Map key val
    m2 = Map key (m val) -> m (Map key val)
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => Map key (m a) -> m (Map key a)
    T.sequence (Map key (m val) -> m (Map key val))
    -> Map key (m val) -> m (Map key val)
    forall a b. (a -> b) -> a -> b
    $ (m val -> m val -> m val)
    -> Map key (m val) -> Map key (m val) -> Map key (m val)
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    M.unionWith (\m val
    xm m val
    ym -> m (m val) -> m val
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (m (m val) -> m val) -> m (m val) -> m val
    forall a b. (a -> b) -> a -> b
    $ (val -> val -> m val) -> m val -> m val -> m (m val)
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 val -> val -> m val
    f m val
    xm m val
    ym) ((val -> m val) -> Map key val -> Map key (m val)
    forall a b k. (a -> b) -> Map k a -> Map k b
    M.map val -> m val
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Map key val
    m1) ((val -> m val) -> Map key val -> Map key (m val)
    forall a b k. (a -> b) -> Map k a -> Map k b
    M.map val -> m val
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Map key val
    m2)

    intersectionWithM :: (Monad m, Ord key) => (val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
    intersectionWithM :: forall (m :: * -> *) key val b.
    (Monad m, Ord key) =>
    (val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
    intersectionWithM val -> val -> m b
    f Map key val
    m1 Map key val
    m2 = Map key (m b) -> m (Map key b)
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => Map key (m a) -> m (Map key a)
    T.sequence (Map key (m b) -> m (Map key b)) -> Map key (m b) -> m (Map key b)
    forall a b. (a -> b) -> a -> b
    $ (val -> val -> m b) -> Map key val -> Map key val -> Map key (m b)
    forall k a b c.
    Ord k =>
    (a -> b -> c) -> Map k a -> Map k b -> Map k c
    M.intersectionWith val -> val -> m b
    f Map key val
    m1 Map key val
    m2

    class Compos1 t where
        compos1 :: (forall a. a -> m a) -> (forall a b. m (a -> b) -> m a -> m b)
               -> (t -> m t) -> t -> m t

    instance Compos1 JType where
        compos1 :: forall (m :: * -> *).
    (forall a. a -> m a)
    -> (forall a b. m (a -> b) -> m a -> m b)
    -> (JType -> m JType)
    -> JType
    -> m JType
    compos1 forall a. a -> m a
    ret forall a b. m (a -> b) -> m a -> m b
    app JType -> m JType
    f JType
    v =
            case JType
    v of
              JTFunc [JType]
    args JType
    body -> ([JType] -> JType -> JType) -> m ([JType] -> JType -> JType)
    forall a. a -> m a
    ret [JType] -> JType -> JType
    JTFunc m ([JType] -> JType -> JType) -> m [JType] -> m (JType -> JType)
    forall a b. m (a -> b) -> m a -> m b
    `app` (JType -> m JType) -> [JType] -> m [JType]
    forall {t :: * -> *} {a} {a}.
    Foldable t =>
    (a -> m a) -> t a -> m [a]
    mapM' JType -> m JType
    f [JType]
    args m (JType -> JType) -> m JType -> m JType
    forall a b. m (a -> b) -> m a -> m b
    `app` JType -> m JType
    f JType
    body
              JTForall [VarRef]
    vars JType
    t -> ([VarRef] -> JType -> JType) -> m ([VarRef] -> JType -> JType)
    forall a. a -> m a
    ret [VarRef] -> JType -> JType
    JTForall m ([VarRef] -> JType -> JType) -> m [VarRef] -> m (JType -> JType)
    forall a b. m (a -> b) -> m a -> m b
    `app` [VarRef] -> m [VarRef]
    forall a. a -> m a
    ret [VarRef]
    vars m (JType -> JType) -> m JType -> m JType
    forall a b. m (a -> b) -> m a -> m b
    `app` JType -> m JType
    f JType
    t
              JTList JType
    t -> (JType -> JType) -> m (JType -> JType)
    forall a. a -> m a
    ret JType -> JType
    JTList m (JType -> JType) -> m JType -> m JType
    forall a b. m (a -> b) -> m a -> m b
    `app` JType -> m JType
    f JType
    t
              JTMap JType
    t -> (JType -> JType) -> m (JType -> JType)
    forall a. a -> m a
    ret JType -> JType
    JTMap m (JType -> JType) -> m JType -> m JType
    forall a b. m (a -> b) -> m a -> m b
    `app` JType -> m JType
    f JType
    t
              JTRecord JType
    t Map String JType
    m -> (JType -> Map String JType -> JType)
    -> m (JType -> Map String JType -> JType)
    forall a. a -> m a
    ret JType -> Map String JType -> JType
    JTRecord m (JType -> Map String JType -> JType)
    -> m JType -> m (Map String JType -> JType)
    forall a b. m (a -> b) -> m a -> m b
    `app` JType -> m JType
    f JType
    t m (Map String JType -> JType) -> m (Map String JType) -> m JType
    forall a b. m (a -> b) -> m a -> m b
    `app` m (Map String JType)
    m'
                  where ([String]
    ls,[JType]
    ts) = [(String, JType)] -> ([String], [JType])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(String, JType)] -> ([String], [JType]))
    -> [(String, JType)] -> ([String], [JType])
    forall a b. (a -> b) -> a -> b
    $ Map String JType -> [(String, JType)]
    forall k a. Map k a -> [(k, a)]
    M.toList Map String JType
    m
                        m' :: m (Map String JType)
    m' = ([JType] -> Map String JType) -> m ([JType] -> Map String JType)
    forall a. a -> m a
    ret ([(String, JType)] -> Map String JType
    forall k a. Eq k => [(k, a)] -> Map k a
    M.fromAscList ([(String, JType)] -> Map String JType)
    -> ([JType] -> [(String, JType)]) -> [JType] -> Map String JType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [String] -> [JType] -> [(String, JType)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [String]
    ls) m ([JType] -> Map String JType)
    -> m [JType] -> m (Map String JType)
    forall a b. m (a -> b) -> m a -> m b
    `app` (JType -> m JType) -> [JType] -> m [JType]
    forall {t :: * -> *} {a} {a}.
    Foldable t =>
    (a -> m a) -> t a -> m [a]
    mapM' JType -> m JType
    f [JType]
    ts
              JType
    x -> JType -> m JType
    forall a. a -> m a
    ret JType
    x
          where
            mapM' :: (a -> m a) -> t a -> m [a]
    mapM' a -> m a
    g = (a -> m [a] -> m [a]) -> m [a] -> t a -> m [a]
    forall a b. (a -> b -> b) -> b -> t a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (m ([a] -> [a]) -> m [a] -> m [a]
    forall a b. m (a -> b) -> m a -> m b
    app (m ([a] -> [a]) -> m [a] -> m [a])
    -> (a -> m ([a] -> [a])) -> a -> m [a] -> m [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m (a -> [a] -> [a]) -> m a -> m ([a] -> [a])
    forall a b. m (a -> b) -> m a -> m b
    app ((a -> [a] -> [a]) -> m (a -> [a] -> [a])
    forall a. a -> m a
    ret (:)) (m a -> m ([a] -> [a])) -> (a -> m a) -> a -> m ([a] -> [a])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> m a
    g) ([a] -> m [a]
    forall a. a -> m a
    ret [])

    composOp1 :: Compos1 t => (t -> t) -> t -> t
    composOp1 :: forall t. Compos1 t => (t -> t) -> t -> t
    composOp1 t -> t
    f = Identity t -> t
    forall a. Identity a -> a
    runIdentity (Identity t -> t) -> (t -> Identity t) -> t -> t
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (t -> Identity t) -> t -> Identity t
    forall t (m :: * -> *).
    (Compos1 t, Monad m) =>
    (t -> m t) -> t -> m t
    composOpM1 (t -> Identity t
    forall a. a -> Identity a
    Identity (t -> Identity t) -> (t -> t) -> t -> Identity t
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t -> t
    f)
    composOpM1 :: (Compos1 t, Monad m) => (t -> m t) -> t -> m t
    composOpM1 :: forall t (m :: * -> *).
    (Compos1 t, Monad m) =>
    (t -> m t) -> t -> m t
    composOpM1 = (forall a. a -> m a)
    -> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
    forall t (m :: * -> *).
    Compos1 t =>
    (forall a. a -> m a)
    -> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
    forall (m :: * -> *).
    (forall a. a -> m a)
    -> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
    compos1 a -> m a
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return m (a -> b) -> m a -> m b
    forall a b. m (a -> b) -> m a -> m b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap
    composOpM1_ :: (Compos1 t, Monad m) => (t -> m ()) -> t -> m ()
    composOpM1_ :: forall t (m :: * -> *).
    (Compos1 t, Monad m) =>
    (t -> m ()) -> t -> m ()
    composOpM1_ = m () -> (m () -> m () -> m ()) -> (t -> m ()) -> t -> m ()
    forall t b. Compos1 t => b -> (b -> b -> b) -> (t -> b) -> t -> b
    composOpFold1 (() -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) m () -> m () -> m ()
    forall a b. m a -> m b -> m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    (>>)
    composOpFold1 :: Compos1 t => b -> (b -> b -> b) -> (t -> b) -> t -> b
    composOpFold1 :: forall t b. Compos1 t => b -> (b -> b -> b) -> (t -> b) -> t -> b
    composOpFold1 b
    z b -> b -> b
    c t -> b
    f = C b t -> b
    forall b a. C b a -> b
    unC (C b t -> b) -> (t -> C b t) -> t -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (forall a. a -> C b a)
    -> (forall a b. C b (a -> b) -> C b a -> C b b)
    -> (t -> C b t)
    -> t
    -> C b t
    forall t (m :: * -> *).
    Compos1 t =>
    (forall a. a -> m a)
    -> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
    forall (m :: * -> *).
    (forall a. a -> m a)
    -> (forall a b. m (a -> b) -> m a -> m b) -> (t -> m t) -> t -> m t
    compos1 (\a
    _ -> b -> C b a
    forall b a. b -> C b a
    C b
    z) (\(C b
    x) (C b
    y) -> b -> C b b
    forall b a. b -> C b a
    C (b -> b -> b
    c b
    x b
    y)) (b -> C b t
    forall b a. b -> C b a
    C (b -> C b t) -> (t -> b) -> t -> C b t
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t -> b
    f)
    newtype C b a = C { forall b a. C b a -> b
    unC :: b }

    -- Basic Types and TMonad
    data StoreVal = SVType JType
                  | SVConstrained (Set Constraint)
                    deriving Int -> StoreVal -> ShowS
    [StoreVal] -> ShowS
    StoreVal -> String
    (Int -> StoreVal -> ShowS)
    -> (StoreVal -> String) -> ([StoreVal] -> ShowS) -> Show StoreVal
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> StoreVal -> ShowS
    showsPrec :: Int -> StoreVal -> ShowS
    $cshow :: StoreVal -> String
    show :: StoreVal -> String
    $cshowList :: [StoreVal] -> ShowS
    showList :: [StoreVal] -> ShowS
    Show
                  {- -- | SVFreshType Int -}

    data TCState = TCS {TCState -> [Map Ident JType]
    tc_env :: [Map Ident JType],
                        TCState -> Map Int StoreVal
    tc_vars :: Map Int StoreVal,
                        TCState -> [Set Int]
    tc_stack :: [Set Int],
                        TCState -> Set Int
    tc_frozen :: Set Int,
                        TCState -> Int
    tc_varCt :: Int,
                        TCState -> [TMonad String]
    tc_context :: [TMonad String]}

    instance Show TCState where
        show :: TCState -> String
    show (TCS [Map Ident JType]
    env Map Int StoreVal
    vars [Set Int]
    stack Set Int
    frozen Int
    varCt [TMonad String]
    cxt) =
            String
    "env: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Map Ident JType] -> String
    forall a. Show a => a -> String
    show [Map Ident JType]
    env String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
            String
    "vars: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Map Int StoreVal -> String
    forall a. Show a => a -> String
    show Map Int StoreVal
    vars String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
            String
    "stack: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Set Int] -> String
    forall a. Show a => a -> String
    show [Set Int]
    stack String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
            String
    "frozen: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Set Int -> String
    forall a. Show a => a -> String
    show Set Int
    frozen String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "\n" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
            String
    "varCt: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    varCt

    tcStateEmpty :: TCState
    tcStateEmpty :: TCState
    tcStateEmpty = [Map Ident JType]
    -> Map Int StoreVal
    -> [Set Int]
    -> Set Int
    -> Int
    -> [TMonad String]
    -> TCState
    TCS [Map Ident JType
    forall k a. Map k a
    M.empty] Map Int StoreVal
    forall k a. Map k a
    M.empty [Set Int
    forall a. Set a
    S.empty] Set Int
    forall a. Set a
    S.empty Int
    0 []

    newtype TMonad a = TMonad (ExceptT String (State TCState) a) deriving ((forall a b. (a -> b) -> TMonad a -> TMonad b)
    -> (forall a b. a -> TMonad b -> TMonad a) -> Functor TMonad
    forall a b. a -> TMonad b -> TMonad a
    forall a b. (a -> b) -> TMonad a -> TMonad b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> TMonad a -> TMonad b
    fmap :: forall a b. (a -> b) -> TMonad a -> TMonad b
    $c<$ :: forall a b. a -> TMonad b -> TMonad a
    <$ :: forall a b. a -> TMonad b -> TMonad a
    Functor, Applicative TMonad
    Applicative TMonad =>
    (forall a b. TMonad a -> (a -> TMonad b) -> TMonad b)
    -> (forall a b. TMonad a -> TMonad b -> TMonad b)
    -> (forall a. a -> TMonad a)
    -> Monad TMonad
    forall a. a -> TMonad a
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall a b. TMonad a -> (a -> TMonad b) -> TMonad b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall a b. TMonad a -> (a -> TMonad b) -> TMonad b
    >>= :: forall a b. TMonad a -> (a -> TMonad b) -> TMonad b
    $c>> :: forall a b. TMonad a -> TMonad b -> TMonad b
    >> :: forall a b. TMonad a -> TMonad b -> TMonad b
    $creturn :: forall a. a -> TMonad a
    return :: forall a. a -> TMonad a
    Monad, MonadState TCState, MonadError String)

    instance Applicative TMonad where
        pure :: forall a. a -> TMonad a
    pure = a -> TMonad a
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
        <*> :: forall a b. TMonad (a -> b) -> TMonad a -> TMonad b
    (<*>) = TMonad (a -> b) -> TMonad a -> TMonad b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    class JTypeCheck a where
        typecheck :: a -> TMonad JType

    evalTMonad :: TMonad a -> Either String a
    evalTMonad :: forall a. TMonad a -> Either String a
    evalTMonad (TMonad ExceptT String (State TCState) a
    x) = State TCState (Either String a) -> TCState -> Either String a
    forall s a. State s a -> s -> a
    evalState (ExceptT String (State TCState) a -> State TCState (Either String a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT ExceptT String (State TCState) a
    x) TCState
    tcStateEmpty

    runTMonad :: TMonad a -> (Either String a, TCState)
    runTMonad :: forall a. TMonad a -> (Either String a, TCState)
    runTMonad (TMonad ExceptT String (State TCState) a
    x) = State TCState (Either String a)
    -> TCState -> (Either String a, TCState)
    forall s a. State s a -> s -> (a, s)
    runState (ExceptT String (State TCState) a -> State TCState (Either String a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT ExceptT String (State TCState) a
    x) TCState
    tcStateEmpty

    withContext :: TMonad a -> TMonad String -> TMonad a
    withContext :: forall a. TMonad a -> TMonad String -> TMonad a
    withContext TMonad a
    act TMonad String
    cxt = do
      cs <- TCState -> [TMonad String]
    tc_context (TCState -> [TMonad String])
    -> TMonad TCState -> TMonad [TMonad String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TMonad TCState
    forall s (m :: * -> *). MonadState s m => m s
    get
      modify (\TCState
    s -> TCState
    s {tc_context = cxt : cs})
      res <- act
      modify (\TCState
    s -> TCState
    s {tc_context = cs})
      return res

    traversem_ :: (F.Foldable t, Monad f) => (a -> f b) -> t a -> f ()
    traversem_ :: forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    traversem_ a -> f b
    f = (a -> f () -> f ()) -> f () -> t a -> f ()
    forall a b. (a -> b -> b) -> b -> t a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    F.foldr (f b -> f () -> f ()
    forall a b. f a -> f b -> f b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    (>>) (f b -> f () -> f ()) -> (a -> f b) -> a -> f () -> f ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> f b
    f) (() -> f ()
    forall a. a -> f a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

    --assums x is resolved
    freeVarsWithNames :: JType -> TMonad (Map Int String)
    freeVarsWithNames :: JType -> TMonad (Map Int String)
    freeVarsWithNames JType
    x =
      Map Int (Either String Int) -> Map Int String
    forall {k}. Map k (Either String Int) -> Map k String
    intsToNames (Map Int (Either String Int) -> Map Int String)
    -> ((Map Int (Either String Int), Set String, Int)
        -> Map Int (Either String Int))
    -> (Map Int (Either String Int), Set String, Int)
    -> Map Int String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (\(Map Int (Either String Int)
    a,Set String
    _,Int
    _) -> Map Int (Either String Int)
    a) ((Map Int (Either String Int), Set String, Int) -> Map Int String)
    -> TMonad (Map Int (Either String Int), Set String, Int)
    -> TMonad (Map Int String)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
           StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    -> (Map Int (Either String Int), Set String, Int)
    -> TMonad (Map Int (Either String Int), Set String, Int)
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
    execStateT (JType
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    go JType
    x) (Map Int (Either String Int)
    forall k a. Map k a
    M.empty, Set String
    forall a. Set a
    S.empty, Int
    0)
        where
          go :: JType -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
          go :: JType
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    go (JTFree VarRef
    vr) = VarRef
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    handleVR VarRef
    vr
          go (JTRigid VarRef
    vr Set Constraint
    cs) = VarRef
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    handleVR VarRef
    vr StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall a b.
    StateT (Map Int (Either String Int), Set String, Int) TMonad a
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad b
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (Constraint
     -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
    -> Set Constraint
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    traversem_ (JType
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    go (JType
     -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
    -> (Constraint -> JType)
    -> Constraint
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Constraint -> JType
    fromC) Set Constraint
    cs
          go JType
    v = (JType
     -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
    -> JType
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall t (m :: * -> *).
    (Compos1 t, Monad m) =>
    (t -> m ()) -> t -> m ()
    composOpM1_ JType
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    go JType
    v

          handleVR :: VarRef
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    handleVR (Maybe String
    mbName, Int
    ref) = do
            (m,ns,ct) <- StateT
      (Map Int (Either String Int), Set String, Int)
      TMonad
      (Map Int (Either String Int), Set String, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
            case M.lookup ref m of
              Just (Left String
    _) -> ()
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall a.
    a -> StateT (Map Int (Either String Int), Set String, Int) TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
              Just (Right Int
    _) -> case Maybe String
    mbName of
                                  Just String
    name -> String
    -> Int
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall {m :: * -> *} {k} {b} {c}.
    (MonadState (Map k (Either String b), Set String, c) m, Ord k) =>
    String -> k -> m ()
    putName String
    name Int
    ref
                                  Maybe String
    Nothing -> ()
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall a.
    a -> StateT (Map Int (Either String Int), Set String, Int) TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
              Maybe (Either String Int)
    Nothing -> do
                case Maybe String
    mbName of
                  Just String
    name -> String
    -> Int
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall {m :: * -> *} {k} {b} {c}.
    (MonadState (Map k (Either String b), Set String, c) m, Ord k) =>
    String -> k -> m ()
    putName String
    name Int
    ref
                  Maybe String
    Nothing -> (Map Int (Either String Int), Set String, Int)
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Int
    -> Either String Int
    -> Map Int (Either String Int)
    -> Map Int (Either String Int)
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert Int
    ref (Int -> Either String Int
    forall a b. b -> Either a b
    Right Int
    ct) Map Int (Either String Int)
    m, Set String
    ns, Int
    ct Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)
                (Constraint
     -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
    -> [Constraint]
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    mapM_ (JType
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    go (JType
     -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
    -> (Constraint -> JType)
    -> Constraint
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Constraint -> JType
    fromC) ([Constraint]
     -> StateT (Map Int (Either String Int), Set String, Int) TMonad ())
    -> StateT
         (Map Int (Either String Int), Set String, Int) TMonad [Constraint]
    -> StateT (Map Int (Either String Int), Set String, Int) TMonad ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TMonad [Constraint]
    -> StateT
         (Map Int (Either String Int), Set String, Int) TMonad [Constraint]
    forall (m :: * -> *) a.
    Monad m =>
    m a -> StateT (Map Int (Either String Int), Set String, Int) m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (VarRef -> TMonad [Constraint]
    lookupConstraintsList (Maybe String
    mbName, Int
    ref))

          putName :: String -> k -> m ()
    putName String
    n k
    ref = do
            (m,ns,ct) <- m (Map k (Either String b), Set String, c)
    forall s (m :: * -> *). MonadState s m => m s
    get
            let n' = Set String -> String -> Int -> String
    mkUnique Set String
    ns String
    n Int
    0
            put (M.insert ref (Left n') m, S.insert n' ns, ct)

          mkUnique :: Set String -> String -> Int -> String
          mkUnique :: Set String -> String -> Int -> String
    mkUnique Set String
    ns String
    n Int
    i
              | String
    n' String -> Set String -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `S.member` Set String
    ns = Set String -> String -> Int -> String
    mkUnique Set String
    ns String
    n (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)
              | Bool
    otherwise = String
    n'
              where n' :: String
    n' | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = String
    n
                       | Bool
    otherwise = String
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i

          fromC :: Constraint -> JType
    fromC (Sub JType
    t) = JType
    t
          fromC (Super JType
    t) = JType
    t

          intsToNames :: Map k (Either String Int) -> Map k String
    intsToNames Map k (Either String Int)
    x = (Either String Int -> String)
    -> Map k (Either String Int) -> Map k String
    forall a b. (a -> b) -> Map k a -> Map k b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ShowS -> (Int -> String) -> Either String Int -> String
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either ShowS
    forall a. a -> a
    id Int -> String
    go) Map k (Either String Int)
    x
              where go :: Int -> String
    go Int
    i = Set String -> String -> Int -> String
    mkUnique ([String] -> Set String
    forall a. Ord a => [a] -> Set a
    S.fromList ([String] -> Set String) -> [String] -> Set String
    forall a b. (a -> b) -> a -> b
    $ [Either String Int] -> [String]
    forall a b. [Either a b] -> [a]
    lefts ([Either String Int] -> [String])
    -> [Either String Int] -> [String]
    forall a b. (a -> b) -> a -> b
    $ Map k (Either String Int) -> [Either String Int]
    forall k a. Map k a -> [a]
    M.elems Map k (Either String Int)
    x) (Int -> String
    int2Name Int
    i) Int
    0
                    int2Name :: Int -> String
    int2Name Int
    i | Int
    q Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 = [Char
    letter]
                               | Bool
    otherwise = Char
    letter Char -> ShowS
    forall a. a -> [a] -> [a]
    : Int -> String
    forall a. Show a => a -> String
    show Int
    q
                        where (Int
    q,Int
    r) = Int -> Int -> (Int, Int)
    forall a. Integral a => a -> a -> (a, a)
    divMod Int
    i Int
    26
                              letter :: Char
    letter = Int -> Char
    forall a. Enum a => Int -> a
    toEnum (Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    'a' Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    r)

    prettyType :: JType -> TMonad String
    prettyType :: JType -> TMonad String
    prettyType JType
    x = do
      xt <- JType -> TMonad JType
    resolveType JType
    x
      names <- freeVarsWithNames xt
      let replaceNames (JTFree VarRef
    ref) = VarRef -> JType
    JTFree (VarRef -> JType) -> VarRef -> JType
    forall a b. (a -> b) -> a -> b
    $ VarRef -> VarRef
    forall {a}. (a, Int) -> VarRef
    fixRef VarRef
    ref
          replaceNames (JTForall [VarRef]
    refs JType
    t) = [VarRef] -> JType -> JType
    JTForall ((VarRef -> VarRef) -> [VarRef] -> [VarRef]
    forall a b. (a -> b) -> [a] -> [b]
    map VarRef -> VarRef
    forall {a}. (a, Int) -> VarRef
    fixRef [VarRef]
    refs) (JType -> JType) -> JType -> JType
    forall a b. (a -> b) -> a -> b
    $ JType -> JType
    replaceNames JType
    t
          replaceNames JType
    v = (JType -> JType) -> JType -> JType
    forall t. Compos1 t => (t -> t) -> t -> t
    composOp1 JType -> JType
    replaceNames JType
    v

          fixRef (a
    _,Int
    ref) = (Int -> Map Int String -> Maybe String
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup Int
    ref Map Int String
    names, Int
    ref)

          prettyConstraints Int
    ref = (Constraint -> String) -> [Constraint] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Constraint -> String
    go ([Constraint] -> [String])
    -> TMonad [Constraint] -> TMonad [String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VarRef -> TMonad [Constraint]
    lookupConstraintsList (Maybe String
    forall a. Maybe a
    Nothing, Int
    ref)
              where
                myName :: String
    myName = case Int -> Map Int String -> Maybe String
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup Int
    ref Map Int String
    names of
                           Just String
    n -> String
    n
                           Maybe String
    Nothing -> String
    "t_"String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++Int -> String
    forall a. Show a => a -> String
    show Int
    ref
                go :: Constraint -> String
    go (Sub JType
    t) = String
    myName String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " <: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Doc -> String
    forall a. Show a => a -> String
    show (Doc -> String) -> Doc -> String
    forall a b. (a -> b) -> a -> b
    $ JType -> Doc
    forall a. JsToDoc a => a -> Doc
    jsToDoc (JType -> Doc) -> JType -> Doc
    forall a b. (a -> b) -> a -> b
    $ JType -> JType
    replaceNames JType
    t)
                go (Super JType
    t) = (Doc -> String
    forall a. Show a => a -> String
    show (Doc -> String) -> Doc -> String
    forall a b. (a -> b) -> a -> b
    $ JType -> Doc
    forall a. JsToDoc a => a -> Doc
    jsToDoc (JType -> Doc) -> JType -> Doc
    forall a b. (a -> b) -> a -> b
    $ JType -> JType
    replaceNames JType
    t) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " <: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    myName

      constraintStrings <- nub . concat <$> mapM prettyConstraints (M.keys names)

      let constraintStr
              | [String] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    constraintStrings = String
    ""
              | Bool
    otherwise = String
    "(" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " [String]
    constraintStrings String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ") => "

      return $ constraintStr ++ (show . jsToDoc $ replaceNames xt)

    tyErr0 :: String -> TMonad a
    tyErr0 :: forall a. String -> TMonad a
    tyErr0 String
    x = String -> TMonad a
    forall a. String -> TMonad a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    x

    tyErr1 :: String -> JType -> TMonad b
    tyErr1 :: forall b. String -> JType -> TMonad b
    tyErr1 String
    s JType
    t = do
      st <- JType -> TMonad String
    prettyType JType
    t
      throwError $ s ++ ": " ++ st

    tyErr2ext :: String -> String -> String -> JType -> JType -> TMonad a
    tyErr2ext :: forall a. String -> String -> String -> JType -> JType -> TMonad a
    tyErr2ext String
    s String
    s1 String
    s2 JType
    t JType
    t' = do
      st <- JType -> TMonad String
    prettyType JType
    t
      st' <- prettyType t'
      throwError $ s ++ ". " ++ s1 ++ ": " ++ st ++ ", " ++ s2 ++ ": " ++ st'

    tyErr2Sub :: JType -> JType -> TMonad a
    tyErr2Sub :: forall a. JType -> JType -> TMonad a
    tyErr2Sub JType
    t JType
    t' = String -> String -> String -> JType -> JType -> TMonad a
    forall a. String -> String -> String -> JType -> JType -> TMonad a
    tyErr2ext String
    "Couldn't apply subtype relation" String
    "Subtype" String
    "Supertype" JType
    t JType
    t'

    prettyEnv :: TMonad [Map Ident String]
    prettyEnv :: TMonad [Map Ident String]
    prettyEnv = (Map Ident JType -> TMonad (Map Ident String))
    -> [Map Ident JType] -> TMonad [Map Ident String]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((JType -> TMonad String)
    -> Map Ident JType -> TMonad (Map Ident String)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Map Ident a -> m (Map Ident b)
    T.mapM JType -> TMonad String
    prettyType) ([Map Ident JType] -> TMonad [Map Ident String])
    -> (TCState -> [Map Ident JType])
    -> TCState
    -> TMonad [Map Ident String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> [Map Ident JType]
    tc_env (TCState -> TMonad [Map Ident String])
    -> TMonad TCState -> TMonad [Map Ident String]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TMonad TCState
    forall s (m :: * -> *). MonadState s m => m s
    get

    runTypecheckRaw :: JTypeCheck a => a -> (Either String JType, TCState)
    runTypecheckRaw :: forall a. JTypeCheck a => a -> (Either String JType, TCState)
    runTypecheckRaw a
    x = TMonad JType -> (Either String JType, TCState)
    forall a. TMonad a -> (Either String a, TCState)
    runTMonad (a -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheckMain a
    x)

    runTypecheckFull :: JTypeCheck a => a -> (Either String (String, [Map Ident String]), TCState)
    runTypecheckFull :: forall a.
    JTypeCheck a =>
    a -> (Either String (String, [Map Ident String]), TCState)
    runTypecheckFull a
    x = TMonad (String, [Map Ident String])
    -> (Either String (String, [Map Ident String]), TCState)
    forall a. TMonad a -> (Either String a, TCState)
    runTMonad (TMonad (String, [Map Ident String])
     -> (Either String (String, [Map Ident String]), TCState))
    -> TMonad (String, [Map Ident String])
    -> (Either String (String, [Map Ident String]), TCState)
    forall a b. (a -> b) -> a -> b
    $ do
                           r <- JType -> TMonad String
    prettyType (JType -> TMonad String) -> TMonad JType -> TMonad String
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< a -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheckMain a
    x
                           e <- prettyEnv
                           return (r,e)

    runTypecheck :: JTypeCheck a => a -> Either String String
    runTypecheck :: forall a. JTypeCheck a => a -> Either String String
    runTypecheck a
    x = TMonad String -> Either String String
    forall a. TMonad a -> Either String a
    evalTMonad (TMonad String -> Either String String)
    -> TMonad String -> Either String String
    forall a b. (a -> b) -> a -> b
    $ JType -> TMonad String
    prettyType (JType -> TMonad String) -> TMonad JType -> TMonad String
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< a -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheckMain a
    x

    evalTypecheck :: JTypeCheck a => a -> Either String [Map Ident String]
    evalTypecheck :: forall a. JTypeCheck a => a -> Either String [Map Ident String]
    evalTypecheck a
    x = TMonad [Map Ident String] -> Either String [Map Ident String]
    forall a. TMonad a -> Either String a
    evalTMonad (TMonad [Map Ident String] -> Either String [Map Ident String])
    -> TMonad [Map Ident String] -> Either String [Map Ident String]
    forall a b. (a -> b) -> a -> b
    $ do
                        _ <- a -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheckMain a
    x
                        e <- prettyEnv
                        return e

    typecheckMain :: JTypeCheck a => a -> TMonad JType
    typecheckMain :: forall a. JTypeCheck a => a -> TMonad JType
    typecheckMain a
    x = TMonad JType
    go TMonad JType -> (String -> TMonad JType) -> TMonad JType
    forall a. TMonad a -> (String -> TMonad a) -> TMonad a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` String -> TMonad JType
    forall a. String -> TMonad a
    handler
        where go :: TMonad JType
    go = do
                r <- a -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck a
    x
                setFrozen . S.unions . tc_stack =<< get
                tryCloseFrozenVars
                return r
              handler :: String -> TMonad b
    handler String
    e = do
                     cxt <- TCState -> [TMonad String]
    tc_context (TCState -> [TMonad String])
    -> TMonad TCState -> TMonad [TMonad String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TMonad TCState
    forall s (m :: * -> *). MonadState s m => m s
    get
                     throwError =<< (unlines . (e:) <$> sequence cxt)

    -- Manipulating VarRefs and Constraints

    addToStack :: Ord a => a -> [Set a] -> [Set a]
    addToStack :: forall a. Ord a => a -> [Set a] -> [Set a]
    addToStack a
    v (Set a
    s:[Set a]
    ss) = a -> Set a -> Set a
    forall a. Ord a => a -> Set a -> Set a
    S.insert a
    v Set a
    s Set a -> [Set a] -> [Set a]
    forall a. a -> [a] -> [a]
    : [Set a]
    ss
    addToStack a
    _ [Set a]
    _ = String -> [Set a]
    forall a. HasCallStack => String -> a
    error String
    "addToStack: no sets" --[S.singleton v]

    newVarRef :: TMonad VarRef
    newVarRef :: TMonad VarRef
    newVarRef = do
      v <- TCState -> Int
    tc_varCt (TCState -> Int) -> TMonad TCState -> TMonad Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TMonad TCState
    forall s (m :: * -> *). MonadState s m => m s
    get
      modify (\TCState
    s -> TCState
    s {tc_varCt = v + 1,
                       tc_stack = addToStack v (tc_stack s)})
      return $ (Nothing, v)

    newTyVar :: TMonad JType
    newTyVar :: TMonad JType
    newTyVar = VarRef -> JType
    JTFree (VarRef -> JType) -> TMonad VarRef -> TMonad JType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TMonad VarRef
    newVarRef

    mapConstraint :: (Monad m, Functor m) => (JType -> m JType) -> Constraint -> m Constraint
    mapConstraint :: forall (m :: * -> *).
    (Monad m, Functor m) =>
    (JType -> m JType) -> Constraint -> m Constraint
    mapConstraint JType -> m JType
    f (Sub JType
    t) = JType -> Constraint
    Sub (JType -> Constraint) -> m JType -> m Constraint
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> JType -> m JType
    f JType
    t
    mapConstraint JType -> m JType
    f (Super JType
    t) = JType -> Constraint
    Super (JType -> Constraint) -> m JType -> m Constraint
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> JType -> m JType
    f JType
    t

    partitionCs :: [Constraint] -> ([JType],[JType])
    partitionCs :: [Constraint] -> ([JType], [JType])
    partitionCs [] = ([],[])
    partitionCs (Sub JType
    t:[Constraint]
    cs) = (JType
    tJType -> [JType] -> [JType]
    forall a. a -> [a] -> [a]
    :[JType]
    subs,[JType]
    sups)
        where ([JType]
    subs,[JType]
    sups) = [Constraint] -> ([JType], [JType])
    partitionCs [Constraint]
    cs
    partitionCs (Super JType
    t:[Constraint]
    cs) = ([JType]
    subs,JType
    tJType -> [JType] -> [JType]
    forall a. a -> [a] -> [a]
    :[JType]
    sups)
        where ([JType]
    subs,[JType]
    sups) = [Constraint] -> ([JType], [JType])
    partitionCs [Constraint]
    cs

    --add mutation
    lookupConstraintsList :: VarRef -> TMonad [Constraint]
    lookupConstraintsList :: VarRef -> TMonad [Constraint]
    lookupConstraintsList vr :: VarRef
    vr@(Maybe String
    _,Int
    ref) = do
        vars <- TCState -> Map Int StoreVal
    tc_vars (TCState -> Map Int StoreVal)
    -> TMonad TCState -> TMonad (Map Int StoreVal)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TMonad TCState
    forall s (m :: * -> *). MonadState s m => m s
    get
        case M.lookup ref vars of
          (Just (SVConstrained Set Constraint
    cs)) -> (Constraint -> Bool) -> [Constraint] -> [Constraint]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Constraint -> Bool
    notLoop ([Constraint] -> [Constraint])
    -> ([Constraint] -> [Constraint]) -> [Constraint] -> [Constraint]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Constraint] -> [Constraint]
    forall a. Eq a => [a] -> [a]
    nub ([Constraint] -> [Constraint])
    -> TMonad [Constraint] -> TMonad [Constraint]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Constraint -> TMonad Constraint)
    -> [Constraint] -> TMonad [Constraint]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((JType -> TMonad JType) -> Constraint -> TMonad Constraint
    forall (m :: * -> *).
    (Monad m, Functor m) =>
    (JType -> m JType) -> Constraint -> m Constraint
    mapConstraint JType -> TMonad JType
    resolveType) (Set Constraint -> [Constraint]
    forall a. Set a -> [a]
    S.toList Set Constraint
    cs)
          (Just (SVType JType
    t)) -> String -> JType -> TMonad [Constraint]
    forall b. String -> JType -> TMonad b
    tyErr1 String
    "lookupConstraints on instantiated type" JType
    t
          Maybe StoreVal
    Nothing -> [Constraint] -> TMonad [Constraint]
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
      where
        notLoop :: Constraint -> Bool
    notLoop (Super (JTFree (Maybe String
    _,Int
    ref'))) | Int
    ref Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    ref' = Bool
    False
        notLoop (Sub   (JTFree (Maybe String
    _,Int
    ref'))) | Int
    ref Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    ref' = Bool
    False
        notLoop Constraint
    _ = Bool
    True

    -- if we instantiate a var to itself, then there's a good chance this results from a looping constraint -- we should be helpful and get rid of any such constraints.
    instantiateVarRef :: VarRef -> JType -> TMonad ()
    instantiateVarRef :: VarRef -> JType -> TMonad ()
    instantiateVarRef vr :: VarRef
    vr@(Maybe String
    _,Int
    ref) (JTFree (Maybe String
    _,Int
    ref')) | Int
    ref Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    ref' = do
        cs <- VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr
        let cs' = [Constraint] -> [Constraint]
    simplify [Constraint]
    cs
        modify (\TCState
    s -> TCState
    s {tc_vars = M.insert ref (SVConstrained (S.fromList cs')) (tc_vars s)})
      where simplify :: [Constraint] -> [Constraint]
    simplify (Sub   (JTFree (Maybe String
    _,Int
    r)):[Constraint]
    cs) | Int
    r Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    ref = [Constraint]
    cs
            simplify (Super (JTFree (Maybe String
    _,Int
    r)):[Constraint]
    cs) | Int
    r Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    ref = [Constraint]
    cs
            simplify (Constraint
    c:[Constraint]
    cs) = Constraint
    c Constraint -> [Constraint] -> [Constraint]
    forall a. a -> [a] -> [a]
    : [Constraint] -> [Constraint]
    simplify [Constraint]
    cs
            simplify [Constraint]
    x = [Constraint]
    x

    instantiateVarRef vr :: VarRef
    vr@(Maybe String
    _,Int
    ref) JType
    t = do
      Int -> JType -> TMonad ()
    occursCheck Int
    ref JType
    t
      cs <- VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr
      modify (\TCState
    s -> TCState
    s {tc_vars = M.insert ref (SVType t) (tc_vars s)})
      checkConstraints t cs

    occursCheck :: Int -> JType -> TMonad ()
    occursCheck :: Int -> JType -> TMonad ()
    occursCheck Int
    ref (JTFree (Maybe String
    _,Int
    i))
      | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    ref = String -> JType -> TMonad ()
    forall b. String -> JType -> TMonad b
    tyErr1 String
    "Occurs check: cannot construct infinite type" (VarRef -> JType
    JTFree (Maybe String
    forall a. Maybe a
    Nothing,Int
    i))
    occursCheck Int
    ref JType
    x = (JType -> TMonad ()) -> JType -> TMonad ()
    forall t (m :: * -> *).
    (Compos1 t, Monad m) =>
    (t -> m ()) -> t -> m ()
    composOpM1_ (Int -> JType -> TMonad ()
    occursCheck Int
    ref) JType
    x

    checkConstraints :: JType -> [Constraint] -> TMonad ()
    checkConstraints :: JType -> [Constraint] -> TMonad ()
    checkConstraints JType
    t [Constraint]
    cs = (Constraint -> TMonad ()) -> [Constraint] -> TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    mapM_ Constraint -> TMonad ()
    go [Constraint]
    cs
        where go :: Constraint -> TMonad ()
    go (Sub JType
    t2) = JType
    t JType -> JType -> TMonad ()
    <: JType
    t2
              go (Super JType
    t2) = JType
    t2 JType -> JType -> TMonad ()
    <: JType
    t

    addConstraint :: VarRef -> Constraint -> TMonad ()
    addConstraint :: VarRef -> Constraint -> TMonad ()
    addConstraint vr :: VarRef
    vr@(Maybe String
    _,Int
    ref) Constraint
    c = case Constraint
    c of
           Sub JType
    t -> case JType
    t of
                      JTFree VarRef
    _ -> Constraint -> TMonad ()
    addC Constraint
    c

                      JTForall [VarRef]
    vars JType
    t -> [Constraint] -> TMonad ()
    normalizeConstraints ([Constraint] -> TMonad ())
    -> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Constraint
    c Constraint -> [Constraint] -> [Constraint]
    forall a. a -> [a] -> [a]
    : ) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr

                      JTFunc [JType]
    args JType
    res -> do
                             (JType -> TMonad ()) -> [JType] -> TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    mapM_ (Int -> JType -> TMonad ()
    occursCheck Int
    ref) (JType
    resJType -> [JType] -> [JType]
    forall a. a -> [a] -> [a]
    :[JType]
    args)
                             [Constraint] -> TMonad ()
    normalizeConstraints ([Constraint] -> TMonad ())
    -> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Constraint
    c Constraint -> [Constraint] -> [Constraint]
    forall a. a -> [a] -> [a]
    :) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr

                      JTRecord JType
    t Map String JType
    m -> Int -> JType -> TMonad ()
    occursCheck Int
    ref JType
    t TMonad () -> TMonad () -> TMonad ()
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                      (JType -> TMonad ()) -> Map String JType -> TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    F.mapM_ (Int -> JType -> TMonad ()
    occursCheck Int
    ref) Map String JType
    m TMonad () -> TMonad () -> TMonad ()
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                      Either (Map String JType, JType) (Map String JType, JType)
    -> TMonad ()
    addRecConstraint ((Map String JType, JType)
    -> Either (Map String JType, JType) (Map String JType, JType)
    forall a b. a -> Either a b
    Left (Map String JType
    m,JType
    t))

                      JTList JType
    t' -> do
                             vr' <- TMonad VarRef
    newVarRef
                             addConstraint vr' (Sub t')
                             instantiateVarRef vr (JTList (JTFree vr'))

                      JTMap JType
    t' -> do
                             vr' <- TMonad VarRef
    newVarRef
                             addConstraint vr' (Sub t')
                             instantiateVarRef vr (JTMap (JTFree vr'))

                      JTRigid VarRef
    _ Set Constraint
    cs -> do
                             (subs,sups) <- [Constraint] -> ([JType], [JType])
    partitionCs ([Constraint] -> ([JType], [JType]))
    -> TMonad [Constraint] -> TMonad ([JType], [JType])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr
                             let (subs1,sups1) = partitionCs $ S.toList cs
                             when ((null sups1 && (not . null) sups) ||
                                   (null subs1 && (not . null) subs)) $ tyErr2Sub (JTFree vr) t
                             mapM_ (uncurry (<:)) [(x,y) | x <- subs, y <- subs1]
                             mapM_ (uncurry (<:)) [(y,x) | x <- sups, y <- sups1]

                             modify (\TCState
    s -> TCState
    s {tc_vars = M.insert ref (SVType t) (tc_vars s)}) --can all this be subsumed by a call to instantiate varref and casing on jtrigid carefully in the <: relationship?
                             -- a polymorphic var is a subtype of another if it is "bigger" on the lattice -- its subtypes are lower and supertypes are higher. sups a > sups b, subs a < subs b
                      JType
    _ -> VarRef -> JType -> TMonad ()
    instantiateVarRef VarRef
    vr JType
    t

           Super JType
    t -> case JType
    t of
                      JTFree VarRef
    _ -> Constraint -> TMonad ()
    addC Constraint
    c

                      JTForall [VarRef]
    vars JType
    t -> [Constraint] -> TMonad ()
    normalizeConstraints ([Constraint] -> TMonad ())
    -> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Constraint
    c Constraint -> [Constraint] -> [Constraint]
    forall a. a -> [a] -> [a]
    : ) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr

                      JTFunc [JType]
    args JType
    res -> do
                             (JType -> TMonad ()) -> [JType] -> TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    mapM_ (Int -> JType -> TMonad ()
    occursCheck Int
    ref) (JType
    resJType -> [JType] -> [JType]
    forall a. a -> [a] -> [a]
    :[JType]
    args)
                             [Constraint] -> TMonad ()
    normalizeConstraints ([Constraint] -> TMonad ())
    -> ([Constraint] -> [Constraint]) -> [Constraint] -> TMonad ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Constraint
    c Constraint -> [Constraint] -> [Constraint]
    forall a. a -> [a] -> [a]
    :) ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr

                      JTRecord JType
    t Map String JType
    m -> Int -> JType -> TMonad ()
    occursCheck Int
    ref JType
    t TMonad () -> TMonad () -> TMonad ()
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                      (JType -> TMonad ()) -> Map String JType -> TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    F.mapM_ (Int -> JType -> TMonad ()
    occursCheck Int
    ref) Map String JType
    m TMonad () -> TMonad () -> TMonad ()
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                      Either (Map String JType, JType) (Map String JType, JType)
    -> TMonad ()
    addRecConstraint ((Map String JType, JType)
    -> Either (Map String JType, JType) (Map String JType, JType)
    forall a b. b -> Either a b
    Right (Map String JType
    m,JType
    t))

                      JTList JType
    t' -> do
                             vr' <- TMonad VarRef
    newVarRef
                             addConstraint vr' (Super t')
                             instantiateVarRef vr (JTList (JTFree vr'))

                      JTMap JType
    t' -> do
                             vr' <- TMonad VarRef
    newVarRef
                             addConstraint vr' (Super t')
                             instantiateVarRef vr (JTMap (JTFree vr'))

                      JTRigid VarRef
    _ Set Constraint
    cs -> do
                             (subs,sups) <- [Constraint] -> ([JType], [JType])
    partitionCs ([Constraint] -> ([JType], [JType]))
    -> TMonad [Constraint] -> TMonad ([JType], [JType])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr
                             let (subs1,sups1) = partitionCs $ S.toList cs
                             when ((null sups1 && (not . null) sups) ||
                                   (null subs1 && (not . null) subs)) $ tyErr2Sub (JTFree vr) t
                             mapM_ (uncurry (<:)) [(y,x) | x <- subs, y <- subs1]
                             mapM_ (uncurry (<:)) [(x,y) | x <- sups, y <- sups1]

                             modify (\TCState
    s -> TCState
    s {tc_vars = M.insert ref (SVType t) (tc_vars s)}) --can all this be subsumed by a call to instantiate varref and casing on jtrigid carefully in the <: relationship?
                             -- a polymorphic var is a subtype of another if it is "bigger" on the lattice -- its subtypes are lower and supertypes are higher. sups a > sups b, subs a < subs b

                      JType
    _ -> VarRef -> JType -> TMonad ()
    instantiateVarRef VarRef
    vr JType
    t
        where
          putCs :: [Constraint] -> m ()
    putCs [Constraint]
    cs =
            (TCState -> TCState) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (\TCState
    s -> TCState
    s {tc_vars = M.insert ref (SVConstrained $ S.fromList $ cs) (tc_vars s)})

          addC :: Constraint -> TMonad ()
    addC Constraint
    constraint = do
            cs <- VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr
            modify (\TCState
    s -> TCState
    s {tc_vars = M.insert ref (SVConstrained (S.fromList $ constraint:cs)) (tc_vars s)})

          findRecordSubs :: [Constraint] -> ([(Map String JType, JType)], [Constraint])
    findRecordSubs [Constraint]
    cs = (Constraint -> Maybe (Map String JType, JType))
    -> [Constraint] -> ([(Map String JType, JType)], [Constraint])
    forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
    partitionOut Constraint -> Maybe (Map String JType, JType)
    go [Constraint]
    cs
              where go :: Constraint -> Maybe (Map String JType, JType)
    go (Sub (JTRecord JType
    t Map String JType
    m)) = (Map String JType, JType) -> Maybe (Map String JType, JType)
    forall a. a -> Maybe a
    Just (Map String JType
    m,JType
    t)
                    go Constraint
    _ = Maybe (Map String JType, JType)
    forall a. Maybe a
    Nothing

          findRecordSups :: [Constraint] -> ([(Map String JType, JType)], [Constraint])
    findRecordSups [Constraint]
    cs = (Constraint -> Maybe (Map String JType, JType))
    -> [Constraint] -> ([(Map String JType, JType)], [Constraint])
    forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
    partitionOut Constraint -> Maybe (Map String JType, JType)
    go [Constraint]
    cs
              where go :: Constraint -> Maybe (Map String JType, JType)
    go (Super (JTRecord JType
    t Map String JType
    m)) = (Map String JType, JType) -> Maybe (Map String JType, JType)
    forall a. a -> Maybe a
    Just (Map String JType
    m,JType
    t)
                    go Constraint
    _ = Maybe (Map String JType, JType)
    forall a. Maybe a
    Nothing

          --left is sub, right is super
          --There really should be at most one existing sub and sup constraint
          addRecConstraint :: Either (Map String JType, JType) (Map String JType, JType)
    -> TMonad ()
    addRecConstraint Either (Map String JType, JType) (Map String JType, JType)
    eM = do
            (subs,restCs) <- [Constraint] -> ([(Map String JType, JType)], [Constraint])
    findRecordSubs ([Constraint] -> ([(Map String JType, JType)], [Constraint]))
    -> TMonad [Constraint]
    -> TMonad ([(Map String JType, JType)], [Constraint])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr
            let (sups,restCs') = findRecordSups restCs

                mergeSubs [] = Maybe (Map key JType, JType)
    -> TMonad (Maybe (Map key JType, JType))
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Map key JType, JType)
    forall a. Maybe a
    Nothing
                mergeSubs [(Map key JType, JType)
    m] = Maybe (Map key JType, JType)
    -> TMonad (Maybe (Map key JType, JType))
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Map key JType, JType)
     -> TMonad (Maybe (Map key JType, JType)))
    -> Maybe (Map key JType, JType)
    -> TMonad (Maybe (Map key JType, JType))
    forall a b. (a -> b) -> a -> b
    $ (Map key JType, JType) -> Maybe (Map key JType, JType)
    forall a. a -> Maybe a
    Just (Map key JType, JType)
    m
                mergeSubs ((Map key JType, JType)
    m:[(Map key JType, JType)]
    ms) = (Map key JType, JType) -> Maybe (Map key JType, JType)
    forall a. a -> Maybe a
    Just ((Map key JType, JType) -> Maybe (Map key JType, JType))
    -> TMonad (Map key JType, JType)
    -> TMonad (Maybe (Map key JType, JType))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Map key JType, JType)
     -> (Map key JType, JType) -> TMonad (Map key JType, JType))
    -> (Map key JType, JType)
    -> [(Map key JType, JType)]
    -> TMonad (Map key JType, JType)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (\(Map key JType
    mp,JType
    t) (Map key JType
    mp',JType
    t') -> do
                                                      mp'' <- (JType -> JType -> TMonad JType)
    -> Map key JType -> Map key JType -> TMonad (Map key JType)
    forall (m :: * -> *) key val.
    (Monad m, Ord key) =>
    (val -> val -> m val)
    -> Map key val -> Map key val -> m (Map key val)
    unionWithM (\JType
    x JType
    y -> [JType] -> TMonad JType
    someLowerBound [JType
    x,JType
    y]) Map key JType
    mp Map key JType
    mp'
                                                      t'' <- someLowerBound [t,t']
                                                      return (mp'',t'')
                                                  ) (Map key JType, JType)
    m [(Map key JType, JType)]
    ms
                mergeSups [] = Maybe (Map key JType, JType)
    -> TMonad (Maybe (Map key JType, JType))
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Map key JType, JType)
    forall a. Maybe a
    Nothing
                mergeSups [(Map key JType, JType)
    m] = Maybe (Map key JType, JType)
    -> TMonad (Maybe (Map key JType, JType))
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Map key JType, JType)
     -> TMonad (Maybe (Map key JType, JType)))
    -> Maybe (Map key JType, JType)
    -> TMonad (Maybe (Map key JType, JType))
    forall a b. (a -> b) -> a -> b
    $ (Map key JType, JType) -> Maybe (Map key JType, JType)
    forall a. a -> Maybe a
    Just (Map key JType, JType)
    m
                mergeSups ((Map key JType, JType)
    m:[(Map key JType, JType)]
    ms) = (Map key JType, JType) -> Maybe (Map key JType, JType)
    forall a. a -> Maybe a
    Just ((Map key JType, JType) -> Maybe (Map key JType, JType))
    -> TMonad (Map key JType, JType)
    -> TMonad (Maybe (Map key JType, JType))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Map key JType, JType)
     -> (Map key JType, JType) -> TMonad (Map key JType, JType))
    -> (Map key JType, JType)
    -> [(Map key JType, JType)]
    -> TMonad (Map key JType, JType)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (\(Map key JType
    mp,JType
    t) (Map key JType
    mp',JType
    t') -> do
                                                                    mp'' <- (JType -> JType -> TMonad JType)
    -> Map key JType -> Map key JType -> TMonad (Map key JType)
    forall (m :: * -> *) key val b.
    (Monad m, Ord key) =>
    (val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
    intersectionWithM (\JType
    x JType
    y -> [JType] -> TMonad JType
    someUpperBound [JType
    x,JType
    y]) Map key JType
    mp Map key JType
    mp'
                                                                    t'' <- someUpperBound [t,t']
                                                                    return (mp'',t'')
                                                                ) (Map key JType, JType)
    m [(Map key JType, JType)]
    ms
            mbSub <- mergeSubs $ case eM of
                                   Left (Map String JType, JType)
    mt -> (Map String JType, JType)
    mt (Map String JType, JType)
    -> [(Map String JType, JType)] -> [(Map String JType, JType)]
    forall a. a -> [a] -> [a]
    : [(Map String JType, JType)]
    subs
                                   Either (Map String JType, JType) (Map String JType, JType)
    _ -> [(Map String JType, JType)]
    subs
            mbSup <- mergeSups $ case eM of
                                   Right (Map String JType, JType)
    mt -> (Map String JType, JType)
    mt (Map String JType, JType)
    -> [(Map String JType, JType)] -> [(Map String JType, JType)]
    forall a. a -> [a] -> [a]
    : [(Map String JType, JType)]
    sups
                                   Either (Map String JType, JType) (Map String JType, JType)
    _ -> [(Map String JType, JType)]
    sups
            normalizeConstraints =<< case (mbSub, mbSup) of
              (Just (Map String JType
    subm,JType
    subt), Just (Map String JType
    supm,JType
    supt)) -> do
                Bool -> TMonad () -> TMonad ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ (JType -> JType -> Bool)
    -> Map String JType -> Map String JType -> Bool
    forall k a b.
    Ord k =>
    (a -> b -> Bool) -> Map k a -> Map k b -> Bool
    M.isSubmapOfBy (\JType
    _ JType
    _ -> Bool
    True) Map String JType
    subm Map String JType
    supm) (TMonad () -> TMonad ()) -> TMonad () -> TMonad ()
    forall a b. (a -> b) -> a -> b
    $ String -> String -> String -> JType -> JType -> TMonad ()
    forall a. String -> String -> String -> JType -> JType -> TMonad a
    tyErr2ext String
    "Incompatible constraints" String
    "Subtype constraint" String
    "Supertype constraint" (JType -> Map String JType -> JType
    JTRecord JType
    subt Map String JType
    subm) (JType -> Map String JType -> JType
    JTRecord JType
    supt Map String JType
    supm)
                _ <- (JType -> JType -> TMonad ())
    -> Map String JType -> Map String JType -> TMonad (Map String ())
    forall (m :: * -> *) key val b.
    (Monad m, Ord key) =>
    (val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
    intersectionWithM (\JType
    x JType
    y -> JType
    y JType -> JType -> TMonad ()
    <: JType
    x) Map String JType
    subm Map String JType
    supm
                _ <- supt <: subt
                return $ Sub (JTRecord subt subm) : Super (JTRecord supt supm) : restCs'
              (Just (Map String JType
    subm,JType
    subt), Maybe (Map String JType, JType)
    Nothing)  -> [Constraint] -> TMonad [Constraint]
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Constraint] -> TMonad [Constraint])
    -> [Constraint] -> TMonad [Constraint]
    forall a b. (a -> b) -> a -> b
    $ JType -> Constraint
    Sub (JType -> Map String JType -> JType
    JTRecord JType
    subt Map String JType
    subm) Constraint -> [Constraint] -> [Constraint]
    forall a. a -> [a] -> [a]
    : [Constraint]
    restCs'
              (Maybe (Map String JType, JType)
    Nothing , Just (Map String JType
    supm,JType
    supt)) -> [Constraint] -> TMonad [Constraint]
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Constraint] -> TMonad [Constraint])
    -> [Constraint] -> TMonad [Constraint]
    forall a b. (a -> b) -> a -> b
    $ JType -> Constraint
    Super (JType -> Map String JType -> JType
    JTRecord JType
    supt Map String JType
    supm) Constraint -> [Constraint] -> [Constraint]
    forall a. a -> [a] -> [a]
    : [Constraint]
    restCs'
              (Maybe (Map String JType, JType), Maybe (Map String JType, JType))
    _ -> [Constraint] -> TMonad [Constraint]
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Constraint]
    restCs'

          --There really should be at most one existing sub and sup constraint
          normalizeConstraints :: [Constraint] -> TMonad ()
    normalizeConstraints [Constraint]
    cl = [Constraint] -> TMonad ()
    forall {m :: * -> *}. MonadState TCState m => [Constraint] -> m ()
    putCs ([Constraint] -> TMonad ()) -> TMonad [Constraint] -> TMonad ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Constraint] -> TMonad [Constraint]
    cannonicalizeConstraints [Constraint]
    cl

    cannonicalizeConstraints :: [Constraint] -> TMonad [Constraint]
    cannonicalizeConstraints :: [Constraint] -> TMonad [Constraint]
    cannonicalizeConstraints [Constraint]
    constraintList = do
            -- trace ("ccl: " ++ show constraintList) $ return ()
            let ([([VarRef], JType)]
    subs,[Constraint]
    restCs)  = [Constraint] -> ([([VarRef], JType)], [Constraint])
    findForallSubs [Constraint]
    constraintList
                ([([VarRef], JType)]
    sups,[Constraint]
    restCs') = [Constraint] -> ([([VarRef], JType)], [Constraint])
    findForallSups [Constraint]
    restCs
            mbSub <- [([VarRef], JType)] -> TMonad (Maybe JType)
    mergeSubs [([VarRef], JType)]
    subs
            mbSup <- mergeSups sups
            case (mbSub, mbSup) of
              (Just JType
    sub, Just JType
    sup) -> do
                JType
    sup JType -> JType -> TMonad ()
    <: JType
    sub
                [Constraint] -> TMonad [Constraint]
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Constraint] -> TMonad [Constraint])
    -> [Constraint] -> TMonad [Constraint]
    forall a b. (a -> b) -> a -> b
    $ JType -> Constraint
    Sub JType
    sub Constraint -> [Constraint] -> [Constraint]
    forall a. a -> [a] -> [a]
    : JType -> Constraint
    Super JType
    sup Constraint -> [Constraint] -> [Constraint]
    forall a. a -> [a] -> [a]
    : [Constraint]
    restCs'
              (Just JType
    sub, Maybe JType
    Nothing)  -> [Constraint] -> TMonad [Constraint]
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Constraint] -> TMonad [Constraint])
    -> [Constraint] -> TMonad [Constraint]
    forall a b. (a -> b) -> a -> b
    $ JType -> Constraint
    Sub JType
    sub Constraint -> [Constraint] -> [Constraint]
    forall a. a -> [a] -> [a]
    : [Constraint]
    restCs'
              (Maybe JType
    Nothing , Just JType
    sup) -> [Constraint] -> TMonad [Constraint]
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Constraint] -> TMonad [Constraint])
    -> [Constraint] -> TMonad [Constraint]
    forall a b. (a -> b) -> a -> b
    $ JType -> Constraint
    Super JType
    sup Constraint -> [Constraint] -> [Constraint]
    forall a. a -> [a] -> [a]
    : [Constraint]
    restCs'
              (Maybe JType, Maybe JType)
    _ -> [Constraint] -> TMonad [Constraint]
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Constraint]
    restCs'
      where

        findForallSubs :: [Constraint] -> ([([VarRef], JType)], [Constraint])
    findForallSubs [Constraint]
    cs = (Constraint -> Maybe ([VarRef], JType))
    -> [Constraint] -> ([([VarRef], JType)], [Constraint])
    forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
    partitionOut Constraint -> Maybe ([VarRef], JType)
    go [Constraint]
    cs
          where go :: Constraint -> Maybe ([VarRef], JType)
    go (Sub (JTForall [VarRef]
    vars JType
    t)) = ([VarRef], JType) -> Maybe ([VarRef], JType)
    forall a. a -> Maybe a
    Just ([VarRef]
    vars,JType
    t)
                go (Sub (JTFree VarRef
    _)) = Maybe ([VarRef], JType)
    forall a. Maybe a
    Nothing
                go (Sub JType
    x) = ([VarRef], JType) -> Maybe ([VarRef], JType)
    forall a. a -> Maybe a
    Just ([],JType
    x)
                go Constraint
    _ = Maybe ([VarRef], JType)
    forall a. Maybe a
    Nothing

        findForallSups :: [Constraint] -> ([([VarRef], JType)], [Constraint])
    findForallSups [Constraint]
    cs = (Constraint -> Maybe ([VarRef], JType))
    -> [Constraint] -> ([([VarRef], JType)], [Constraint])
    forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
    partitionOut Constraint -> Maybe ([VarRef], JType)
    go [Constraint]
    cs
          where go :: Constraint -> Maybe ([VarRef], JType)
    go (Super (JTForall [VarRef]
    vars JType
    t)) = ([VarRef], JType) -> Maybe ([VarRef], JType)
    forall a. a -> Maybe a
    Just ([VarRef]
    vars,JType
    t)
                go (Super (JTFree VarRef
    _)) = Maybe ([VarRef], JType)
    forall a. Maybe a
    Nothing
                go (Super JType
    x) = ([VarRef], JType) -> Maybe ([VarRef], JType)
    forall a. a -> Maybe a
    Just ([],JType
    x)
                go Constraint
    _ = Maybe ([VarRef], JType)
    forall a. Maybe a
    Nothing

        findFuncs :: [JType] -> ([([JType], JType)], [JType])
    findFuncs [JType]
    cs = (JType -> Maybe ([JType], JType))
    -> [JType] -> ([([JType], JType)], [JType])
    forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
    partitionOut JType -> Maybe ([JType], JType)
    go [JType]
    cs
            where go :: JType -> Maybe ([JType], JType)
    go (JTFunc [JType]
    args JType
    ret) = ([JType], JType) -> Maybe ([JType], JType)
    forall a. a -> Maybe a
    Just ([JType]
    args, JType
    ret)
                  go JType
    _ = Maybe ([JType], JType)
    forall a. Maybe a
    Nothing

        mergeSubs :: [([VarRef], JType)] -> TMonad (Maybe JType)
    mergeSubs [] = Maybe JType -> TMonad (Maybe JType)
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe JType
    forall a. Maybe a
    Nothing
        mergeSubs [([],JType
    t)] = Maybe JType -> TMonad (Maybe JType)
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe JType -> TMonad (Maybe JType))
    -> Maybe JType -> TMonad (Maybe JType)
    forall a b. (a -> b) -> a -> b
    $ JType -> Maybe JType
    forall a. a -> Maybe a
    Just (JType -> Maybe JType) -> JType -> Maybe JType
    forall a b. (a -> b) -> a -> b
    $ JType
    t
        mergeSubs [([VarRef], JType)
    s] = Maybe JType -> TMonad (Maybe JType)
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe JType -> TMonad (Maybe JType))
    -> Maybe JType -> TMonad (Maybe JType)
    forall a b. (a -> b) -> a -> b
    $ JType -> Maybe JType
    forall a. a -> Maybe a
    Just (JType -> Maybe JType) -> JType -> Maybe JType
    forall a b. (a -> b) -> a -> b
    $ ([VarRef] -> JType -> JType) -> ([VarRef], JType) -> JType
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry [VarRef] -> JType -> JType
    JTForall ([VarRef], JType)
    s
        mergeSubs [([VarRef], JType)]
    ss = do
          rt <- TMonad JType
    newTyVar
          (_,frame) <- withLocalScope $ do
              instantiatedTypes <- mapM (uncurry instantiateScheme) ss
              let (funcTypes, otherTypes) = findFuncs instantiatedTypes
              when (not . null $ funcTypes) $ do
                         let (argss,rets) = unzip funcTypes
                             lft = [([JType], JType)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [([JType], JType)]
    funcTypes
                         args' <- mapM someUpperBound $ filter ((== lft) . length) $ transpose argss
                         ret'  <- someLowerBound rets
                         rt <: JTFunc args' ret'
              mapM_ (rt <:) otherTypes
    --        ((args',ret'):_,o:_) -> tyErr2ext "Incompatible Subtype Constraints" "Subtype constraint" "Subtype constraint" (JTFunc args' ret') o
          rt' <- resolveType rt
          case rt' of
            (JTFunc [JType]
    args JType
    res) -> do
              freeVarsInArgs <- [Set Int] -> Set Int
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    S.unions ([Set Int] -> Set Int) -> TMonad [Set Int] -> TMonad (Set Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (JType -> TMonad (Set Int)) -> [JType] -> TMonad [Set Int]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM JType -> TMonad (Set Int)
    freeVars [JType]
    args
              freeVarsInRes  <- freeVars res
              setFrozen $ frame `S.difference` (freeVarsInArgs `S.intersection` freeVarsInRes)
            JType
    _ -> Set Int -> TMonad ()
    setFrozen Set Int
    frame
          -- tryCloseFrozenVars
          Just <$> resolveType (JTForall (frame2VarRefs frame) rt')

        mergeSups :: [([VarRef], JType)] -> TMonad (Maybe JType)
    mergeSups [] = Maybe JType -> TMonad (Maybe JType)
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe JType
    forall a. Maybe a
    Nothing
        mergeSups [([],JType
    t)] = Maybe JType -> TMonad (Maybe JType)
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe JType -> TMonad (Maybe JType))
    -> Maybe JType -> TMonad (Maybe JType)
    forall a b. (a -> b) -> a -> b
    $ JType -> Maybe JType
    forall a. a -> Maybe a
    Just (JType -> Maybe JType) -> JType -> Maybe JType
    forall a b. (a -> b) -> a -> b
    $ JType
    t
        mergeSups [([VarRef], JType)
    s] = Maybe JType -> TMonad (Maybe JType)
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe JType -> TMonad (Maybe JType))
    -> Maybe JType -> TMonad (Maybe JType)
    forall a b. (a -> b) -> a -> b
    $ JType -> Maybe JType
    forall a. a -> Maybe a
    Just (JType -> Maybe JType) -> JType -> Maybe JType
    forall a b. (a -> b) -> a -> b
    $ ([VarRef] -> JType -> JType) -> ([VarRef], JType) -> JType
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry [VarRef] -> JType -> JType
    JTForall ([VarRef], JType)
    s
        mergeSups [([VarRef], JType)]
    ss = do
          rt <- TMonad JType
    newTyVar
          (_,frame) <- withLocalScope $ do
               instantiatedTypes <- mapM (uncurry instantiateScheme) ss
               let (funcTypes, otherTypes) = findFuncs instantiatedTypes
               when (not . null $ funcTypes) $ do
                         let (argss,rets) = unzip funcTypes
                         args' <- mapM someLowerBound $ transpose argss
                         ret'  <- someUpperBound rets
                         rt <: JTFunc args' ret'
               mapM_ (<: rt) otherTypes
    --        ((args',ret'):_,o:_) -> tyErr2ext "Incompatible Supertype Constraints" "Supertype constraint" ("Supertype constraint" ++ show o) (JTFunc args' ret') o
          rt' <- resolveType rt

          case rt' of
            (JTFunc [JType]
    args JType
    res) -> do
              freeVarsInArgs <- [Set Int] -> Set Int
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    S.unions ([Set Int] -> Set Int) -> TMonad [Set Int] -> TMonad (Set Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (JType -> TMonad (Set Int)) -> [JType] -> TMonad [Set Int]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM JType -> TMonad (Set Int)
    freeVars [JType]
    args
              freeVarsInRes  <- freeVars res
              setFrozen $ frame `S.difference` (freeVarsInArgs `S.intersection` freeVarsInRes)
            JType
    _ -> Set Int -> TMonad ()
    setFrozen Set Int
    frame
          -- tryCloseFrozenVars
          Just <$> resolveType (JTForall (frame2VarRefs frame) rt')

    tryCloseFrozenVars :: TMonad ()
    tryCloseFrozenVars :: TMonad ()
    tryCloseFrozenVars = ReaderT [Either Int Int] TMonad () -> [Either Int Int] -> TMonad ()
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT (Set Int -> ReaderT [Either Int Int] TMonad ()
    loop (Set Int -> ReaderT [Either Int Int] TMonad ())
    -> (TCState -> Set Int)
    -> TCState
    -> ReaderT [Either Int Int] TMonad ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> Set Int
    tc_frozen (TCState -> ReaderT [Either Int Int] TMonad ())
    -> ReaderT [Either Int Int] TMonad TCState
    -> ReaderT [Either Int Int] TMonad ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ReaderT [Either Int Int] TMonad TCState
    forall s (m :: * -> *). MonadState s m => m s
    get) []
        where
          loop :: Set Int -> ReaderT [Either Int Int] TMonad ()
    loop Set Int
    frozen = do
            (Int -> ReaderT [Either Int Int] TMonad ())
    -> [Int] -> ReaderT [Either Int Int] TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    mapM_ Int -> ReaderT [Either Int Int] TMonad ()
    go ([Int] -> ReaderT [Either Int Int] TMonad ())
    -> [Int] -> ReaderT [Either Int Int] TMonad ()
    forall a b. (a -> b) -> a -> b
    $ Set Int -> [Int]
    forall a. Set a -> [a]
    S.toList Set Int
    frozen
            newFrozen <- TCState -> Set Int
    tc_frozen (TCState -> Set Int)
    -> ReaderT [Either Int Int] TMonad TCState
    -> ReaderT [Either Int Int] TMonad (Set Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TMonad TCState -> ReaderT [Either Int Int] TMonad TCState
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ReaderT [Either Int Int] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TMonad TCState
    forall s (m :: * -> *). MonadState s m => m s
    get
            if S.null (newFrozen  `S.difference` frozen)
               then return ()
               else loop newFrozen
          go :: Int -> ReaderT [Either Int Int] TMonad ()
          go :: Int -> ReaderT [Either Int Int] TMonad ()
    go Int
    i = do
            s <- ReaderT [Either Int Int] TMonad [Either Int Int]
    forall r (m :: * -> *). MonadReader r m => m r
    ask
            case findLoop i s of
              -- if no set is returned, then that means we just return (i.e. the constraint is dull)
              Just Maybe [Int]
    Nothing  -> () -> ReaderT [Either Int Int] TMonad ()
    forall a. a -> ReaderT [Either Int Int] TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
              -- if a set is returned, then all vars in the set should be tied together
              Just (Just [Int]
    vrs) -> [Int] -> ReaderT [Either Int Int] TMonad ()
    unifyGroup [Int]
    vrs
              Maybe (Maybe [Int])
    Nothing       -> do
                  t <- TMonad JType -> ReaderT [Either Int Int] TMonad JType
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ReaderT [Either Int Int] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TMonad JType -> ReaderT [Either Int Int] TMonad JType)
    -> TMonad JType -> ReaderT [Either Int Int] TMonad JType
    forall a b. (a -> b) -> a -> b
    $ JType -> TMonad JType
    resolveTypeShallow (VarRef -> JType
    JTFree (Maybe String
    forall a. Maybe a
    Nothing, Int
    i))
                  case t of
                    (JTFree VarRef
    vr) -> do
                         l <- VarRef -> ReaderT [Either Int Int] TMonad [Constraint]
    tryClose VarRef
    vr
                         case l of
                           [] -> () -> ReaderT [Either Int Int] TMonad ()
    forall a. a -> ReaderT [Either Int Int] TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                           [Constraint]
    cl -> do
                             (Constraint -> ReaderT [Either Int Int] TMonad ())
    -> [Constraint] -> ReaderT [Either Int Int] TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    mapM_ (VarRef -> Constraint -> ReaderT [Either Int Int] TMonad ()
    forall {a}.
    (a, Int) -> Constraint -> ReaderT [Either Int Int] TMonad ()
    go' VarRef
    vr) [Constraint]
    cl
                             TMonad () -> ReaderT [Either Int Int] TMonad ()
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ReaderT [Either Int Int] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ((Constraint -> TMonad Constraint) -> [Constraint] -> TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    mapM_ ((JType -> TMonad JType) -> Constraint -> TMonad Constraint
    forall (m :: * -> *).
    (Monad m, Functor m) =>
    (JType -> m JType) -> Constraint -> m Constraint
    mapConstraint JType -> TMonad JType
    resolveType) [Constraint]
    cl)
                              -- not clear if we need to call again. if we resolve any constraints, they should point us back upwards...
                             --if cl remains free, recannonicalize it?
                    JType
    _ -> () -> ReaderT [Either Int Int] TMonad ()
    forall a. a -> ReaderT [Either Int Int] TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          -- Left is super, right is sub
          go' :: (a, Int) -> Constraint -> ReaderT [Either Int Int] TMonad ()
    go' (a
    _,Int
    ref) (Sub (JTFree (Maybe String
    _,Int
    i)))
              | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    ref = () -> ReaderT [Either Int Int] TMonad ()
    forall a. a -> ReaderT [Either Int Int] TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
              | Bool
    otherwise = -- trace (show ("super: " ++ show (ref,i))) $
                            ([Either Int Int] -> [Either Int Int])
    -> ReaderT [Either Int Int] TMonad ()
    -> ReaderT [Either Int Int] TMonad ()
    forall a.
    ([Either Int Int] -> [Either Int Int])
    -> ReaderT [Either Int Int] TMonad a
    -> ReaderT [Either Int Int] TMonad a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\[Either Int Int]
    s -> Int -> Either Int Int
    forall a b. a -> Either a b
    Left Int
    ref Either Int Int -> [Either Int Int] -> [Either Int Int]
    forall a. a -> [a] -> [a]
    : [Either Int Int]
    s) (ReaderT [Either Int Int] TMonad ()
     -> ReaderT [Either Int Int] TMonad ())
    -> ReaderT [Either Int Int] TMonad ()
    -> ReaderT [Either Int Int] TMonad ()
    forall a b. (a -> b) -> a -> b
    $ Int -> ReaderT [Either Int Int] TMonad ()
    go Int
    i
          go' (a
    _,Int
    ref) (Super (JTFree (Maybe String
    _,Int
    i)))
              | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    ref = () -> ReaderT [Either Int Int] TMonad ()
    forall a. a -> ReaderT [Either Int Int] TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
              | Bool
    otherwise = -- trace (show ("sub: " ++ show (ref,i))) $
                            ([Either Int Int] -> [Either Int Int])
    -> ReaderT [Either Int Int] TMonad ()
    -> ReaderT [Either Int Int] TMonad ()
    forall a.
    ([Either Int Int] -> [Either Int Int])
    -> ReaderT [Either Int Int] TMonad a
    -> ReaderT [Either Int Int] TMonad a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (\[Either Int Int]
    s -> Int -> Either Int Int
    forall a b. b -> Either a b
    Right Int
    ref Either Int Int -> [Either Int Int] -> [Either Int Int]
    forall a. a -> [a] -> [a]
    : [Either Int Int]
    s) (ReaderT [Either Int Int] TMonad ()
     -> ReaderT [Either Int Int] TMonad ())
    -> ReaderT [Either Int Int] TMonad ()
    -> ReaderT [Either Int Int] TMonad ()
    forall a b. (a -> b) -> a -> b
    $ Int -> ReaderT [Either Int Int] TMonad ()
    go Int
    i
          go' (a, Int)
    _ Constraint
    _ = () -> ReaderT [Either Int Int] TMonad ()
    forall a. a -> ReaderT [Either Int Int] TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

          unifyGroup :: [Int] -> ReaderT [Either Int Int] TMonad ()
          unifyGroup :: [Int] -> ReaderT [Either Int Int] TMonad ()
    unifyGroup (Int
    vr:[Int]
    vrs) = TMonad () -> ReaderT [Either Int Int] TMonad ()
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ReaderT [Either Int Int] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TMonad () -> ReaderT [Either Int Int] TMonad ())
    -> TMonad () -> ReaderT [Either Int Int] TMonad ()
    forall a b. (a -> b) -> a -> b
    $ (Int -> TMonad ()) -> [Int] -> TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    mapM_ (\Int
    x -> VarRef -> JType -> TMonad ()
    instantiateVarRef (Maybe String
    forall a. Maybe a
    Nothing, Int
    x) (VarRef -> JType
    JTFree (Maybe String
    forall a. Maybe a
    Nothing,Int
    vr))) [Int]
    vrs
          unifyGroup [] = () -> ReaderT [Either Int Int] TMonad ()
    forall a. a -> ReaderT [Either Int Int] TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

          findLoop :: p -> [Either p p] -> Maybe (Maybe [p])
    findLoop p
    i cs :: [Either p p]
    cs@(Either p p
    c:[Either p p]
    _) = [p] -> [Either p p] -> Maybe (Maybe [p])
    go [] [Either p p]
    cs
              where
                cTyp :: Bool
    cTyp = Either p p -> Bool
    forall a b. Either a b -> Bool
    eitherIsLeft Either p p
    c
                go :: [p] -> [Either p p] -> Maybe (Maybe [p])
    go [p]
    accum (Either p p
    r:[Either p p]
    rs)
                   | (p -> p) -> (p -> p) -> Either p p -> p
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either p -> p
    forall a. a -> a
    id p -> p
    forall a. a -> a
    id Either p p
    r p -> p -> Bool
    forall a. Eq a => a -> a -> Bool
    == p
    i Bool -> Bool -> Bool
    && Either p p -> Bool
    forall a b. Either a b -> Bool
    eitherIsLeft Either p p
    r Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    cTyp = Maybe [p] -> Maybe (Maybe [p])
    forall a. a -> Maybe a
    Just (Maybe [p] -> Maybe (Maybe [p])) -> Maybe [p] -> Maybe (Maybe [p])
    forall a b. (a -> b) -> a -> b
    $ [p] -> Maybe [p]
    forall a. a -> Maybe a
    Just ((p -> p) -> (p -> p) -> Either p p -> p
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either p -> p
    forall a. a -> a
    id p -> p
    forall a. a -> a
    id Either p p
    r p -> [p] -> [p]
    forall a. a -> [a] -> [a]
    : [p]
    accum)
                      -- i.e. there's a cycle to close
                   | (p -> p) -> (p -> p) -> Either p p -> p
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either p -> p
    forall a. a -> a
    id p -> p
    forall a. a -> a
    id Either p p
    r p -> p -> Bool
    forall a. Eq a => a -> a -> Bool
    == p
    i = Maybe [p] -> Maybe (Maybe [p])
    forall a. a -> Maybe a
    Just Maybe [p]
    forall a. Maybe a
    Nothing
                      -- i.e. there's a "dull" cycle
                   | Either p p -> Bool
    forall a b. Either a b -> Bool
    eitherIsLeft Either p p
    r Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Bool
    cTyp = Maybe (Maybe [p])
    forall a. Maybe a
    Nothing -- we stop looking for a cycle because the chain is broken
                   | Bool
    otherwise = [p] -> [Either p p] -> Maybe (Maybe [p])
    go ((p -> p) -> (p -> p) -> Either p p -> p
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either p -> p
    forall a. a -> a
    id p -> p
    forall a. a -> a
    id Either p p
    r p -> [p] -> [p]
    forall a. a -> [a] -> [a]
    : [p]
    accum) [Either p p]
    rs
                go [p]
    _ [] = Maybe (Maybe [p])
    forall a. Maybe a
    Nothing

          findLoop p
    i [] = Maybe (Maybe [p])
    forall a. Maybe a
    Nothing

          tryClose :: VarRef -> ReaderT [Either Int Int] TMonad [Constraint]
    tryClose vr :: VarRef
    vr@(Maybe String
    _,Int
    i) = do
            cl <- TMonad [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ReaderT [Either Int Int] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift(TMonad [Constraint]
     -> ReaderT [Either Int Int] TMonad [Constraint])
    -> TMonad [Constraint]
    -> ReaderT [Either Int Int] TMonad [Constraint]
    forall a b. (a -> b) -> a -> b
    $ [Constraint] -> TMonad [Constraint]
    cannonicalizeConstraints ([Constraint] -> TMonad [Constraint])
    -> TMonad [Constraint] -> TMonad [Constraint]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr
            -- trace ("tryclose: " ++ show vr) $ trace (show cl) $ return ()
            case partitionCs cl of
              ([JType]
    _,[JType
    s]) -> TMonad () -> ReaderT [Either Int Int] TMonad ()
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ReaderT [Either Int Int] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (VarRef -> JType -> TMonad ()
    instantiateVarRef VarRef
    vr JType
    s) ReaderT [Either Int Int] TMonad ()
    -> ReaderT [Either Int Int] TMonad ()
    -> ReaderT [Either Int Int] TMonad ()
    forall a b.
    ReaderT [Either Int Int] TMonad a
    -> ReaderT [Either Int Int] TMonad b
    -> ReaderT [Either Int Int] TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Int -> ReaderT [Either Int Int] TMonad ()
    go Int
    i ReaderT [Either Int Int] TMonad ()
    -> ReaderT [Either Int Int] TMonad [Constraint]
    -> ReaderT [Either Int Int] TMonad [Constraint]
    forall a b.
    ReaderT [Either Int Int] TMonad a
    -> ReaderT [Either Int Int] TMonad b
    -> ReaderT [Either Int Int] TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
    forall a. a -> ReaderT [Either Int Int] TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] -- prefer lower bound (supertype constraint)
              ([JType
    s],[JType]
    _) -> TMonad () -> ReaderT [Either Int Int] TMonad ()
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ReaderT [Either Int Int] m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (VarRef -> JType -> TMonad ()
    instantiateVarRef VarRef
    vr JType
    s) ReaderT [Either Int Int] TMonad ()
    -> ReaderT [Either Int Int] TMonad ()
    -> ReaderT [Either Int Int] TMonad ()
    forall a b.
    ReaderT [Either Int Int] TMonad a
    -> ReaderT [Either Int Int] TMonad b
    -> ReaderT [Either Int Int] TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Int -> ReaderT [Either Int Int] TMonad ()
    go Int
    i ReaderT [Either Int Int] TMonad ()
    -> ReaderT [Either Int Int] TMonad [Constraint]
    -> ReaderT [Either Int Int] TMonad [Constraint]
    forall a b.
    ReaderT [Either Int Int] TMonad a
    -> ReaderT [Either Int Int] TMonad b
    -> ReaderT [Either Int Int] TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
    forall a. a -> ReaderT [Either Int Int] TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
              ([JType], [JType])
    _ -> [Constraint] -> ReaderT [Either Int Int] TMonad [Constraint]
    forall a. a -> ReaderT [Either Int Int] TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Constraint]
    cl

    -- Manipulating the environment
    withLocalScope :: TMonad a -> TMonad (a, Set Int)
    withLocalScope :: forall a. TMonad a -> TMonad (a, Set Int)
    withLocalScope TMonad a
    act = do
      (TCState -> TCState) -> TMonad ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (\TCState
    s -> TCState
    s {tc_env   = M.empty : tc_env s,
                       tc_stack = S.empty : tc_stack s})
      res <- TMonad a
    act
      frame <- head . tc_stack <$> get
      modify (\TCState
    s -> TCState
    s {tc_env   = drop 1 $ tc_env s,
                       tc_stack = drop 1 $ tc_stack s})
      return (res, frame)

    setFrozen :: Set Int -> TMonad ()
    setFrozen :: Set Int -> TMonad ()
    setFrozen Set Int
    x = (TCState -> TCState) -> TMonad ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (\TCState
    s -> TCState
    s {tc_frozen = tc_frozen s `S.union` x})

    -- addRefsToStack x = modify (\s -> s {tc_stack = F.foldr addToStack (tc_stack s) x })

    frame2VarRefs :: Set t -> [(Maybe a, t)]
    frame2VarRefs :: forall t a. Set t -> [(Maybe a, t)]
    frame2VarRefs Set t
    frame = (\t
    x -> (Maybe a
    forall a. Maybe a
    Nothing,t
    x)) (t -> (Maybe a, t)) -> [t] -> [(Maybe a, t)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Set t -> [t]
    forall a. Set a -> [a]
    S.toList Set t
    frame

    addEnv :: Ident -> JType -> TMonad ()
    addEnv :: Ident -> JType -> TMonad ()
    addEnv Ident
    ident JType
    typ = do
      envstack <- TCState -> [Map Ident JType]
    tc_env (TCState -> [Map Ident JType])
    -> TMonad TCState -> TMonad [Map Ident JType]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TMonad TCState
    forall s (m :: * -> *). MonadState s m => m s
    get
      case envstack of
        (Map Ident JType
    e:[Map Ident JType]
    es) -> (TCState -> TCState) -> TMonad ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (\TCState
    s -> TCState
    s {tc_env = M.insert ident typ e : es}) -- we clobber/shadow var names
        [Map Ident JType]
    _ -> String -> TMonad ()
    forall a. String -> TMonad a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    "empty env stack (this should never happen)"

    newVarDecl :: Ident -> TMonad JType
    newVarDecl :: Ident -> TMonad JType
    newVarDecl Ident
    ident = do
      v <- TMonad JType
    newTyVar
      addEnv ident v
      return v

    resolveTypeGen :: ((JType -> TMonad JType) -> JType -> TMonad JType) -> JType -> TMonad JType
    resolveTypeGen :: ((JType -> TMonad JType) -> JType -> TMonad JType)
    -> JType -> TMonad JType
    resolveTypeGen (JType -> TMonad JType) -> JType -> TMonad JType
    f JType
    typ = JType -> TMonad JType
    go JType
    typ
        where
          go :: JType -> TMonad JType
          go :: JType -> TMonad JType
    go x :: JType
    x@(JTFree (Maybe String
    _, Int
    ref)) = do
            vars <- TCState -> Map Int StoreVal
    tc_vars (TCState -> Map Int StoreVal)
    -> TMonad TCState -> TMonad (Map Int StoreVal)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TMonad TCState
    forall s (m :: * -> *). MonadState s m => m s
    get
            case M.lookup ref vars of
              Just (SVType JType
    t) -> do
                res <- JType -> TMonad JType
    go JType
    t
                when (res /= t) $ modify (\TCState
    s -> TCState
    s {tc_vars = M.insert ref (SVType res) $ tc_vars s}) --mutation, shortcuts pointer chasing
                return res
              Maybe StoreVal
    _ -> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    x

          -- | Eliminates resolved vars from foralls, eliminates empty foralls.
          go (JTForall [VarRef]
    refs JType
    t) = do
            refs' <- [Maybe VarRef] -> [VarRef]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe VarRef] -> [VarRef])
    -> TMonad [Maybe VarRef] -> TMonad [VarRef]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (VarRef -> TMonad (Maybe VarRef))
    -> [VarRef] -> TMonad [Maybe VarRef]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM VarRef -> TMonad (Maybe VarRef)
    forall {m :: * -> *} {a}.
    MonadState TCState m =>
    (a, Int) -> m (Maybe (a, Int))
    checkRef [VarRef]
    refs
            if null refs'
               then go t
               else JTForall refs' <$> go t
          go JType
    x = (JType -> TMonad JType) -> JType -> TMonad JType
    f JType -> TMonad JType
    go JType
    x

          checkRef :: (a, Int) -> m (Maybe (a, Int))
    checkRef x :: (a, Int)
    x@(a
    _, Int
    ref) = do
            vars <- TCState -> Map Int StoreVal
    tc_vars (TCState -> Map Int StoreVal) -> m TCState -> m (Map Int StoreVal)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m TCState
    forall s (m :: * -> *). MonadState s m => m s
    get
            case M.lookup ref vars of
              Just (SVType JType
    t) -> Maybe (a, Int) -> m (Maybe (a, Int))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (a, Int)
    forall a. Maybe a
    Nothing
              Maybe StoreVal
    _ -> Maybe (a, Int) -> m (Maybe (a, Int))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (a, Int) -> m (Maybe (a, Int)))
    -> Maybe (a, Int) -> m (Maybe (a, Int))
    forall a b. (a -> b) -> a -> b
    $ (a, Int) -> Maybe (a, Int)
    forall a. a -> Maybe a
    Just (a, Int)
    x

    resolveType :: JType -> TMonad JType
    resolveType = ((JType -> TMonad JType) -> JType -> TMonad JType)
    -> JType -> TMonad JType
    resolveTypeGen (JType -> TMonad JType) -> JType -> TMonad JType
    forall t (m :: * -> *).
    (Compos1 t, Monad m) =>
    (t -> m t) -> t -> m t
    composOpM1
    resolveTypeShallow :: JType -> TMonad JType
    resolveTypeShallow = ((JType -> TMonad JType) -> JType -> TMonad JType)
    -> JType -> TMonad JType
    resolveTypeGen ((JType -> TMonad JType)
    -> (JType -> TMonad JType) -> JType -> TMonad JType
    forall a b. a -> b -> a
    const JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return)

    --TODO create proper bounds for records
    integrateLocalType :: JLocalType -> TMonad JType
    integrateLocalType :: JLocalType -> TMonad JType
    integrateLocalType ([(VarRef, Constraint)]
    env,JType
    typ) = do
      (r, frame) <- TMonad JType -> TMonad (JType, Set Int)
    forall a. TMonad a -> TMonad (a, Set Int)
    withLocalScope (TMonad JType -> TMonad (JType, Set Int))
    -> TMonad JType -> TMonad (JType, Set Int)
    forall a b. (a -> b) -> a -> b
    $ (StateT (Map Int JType) TMonad JType
     -> Map Int JType -> TMonad JType)
    -> Map Int JType
    -> StateT (Map Int JType) TMonad JType
    -> TMonad JType
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip StateT (Map Int JType) TMonad JType
    -> Map Int JType -> TMonad JType
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT Map Int JType
    forall k a. Map k a
    M.empty (StateT (Map Int JType) TMonad JType -> TMonad JType)
    -> StateT (Map Int JType) TMonad JType -> TMonad JType
    forall a b. (a -> b) -> a -> b
    $ do
                                     ((VarRef, Constraint) -> StateT (Map Int JType) TMonad ())
    -> [(VarRef, Constraint)] -> StateT (Map Int JType) TMonad ()
    forall (t :: * -> *) (f :: * -> *) a b.
    (Foldable t, Monad f) =>
    (a -> f b) -> t a -> f ()
    mapM_ (VarRef, Constraint) -> StateT (Map Int JType) TMonad ()
    forall {t :: (* -> *) -> * -> *}.
    (MonadTrans t, MonadState (Map Int JType) (t TMonad)) =>
    (VarRef, Constraint) -> t TMonad ()
    integrateEnv [(VarRef, Constraint)]
    env
                                     JType -> StateT (Map Int JType) TMonad JType
    forall {t :: (* -> *) -> * -> *}.
    (MonadState (Map Int JType) (t TMonad), MonadTrans t) =>
    JType -> t TMonad JType
    cloneType JType
    typ
      resolveType $ JTForall (frame2VarRefs frame) r
        where
          getRef :: (Maybe String, k) -> t TMonad JType
    getRef (Maybe String
    mbName, k
    ref) = do
                m <- t TMonad (Map k JType)
    forall s (m :: * -> *). MonadState s m => m s
    get
                case M.lookup ref m of
                  Just JType
    newTy -> JType -> t TMonad JType
    forall a. a -> t TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    newTy
                  Maybe JType
    Nothing -> do
                    newTy <- (\VarRef
    x -> VarRef -> JType
    JTFree (Maybe String
    mbName, VarRef -> Int
    forall a b. (a, b) -> b
    snd VarRef
    x)) (VarRef -> JType) -> t TMonad VarRef -> t TMonad JType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TMonad VarRef -> t TMonad VarRef
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TMonad VarRef
    newVarRef
                    put $ M.insert ref newTy m
                    return newTy

          integrateEnv :: (VarRef, Constraint) -> t TMonad ()
    integrateEnv (VarRef
    vr,Constraint
    c) = do
            newTy <- VarRef -> t TMonad JType
    forall {t :: (* -> *) -> * -> *} {k}.
    (MonadState (Map k JType) (t TMonad), Ord k, MonadTrans t) =>
    (Maybe String, k) -> t TMonad JType
    getRef VarRef
    vr
            case c of
              (Sub JType
    t) -> TMonad () -> t TMonad ()
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TMonad () -> t TMonad ())
    -> (JType -> TMonad ()) -> JType -> t TMonad ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (JType
    newTy JType -> JType -> TMonad ()
    <:) (JType -> t TMonad ()) -> t TMonad JType -> t TMonad ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< JType -> t TMonad JType
    forall {t :: (* -> *) -> * -> *}.
    (MonadState (Map Int JType) (t TMonad), MonadTrans t) =>
    JType -> t TMonad JType
    cloneType JType
    t
              (Super JType
    t) -> TMonad () -> t TMonad ()
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TMonad () -> t TMonad ())
    -> (JType -> TMonad ()) -> JType -> t TMonad ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (JType -> JType -> TMonad ()
    <: JType
    newTy) (JType -> t TMonad ()) -> t TMonad JType -> t TMonad ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< JType -> t TMonad JType
    forall {t :: (* -> *) -> * -> *}.
    (MonadState (Map Int JType) (t TMonad), MonadTrans t) =>
    JType -> t TMonad JType
    cloneType JType
    t

          cloneType :: JType -> t TMonad JType
    cloneType (JTFree VarRef
    vr) = VarRef -> t TMonad JType
    forall {t :: (* -> *) -> * -> *} {k}.
    (MonadState (Map k JType) (t TMonad), Ord k, MonadTrans t) =>
    (Maybe String, k) -> t TMonad JType
    getRef VarRef
    vr
          cloneType JType
    x = (JType -> t TMonad JType) -> JType -> t TMonad JType
    forall t (m :: * -> *).
    (Compos1 t, Monad m) =>
    (t -> m t) -> t -> m t
    composOpM1 JType -> t TMonad JType
    cloneType JType
    x

    lookupEnv :: Ident -> TMonad JType
    lookupEnv :: Ident -> TMonad JType
    lookupEnv Ident
    ident = JType -> TMonad JType
    resolveType (JType -> TMonad JType) -> TMonad JType -> TMonad JType
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [Map Ident JType] -> TMonad JType
    forall {a}. [Map Ident a] -> TMonad a
    go ([Map Ident JType] -> TMonad JType)
    -> (TCState -> [Map Ident JType]) -> TCState -> TMonad JType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> [Map Ident JType]
    tc_env (TCState -> TMonad JType) -> TMonad TCState -> TMonad JType
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TMonad TCState
    forall s (m :: * -> *). MonadState s m => m s
    get
        where go :: [Map Ident a] -> TMonad a
    go (Map Ident a
    e:[Map Ident a]
    es) = case Ident -> Map Ident a -> Maybe a
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup Ident
    ident Map Ident a
    e of
                            Just a
    t -> a -> TMonad a
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    t
                            Maybe a
    Nothing -> [Map Ident a] -> TMonad a
    go [Map Ident a]
    es
              go [Map Ident a]
    _ = String -> TMonad a
    forall a. String -> TMonad a
    tyErr0 (String -> TMonad a) -> String -> TMonad a
    forall a b. (a -> b) -> a -> b
    $ String
    "unable to resolve variable name: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Doc -> String
    forall a. Show a => a -> String
    show (Doc -> String) -> Doc -> String
    forall a b. (a -> b) -> a -> b
    $ Ident -> Doc
    forall a. JsToDoc a => a -> Doc
    jsToDoc (Ident -> Doc) -> Ident -> Doc
    forall a b. (a -> b) -> a -> b
    $ Ident
    ident)

    freeVars :: JType -> TMonad (Set Int)
    freeVars :: JType -> TMonad (Set Int)
    freeVars JType
    t = WriterT (Set Int) TMonad () -> TMonad (Set Int)
    forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
    execWriterT (WriterT (Set Int) TMonad () -> TMonad (Set Int))
    -> (JType -> WriterT (Set Int) TMonad ())
    -> JType
    -> TMonad (Set Int)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . JType -> WriterT (Set Int) TMonad ()
    forall {m :: * -> *}. MonadWriter (Set Int) m => JType -> m ()
    go (JType -> TMonad (Set Int)) -> TMonad JType -> TMonad (Set Int)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< JType -> TMonad JType
    resolveType JType
    t
        where go :: JType -> m ()
    go (JTFree (Maybe String
    _, Int
    ref)) = Set Int -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (Int -> Set Int
    forall a. a -> Set a
    S.singleton Int
    ref)
              go JType
    x = (JType -> m ()) -> JType -> m ()
    forall t (m :: * -> *).
    (Compos1 t, Monad m) =>
    (t -> m ()) -> t -> m ()
    composOpM1_ JType -> m ()
    go JType
    x

    --only works on resolved types
    instantiateScheme :: [VarRef] -> JType -> TMonad JType
    instantiateScheme :: [VarRef] -> JType -> TMonad JType
    instantiateScheme [VarRef]
    vrs JType
    t = StateT (Map Int JType) TMonad JType
    -> Map Int JType -> TMonad JType
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT (JType -> StateT (Map Int JType) TMonad JType
    go JType
    t) Map Int JType
    forall k a. Map k a
    M.empty
        where
          schemeVars :: Set Int
    schemeVars = [Int] -> Set Int
    forall a. Ord a => [a] -> Set a
    S.fromList ([Int] -> Set Int) -> [Int] -> Set Int
    forall a b. (a -> b) -> a -> b
    $ (VarRef -> Int) -> [VarRef] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map VarRef -> Int
    forall a b. (a, b) -> b
    snd [VarRef]
    vrs
          go :: JType -> StateT (Map Int JType) TMonad JType
          go :: JType -> StateT (Map Int JType) TMonad JType
    go (JTFree vr :: VarRef
    vr@(Maybe String
    mbName, Int
    ref))
              | Int
    ref Int -> Set Int -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `S.member` Set Int
    schemeVars = do
                           m <- StateT (Map Int JType) TMonad (Map Int JType)
    forall s (m :: * -> *). MonadState s m => m s
    get
                           case M.lookup ref m of
                             Just JType
    newTy -> JType -> StateT (Map Int JType) TMonad JType
    forall a. a -> StateT (Map Int JType) TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    newTy
                             Maybe JType
    Nothing -> do
                               newRef <- (\VarRef
    x -> (Maybe String
    mbName, VarRef -> Int
    forall a b. (a, b) -> b
    snd VarRef
    x)) (VarRef -> VarRef)
    -> StateT (Map Int JType) TMonad VarRef
    -> StateT (Map Int JType) TMonad VarRef
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TMonad VarRef -> StateT (Map Int JType) TMonad VarRef
    forall (m :: * -> *) a.
    Monad m =>
    m a -> StateT (Map Int JType) m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift TMonad VarRef
    newVarRef
                               put $ M.insert ref (JTFree newRef) m
                               mapM_ (lift . addConstraint newRef <=< mapConstraint go) =<< lift (lookupConstraintsList vr)
                               return (JTFree newRef)
          go JType
    x = (JType -> StateT (Map Int JType) TMonad JType)
    -> JType -> StateT (Map Int JType) TMonad JType
    forall t (m :: * -> *).
    (Compos1 t, Monad m) =>
    (t -> m t) -> t -> m t
    composOpM1 JType -> StateT (Map Int JType) TMonad JType
    go JType
    x

    --only works on resolved types
    instantiateRigidScheme :: [VarRef] -> JType -> TMonad JType
    instantiateRigidScheme :: [VarRef] -> JType -> TMonad JType
    instantiateRigidScheme [VarRef]
    vrs JType
    t = StateT (Map Int JType) TMonad JType
    -> Map Int JType -> TMonad JType
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT (JType -> StateT (Map Int JType) TMonad JType
    go JType
    t) Map Int JType
    forall k a. Map k a
    M.empty
        where
          schemeVars :: Set Int
    schemeVars = [Int] -> Set Int
    forall a. Ord a => [a] -> Set a
    S.fromList ([Int] -> Set Int) -> [Int] -> Set Int
    forall a b. (a -> b) -> a -> b
    $ (VarRef -> Int) -> [VarRef] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map VarRef -> Int
    forall a b. (a, b) -> b
    snd [VarRef]
    vrs
          go :: JType -> StateT (Map Int JType) TMonad JType
          go :: JType -> StateT (Map Int JType) TMonad JType
    go (JTFree vr :: VarRef
    vr@(Maybe String
    mbName, Int
    ref))
              | Int
    ref Int -> Set Int -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `S.member` Set Int
    schemeVars = do
                           m <- StateT (Map Int JType) TMonad (Map Int JType)
    forall s (m :: * -> *). MonadState s m => m s
    get
                           case M.lookup ref m of
                             Just JType
    newTy -> JType -> StateT (Map Int JType) TMonad JType
    forall a. a -> StateT (Map Int JType) TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    newTy
                             Maybe JType
    Nothing -> do
                               newRef <- VarRef -> Set Constraint -> JType
    JTRigid VarRef
    vr (Set Constraint -> JType)
    -> ([Constraint] -> Set Constraint) -> [Constraint] -> JType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Constraint] -> Set Constraint
    forall a. Ord a => [a] -> Set a
    S.fromList ([Constraint] -> JType)
    -> StateT (Map Int JType) TMonad [Constraint]
    -> StateT (Map Int JType) TMonad JType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TMonad [Constraint] -> StateT (Map Int JType) TMonad [Constraint]
    forall (m :: * -> *) a.
    Monad m =>
    m a -> StateT (Map Int JType) m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (VarRef -> TMonad [Constraint]
    lookupConstraintsList VarRef
    vr)
                               put $ M.insert ref newRef m
                               return newRef
          go JType
    x = (JType -> StateT (Map Int JType) TMonad JType)
    -> JType -> StateT (Map Int JType) TMonad JType
    forall t (m :: * -> *).
    (Compos1 t, Monad m) =>
    (t -> m t) -> t -> m t
    composOpM1 JType -> StateT (Map Int JType) TMonad JType
    go JType
    x

    --only works on resolved types
    checkEscapedVars :: [VarRef] -> JType -> TMonad ()
    checkEscapedVars :: [VarRef] -> JType -> TMonad ()
    checkEscapedVars [VarRef]
    vrs JType
    t = JType -> TMonad ()
    go JType
    t
        where
          vs :: Set Int
    vs = [Int] -> Set Int
    forall a. Ord a => [a] -> Set a
    S.fromList ([Int] -> Set Int) -> [Int] -> Set Int
    forall a b. (a -> b) -> a -> b
    $ (VarRef -> Int) -> [VarRef] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map VarRef -> Int
    forall a b. (a, b) -> b
    snd [VarRef]
    vrs
          go :: JType -> TMonad ()
    go t :: JType
    t@(JTRigid (Maybe String
    _,Int
    ref) Set Constraint
    _)
              | Int
    ref Int -> Set Int -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `S.member` Set Int
    vs = String -> JType -> TMonad ()
    forall b. String -> JType -> TMonad b
    tyErr1 String
    "Qualified var escapes into environment" JType
    t
              | Bool
    otherwise = () -> TMonad ()
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          go JType
    x = (JType -> TMonad ()) -> JType -> TMonad ()
    forall t (m :: * -> *).
    (Compos1 t, Monad m) =>
    (t -> m ()) -> t -> m ()
    composOpM1_ JType -> TMonad ()
    go JType
    x

    -- Subtyping
    (<:) :: JType -> JType -> TMonad ()
    JType
    x <: :: JType -> JType -> TMonad ()
    <: JType
    y = do
         xt <- JType -> TMonad JType
    resolveTypeShallow JType
    x --shallow because subtyping can close
         yt <- resolveTypeShallow y
         -- trace ("sub : " ++ show xt ++ ", " ++ show yt) $ return ()
         if xt == yt
            then return ()
            else go xt yt `withContext` (do
                                          xt <- prettyType x
                                          yt <- prettyType y
                                          return $ "When applying subtype constraint: " ++ xt ++ " <: " ++ yt)
      where

        go :: JType -> JType -> TMonad ()
    go JType
    _ JType
    JTStat = () -> TMonad ()
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        go JType
    JTImpossible JType
    _ = () -> TMonad ()
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

        go xt :: JType
    xt@(JTFree VarRef
    ref) yt :: JType
    yt@(JTFree VarRef
    ref2) = VarRef -> Constraint -> TMonad ()
    addConstraint VarRef
    ref  (JType -> Constraint
    Sub JType
    yt) TMonad () -> TMonad () -> TMonad ()
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                              VarRef -> Constraint -> TMonad ()
    addConstraint VarRef
    ref2 (JType -> Constraint
    Super JType
    xt)

        go (JTFree VarRef
    ref) JType
    yt = VarRef -> Constraint -> TMonad ()
    addConstraint VarRef
    ref (JType -> Constraint
    Sub JType
    yt)
        go JType
    xt (JTFree VarRef
    ref) = VarRef -> Constraint -> TMonad ()
    addConstraint VarRef
    ref (JType -> Constraint
    Super JType
    xt)

        --above or below jtfrees ?

        -- v <: \/ a. t --> v <: t[a:=x], x not in conclusion
        go JType
    xt yt :: JType
    yt@(JTForall [VarRef]
    vars JType
    t) = do
               t' <- [VarRef] -> JType -> TMonad JType
    instantiateRigidScheme [VarRef]
    vars JType
    t
               go xt t'
               checkEscapedVars vars =<< resolveType xt
               --then check that no fresh types appear in xt

        -- \/ a. t <: v --> [t] <: v
        go (JTForall [VarRef]
    vars JType
    t) JType
    yt = do
               t' <- [VarRef] -> JType -> TMonad JType
    instantiateScheme [VarRef]
    vars JType
    t
               go t' yt

        go xt :: JType
    xt@(JTFunc [JType]
    argsx JType
    retx) yt :: JType
    yt@(JTFunc [JType]
    argsy JType
    rety) = do
               -- TODO: zipWithM_ (<:) (appArgst ++ repeat JTStat) argst -- handle empty args cases
               Bool -> TMonad () -> TMonad ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([JType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [JType]
    argsy Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < [JType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [JType]
    argsx) (TMonad () -> TMonad ()) -> TMonad () -> TMonad ()
    forall a b. (a -> b) -> a -> b
    $ JType -> JType -> TMonad ()
    forall a. JType -> JType -> TMonad a
    tyErr2Sub JType
    xt JType
    yt
               (JType -> JType -> TMonad ()) -> [JType] -> [JType] -> TMonad ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ JType -> JType -> TMonad ()
    (<:) [JType]
    argsy [JType]
    argsx -- functions are contravariant in argument type
               JType
    retx JType -> JType -> TMonad ()
    <: JType
    rety -- functions are covariant in return type
        go (JTList JType
    xt) (JTList JType
    yt) = JType
    xt JType -> JType -> TMonad ()
    <: JType
    yt
        go (JTMap JType
    xt) (JTMap JType
    yt) = JType
    xt JType -> JType -> TMonad ()
    <: JType
    yt
        go (JTRecord JType
    xt Map String JType
    xm) (JTRecord JType
    yt Map String JType
    ym)
            | (JType -> JType -> Bool)
    -> Map String JType -> Map String JType -> Bool
    forall k a b.
    Ord k =>
    (a -> b -> Bool) -> Map k a -> Map k b -> Bool
    M.isSubmapOfBy (\JType
    _ JType
    _ -> Bool
    True) Map String JType
    ym Map String JType
    xm = JType
    xt JType -> JType -> TMonad ()
    <: JType
    yt TMonad () -> TMonad (Map String ()) -> TMonad (Map String ())
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (JType -> JType -> TMonad ())
    -> Map String JType -> Map String JType -> TMonad (Map String ())
    forall (m :: * -> *) key val b.
    (Monad m, Ord key) =>
    (val -> val -> m b) -> Map key val -> Map key val -> m (Map key b)
    intersectionWithM JType -> JType -> TMonad ()
    (<:) Map String JType
    xm Map String JType
    ym TMonad (Map String ()) -> TMonad () -> TMonad ()
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> () -> TMonad ()
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return () --TODO not right?
        go JType
    xt JType
    yt = JType -> JType -> TMonad ()
    forall a. JType -> JType -> TMonad a
    tyErr2Sub JType
    xt JType
    yt

    (<<:>) :: TMonad JType -> TMonad JType -> TMonad ()
    TMonad JType
    x <<:> :: TMonad JType -> TMonad JType -> TMonad ()
    <<:> TMonad JType
    y = TMonad (TMonad ()) -> TMonad ()
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (TMonad (TMonad ()) -> TMonad ())
    -> TMonad (TMonad ()) -> TMonad ()
    forall a b. (a -> b) -> a -> b
    $ (JType -> JType -> TMonad ())
    -> TMonad JType -> TMonad JType -> TMonad (TMonad ())
    forall a b c. (a -> b -> c) -> TMonad a -> TMonad b -> TMonad c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 JType -> JType -> TMonad ()
    (<:) TMonad JType
    x TMonad JType
    y

    someUpperBound :: [JType] -> TMonad JType
    someUpperBound :: [JType] -> TMonad JType
    someUpperBound [] = JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTStat
    someUpperBound [JType]
    xs = do
      res <- TMonad JType
    newTyVar
      b <- (mapM_ (<: res) xs >> return True) `catchError` \String
    e -> Bool -> TMonad Bool
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      if b then return res else return JTStat

    someLowerBound :: [JType] -> TMonad JType
    someLowerBound :: [JType] -> TMonad JType
    someLowerBound [] = JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTImpossible
    someLowerBound [JType]
    xs = do
      res <- TMonad JType
    newTyVar
      mapM_ (res <:) xs
      return res
    --  b <- (mapM_ (res <:) xs >> return True) `catchError` \e -> return False
    --  if b then return res else return JTImpossible

    (=.=) :: JType -> JType -> TMonad JType
    JType
    x =.= :: JType -> JType -> TMonad JType
    =.= JType
    y = do
          JType
    x JType -> JType -> TMonad ()
    <: JType
    y
          JType
    y JType -> JType -> TMonad ()
    <: JType
    x
          JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    x

    --todo difft ixing. a[b] --num lookup, a#[b] --string lookup, a.[b] --num literal lookup (i.e. tuple projection)

    instance JTypeCheck JExpr where
        typecheck :: JExpr -> TMonad JType
    typecheck (ValExpr JVal
    e) = JVal -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JVal
    e
        typecheck (SelExpr JExpr
    e (StrI String
    i)) =
            do et <- JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e
               case et of
                 (JTRecord JType
    t Map String JType
    m) -> case String -> Map String JType -> Maybe JType
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup String
    i Map String JType
    m of
                                   Just JType
    res -> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    res
                                   Maybe JType
    Nothing -> String -> JType -> TMonad JType
    forall b. String -> JType -> TMonad b
    tyErr1 (String
    "Record contains no field named " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    i) JType
    et -- record extension would go here
                 (JTFree VarRef
    r) -> do
                                res <- TMonad JType
    newTyVar
                                addConstraint r (Sub (JTRecord res (M.singleton i res)))
                                return res
                 JType
    _ -> String -> JType -> TMonad JType
    forall b. String -> JType -> TMonad b
    tyErr1 String
    "Cannot use record selector on this value" JType
    et
        typecheck (IdxExpr JExpr
    e JExpr
    e1) = TMonad JType
    forall a. HasCallStack => a
    undefined --this is tricky
        typecheck (InfixExpr String
    s JExpr
    e JExpr
    e1)
            | String
    s String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String
    "-",String
    "/",String
    "*"] = JType -> TMonad ()
    setFixed JType
    JTNum TMonad () -> TMonad JType -> TMonad JType
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTNum
            | String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "+" = JType -> TMonad ()
    setFixed JType
    JTNum TMonad () -> TMonad JType -> TMonad JType
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTNum -- `orElse` setFixed JTStr --TODO: Intersection types
            | String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "++" = JType -> TMonad ()
    setFixed JType
    JTString TMonad () -> TMonad JType -> TMonad JType
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTString
            | String
    s String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String
    ">",String
    "<"] = JType -> TMonad ()
    setFixed JType
    JTNum TMonad () -> TMonad JType -> TMonad JType
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTBool
            | String
    s String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String
    "==",String
    "/="] = do
                                et <- JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e
                                e1t <- typecheck e1
                                _ <- et =.= e1t
                                return JTBool
            | String
    s String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String
    "||",String
    "&&"] = JType -> TMonad ()
    setFixed JType
    JTBool TMonad () -> TMonad JType -> TMonad JType
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTBool
            | Bool
    otherwise = String -> TMonad JType
    forall a. String -> TMonad a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> TMonad JType) -> String -> TMonad JType
    forall a b. (a -> b) -> a -> b
    $ String
    "Unhandled operator: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s
            where setFixed :: JType -> TMonad ()
    setFixed JType
    t = do
                      JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e  TMonad JType -> TMonad JType -> TMonad ()
    <<:> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    t
                      JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e1 TMonad JType -> TMonad JType -> TMonad ()
    <<:> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    t

        typecheck (PPostExpr Bool
    _ String
    _ JExpr
    e) = case JExpr
    e of
                                     (SelExpr JExpr
    _ Ident
    _) -> TMonad JType
    go
                                     (ValExpr (JVar Ident
    _)) -> TMonad JType
    go
                                     (IdxExpr JExpr
    _ JExpr
    _) -> TMonad JType
    go
                                     JExpr
    _ -> String -> JType -> TMonad JType
    forall b. String -> JType -> TMonad b
    tyErr1 String
    "Value not compatible with postfix assignment" (JType -> TMonad JType) -> TMonad JType -> TMonad JType
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e
            where go :: TMonad JType
    go = (JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e TMonad JType -> TMonad JType -> TMonad ()
    <<:> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTNum) TMonad () -> TMonad JType -> TMonad JType
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTNum

        typecheck (IfExpr JExpr
    e JExpr
    e1 JExpr
    e2) = do
                                JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e TMonad JType -> TMonad JType -> TMonad ()
    <<:> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTBool
                                TMonad (TMonad JType) -> TMonad JType
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (TMonad (TMonad JType) -> TMonad JType)
    -> TMonad (TMonad JType) -> TMonad JType
    forall a b. (a -> b) -> a -> b
    $ (JType -> JType -> TMonad JType)
    -> TMonad JType -> TMonad JType -> TMonad (TMonad JType)
    forall a b c. (a -> b -> c) -> TMonad a -> TMonad b -> TMonad c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 (\JType
    x JType
    y -> [JType] -> TMonad JType
    someUpperBound [JType
    x,JType
    y]) (JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e1) (JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e2)

        typecheck (NewExpr JExpr
    e) = TMonad JType
    forall a. HasCallStack => a
    undefined --yipe

        --when we instantiate a scheme, all the elements of the head
        --that are not in the tail are henceforth unreachable and can be closed
        --but that's just an optimization
        typecheck (ApplExpr JExpr
    e [JExpr]
    appArgse) = do
                                et <- JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e
                                appArgst <- mapM typecheck appArgse
                                let go (JTForall [VarRef]
    vars JType
    t) = JType -> TMonad JType
    go (JType -> TMonad JType) -> TMonad JType -> TMonad JType
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [VarRef] -> JType -> TMonad JType
    instantiateScheme [VarRef]
    vars JType
    t
                                    go (JTFunc [JType]
    argst JType
    rett) = do
                                            (JType -> JType -> TMonad ()) -> [JType] -> [JType] -> TMonad ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ JType -> JType -> TMonad ()
    (<:) ([JType]
    appArgst [JType] -> [JType] -> [JType]
    forall a. [a] -> [a] -> [a]
    ++ JType -> [JType]
    forall a. a -> [a]
    repeat JType
    JTStat) [JType]
    argst
                                            JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    rett
                                    go (JTFree VarRef
    vr) = do
                                            ret <- TMonad JType
    newTyVar
                                            addConstraint vr (Sub (JTFunc appArgst ret))
                                            return ret
                                    go JType
    x = String -> JType -> TMonad JType
    forall b. String -> JType -> TMonad b
    tyErr1 String
    "Cannot apply value as function" JType
    x
                                go et

        typecheck (UnsatExpr IdentSupply JExpr
    _) = TMonad JType
    forall a. HasCallStack => a
    undefined --saturate (avoiding creation of existing ids) then typecheck
        typecheck (AntiExpr String
    s) = String -> TMonad JType
    forall a. HasCallStack => String -> a
    error (String -> TMonad JType) -> String -> TMonad JType
    forall a b. (a -> b) -> a -> b
    $ String
    "Antiquoted expression not provided with explicit signature: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    s

        --TODO: if we're typechecking a function, we can assign the types of the args to the given args
        typecheck (TypeExpr Bool
    forceType JExpr
    e JLocalType
    t)
                  | Bool
    forceType = JLocalType -> TMonad JType
    integrateLocalType JLocalType
    t
                  | Bool
    otherwise = do
                                t1 <- JLocalType -> TMonad JType
    integrateLocalType JLocalType
    t
                                typecheck e <<:> return t1
                                return t1

    instance JTypeCheck JVal where
        typecheck :: JVal -> TMonad JType
    typecheck (JVar Ident
    i) =
            case Ident
    i of
              StrI String
    "true" -> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTBool
              StrI String
    "false" -> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTBool
              StrI String
    "null"  -> TMonad JType
    newTyVar
              StrI String
    _ -> Ident -> TMonad JType
    lookupEnv Ident
    i

        typecheck (JInt Integer
    _) = JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTNum
        typecheck (JDouble SaneDouble
    _) = JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTNum
        typecheck (JStr String
    _) = JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTString
        typecheck (JList [JExpr]
    xs) = JVal -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck (Map String JExpr -> JVal
    JHash (Map String JExpr -> JVal) -> Map String JExpr -> JVal
    forall a b. (a -> b) -> a -> b
    $ [(String, JExpr)] -> Map String JExpr
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList ([(String, JExpr)] -> Map String JExpr)
    -> [(String, JExpr)] -> Map String JExpr
    forall a b. (a -> b) -> a -> b
    $ [String] -> [JExpr] -> [(String, JExpr)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip ((Int -> String) -> [Int] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> String
    forall a. Show a => a -> String
    show [(Int
    0::Int)..]) [JExpr]
    xs)
                               -- fmap JTList . someUpperBound =<< mapM typecheck xs
        typecheck (JRegEx String
    _) = TMonad JType
    forall a. HasCallStack => a
    undefined --regex object
        typecheck (JHash Map String JExpr
    mp) = do
          mp' <- (JExpr -> TMonad JType)
    -> Map String JExpr -> TMonad (Map String JType)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Map String a -> m (Map String b)
    T.mapM JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck Map String JExpr
    mp
          t <- if M.null mp'
                 then return JTImpossible
                 else someUpperBound $ M.elems mp'
          return $ JTRecord t mp'
        typecheck (JFunc [Ident]
    args JStat
    body) = do
              ((argst',res'), frame) <- TMonad ([JType], JType) -> TMonad (([JType], JType), Set Int)
    forall a. TMonad a -> TMonad (a, Set Int)
    withLocalScope (TMonad ([JType], JType) -> TMonad (([JType], JType), Set Int))
    -> TMonad ([JType], JType) -> TMonad (([JType], JType), Set Int)
    forall a b. (a -> b) -> a -> b
    $ do
                                          argst <- (Ident -> TMonad JType) -> [Ident] -> TMonad [JType]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Ident -> TMonad JType
    newVarDecl [Ident]
    args
                                          res <- typecheck body
                                          return (argst,res)
              rt <- resolveType $ JTFunc argst' res'
              freeVarsInArgs <- S.unions <$> mapM freeVars argst'
              freeVarsInRes  <- freeVars res'
              setFrozen $ frame `S.difference` (freeVarsInArgs `S.intersection` freeVarsInRes)
              tryCloseFrozenVars
              resolveType $ JTForall (frame2VarRefs frame) rt

        typecheck (UnsatVal IdentSupply JVal
    _) = TMonad JType
    forall a. HasCallStack => a
    undefined --saturate (avoiding creation of existing ids) then typecheck

    instance JTypeCheck JStat where
        typecheck :: JStat -> TMonad JType
    typecheck (DeclStat Ident
    ident Maybe JLocalType
    Nothing) = Ident -> TMonad JType
    newVarDecl Ident
    ident TMonad JType -> TMonad JType -> TMonad JType
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTStat
        typecheck (DeclStat Ident
    ident (Just JLocalType
    t)) = JLocalType -> TMonad JType
    integrateLocalType JLocalType
    t TMonad JType -> (JType -> TMonad ()) -> TMonad ()
    forall a b. TMonad a -> (a -> TMonad b) -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Ident -> JType -> TMonad ()
    addEnv Ident
    ident TMonad () -> TMonad JType -> TMonad JType
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTStat
        typecheck (ReturnStat JExpr
    e) = JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e
        typecheck (IfStat JExpr
    e JStat
    s JStat
    s1) = do
                                JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e TMonad JType -> TMonad JType -> TMonad ()
    <<:> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTBool
                                TMonad (TMonad JType) -> TMonad JType
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (TMonad (TMonad JType) -> TMonad JType)
    -> TMonad (TMonad JType) -> TMonad JType
    forall a b. (a -> b) -> a -> b
    $ (JType -> JType -> TMonad JType)
    -> TMonad JType -> TMonad JType -> TMonad (TMonad JType)
    forall a b c. (a -> b -> c) -> TMonad a -> TMonad b -> TMonad c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 (\JType
    x JType
    y -> [JType] -> TMonad JType
    someUpperBound [JType
    x,JType
    y]) (JStat -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JStat
    s) (JStat -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JStat
    s1)
        typecheck (WhileStat Bool
    _ JExpr
    e JStat
    s) = do
                                JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e TMonad JType -> TMonad JType -> TMonad ()
    <<:> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTBool
                                JStat -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JStat
    s
        typecheck (ForInStat Bool
    _ Ident
    _ JExpr
    _ JStat
    _) = TMonad JType
    forall a. HasCallStack => a
    undefined -- yipe!
        typecheck (SwitchStat JExpr
    e [(JExpr, JStat)]
    xs JStat
    d) = TMonad JType
    forall a. HasCallStack => a
    undefined -- check e, unify e with firsts, check seconds, take glb of seconds
                                        --oh, hey, add typecase to language!?
        typecheck (TryStat JStat
    _ Ident
    _ JStat
    _ JStat
    _) = TMonad JType
    forall a. HasCallStack => a
    undefined -- should be easy
        typecheck (BlockStat [JStat]
    xs) = do
                                ts <- (JStat -> TMonad JType) -> [JStat] -> TMonad [JType]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM JStat -> TMonad JType
    forall a. (JsToDoc a, JMacro a, JTypeCheck a) => a -> TMonad JType
    typecheckWithBlock [JStat]
    xs
                                someUpperBound $ stripStat ts
            where stripStat :: [JType] -> [JType]
    stripStat (JType
    JTStat:[JType]
    ts) = [JType] -> [JType]
    stripStat [JType]
    ts
                  stripStat (JType
    t:[JType]
    ts) = JType
    t JType -> [JType] -> [JType]
    forall a. a -> [a] -> [a]
    : [JType] -> [JType]
    stripStat [JType]
    ts
                  stripStat [JType]
    t = [JType]
    t
        typecheck (ApplStat JExpr
    args [JExpr]
    body) = JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck (JExpr -> [JExpr] -> JExpr
    ApplExpr JExpr
    args [JExpr]
    body) TMonad JType -> TMonad JType -> TMonad JType
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTStat
        typecheck (PPostStat Bool
    b String
    s JExpr
    e) = JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck (Bool -> String -> JExpr -> JExpr
    PPostExpr Bool
    b String
    s JExpr
    e) TMonad JType -> TMonad JType -> TMonad JType
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTStat
        typecheck (AssignStat JExpr
    e JExpr
    e1) = do
          JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e1 TMonad JType -> TMonad JType -> TMonad ()
    <<:> JExpr -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck JExpr
    e
          JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTStat
        typecheck (UnsatBlock IdentSupply JStat
    _) = TMonad JType
    forall a. HasCallStack => a
    undefined --oyvey
        typecheck (AntiStat String
    _) = TMonad JType
    forall a. HasCallStack => a
    undefined --oyvey
        typecheck (BreakStat Maybe String
    _) = JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTStat
        typecheck (ForeignStat Ident
    i JLocalType
    t) = JLocalType -> TMonad JType
    integrateLocalType JLocalType
    t TMonad JType -> (JType -> TMonad ()) -> TMonad ()
    forall a b. TMonad a -> (a -> TMonad b) -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Ident -> JType -> TMonad ()
    addEnv Ident
    i TMonad () -> TMonad JType -> TMonad JType
    forall a b. TMonad a -> TMonad b -> TMonad b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> JType -> TMonad JType
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return JType
    JTStat

    typecheckWithBlock :: (JsToDoc a, JMacro a, JTypeCheck a) => a -> TMonad JType
    typecheckWithBlock :: forall a. (JsToDoc a, JMacro a, JTypeCheck a) => a -> TMonad JType
    typecheckWithBlock a
    stat = a -> TMonad JType
    forall a. JTypeCheck a => a -> TMonad JType
    typecheck a
    stat TMonad JType -> TMonad String -> TMonad JType
    forall a. TMonad a -> TMonad String -> TMonad a
    `withContext` (String -> TMonad String
    forall a. a -> TMonad a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (String -> TMonad String) -> String -> TMonad String
    forall a b. (a -> b) -> a -> b
    $ String
    "In statement: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Text -> String
    T.unpack (Text -> String) -> (Doc -> Text) -> Doc -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SimpleDoc -> Text
    displayT (SimpleDoc -> Text) -> (Doc -> SimpleDoc) -> Doc -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> SimpleDoc
    renderCompact (Doc -> String) -> Doc -> String
    forall a b. (a -> b) -> a -> b
    $ a -> Doc
    forall a. (JsToDoc a, JMacro a) => a -> Doc
    renderJs a
    stat))