    {-# LANGUAGE CPP #-}
    --
    -- Copyright (c) 2005 Lennart Augustsson
    -- See LICENSE for licensing details.
    --
    module Djinn.HCheck (
      htCheckEnv,
      htCheckType
    ) where

    import Data.List (union)
    --import Control.Monad.Trans
    #if MIN_VERSION_mtl(2,2,0)
    import Control.Monad.Except ()
    #else
    import Control.Monad.Error ()
    #endif
    import Control.Monad.State
    import Data.Graph (SCC (..), stronglyConnComp)
    import Data.IntMap (IntMap, empty, insert, (!))

    import Djinn.HTypes

    -- import Debug.Trace

    #if MIN_VERSION_mtl(2,3,0)
    -- mtl >= 2.3 does not define liftM2
    liftM2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c
    liftM2 :: forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftM2 a -> b -> c
    f f a
    x f b
    y = a -> b -> c
    f (a -> b -> c) -> f a -> f (b -> c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f a
    x f (b -> c) -> f b -> f c
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> f b
    y
    #endif

    type KState = (Int, IntMap (Maybe HKind))
    initState :: KState
    initState :: KState
    initState = (Int
    0, IntMap (Maybe HKind)
    forall a. IntMap a
    empty)

    type M a = StateT KState (Either String) a

    type KEnv = [(HSymbol, HKind)]

    newKVar :: M HKind
    newKVar :: M HKind
    newKVar = do
      (Int
    i, IntMap (Maybe HKind)
    m) <- StateT KState (Either HSymbol) KState
    forall s (m :: * -> *). MonadState s m => m s
    get
      KState -> StateT KState (Either HSymbol) ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1, Int -> Maybe HKind -> IntMap (Maybe HKind) -> IntMap (Maybe HKind)
    forall a. Int -> a -> IntMap a -> IntMap a
    insert Int
    i Maybe HKind
    forall a. Maybe a
    Nothing IntMap (Maybe HKind)
    m)
      HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HKind -> M HKind) -> HKind -> M HKind
    forall a b. (a -> b) -> a -> b
    $ Int -> HKind
    KVar Int
    i

    getVar :: Int -> M (Maybe HKind)
    getVar :: Int -> M (Maybe HKind)
    getVar Int
    i = do
      (Int
    _, IntMap (Maybe HKind)
    m) <- StateT KState (Either HSymbol) KState
    forall s (m :: * -> *). MonadState s m => m s
    get
      case IntMap (Maybe HKind)
    mIntMap (Maybe HKind) -> Int -> Maybe HKind
    forall a. IntMap a -> Int -> a
    !Int
    i of
        Just (KVar Int
    i') -> Int -> M (Maybe HKind)
    getVar Int
    i'
        Maybe HKind
    mk -> Maybe HKind -> M (Maybe HKind)
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe HKind
    mk

    addMap :: Int -> HKind -> M ()
    addMap :: Int -> HKind -> StateT KState (Either HSymbol) ()
    addMap Int
    i HKind
    k = do
      (Int
    n, IntMap (Maybe HKind)
    m) <- StateT KState (Either HSymbol) KState
    forall s (m :: * -> *). MonadState s m => m s
    get
      KState -> StateT KState (Either HSymbol) ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Int
    n, Int -> Maybe HKind -> IntMap (Maybe HKind) -> IntMap (Maybe HKind)
    forall a. Int -> a -> IntMap a -> IntMap a
    insert Int
    i (HKind -> Maybe HKind
    forall a. a -> Maybe a
    Just HKind
    k) IntMap (Maybe HKind)
    m)

    clearState :: M ()
    clearState :: StateT KState (Either HSymbol) ()
    clearState = KState -> StateT KState (Either HSymbol) ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put KState
    initState

    htCheckType :: [(HSymbol, ([HSymbol], HType, HKind))] -> HType -> Either String ()
    htCheckType :: [(HSymbol, ([HSymbol], HType, HKind))]
    -> HType -> Either HSymbol ()
    htCheckType [(HSymbol, ([HSymbol], HType, HKind))]
    its HType
    t = (StateT KState (Either HSymbol) () -> KState -> Either HSymbol ())
    -> KState -> StateT KState (Either HSymbol) () -> Either HSymbol ()
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip StateT KState (Either HSymbol) () -> KState -> Either HSymbol ()
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT KState
    initState (StateT KState (Either HSymbol) () -> Either HSymbol ())
    -> StateT KState (Either HSymbol) () -> Either HSymbol ()
    forall a b. (a -> b) -> a -> b
    $ do
      let vs :: [HSymbol]
    vs = HType -> [HSymbol]
    getHTVars HType
    t
      [HKind]
    ks <- (HSymbol -> M HKind)
    -> [HSymbol] -> StateT KState (Either HSymbol) [HKind]
    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 (M HKind -> HSymbol -> M HKind
    forall a b. a -> b -> a
    const M HKind
    newKVar) [HSymbol]
    vs
      let env :: [(HSymbol, HKind)]
    env = [HSymbol] -> [HKind] -> [(HSymbol, HKind)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [HSymbol]
    vs [HKind]
    ks [(HSymbol, HKind)] -> [(HSymbol, HKind)] -> [(HSymbol, HKind)]
    forall a. [a] -> [a] -> [a]
    ++ [(HSymbol
    i, HKind
    k) | (HSymbol
    i, ([HSymbol]
    _, HType
    _, HKind
    k)) <- [(HSymbol, ([HSymbol], HType, HKind))]
    its ]
      [(HSymbol, HKind)] -> HType -> StateT KState (Either HSymbol) ()
    iHKindStar [(HSymbol, HKind)]
    env HType
    t

    htCheckEnv :: [(HSymbol, ([HSymbol], HType, a))] -> Either String [(HSymbol, ([HSymbol], HType, HKind))]
    htCheckEnv :: forall a.
    [(HSymbol, ([HSymbol], HType, a))]
    -> Either HSymbol [(HSymbol, ([HSymbol], HType, HKind))]
    htCheckEnv [(HSymbol, ([HSymbol], HType, a))]
    its =
      let graph :: [((HSymbol, ([HSymbol], HType, a)), HSymbol, [HSymbol])]
    graph = [ ((HSymbol, ([HSymbol], HType, a))
    n, HSymbol
    i, HType -> [HSymbol]
    getHTCons HType
    t) | n :: (HSymbol, ([HSymbol], HType, a))
    n@(HSymbol
    i, ([HSymbol]
    _, HType
    t, a
    _)) <- [(HSymbol, ([HSymbol], HType, a))]
    its ]
          order :: [SCC (HSymbol, ([HSymbol], HType, a))]
    order = [((HSymbol, ([HSymbol], HType, a)), HSymbol, [HSymbol])]
    -> [SCC (HSymbol, ([HSymbol], HType, a))]
    forall key node. Ord key => [(node, key, [key])] -> [SCC node]
    stronglyConnComp [((HSymbol, ([HSymbol], HType, a)), HSymbol, [HSymbol])]
    graph
       in case [ [(HSymbol, ([HSymbol], HType, a))]
    c | CyclicSCC [(HSymbol, ([HSymbol], HType, a))]
    c <- [SCC (HSymbol, ([HSymbol], HType, a))]
    order ] of
            [(HSymbol, ([HSymbol], HType, a))]
    c : [[(HSymbol, ([HSymbol], HType, a))]]
    _ -> HSymbol -> Either HSymbol [(HSymbol, ([HSymbol], HType, HKind))]
    forall a b. a -> Either a b
    Left (HSymbol -> Either HSymbol [(HSymbol, ([HSymbol], HType, HKind))])
    -> HSymbol -> Either HSymbol [(HSymbol, ([HSymbol], HType, HKind))]
    forall a b. (a -> b) -> a -> b
    $ HSymbol
    "Recursive types are not allowed: " HSymbol -> HSymbol -> HSymbol
    forall a. [a] -> [a] -> [a]
    ++ [HSymbol] -> HSymbol
    unwords [ HSymbol
    i | (HSymbol
    i, ([HSymbol], HType, a)
    _) <- [(HSymbol, ([HSymbol], HType, a))]
    c ]
            [] -> (StateT
       KState (Either HSymbol) [(HSymbol, ([HSymbol], HType, HKind))]
     -> KState -> Either HSymbol [(HSymbol, ([HSymbol], HType, HKind))])
    -> KState
    -> StateT
         KState (Either HSymbol) [(HSymbol, ([HSymbol], HType, HKind))]
    -> Either HSymbol [(HSymbol, ([HSymbol], HType, HKind))]
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip StateT
      KState (Either HSymbol) [(HSymbol, ([HSymbol], HType, HKind))]
    -> KState -> Either HSymbol [(HSymbol, ([HSymbol], HType, HKind))]
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT KState
    initState (StateT
       KState (Either HSymbol) [(HSymbol, ([HSymbol], HType, HKind))]
     -> Either HSymbol [(HSymbol, ([HSymbol], HType, HKind))])
    -> StateT
         KState (Either HSymbol) [(HSymbol, ([HSymbol], HType, HKind))]
    -> Either HSymbol [(HSymbol, ([HSymbol], HType, HKind))]
    forall a b. (a -> b) -> a -> b
    $ StateT
      KState (Either HSymbol) [(HSymbol, ([HSymbol], HType, HKind))]
    addKinds
                    where addKinds :: StateT
      KState (Either HSymbol) [(HSymbol, ([HSymbol], HType, HKind))]
    addKinds = do
                            [(HSymbol, HKind)]
    env <- [(HSymbol, HKind)]
    -> [(HSymbol, ([HSymbol], HType, a))] -> M [(HSymbol, HKind)]
    forall a.
    [(HSymbol, HKind)]
    -> [(HSymbol, ([HSymbol], HType, a))] -> M [(HSymbol, HKind)]
    inferHKinds [] ([(HSymbol, ([HSymbol], HType, a))] -> M [(HSymbol, HKind)])
    -> [(HSymbol, ([HSymbol], HType, a))] -> M [(HSymbol, HKind)]
    forall a b. (a -> b) -> a -> b
    $ (SCC (HSymbol, ([HSymbol], HType, a))
     -> (HSymbol, ([HSymbol], HType, a)))
    -> [SCC (HSymbol, ([HSymbol], HType, a))]
    -> [(HSymbol, ([HSymbol], HType, a))]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ (AcyclicSCC (HSymbol, ([HSymbol], HType, a))
    n) -> (HSymbol, ([HSymbol], HType, a))
    n) [SCC (HSymbol, ([HSymbol], HType, a))]
    order
                            let getK :: HSymbol -> HKind
    getK HSymbol
    i = HKind -> (HKind -> HKind) -> Maybe HKind -> HKind
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (HSymbol -> HKind
    forall a. HasCallStack => HSymbol -> a
    error (HSymbol -> HKind) -> HSymbol -> HKind
    forall a b. (a -> b) -> a -> b
    $ HSymbol
    "htCheck " HSymbol -> HSymbol -> HSymbol
    forall a. [a] -> [a] -> [a]
    ++ HSymbol
    i) HKind -> HKind
    forall a. a -> a
    id (Maybe HKind -> HKind) -> Maybe HKind -> HKind
    forall a b. (a -> b) -> a -> b
    $ HSymbol -> [(HSymbol, HKind)] -> Maybe HKind
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup HSymbol
    i [(HSymbol, HKind)]
    env
                            [(HSymbol, ([HSymbol], HType, HKind))]
    -> StateT
         KState (Either HSymbol) [(HSymbol, ([HSymbol], HType, HKind))]
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ (HSymbol
    i, ([HSymbol]
    vs, HType
    t, HSymbol -> HKind
    getK HSymbol
    i)) | (HSymbol
    i, ([HSymbol]
    vs, HType
    t, a
    _)) <- [(HSymbol, ([HSymbol], HType, a))]
    its ]

    inferHKinds :: KEnv -> [(HSymbol, ([HSymbol], HType, a))] -> M KEnv
    inferHKinds :: forall a.
    [(HSymbol, HKind)]
    -> [(HSymbol, ([HSymbol], HType, a))] -> M [(HSymbol, HKind)]
    inferHKinds [(HSymbol, HKind)]
    env [] = [(HSymbol, HKind)] -> M [(HSymbol, HKind)]
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(HSymbol, HKind)]
    env
    inferHKinds [(HSymbol, HKind)]
    env ((HSymbol
    i, ([HSymbol]
    vs, HType
    t, a
    _)) : [(HSymbol, ([HSymbol], HType, a))]
    its) = do
      HKind
    k <- [(HSymbol, HKind)] -> [HSymbol] -> HType -> M HKind
    inferHKind [(HSymbol, HKind)]
    env [HSymbol]
    vs HType
    t
      [(HSymbol, HKind)]
    -> [(HSymbol, ([HSymbol], HType, a))] -> M [(HSymbol, HKind)]
    forall a.
    [(HSymbol, HKind)]
    -> [(HSymbol, ([HSymbol], HType, a))] -> M [(HSymbol, HKind)]
    inferHKinds ((HSymbol
    i, HKind
    k) (HSymbol, HKind) -> [(HSymbol, HKind)] -> [(HSymbol, HKind)]
    forall a. a -> [a] -> [a]
    : [(HSymbol, HKind)]
    env) [(HSymbol, ([HSymbol], HType, a))]
    its

    inferHKind :: KEnv -> [HSymbol] -> HType -> M HKind
    inferHKind :: [(HSymbol, HKind)] -> [HSymbol] -> HType -> M HKind
    inferHKind [(HSymbol, HKind)]
    _ [HSymbol]
    _ (HTAbstract HSymbol
    _ HKind
    k) = HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    k
    inferHKind [(HSymbol, HKind)]
    env [HSymbol]
    vs HType
    t = do
      StateT KState (Either HSymbol) ()
    clearState
      [HKind]
    ks <- (HSymbol -> M HKind)
    -> [HSymbol] -> StateT KState (Either HSymbol) [HKind]
    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 (M HKind -> HSymbol -> M HKind
    forall a b. a -> b -> a
    const M HKind
    newKVar) [HSymbol]
    vs
      let env' :: [(HSymbol, HKind)]
    env' = [HSymbol] -> [HKind] -> [(HSymbol, HKind)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [HSymbol]
    vs [HKind]
    ks [(HSymbol, HKind)] -> [(HSymbol, HKind)] -> [(HSymbol, HKind)]
    forall a. [a] -> [a] -> [a]
    ++ [(HSymbol, HKind)]
    env
      HKind
    k <- [(HSymbol, HKind)] -> HType -> M HKind
    iHKind [(HSymbol, HKind)]
    env' HType
    t
      HKind -> M HKind
    ground (HKind -> M HKind) -> HKind -> M HKind
    forall a b. (a -> b) -> a -> b
    $ (HKind -> HKind -> HKind) -> HKind -> [HKind] -> HKind
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr HKind -> HKind -> HKind
    KArrow HKind
    k [HKind]
    ks

    iHKind :: KEnv -> HType -> M HKind
    iHKind :: [(HSymbol, HKind)] -> HType -> M HKind
    iHKind [(HSymbol, HKind)]
    env (HTApp HType
    f HType
    a) = do
      HKind
    kf <- [(HSymbol, HKind)] -> HType -> M HKind
    iHKind [(HSymbol, HKind)]
    env HType
    f
      HKind
    ka <- [(HSymbol, HKind)] -> HType -> M HKind
    iHKind [(HSymbol, HKind)]
    env HType
    a
      HKind
    r <- M HKind
    newKVar
      HKind -> HKind -> StateT KState (Either HSymbol) ()
    unifyK (HKind -> HKind -> HKind
    KArrow HKind
    ka HKind
    r) HKind
    kf
      HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    r
    iHKind [(HSymbol, HKind)]
    env (HTVar HSymbol
    v) = do
      [(HSymbol, HKind)] -> HSymbol -> M HKind
    getVarHKind [(HSymbol, HKind)]
    env HSymbol
    v
    iHKind [(HSymbol, HKind)]
    env (HTCon HSymbol
    c) = do
      [(HSymbol, HKind)] -> HSymbol -> M HKind
    getConHKind [(HSymbol, HKind)]
    env HSymbol
    c
    iHKind [(HSymbol, HKind)]
    env (HTTuple [HType]
    ts) = do
      (HType -> StateT KState (Either HSymbol) ())
    -> [HType] -> StateT KState (Either HSymbol) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ([(HSymbol, HKind)] -> HType -> StateT KState (Either HSymbol) ()
    iHKindStar [(HSymbol, HKind)]
    env) [HType]
    ts
      HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    KStar
    iHKind [(HSymbol, HKind)]
    env (HTArrow HType
    f HType
    a) = do
      [(HSymbol, HKind)] -> HType -> StateT KState (Either HSymbol) ()
    iHKindStar [(HSymbol, HKind)]
    env HType
    f
      [(HSymbol, HKind)] -> HType -> StateT KState (Either HSymbol) ()
    iHKindStar [(HSymbol, HKind)]
    env HType
    a
      HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    KStar
    iHKind [(HSymbol, HKind)]
    env (HTUnion [(HSymbol, [HType])]
    cs) = do
      ((HSymbol, [HType]) -> StateT KState (Either HSymbol) ())
    -> [(HSymbol, [HType])] -> StateT KState (Either HSymbol) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (\ (HSymbol
    _, [HType]
    ts) -> (HType -> StateT KState (Either HSymbol) ())
    -> [HType] -> StateT KState (Either HSymbol) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ([(HSymbol, HKind)] -> HType -> StateT KState (Either HSymbol) ()
    iHKindStar [(HSymbol, HKind)]
    env) [HType]
    ts) [(HSymbol, [HType])]
    cs
      HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    KStar
    iHKind [(HSymbol, HKind)]
    _ (HTAbstract HSymbol
    _ HKind
    _) = HSymbol -> M HKind
    forall a. HasCallStack => HSymbol -> a
    error HSymbol
    "iHKind HTAbstract"

    iHKindStar :: KEnv -> HType -> M ()
    iHKindStar :: [(HSymbol, HKind)] -> HType -> StateT KState (Either HSymbol) ()
    iHKindStar [(HSymbol, HKind)]
    env HType
    t = do
      HKind
    k <- [(HSymbol, HKind)] -> HType -> M HKind
    iHKind [(HSymbol, HKind)]
    env HType
    t
      HKind -> HKind -> StateT KState (Either HSymbol) ()
    unifyK HKind
    k HKind
    KStar

    unifyK :: HKind -> HKind -> M ()
    unifyK :: HKind -> HKind -> StateT KState (Either HSymbol) ()
    unifyK HKind
    k1 HKind
    k2 = do
      let follow :: HKind -> M HKind
    follow k :: HKind
    k@(KVar Int
    i) = Int -> M (Maybe HKind)
    getVar Int
    i M (Maybe HKind) -> (Maybe HKind -> M HKind) -> M HKind
    forall a b.
    StateT KState (Either HSymbol) a
    -> (a -> StateT KState (Either HSymbol) b)
    -> StateT KState (Either HSymbol) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (HKind -> M HKind)
    -> (Maybe HKind -> HKind) -> Maybe HKind -> M HKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HKind -> (HKind -> HKind) -> Maybe HKind -> HKind
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe HKind
    k HKind -> HKind
    forall a. a -> a
    id
          follow HKind
    k = HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    k
          unify :: HKind -> HKind -> StateT KState (Either HSymbol) ()
    unify HKind
    KStar HKind
    KStar = () -> StateT KState (Either HSymbol) ()
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          unify (KArrow HKind
    k11 HKind
    k12) (KArrow HKind
    k21 HKind
    k22) = do HKind -> HKind -> StateT KState (Either HSymbol) ()
    unifyK HKind
    k11 HKind
    k21; HKind -> HKind -> StateT KState (Either HSymbol) ()
    unifyK HKind
    k12 HKind
    k22
          unify (KVar Int
    i1) (KVar Int
    i2) | Int
    i1 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    i2 = () -> StateT KState (Either HSymbol) ()
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          unify (KVar Int
    i) HKind
    k = do Int -> HKind -> StateT KState (Either HSymbol) ()
    occurs Int
    i HKind
    k; Int -> HKind -> StateT KState (Either HSymbol) ()
    addMap Int
    i HKind
    k
          unify HKind
    k (KVar Int
    i) = do Int -> HKind -> StateT KState (Either HSymbol) ()
    occurs Int
    i HKind
    k; Int -> HKind -> StateT KState (Either HSymbol) ()
    addMap Int
    i HKind
    k
          unify HKind
    _ HKind
    _ = Either HSymbol () -> StateT KState (Either HSymbol) ()
    forall (m :: * -> *) a. Monad m => m a -> StateT KState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Either HSymbol () -> StateT KState (Either HSymbol) ())
    -> Either HSymbol () -> StateT KState (Either HSymbol) ()
    forall a b. (a -> b) -> a -> b
    $ HSymbol -> Either HSymbol ()
    forall a b. a -> Either a b
    Left (HSymbol -> Either HSymbol ()) -> HSymbol -> Either HSymbol ()
    forall a b. (a -> b) -> a -> b
    $ HSymbol
    "kind error: " HSymbol -> HSymbol -> HSymbol
    forall a. [a] -> [a] -> [a]
    ++ (HKind, HKind) -> HSymbol
    forall a. Show a => a -> HSymbol
    show (HKind
    k1, HKind
    k2)
          occurs :: Int -> HKind -> StateT KState (Either HSymbol) ()
    occurs Int
    _ HKind
    KStar = () -> StateT KState (Either HSymbol) ()
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          occurs Int
    i (KArrow HKind
    f HKind
    a) = do HKind -> M HKind
    follow HKind
    f M HKind
    -> (HKind -> StateT KState (Either HSymbol) ())
    -> StateT KState (Either HSymbol) ()
    forall a b.
    StateT KState (Either HSymbol) a
    -> (a -> StateT KState (Either HSymbol) b)
    -> StateT KState (Either HSymbol) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Int -> HKind -> StateT KState (Either HSymbol) ()
    occurs Int
    i; HKind -> M HKind
    follow HKind
    a M HKind
    -> (HKind -> StateT KState (Either HSymbol) ())
    -> StateT KState (Either HSymbol) ()
    forall a b.
    StateT KState (Either HSymbol) a
    -> (a -> StateT KState (Either HSymbol) b)
    -> StateT KState (Either HSymbol) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Int -> HKind -> StateT KState (Either HSymbol) ()
    occurs Int
    i
          occurs Int
    i (KVar Int
    i') = if Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    i' then Either HSymbol () -> StateT KState (Either HSymbol) ()
    forall (m :: * -> *) a. Monad m => m a -> StateT KState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Either HSymbol () -> StateT KState (Either HSymbol) ())
    -> Either HSymbol () -> StateT KState (Either HSymbol) ()
    forall a b. (a -> b) -> a -> b
    $ HSymbol -> Either HSymbol ()
    forall a b. a -> Either a b
    Left HSymbol
    "cyclic kind" else () -> StateT KState (Either HSymbol) ()
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      HKind
    k1' <- HKind -> M HKind
    follow HKind
    k1
      HKind
    k2' <- HKind -> M HKind
    follow HKind
    k2
      HKind -> HKind -> StateT KState (Either HSymbol) ()
    unify HKind
    k1' HKind
    k2'

    getVarHKind :: KEnv -> HSymbol -> M HKind
    getVarHKind :: [(HSymbol, HKind)] -> HSymbol -> M HKind
    getVarHKind [(HSymbol, HKind)]
    env HSymbol
    v = case HSymbol -> [(HSymbol, HKind)] -> Maybe HKind
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup HSymbol
    v [(HSymbol, HKind)]
    env of
      Just HKind
    k -> HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    k
      Maybe HKind
    Nothing -> Either HSymbol HKind -> M HKind
    forall (m :: * -> *) a. Monad m => m a -> StateT KState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Either HSymbol HKind -> M HKind)
    -> Either HSymbol HKind -> M HKind
    forall a b. (a -> b) -> a -> b
    $ HSymbol -> Either HSymbol HKind
    forall a b. a -> Either a b
    Left (HSymbol -> Either HSymbol HKind)
    -> HSymbol -> Either HSymbol HKind
    forall a b. (a -> b) -> a -> b
    $ HSymbol
    "Undefined type variable " HSymbol -> HSymbol -> HSymbol
    forall a. [a] -> [a] -> [a]
    ++ HSymbol
    v

    getConHKind :: KEnv -> HSymbol -> M HKind
    getConHKind :: [(HSymbol, HKind)] -> HSymbol -> M HKind
    getConHKind [(HSymbol, HKind)]
    env HSymbol
    v = case HSymbol -> [(HSymbol, HKind)] -> Maybe HKind
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup HSymbol
    v [(HSymbol, HKind)]
    env of
      Just HKind
    k -> HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    k
      Maybe HKind
    Nothing -> Either HSymbol HKind -> M HKind
    forall (m :: * -> *) a. Monad m => m a -> StateT KState m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Either HSymbol HKind -> M HKind)
    -> Either HSymbol HKind -> M HKind
    forall a b. (a -> b) -> a -> b
    $ HSymbol -> Either HSymbol HKind
    forall a b. a -> Either a b
    Left (HSymbol -> Either HSymbol HKind)
    -> HSymbol -> Either HSymbol HKind
    forall a b. (a -> b) -> a -> b
    $ HSymbol
    "Undefined type " HSymbol -> HSymbol -> HSymbol
    forall a. [a] -> [a] -> [a]
    ++ HSymbol
    v

    ground :: HKind -> M HKind
    ground :: HKind -> M HKind
    ground HKind
    KStar = HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    KStar
    ground (KArrow HKind
    k1 HKind
    k2) = (HKind -> HKind -> HKind) -> M HKind -> M HKind -> M HKind
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftM2 HKind -> HKind -> HKind
    KArrow (HKind -> M HKind
    ground HKind
    k1) (HKind -> M HKind
    ground HKind
    k2)
    ground (KVar Int
    i) = do
      Maybe HKind
    mk <- Int -> M (Maybe HKind)
    getVar Int
    i
      case Maybe HKind
    mk of
        Just HKind
    k -> HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    k
        Maybe HKind
    Nothing -> HKind -> M HKind
    forall a. a -> StateT KState (Either HSymbol) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return HKind
    KStar

    getHTCons :: HType -> [HSymbol]
    getHTCons :: HType -> [HSymbol]
    getHTCons (HTApp HType
    f HType
    a)      = HType -> [HSymbol]
    getHTCons HType
    f [HSymbol] -> [HSymbol] -> [HSymbol]
    forall a. Eq a => [a] -> [a] -> [a]
    `union` HType -> [HSymbol]
    getHTCons HType
    a
    getHTCons (HTVar HSymbol
    _)        = []
    getHTCons (HTCon HSymbol
    s)        = [HSymbol
    s]
    getHTCons (HTTuple [HType]
    ts)     = ([HSymbol] -> [HSymbol] -> [HSymbol])
    -> [HSymbol] -> [[HSymbol]] -> [HSymbol]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr [HSymbol] -> [HSymbol] -> [HSymbol]
    forall a. Eq a => [a] -> [a] -> [a]
    union [] ((HType -> [HSymbol]) -> [HType] -> [[HSymbol]]
    forall a b. (a -> b) -> [a] -> [b]
    map HType -> [HSymbol]
    getHTCons [HType]
    ts)
    getHTCons (HTArrow HType
    f HType
    a)    = HType -> [HSymbol]
    getHTCons HType
    f [HSymbol] -> [HSymbol] -> [HSymbol]
    forall a. Eq a => [a] -> [a] -> [a]
    `union` HType -> [HSymbol]
    getHTCons HType
    a
    getHTCons (HTUnion [(HSymbol, [HType])]
    alts)   = ([HSymbol] -> [HSymbol] -> [HSymbol])
    -> [HSymbol] -> [[HSymbol]] -> [HSymbol]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr [HSymbol] -> [HSymbol] -> [HSymbol]
    forall a. Eq a => [a] -> [a] -> [a]
    union [] [ HType -> [HSymbol]
    getHTCons HType
    t | (HSymbol
    _, [HType]
    ts) <- [(HSymbol, [HType])]
    alts, HType
    t <- [HType]
    ts ]
    getHTCons (HTAbstract HSymbol
    _ HKind
    _) = []