{-# LANGUAGE CPP #-}
module Djinn.HCheck (
htCheckEnv,
htCheckType
) where
import Data.List (union)
#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
#if MIN_VERSION_mtl(2,3,0)
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
_) = []