{-# 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
_) = []