{-# 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 f x y = f <$> x <*> 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 String) KState
forall s (m :: * -> *). MonadState s m => m s
get
KState -> StateT KState (Either String) ()
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 (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 String) 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 (m :: * -> *) a. Monad m => a -> m a
return Maybe HKind
mk
addMap :: Int -> HKind -> M ()
addMap :: Int -> HKind -> StateT KState (Either String) ()
addMap Int
i HKind
k = do
(Int
n, IntMap (Maybe HKind)
m) <- StateT KState (Either String) KState
forall s (m :: * -> *). MonadState s m => m s
get
KState -> StateT KState (Either String) ()
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 String) ()
clearState = KState -> StateT KState (Either String) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put KState
initState
htCheckType :: [(HSymbol, ([HSymbol], HType, HKind))] -> HType -> Either String ()
htCheckType :: [(String, ([String], HType, HKind))] -> HType -> Either String ()
htCheckType [(String, ([String], HType, HKind))]
its HType
t = (StateT KState (Either String) () -> KState -> Either String ())
-> KState -> StateT KState (Either String) () -> Either String ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT KState (Either String) () -> KState -> Either String ()
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT KState
initState (StateT KState (Either String) () -> Either String ())
-> StateT KState (Either String) () -> Either String ()
forall a b. (a -> b) -> a -> b
$ do
let vs :: [String]
vs = HType -> [String]
getHTVars HType
t
[HKind]
ks <- (String -> M HKind)
-> [String] -> StateT KState (Either String) [HKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (M HKind -> String -> M HKind
forall a b. a -> b -> a
const M HKind
newKVar) [String]
vs
let env :: [(String, HKind)]
env = [String] -> [HKind] -> [(String, HKind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
vs [HKind]
ks [(String, HKind)] -> [(String, HKind)] -> [(String, HKind)]
forall a. [a] -> [a] -> [a]
++ [(String
i, HKind
k) | (String
i, ([String]
_, HType
_, HKind
k)) <- [(String, ([String], HType, HKind))]
its ]
[(String, HKind)] -> HType -> StateT KState (Either String) ()
iHKindStar [(String, HKind)]
env HType
t
htCheckEnv :: [(HSymbol, ([HSymbol], HType, a))] -> Either String [(HSymbol, ([HSymbol], HType, HKind))]
htCheckEnv :: [(String, ([String], HType, a))]
-> Either String [(String, ([String], HType, HKind))]
htCheckEnv [(String, ([String], HType, a))]
its =
let graph :: [((String, ([String], HType, a)), String, [String])]
graph = [ ((String, ([String], HType, a))
n, String
i, HType -> [String]
getHTCons HType
t) | n :: (String, ([String], HType, a))
n@(String
i, ([String]
_, HType
t, a
_)) <- [(String, ([String], HType, a))]
its ]
order :: [SCC (String, ([String], HType, a))]
order = [((String, ([String], HType, a)), String, [String])]
-> [SCC (String, ([String], HType, a))]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp [((String, ([String], HType, a)), String, [String])]
graph
in case [ [(String, ([String], HType, a))]
c | CyclicSCC [(String, ([String], HType, a))]
c <- [SCC (String, ([String], HType, a))]
order ] of
[(String, ([String], HType, a))]
c : [[(String, ([String], HType, a))]]
_ -> String -> Either String [(String, ([String], HType, HKind))]
forall a b. a -> Either a b
Left (String -> Either String [(String, ([String], HType, HKind))])
-> String -> Either String [(String, ([String], HType, HKind))]
forall a b. (a -> b) -> a -> b
$ String
"Recursive types are not allowed: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [ String
i | (String
i, ([String], HType, a)
_) <- [(String, ([String], HType, a))]
c ]
[] -> (StateT KState (Either String) [(String, ([String], HType, HKind))]
-> KState -> Either String [(String, ([String], HType, HKind))])
-> KState
-> StateT
KState (Either String) [(String, ([String], HType, HKind))]
-> Either String [(String, ([String], HType, HKind))]
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT KState (Either String) [(String, ([String], HType, HKind))]
-> KState -> Either String [(String, ([String], HType, HKind))]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT KState
initState (StateT KState (Either String) [(String, ([String], HType, HKind))]
-> Either String [(String, ([String], HType, HKind))])
-> StateT
KState (Either String) [(String, ([String], HType, HKind))]
-> Either String [(String, ([String], HType, HKind))]
forall a b. (a -> b) -> a -> b
$ StateT KState (Either String) [(String, ([String], HType, HKind))]
addKinds
where addKinds :: StateT KState (Either String) [(String, ([String], HType, HKind))]
addKinds = do
[(String, HKind)]
env <- [(String, HKind)]
-> [(String, ([String], HType, a))] -> M [(String, HKind)]
forall a.
[(String, HKind)]
-> [(String, ([String], HType, a))] -> M [(String, HKind)]
inferHKinds [] ([(String, ([String], HType, a))] -> M [(String, HKind)])
-> [(String, ([String], HType, a))] -> M [(String, HKind)]
forall a b. (a -> b) -> a -> b
$ (SCC (String, ([String], HType, a))
-> (String, ([String], HType, a)))
-> [SCC (String, ([String], HType, a))]
-> [(String, ([String], HType, a))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (AcyclicSCC (String, ([String], HType, a))
n) -> (String, ([String], HType, a))
n) [SCC (String, ([String], HType, a))]
order
let getK :: String -> HKind
getK String
i = HKind -> (HKind -> HKind) -> Maybe HKind -> HKind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> HKind
forall a. HasCallStack => String -> a
error (String -> HKind) -> String -> HKind
forall a b. (a -> b) -> a -> b
$ String
"htCheck " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
i) HKind -> HKind
forall a. a -> a
id (Maybe HKind -> HKind) -> Maybe HKind -> HKind
forall a b. (a -> b) -> a -> b
$ String -> [(String, HKind)] -> Maybe HKind
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
i [(String, HKind)]
env
[(String, ([String], HType, HKind))]
-> StateT
KState (Either String) [(String, ([String], HType, HKind))]
forall (m :: * -> *) a. Monad m => a -> m a
return [ (String
i, ([String]
vs, HType
t, String -> HKind
getK String
i)) | (String
i, ([String]
vs, HType
t, a
_)) <- [(String, ([String], HType, a))]
its ]
inferHKinds :: KEnv -> [(HSymbol, ([HSymbol], HType, a))] -> M KEnv
inferHKinds :: [(String, HKind)]
-> [(String, ([String], HType, a))] -> M [(String, HKind)]
inferHKinds [(String, HKind)]
env [] = [(String, HKind)] -> M [(String, HKind)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(String, HKind)]
env
inferHKinds [(String, HKind)]
env ((String
i, ([String]
vs, HType
t, a
_)) : [(String, ([String], HType, a))]
its) = do
HKind
k <- [(String, HKind)] -> [String] -> HType -> M HKind
inferHKind [(String, HKind)]
env [String]
vs HType
t
[(String, HKind)]
-> [(String, ([String], HType, a))] -> M [(String, HKind)]
forall a.
[(String, HKind)]
-> [(String, ([String], HType, a))] -> M [(String, HKind)]
inferHKinds ((String
i, HKind
k) (String, HKind) -> [(String, HKind)] -> [(String, HKind)]
forall a. a -> [a] -> [a]
: [(String, HKind)]
env) [(String, ([String], HType, a))]
its
inferHKind :: KEnv -> [HSymbol] -> HType -> M HKind
inferHKind :: [(String, HKind)] -> [String] -> HType -> M HKind
inferHKind [(String, HKind)]
_ [String]
_ (HTAbstract String
_ HKind
k) = HKind -> M HKind
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
k
inferHKind [(String, HKind)]
env [String]
vs HType
t = do
StateT KState (Either String) ()
clearState
[HKind]
ks <- (String -> M HKind)
-> [String] -> StateT KState (Either String) [HKind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (M HKind -> String -> M HKind
forall a b. a -> b -> a
const M HKind
newKVar) [String]
vs
let env' :: [(String, HKind)]
env' = [String] -> [HKind] -> [(String, HKind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
vs [HKind]
ks [(String, HKind)] -> [(String, HKind)] -> [(String, HKind)]
forall a. [a] -> [a] -> [a]
++ [(String, HKind)]
env
HKind
k <- [(String, HKind)] -> HType -> M HKind
iHKind [(String, 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 (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 :: [(String, HKind)] -> HType -> M HKind
iHKind [(String, HKind)]
env (HTApp HType
f HType
a) = do
HKind
kf <- [(String, HKind)] -> HType -> M HKind
iHKind [(String, HKind)]
env HType
f
HKind
ka <- [(String, HKind)] -> HType -> M HKind
iHKind [(String, HKind)]
env HType
a
HKind
r <- M HKind
newKVar
HKind -> HKind -> StateT KState (Either String) ()
unifyK (HKind -> HKind -> HKind
KArrow HKind
ka HKind
r) HKind
kf
HKind -> M HKind
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
r
iHKind [(String, HKind)]
env (HTVar String
v) = do
[(String, HKind)] -> String -> M HKind
getVarHKind [(String, HKind)]
env String
v
iHKind [(String, HKind)]
env (HTCon String
c) = do
[(String, HKind)] -> String -> M HKind
getConHKind [(String, HKind)]
env String
c
iHKind [(String, HKind)]
env (HTTuple [HType]
ts) = do
(HType -> StateT KState (Either String) ())
-> [HType] -> StateT KState (Either String) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([(String, HKind)] -> HType -> StateT KState (Either String) ()
iHKindStar [(String, HKind)]
env) [HType]
ts
HKind -> M HKind
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
KStar
iHKind [(String, HKind)]
env (HTArrow HType
f HType
a) = do
[(String, HKind)] -> HType -> StateT KState (Either String) ()
iHKindStar [(String, HKind)]
env HType
f
[(String, HKind)] -> HType -> StateT KState (Either String) ()
iHKindStar [(String, HKind)]
env HType
a
HKind -> M HKind
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
KStar
iHKind [(String, HKind)]
env (HTUnion [(String, [HType])]
cs) = do
((String, [HType]) -> StateT KState (Either String) ())
-> [(String, [HType])] -> StateT KState (Either String) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (String
_, [HType]
ts) -> (HType -> StateT KState (Either String) ())
-> [HType] -> StateT KState (Either String) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([(String, HKind)] -> HType -> StateT KState (Either String) ()
iHKindStar [(String, HKind)]
env) [HType]
ts) [(String, [HType])]
cs
HKind -> M HKind
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
KStar
iHKind [(String, HKind)]
_ (HTAbstract String
_ HKind
_) = String -> M HKind
forall a. HasCallStack => String -> a
error String
"iHKind HTAbstract"
iHKindStar :: KEnv -> HType -> M ()
iHKindStar :: [(String, HKind)] -> HType -> StateT KState (Either String) ()
iHKindStar [(String, HKind)]
env HType
t = do
HKind
k <- [(String, HKind)] -> HType -> M HKind
iHKind [(String, HKind)]
env HType
t
HKind -> HKind -> StateT KState (Either String) ()
unifyK HKind
k HKind
KStar
unifyK :: HKind -> HKind -> M ()
unifyK :: HKind -> HKind -> StateT KState (Either String) ()
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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= HKind -> M HKind
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 (m :: * -> *) a. Monad m => a -> m a
return HKind
k
unify :: HKind -> HKind -> StateT KState (Either String) ()
unify HKind
KStar HKind
KStar = () -> StateT KState (Either String) ()
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 String) ()
unifyK HKind
k11 HKind
k21; HKind -> HKind -> StateT KState (Either String) ()
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 String) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
unify (KVar Int
i) HKind
k = do Int -> HKind -> StateT KState (Either String) ()
occurs Int
i HKind
k; Int -> HKind -> StateT KState (Either String) ()
addMap Int
i HKind
k
unify HKind
k (KVar Int
i) = do Int -> HKind -> StateT KState (Either String) ()
occurs Int
i HKind
k; Int -> HKind -> StateT KState (Either String) ()
addMap Int
i HKind
k
unify HKind
_ HKind
_ = Either String () -> StateT KState (Either String) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Either String () -> StateT KState (Either String) ())
-> Either String () -> StateT KState (Either String) ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ String
"kind error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (HKind, HKind) -> String
forall a. Show a => a -> String
show (HKind
k1, HKind
k2)
occurs :: Int -> HKind -> StateT KState (Either String) ()
occurs Int
_ HKind
KStar = () -> StateT KState (Either String) ()
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 String) ())
-> StateT KState (Either String) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> HKind -> StateT KState (Either String) ()
occurs Int
i; HKind -> M HKind
follow HKind
a M HKind
-> (HKind -> StateT KState (Either String) ())
-> StateT KState (Either String) ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> HKind -> StateT KState (Either String) ()
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 String () -> StateT KState (Either String) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Either String () -> StateT KState (Either String) ())
-> Either String () -> StateT KState (Either String) ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left String
"cyclic kind" else () -> StateT KState (Either String) ()
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 String) ()
unify HKind
k1' HKind
k2'
getVarHKind :: KEnv -> HSymbol -> M HKind
getVarHKind :: [(String, HKind)] -> String -> M HKind
getVarHKind [(String, HKind)]
env String
v = case String -> [(String, HKind)] -> Maybe HKind
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
v [(String, HKind)]
env of
Just HKind
k -> HKind -> M HKind
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
k
Maybe HKind
Nothing -> Either String HKind -> M HKind
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Either String HKind -> M HKind) -> Either String HKind -> M HKind
forall a b. (a -> b) -> a -> b
$ String -> Either String HKind
forall a b. a -> Either a b
Left (String -> Either String HKind) -> String -> Either String HKind
forall a b. (a -> b) -> a -> b
$ String
"Undefined type variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v
getConHKind :: KEnv -> HSymbol -> M HKind
getConHKind :: [(String, HKind)] -> String -> M HKind
getConHKind [(String, HKind)]
env String
v = case String -> [(String, HKind)] -> Maybe HKind
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
v [(String, HKind)]
env of
Just HKind
k -> HKind -> M HKind
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
k
Maybe HKind
Nothing -> Either String HKind -> M HKind
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Either String HKind -> M HKind) -> Either String HKind -> M HKind
forall a b. (a -> b) -> a -> b
$ String -> Either String HKind
forall a b. a -> Either a b
Left (String -> Either String HKind) -> String -> Either String HKind
forall a b. (a -> b) -> a -> b
$ String
"Undefined type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v
ground :: HKind -> M HKind
ground :: HKind -> M HKind
ground HKind
KStar = HKind -> M HKind
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 (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
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 (m :: * -> *) a. Monad m => a -> m a
return HKind
k
Maybe HKind
Nothing -> HKind -> M HKind
forall (m :: * -> *) a. Monad m => a -> m a
return HKind
KStar
getHTCons :: HType -> [HSymbol]
getHTCons :: HType -> [String]
getHTCons (HTApp HType
f HType
a) = HType -> [String]
getHTCons HType
f [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`union` HType -> [String]
getHTCons HType
a
getHTCons (HTVar String
_) = []
getHTCons (HTCon String
s) = [String
s]
getHTCons (HTTuple [HType]
ts) = ([String] -> [String] -> [String])
-> [String] -> [[String]] -> [String]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
union [] ((HType -> [String]) -> [HType] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map HType -> [String]
getHTCons [HType]
ts)
getHTCons (HTArrow HType
f HType
a) = HType -> [String]
getHTCons HType
f [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
`union` HType -> [String]
getHTCons HType
a
getHTCons (HTUnion [(String, [HType])]
alts) = ([String] -> [String] -> [String])
-> [String] -> [[String]] -> [String]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
union [] [ HType -> [String]
getHTCons HType
t | (String
_, [HType]
ts) <- [(String, [HType])]
alts, HType
t <- [HType]
ts ]
getHTCons (HTAbstract String
_ HKind
_) = []