{-# LANGUAGE CPP #-}
module Checks.KindCheck (kindCheck) where
#if __GLASGOW_HASKELL__ >= 804
import Prelude hiding ((<>))
#endif
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative ((<$>), (<*>))
#endif
import Control.Monad (when, foldM)
import Control.Monad.Fix (mfix)
import qualified Control.Monad.State as S (State, runState, gets, modify)
import Data.List (partition, nub)
import Curry.Base.Ident
import Curry.Base.Position
import Curry.Base.SpanInfo ()
import Curry.Base.Pretty
import Curry.Syntax
import Curry.Syntax.Pretty
import Base.CurryKinds
import Base.Expr
import Base.Kinds
import Base.KindSubst
import Base.Messages (Message, posMessage, internalError)
import Base.SCC
import Base.TopEnv
import Base.Types
import Base.TypeExpansion
import Env.Class
import Env.TypeConstructor
kindCheck :: TCEnv -> ClassEnv -> Module a -> ((TCEnv, ClassEnv), [Message])
kindCheck :: TCEnv -> ClassEnv -> Module a -> ((TCEnv, ClassEnv), [Message])
kindCheck tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv (Module _ _ m :: ModuleIdent
m _ _ ds :: [Decl a]
ds) = KCM (TCEnv, ClassEnv) -> KCState -> ((TCEnv, ClassEnv), [Message])
forall a. KCM a -> KCState -> (a, [Message])
runKCM KCM (TCEnv, ClassEnv)
check KCState
initState
where
check :: KCM (TCEnv, ClassEnv)
check = do
[Decl a] -> KCM ()
forall a. [Decl a] -> KCM ()
checkNonRecursiveTypes [Decl a]
tds KCM () -> KCM () -> KCM ()
&&> [Decl a] -> KCM ()
forall a. [Decl a] -> KCM ()
checkAcyclicSuperClasses [Decl a]
cds
[Message]
errs <- (KCState -> [Message]) -> StateT KCState Identity [Message]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets KCState -> [Message]
errors
if [Message] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Message]
errs
then KCM (TCEnv, ClassEnv)
checkDecls
else (TCEnv, ClassEnv) -> KCM (TCEnv, ClassEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCEnv
tcEnv, ClassEnv
clsEnv)
checkDecls :: KCM (TCEnv, ClassEnv)
checkDecls = do
(tcEnv' :: TCEnv
tcEnv', clsEnv' :: ClassEnv
clsEnv') <- TCEnv -> ClassEnv -> [Decl a] -> KCM (TCEnv, ClassEnv)
forall a. TCEnv -> ClassEnv -> [Decl a] -> KCM (TCEnv, ClassEnv)
kcDecls TCEnv
tcEnv ClassEnv
clsEnv [Decl a]
tcds
(Decl a -> KCM ()) -> [Decl a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> Decl a -> KCM ()
forall a. TCEnv -> Decl a -> KCM ()
kcDecl TCEnv
tcEnv') [Decl a]
ods
(TCEnv, ClassEnv) -> KCM (TCEnv, ClassEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCEnv
tcEnv', ClassEnv
clsEnv')
tds :: [Decl a]
tds = (Decl a -> Bool) -> [Decl a] -> [Decl a]
forall a. (a -> Bool) -> [a] -> [a]
filter Decl a -> Bool
forall a. Decl a -> Bool
isTypeDecl [Decl a]
tcds
cds :: [Decl a]
cds = (Decl a -> Bool) -> [Decl a] -> [Decl a]
forall a. (a -> Bool) -> [a] -> [a]
filter Decl a -> Bool
forall a. Decl a -> Bool
isClassDecl [Decl a]
tcds
(tcds :: [Decl a]
tcds, ods :: [Decl a]
ods) = (Decl a -> Bool) -> [Decl a] -> ([Decl a], [Decl a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Decl a -> Bool
forall a. Decl a -> Bool
isTypeOrClassDecl [Decl a]
ds
initState :: KCState
initState = ModuleIdent -> KindSubst -> Int -> [Message] -> KCState
KCState ModuleIdent
m KindSubst
forall a b. Subst a b
idSubst 0 []
type KCM = S.State KCState
data KCState = KCState
{ KCState -> ModuleIdent
moduleIdent :: ModuleIdent
, KCState -> KindSubst
kindSubst :: KindSubst
, KCState -> Int
nextId :: Int
, KCState -> [Message]
errors :: [Message]
}
(&&>) :: KCM () -> KCM () -> KCM ()
pre :: KCM ()
pre &&> :: KCM () -> KCM () -> KCM ()
&&> suf :: KCM ()
suf = do
[Message]
errs <- KCM ()
pre KCM ()
-> StateT KCState Identity [Message]
-> StateT KCState Identity [Message]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (KCState -> [Message]) -> StateT KCState Identity [Message]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets KCState -> [Message]
errors
Bool -> KCM () -> KCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Message] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Message]
errs) KCM ()
suf
runKCM :: KCM a -> KCState -> (a, [Message])
runKCM :: KCM a -> KCState -> (a, [Message])
runKCM kcm :: KCM a
kcm s :: KCState
s = let (a :: a
a, s' :: KCState
s') = KCM a -> KCState -> (a, KCState)
forall s a. State s a -> s -> (a, s)
S.runState KCM a
kcm KCState
s in (a
a, [Message] -> [Message]
forall a. [a] -> [a]
reverse ([Message] -> [Message]) -> [Message] -> [Message]
forall a b. (a -> b) -> a -> b
$ KCState -> [Message]
errors KCState
s')
getModuleIdent :: KCM ModuleIdent
getModuleIdent :: KCM ModuleIdent
getModuleIdent = (KCState -> ModuleIdent) -> KCM ModuleIdent
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets KCState -> ModuleIdent
moduleIdent
getKindSubst :: KCM KindSubst
getKindSubst :: KCM KindSubst
getKindSubst = (KCState -> KindSubst) -> KCM KindSubst
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets KCState -> KindSubst
kindSubst
modifyKindSubst :: (KindSubst -> KindSubst) -> KCM ()
modifyKindSubst :: (KindSubst -> KindSubst) -> KCM ()
modifyKindSubst f :: KindSubst -> KindSubst
f = (KCState -> KCState) -> KCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
S.modify ((KCState -> KCState) -> KCM ()) -> (KCState -> KCState) -> KCM ()
forall a b. (a -> b) -> a -> b
$ \s :: KCState
s -> KCState
s { kindSubst :: KindSubst
kindSubst = KindSubst -> KindSubst
f (KindSubst -> KindSubst) -> KindSubst -> KindSubst
forall a b. (a -> b) -> a -> b
$ KCState -> KindSubst
kindSubst KCState
s }
getNextId :: KCM Int
getNextId :: KCM Int
getNextId = do
Int
nid <- (KCState -> Int) -> KCM Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
S.gets KCState -> Int
nextId
(KCState -> KCState) -> KCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
S.modify ((KCState -> KCState) -> KCM ()) -> (KCState -> KCState) -> KCM ()
forall a b. (a -> b) -> a -> b
$ \s :: KCState
s -> KCState
s { nextId :: Int
nextId = Int -> Int
forall a. Enum a => a -> a
succ Int
nid }
Int -> KCM Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
nid
report :: Message -> KCM ()
report :: Message -> KCM ()
report err :: Message
err = (KCState -> KCState) -> KCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
S.modify (\s :: KCState
s -> KCState
s { errors :: [Message]
errors = Message
err Message -> [Message] -> [Message]
forall a. a -> [a] -> [a]
: KCState -> [Message]
errors KCState
s })
ok :: KCM ()
ok :: KCM ()
ok = () -> KCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
bt :: Decl a -> [Ident]
bt :: Decl a -> [Ident]
bt (DataDecl _ tc :: Ident
tc _ _ _) = [Ident
tc]
bt (ExternalDataDecl _ tc :: Ident
tc _) = [Ident
tc]
bt (NewtypeDecl _ tc :: Ident
tc _ _ _) = [Ident
tc]
bt (TypeDecl _ tc :: Ident
tc _ _) = [Ident
tc]
bt (ClassDecl _ _ cls :: Ident
cls _ _) = [Ident
cls]
bt _ = []
ft :: ModuleIdent -> Decl a -> [Ident]
ft :: ModuleIdent -> Decl a -> [Ident]
ft m :: ModuleIdent
m d :: Decl a
d = ModuleIdent -> Decl a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Decl a
d []
class HasType a where
fts :: ModuleIdent -> a -> [Ident] -> [Ident]
instance HasType a => HasType [a] where
fts :: ModuleIdent -> [a] -> [Ident] -> [Ident]
fts m :: ModuleIdent
m = ([Ident] -> [a] -> [Ident]) -> [a] -> [Ident] -> [Ident]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (([Ident] -> [a] -> [Ident]) -> [a] -> [Ident] -> [Ident])
-> ([Ident] -> [a] -> [Ident]) -> [a] -> [Ident] -> [Ident]
forall a b. (a -> b) -> a -> b
$ (a -> [Ident] -> [Ident]) -> [Ident] -> [a] -> [Ident]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((a -> [Ident] -> [Ident]) -> [Ident] -> [a] -> [Ident])
-> (a -> [Ident] -> [Ident]) -> [Ident] -> [a] -> [Ident]
forall a b. (a -> b) -> a -> b
$ ModuleIdent -> a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m
instance HasType a => HasType (Maybe a) where
fts :: ModuleIdent -> Maybe a -> [Ident] -> [Ident]
fts m :: ModuleIdent
m = ([Ident] -> [Ident])
-> (a -> [Ident] -> [Ident]) -> Maybe a -> [Ident] -> [Ident]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Ident] -> [Ident]
forall a. a -> a
id ((a -> [Ident] -> [Ident]) -> Maybe a -> [Ident] -> [Ident])
-> (a -> [Ident] -> [Ident]) -> Maybe a -> [Ident] -> [Ident]
forall a b. (a -> b) -> a -> b
$ ModuleIdent -> a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m
instance HasType (Decl a) where
fts :: ModuleIdent -> Decl a -> [Ident] -> [Ident]
fts _ (InfixDecl _ _ _ _) = [Ident] -> [Ident]
forall a. a -> a
id
fts m :: ModuleIdent
m (DataDecl _ _ _ cs :: [ConstrDecl]
cs clss :: [QualIdent]
clss) = ModuleIdent -> [ConstrDecl] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [ConstrDecl]
cs ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> [QualIdent] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [QualIdent]
clss
fts _ (ExternalDataDecl _ _ _) = [Ident] -> [Ident]
forall a. a -> a
id
fts m :: ModuleIdent
m (NewtypeDecl _ _ _ nc :: NewConstrDecl
nc clss :: [QualIdent]
clss) = ModuleIdent -> NewConstrDecl -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m NewConstrDecl
nc ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> [QualIdent] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [QualIdent]
clss
fts m :: ModuleIdent
m (TypeDecl _ _ _ ty :: TypeExpr
ty) = ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty
fts m :: ModuleIdent
m (TypeSig _ _ ty :: QualTypeExpr
ty) = ModuleIdent -> QualTypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m QualTypeExpr
ty
fts m :: ModuleIdent
m (FunctionDecl _ _ _ eqs :: [Equation a]
eqs) = ModuleIdent -> [Equation a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Equation a]
eqs
fts _ (ExternalDecl _ _) = [Ident] -> [Ident]
forall a. a -> a
id
fts m :: ModuleIdent
m (PatternDecl _ _ rhs :: Rhs a
rhs) = ModuleIdent -> Rhs a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Rhs a
rhs
fts _ (FreeDecl _ _) = [Ident] -> [Ident]
forall a. a -> a
id
fts m :: ModuleIdent
m (DefaultDecl _ tys :: [TypeExpr]
tys) = ModuleIdent -> [TypeExpr] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [TypeExpr]
tys
fts m :: ModuleIdent
m (ClassDecl _ cx :: Context
cx _ _ ds :: [Decl a]
ds) = ModuleIdent -> Context -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Context
cx ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> [Decl a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Decl a]
ds
fts m :: ModuleIdent
m (InstanceDecl _ cx :: Context
cx cls :: QualIdent
cls inst :: TypeExpr
inst ds :: [Decl a]
ds) =
ModuleIdent -> Context -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Context
cx ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> QualIdent -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m QualIdent
cls ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
inst ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> [Decl a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Decl a]
ds
instance HasType ConstrDecl where
fts :: ModuleIdent -> ConstrDecl -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (ConstrDecl _ _ tys :: [TypeExpr]
tys) = ModuleIdent -> [TypeExpr] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [TypeExpr]
tys
fts m :: ModuleIdent
m (ConOpDecl _ ty1 :: TypeExpr
ty1 _ ty2 :: TypeExpr
ty2) = ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty1 ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty2
fts m :: ModuleIdent
m (RecordDecl _ _ fs :: [FieldDecl]
fs) = ModuleIdent -> [FieldDecl] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [FieldDecl]
fs
instance HasType FieldDecl where
fts :: ModuleIdent -> FieldDecl -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (FieldDecl _ _ ty :: TypeExpr
ty) = ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty
instance HasType NewConstrDecl where
fts :: ModuleIdent -> NewConstrDecl -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (NewConstrDecl _ _ ty :: TypeExpr
ty) = ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty
fts m :: ModuleIdent
m (NewRecordDecl _ _ (_, ty :: TypeExpr
ty)) = ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty
instance HasType Constraint where
fts :: ModuleIdent -> Constraint -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (Constraint _ qcls :: QualIdent
qcls _) = ModuleIdent -> QualIdent -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m QualIdent
qcls
instance HasType QualTypeExpr where
fts :: ModuleIdent -> QualTypeExpr -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (QualTypeExpr _ cx :: Context
cx ty :: TypeExpr
ty) = ModuleIdent -> Context -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Context
cx ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty
instance HasType TypeExpr where
fts :: ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (ConstructorType _ tc :: QualIdent
tc) = ModuleIdent -> QualIdent -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m QualIdent
tc
fts m :: ModuleIdent
m (ApplyType _ ty1 :: TypeExpr
ty1 ty2 :: TypeExpr
ty2) = ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty1 ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty2
fts _ (VariableType _ _) = [Ident] -> [Ident]
forall a. a -> a
id
fts m :: ModuleIdent
m (TupleType _ tys :: [TypeExpr]
tys) = (Int -> Ident
tupleId ([TypeExpr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeExpr]
tys) Ident -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
:) ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> [TypeExpr] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [TypeExpr]
tys
fts m :: ModuleIdent
m (ListType _ ty :: TypeExpr
ty) = (Ident
listId Ident -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
:) ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty
fts m :: ModuleIdent
m (ArrowType _ ty1 :: TypeExpr
ty1 ty2 :: TypeExpr
ty2) = (Ident
arrowId Ident -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
:) ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty1 ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty2
fts m :: ModuleIdent
m (ParenType _ ty :: TypeExpr
ty) = ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty
fts m :: ModuleIdent
m (ForallType _ _ ty :: TypeExpr
ty) = ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty
instance HasType (Equation a) where
fts :: ModuleIdent -> Equation a -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (Equation _ _ rhs :: Rhs a
rhs) = ModuleIdent -> Rhs a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Rhs a
rhs
instance HasType (Rhs a) where
fts :: ModuleIdent -> Rhs a -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (SimpleRhs _ e :: Expression a
e ds :: [Decl a]
ds) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> [Decl a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Decl a]
ds
fts m :: ModuleIdent
m (GuardedRhs _ es :: [CondExpr a]
es ds :: [Decl a]
ds) = ModuleIdent -> [CondExpr a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [CondExpr a]
es ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> [Decl a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Decl a]
ds
instance HasType (CondExpr a) where
fts :: ModuleIdent -> CondExpr a -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (CondExpr _ g :: Expression a
g e :: Expression a
e) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
g ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e
instance HasType (Expression a) where
fts :: ModuleIdent -> Expression a -> [Ident] -> [Ident]
fts _ (Literal _ _ _) = [Ident] -> [Ident]
forall a. a -> a
id
fts _ (Variable _ _ _) = [Ident] -> [Ident]
forall a. a -> a
id
fts _ (Constructor _ _ _) = [Ident] -> [Ident]
forall a. a -> a
id
fts m :: ModuleIdent
m (Paren _ e :: Expression a
e) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e
fts m :: ModuleIdent
m (Typed _ e :: Expression a
e ty :: QualTypeExpr
ty) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> QualTypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m QualTypeExpr
ty
fts m :: ModuleIdent
m (Record _ _ _ fs :: [Field (Expression a)]
fs) = ModuleIdent -> [Field (Expression a)] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Field (Expression a)]
fs
fts m :: ModuleIdent
m (RecordUpdate _ e :: Expression a
e fs :: [Field (Expression a)]
fs) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> [Field (Expression a)] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Field (Expression a)]
fs
fts m :: ModuleIdent
m (Tuple _ es :: [Expression a]
es) = ModuleIdent -> [Expression a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Expression a]
es
fts m :: ModuleIdent
m (List _ _ es :: [Expression a]
es) = ModuleIdent -> [Expression a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Expression a]
es
fts m :: ModuleIdent
m (ListCompr _ e :: Expression a
e stms :: [Statement a]
stms) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> [Statement a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Statement a]
stms
fts m :: ModuleIdent
m (EnumFrom _ e :: Expression a
e) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e
fts m :: ModuleIdent
m (EnumFromThen _ e1 :: Expression a
e1 e2 :: Expression a
e2) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e1 ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e2
fts m :: ModuleIdent
m (EnumFromTo _ e1 :: Expression a
e1 e2 :: Expression a
e2) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e1 ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e2
fts m :: ModuleIdent
m (EnumFromThenTo _ e1 :: Expression a
e1 e2 :: Expression a
e2 e3 :: Expression a
e3) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e1 ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e2 ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e3
fts m :: ModuleIdent
m (UnaryMinus _ e :: Expression a
e) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e
fts m :: ModuleIdent
m (Apply _ e1 :: Expression a
e1 e2 :: Expression a
e2) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e1 ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e2
fts m :: ModuleIdent
m (InfixApply _ e1 :: Expression a
e1 _ e2 :: Expression a
e2) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e1 ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e2
fts m :: ModuleIdent
m (LeftSection _ e :: Expression a
e _) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e
fts m :: ModuleIdent
m (RightSection _ _ e :: Expression a
e) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e
fts m :: ModuleIdent
m (Lambda _ _ e :: Expression a
e) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e
fts m :: ModuleIdent
m (Let _ ds :: [Decl a]
ds e :: Expression a
e) = ModuleIdent -> [Decl a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Decl a]
ds ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e
fts m :: ModuleIdent
m (Do _ stms :: [Statement a]
stms e :: Expression a
e) = ModuleIdent -> [Statement a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Statement a]
stms ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e
fts m :: ModuleIdent
m (IfThenElse _ e1 :: Expression a
e1 e2 :: Expression a
e2 e3 :: Expression a
e3) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e1 ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e2 ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e3
fts m :: ModuleIdent
m (Case _ _ e :: Expression a
e as :: [Alt a]
as) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e ([Ident] -> [Ident]) -> ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleIdent -> [Alt a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Alt a]
as
instance HasType (Statement a) where
fts :: ModuleIdent -> Statement a -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (StmtExpr _ e :: Expression a
e) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e
fts m :: ModuleIdent
m (StmtDecl _ ds :: [Decl a]
ds) = ModuleIdent -> [Decl a] -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m [Decl a]
ds
fts m :: ModuleIdent
m (StmtBind _ _ e :: Expression a
e) = ModuleIdent -> Expression a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Expression a
e
instance HasType (Alt a) where
fts :: ModuleIdent -> Alt a -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (Alt _ _ rhs :: Rhs a
rhs) = ModuleIdent -> Rhs a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m Rhs a
rhs
instance HasType a => HasType (Field a) where
fts :: ModuleIdent -> Field a -> [Ident] -> [Ident]
fts m :: ModuleIdent
m (Field _ _ x :: a
x) = ModuleIdent -> a -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m a
x
instance HasType QualIdent where
fts :: ModuleIdent -> QualIdent -> [Ident] -> [Ident]
fts m :: ModuleIdent
m qident :: QualIdent
qident = ([Ident] -> [Ident])
-> (Ident -> [Ident] -> [Ident])
-> Maybe Ident
-> [Ident]
-> [Ident]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Ident] -> [Ident]
forall a. a -> a
id (:) (ModuleIdent -> QualIdent -> Maybe Ident
localIdent ModuleIdent
m QualIdent
qident)
ft' :: ModuleIdent -> Decl a -> [Ident]
ft' :: ModuleIdent -> Decl a -> [Ident]
ft' _ (DataDecl _ _ _ _ _) = []
ft' _ (ExternalDataDecl _ _ _) = []
ft' m :: ModuleIdent
m (NewtypeDecl _ _ _ nc :: NewConstrDecl
nc _) = ModuleIdent -> NewConstrDecl -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m NewConstrDecl
nc []
ft' m :: ModuleIdent
m (TypeDecl _ _ _ ty :: TypeExpr
ty) = ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
forall a. HasType a => ModuleIdent -> a -> [Ident] -> [Ident]
fts ModuleIdent
m TypeExpr
ty []
ft' _ _ = []
checkNonRecursiveTypes :: [Decl a] -> KCM ()
checkNonRecursiveTypes :: [Decl a] -> KCM ()
checkNonRecursiveTypes ds :: [Decl a]
ds = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
([Decl a] -> KCM ()) -> [[Decl a]] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Decl a] -> KCM ()
forall a. [Decl a] -> KCM ()
checkTypeAndNewtypeDecls ([[Decl a]] -> KCM ()) -> [[Decl a]] -> KCM ()
forall a b. (a -> b) -> a -> b
$ (Decl a -> [Ident])
-> (Decl a -> [Ident]) -> [Decl a] -> [[Decl a]]
forall b a. Eq b => (a -> [b]) -> (a -> [b]) -> [a] -> [[a]]
scc Decl a -> [Ident]
forall a. Decl a -> [Ident]
bt (ModuleIdent -> Decl a -> [Ident]
forall a. ModuleIdent -> Decl a -> [Ident]
ft' ModuleIdent
m) [Decl a]
ds
checkTypeAndNewtypeDecls :: [Decl a] -> KCM ()
checkTypeAndNewtypeDecls :: [Decl a] -> KCM ()
checkTypeAndNewtypeDecls [] =
String -> KCM ()
forall a. String -> a
internalError "Checks.KindCheck.checkTypeAndNewtypeDecls: empty list"
checkTypeAndNewtypeDecls [DataDecl _ _ _ _ _] = KCM ()
ok
checkTypeAndNewtypeDecls [ExternalDataDecl _ _ _] = KCM ()
ok
checkTypeAndNewtypeDecls [d :: Decl a
d] | Decl a -> Bool
forall a. Decl a -> Bool
isTypeOrNewtypeDecl Decl a
d = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
let tc :: Ident
tc = Decl a -> Ident
forall a. Decl a -> Ident
typeConstructor Decl a
d
Bool -> KCM () -> KCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Ident
tc Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ModuleIdent -> Decl a -> [Ident]
forall a. ModuleIdent -> Decl a -> [Ident]
ft ModuleIdent
m Decl a
d) (KCM () -> KCM ()) -> KCM () -> KCM ()
forall a b. (a -> b) -> a -> b
$ Message -> KCM ()
report (Message -> KCM ()) -> Message -> KCM ()
forall a b. (a -> b) -> a -> b
$ [Ident] -> Message
errRecursiveTypes [Ident
tc]
checkTypeAndNewtypeDecls (d :: Decl a
d:ds :: [Decl a]
ds) | Decl a -> Bool
forall a. Decl a -> Bool
isTypeOrNewtypeDecl Decl a
d =
Message -> KCM ()
report (Message -> KCM ()) -> Message -> KCM ()
forall a b. (a -> b) -> a -> b
$ [Ident] -> Message
errRecursiveTypes ([Ident] -> Message) -> [Ident] -> Message
forall a b. (a -> b) -> a -> b
$
Decl a -> Ident
forall a. Decl a -> Ident
typeConstructor Decl a
d Ident -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
: [Decl a -> Ident
forall a. Decl a -> Ident
typeConstructor Decl a
d' | Decl a
d' <- [Decl a]
ds, Decl a -> Bool
forall a. Decl a -> Bool
isTypeOrNewtypeDecl Decl a
d']
checkTypeAndNewtypeDecls _ = String -> KCM ()
forall a. String -> a
internalError
"Checks.KindCheck.checkTypeAndNewtypeDecls: no type or newtype declarations"
fc :: ModuleIdent -> Context -> [Ident]
fc :: ModuleIdent -> Context -> [Ident]
fc m :: ModuleIdent
m = (Constraint -> [Ident] -> [Ident]) -> [Ident] -> Context -> [Ident]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Constraint -> [Ident] -> [Ident]
fc' []
where
fc' :: Constraint -> [Ident] -> [Ident]
fc' (Constraint _ qcls :: QualIdent
qcls _) = ([Ident] -> [Ident])
-> (Ident -> [Ident] -> [Ident])
-> Maybe Ident
-> [Ident]
-> [Ident]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Ident] -> [Ident]
forall a. a -> a
id (:) (ModuleIdent -> QualIdent -> Maybe Ident
localIdent ModuleIdent
m QualIdent
qcls)
checkAcyclicSuperClasses :: [Decl a] -> KCM ()
checkAcyclicSuperClasses :: [Decl a] -> KCM ()
checkAcyclicSuperClasses ds :: [Decl a]
ds = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
([Decl a] -> KCM ()) -> [[Decl a]] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Decl a] -> KCM ()
forall a. [Decl a] -> KCM ()
checkClassDecl ([[Decl a]] -> KCM ()) -> [[Decl a]] -> KCM ()
forall a b. (a -> b) -> a -> b
$ (Decl a -> [Ident])
-> (Decl a -> [Ident]) -> [Decl a] -> [[Decl a]]
forall b a. Eq b => (a -> [b]) -> (a -> [b]) -> [a] -> [[a]]
scc Decl a -> [Ident]
forall a. Decl a -> [Ident]
bt (\(ClassDecl _ cx :: Context
cx _ _ _) -> ModuleIdent -> Context -> [Ident]
fc ModuleIdent
m Context
cx) [Decl a]
ds
checkClassDecl :: [Decl a] -> KCM ()
checkClassDecl :: [Decl a] -> KCM ()
checkClassDecl [] =
String -> KCM ()
forall a. String -> a
internalError "Checks.KindCheck.checkClassDecl: empty list"
checkClassDecl [ClassDecl _ cx :: Context
cx cls :: Ident
cls _ _] = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
Bool -> KCM () -> KCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Ident
cls Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ModuleIdent -> Context -> [Ident]
fc ModuleIdent
m Context
cx) (KCM () -> KCM ()) -> KCM () -> KCM ()
forall a b. (a -> b) -> a -> b
$ Message -> KCM ()
report (Message -> KCM ()) -> Message -> KCM ()
forall a b. (a -> b) -> a -> b
$ [Ident] -> Message
errRecursiveClasses [Ident
cls]
checkClassDecl (ClassDecl _ _ cls :: Ident
cls _ _ : ds :: [Decl a]
ds) =
Message -> KCM ()
report (Message -> KCM ()) -> Message -> KCM ()
forall a b. (a -> b) -> a -> b
$ [Ident] -> Message
errRecursiveClasses ([Ident] -> Message) -> [Ident] -> Message
forall a b. (a -> b) -> a -> b
$ Ident
cls Ident -> [Ident] -> [Ident]
forall a. a -> [a] -> [a]
: [Ident
cls' | ClassDecl _ _ cls' :: Ident
cls' _ _ <- [Decl a]
ds]
checkClassDecl _ =
String -> KCM ()
forall a. String -> a
internalError "Checks.KindCheck.checkClassDecl: no class declaration"
bindKind :: ModuleIdent -> TCEnv -> ClassEnv -> TCEnv -> Decl a -> KCM TCEnv
bindKind :: ModuleIdent -> TCEnv -> ClassEnv -> TCEnv -> Decl a -> KCM TCEnv
bindKind m :: ModuleIdent
m tcEnv' :: TCEnv
tcEnv' clsEnv :: ClassEnv
clsEnv tcEnv :: TCEnv
tcEnv (DataDecl _ tc :: Ident
tc tvs :: [Ident]
tvs cs :: [ConstrDecl]
cs _) =
(QualIdent -> Kind -> [DataConstr] -> TypeInfo)
-> Ident
-> [Ident]
-> Maybe Kind
-> [DataConstr]
-> TCEnv
-> KCM TCEnv
forall a.
(QualIdent -> Kind -> a -> TypeInfo)
-> Ident -> [Ident] -> Maybe Kind -> a -> TCEnv -> KCM TCEnv
bindTypeConstructor QualIdent -> Kind -> [DataConstr] -> TypeInfo
DataType Ident
tc [Ident]
tvs (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
KindStar) ((ConstrDecl -> DataConstr) -> [ConstrDecl] -> [DataConstr]
forall a b. (a -> b) -> [a] -> [b]
map ConstrDecl -> DataConstr
mkData [ConstrDecl]
cs) TCEnv
tcEnv
where
mkData :: ConstrDecl -> DataConstr
mkData (ConstrDecl _ c :: Ident
c tys :: [TypeExpr]
tys) = Ident -> [TypeExpr] -> DataConstr
mkData' Ident
c [TypeExpr]
tys
mkData (ConOpDecl _ ty1 :: TypeExpr
ty1 op :: Ident
op ty2 :: TypeExpr
ty2) = Ident -> [TypeExpr] -> DataConstr
mkData' Ident
op [TypeExpr
ty1, TypeExpr
ty2]
mkData (RecordDecl _ c :: Ident
c fs :: [FieldDecl]
fs) =
let (labels :: [Ident]
labels, tys :: [TypeExpr]
tys) = [(Ident, TypeExpr)] -> ([Ident], [TypeExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Ident
l, TypeExpr
ty) | FieldDecl _ ls :: [Ident]
ls ty :: TypeExpr
ty <- [FieldDecl]
fs, Ident
l <- [Ident]
ls]
in Ident -> [Ident] -> [TypeExpr] -> DataConstr
mkRec Ident
c [Ident]
labels [TypeExpr]
tys
mkData' :: Ident -> [TypeExpr] -> DataConstr
mkData' c :: Ident
c tys :: [TypeExpr]
tys = Ident -> [Type] -> DataConstr
DataConstr Ident
c [Type]
tys'
where qtc :: QualIdent
qtc = ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
m Ident
tc
PredType _ ty :: Type
ty = ModuleIdent
-> TCEnv
-> ClassEnv
-> QualIdent
-> [Ident]
-> [TypeExpr]
-> PredType
expandConstrType ModuleIdent
m TCEnv
tcEnv' ClassEnv
clsEnv QualIdent
qtc [Ident]
tvs [TypeExpr]
tys
tys' :: [Type]
tys' = Type -> [Type]
arrowArgs Type
ty
mkRec :: Ident -> [Ident] -> [TypeExpr] -> DataConstr
mkRec c :: Ident
c ls :: [Ident]
ls tys :: [TypeExpr]
tys =
Ident -> [Ident] -> [Type] -> DataConstr
RecordConstr Ident
c [Ident]
ls [Type]
tys'
where qtc :: QualIdent
qtc = ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
m Ident
tc
PredType _ ty :: Type
ty = ModuleIdent
-> TCEnv
-> ClassEnv
-> QualIdent
-> [Ident]
-> [TypeExpr]
-> PredType
expandConstrType ModuleIdent
m TCEnv
tcEnv' ClassEnv
clsEnv QualIdent
qtc [Ident]
tvs [TypeExpr]
tys
tys' :: [Type]
tys' = Type -> [Type]
arrowArgs Type
ty
bindKind _ _ _ tcEnv :: TCEnv
tcEnv (ExternalDataDecl _ tc :: Ident
tc tvs :: [Ident]
tvs) =
(QualIdent -> Kind -> [DataConstr] -> TypeInfo)
-> Ident
-> [Ident]
-> Maybe Kind
-> [DataConstr]
-> TCEnv
-> KCM TCEnv
forall a.
(QualIdent -> Kind -> a -> TypeInfo)
-> Ident -> [Ident] -> Maybe Kind -> a -> TCEnv -> KCM TCEnv
bindTypeConstructor QualIdent -> Kind -> [DataConstr] -> TypeInfo
DataType Ident
tc [Ident]
tvs (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
KindStar) [] TCEnv
tcEnv
bindKind m :: ModuleIdent
m tcEnv' :: TCEnv
tcEnv' _ tcEnv :: TCEnv
tcEnv (NewtypeDecl _ tc :: Ident
tc tvs :: [Ident]
tvs nc :: NewConstrDecl
nc _) =
(QualIdent -> Kind -> DataConstr -> TypeInfo)
-> Ident
-> [Ident]
-> Maybe Kind
-> DataConstr
-> TCEnv
-> KCM TCEnv
forall a.
(QualIdent -> Kind -> a -> TypeInfo)
-> Ident -> [Ident] -> Maybe Kind -> a -> TCEnv -> KCM TCEnv
bindTypeConstructor QualIdent -> Kind -> DataConstr -> TypeInfo
RenamingType Ident
tc [Ident]
tvs (Kind -> Maybe Kind
forall a. a -> Maybe a
Just Kind
KindStar) (NewConstrDecl -> DataConstr
mkData NewConstrDecl
nc) TCEnv
tcEnv
where
mkData :: NewConstrDecl -> DataConstr
mkData (NewConstrDecl _ c :: Ident
c ty :: TypeExpr
ty) = Ident -> [Type] -> DataConstr
DataConstr Ident
c [Type
ty']
where ty' :: Type
ty' = ModuleIdent -> TCEnv -> [Ident] -> TypeExpr -> Type
expandMonoType ModuleIdent
m TCEnv
tcEnv' [Ident]
tvs TypeExpr
ty
mkData (NewRecordDecl _ c :: Ident
c (l :: Ident
l, ty :: TypeExpr
ty)) = Ident -> [Ident] -> [Type] -> DataConstr
RecordConstr Ident
c [Ident
l] [Type
ty']
where ty' :: Type
ty' = ModuleIdent -> TCEnv -> [Ident] -> TypeExpr -> Type
expandMonoType ModuleIdent
m TCEnv
tcEnv' [Ident]
tvs TypeExpr
ty
bindKind m :: ModuleIdent
m tcEnv' :: TCEnv
tcEnv' _ tcEnv :: TCEnv
tcEnv (TypeDecl _ tc :: Ident
tc tvs :: [Ident]
tvs ty :: TypeExpr
ty) =
(QualIdent -> Kind -> Type -> TypeInfo)
-> Ident -> [Ident] -> Maybe Kind -> Type -> TCEnv -> KCM TCEnv
forall a.
(QualIdent -> Kind -> a -> TypeInfo)
-> Ident -> [Ident] -> Maybe Kind -> a -> TCEnv -> KCM TCEnv
bindTypeConstructor QualIdent -> Kind -> Type -> TypeInfo
aliasType Ident
tc [Ident]
tvs Maybe Kind
forall a. Maybe a
Nothing Type
ty' TCEnv
tcEnv
where
aliasType :: QualIdent -> Kind -> Type -> TypeInfo
aliasType tc' :: QualIdent
tc' k :: Kind
k = QualIdent -> Kind -> Int -> Type -> TypeInfo
AliasType QualIdent
tc' Kind
k (Int -> Type -> TypeInfo) -> Int -> Type -> TypeInfo
forall a b. (a -> b) -> a -> b
$ [Ident] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ident]
tvs
ty' :: Type
ty' = ModuleIdent -> TCEnv -> [Ident] -> TypeExpr -> Type
expandMonoType ModuleIdent
m TCEnv
tcEnv' [Ident]
tvs TypeExpr
ty
bindKind m :: ModuleIdent
m tcEnv' :: TCEnv
tcEnv' clsEnv :: ClassEnv
clsEnv tcEnv :: TCEnv
tcEnv (ClassDecl _ _ cls :: Ident
cls tv :: Ident
tv ds :: [Decl a]
ds) =
Ident -> [ClassMethod] -> TCEnv -> KCM TCEnv
bindTypeClass Ident
cls ((Decl a -> [ClassMethod]) -> [Decl a] -> [ClassMethod]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Decl a -> [ClassMethod]
forall a. Decl a -> [ClassMethod]
mkMethods [Decl a]
ds) TCEnv
tcEnv
where
mkMethods :: Decl a -> [ClassMethod]
mkMethods (TypeSig _ fs :: [Ident]
fs qty :: QualTypeExpr
qty) = (Ident -> ClassMethod) -> [Ident] -> [ClassMethod]
forall a b. (a -> b) -> [a] -> [b]
map (QualTypeExpr -> Ident -> ClassMethod
mkMethod QualTypeExpr
qty) [Ident]
fs
mkMethods _ = []
mkMethod :: QualTypeExpr -> Ident -> ClassMethod
mkMethod qty :: QualTypeExpr
qty f :: Ident
f = Ident -> Maybe Int -> PredType -> ClassMethod
ClassMethod Ident
f (Ident -> [Decl a] -> Maybe Int
forall a. Ident -> [Decl a] -> Maybe Int
findArity Ident
f [Decl a]
ds) (PredType -> ClassMethod) -> PredType -> ClassMethod
forall a b. (a -> b) -> a -> b
$
ModuleIdent
-> TCEnv
-> ClassEnv
-> QualIdent
-> Ident
-> QualTypeExpr
-> PredType
expandMethodType ModuleIdent
m TCEnv
tcEnv' ClassEnv
clsEnv (Ident -> QualIdent
qualify Ident
cls) Ident
tv QualTypeExpr
qty
findArity :: Ident -> [Decl a] -> Maybe Int
findArity _ [] = Maybe Int
forall a. Maybe a
Nothing
findArity f :: Ident
f (FunctionDecl _ _ f' :: Ident
f' eqs :: [Equation a]
eqs:_) | Ident
f Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
== Ident
f' =
Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Equation a -> Int
forall a. Equation a -> Int
eqnArity (Equation a -> Int) -> Equation a -> Int
forall a b. (a -> b) -> a -> b
$ [Equation a] -> Equation a
forall a. [a] -> a
head [Equation a]
eqs
findArity f :: Ident
f (_:ds' :: [Decl a]
ds') = Ident -> [Decl a] -> Maybe Int
findArity Ident
f [Decl a]
ds'
bindKind _ _ _ tcEnv :: TCEnv
tcEnv _ = TCEnv -> KCM TCEnv
forall (m :: * -> *) a. Monad m => a -> m a
return TCEnv
tcEnv
bindTypeConstructor :: (QualIdent -> Kind -> a -> TypeInfo) -> Ident
-> [Ident] -> Maybe Kind -> a -> TCEnv -> KCM TCEnv
bindTypeConstructor :: (QualIdent -> Kind -> a -> TypeInfo)
-> Ident -> [Ident] -> Maybe Kind -> a -> TCEnv -> KCM TCEnv
bindTypeConstructor f :: QualIdent -> Kind -> a -> TypeInfo
f tc :: Ident
tc tvs :: [Ident]
tvs k :: Maybe Kind
k x :: a
x tcEnv :: TCEnv
tcEnv = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
Kind
k' <- KCM Kind -> (Kind -> KCM Kind) -> Maybe Kind -> KCM Kind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe KCM Kind
freshKindVar Kind -> KCM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Kind
k
[Kind]
ks <- (Ident -> KCM Kind) -> [Ident] -> StateT KCState Identity [Kind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (KCM Kind -> Ident -> KCM Kind
forall a b. a -> b -> a
const KCM Kind
freshKindVar) [Ident]
tvs
let qtc :: QualIdent
qtc = ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
m Ident
tc
ti :: TypeInfo
ti = QualIdent -> Kind -> a -> TypeInfo
f QualIdent
qtc ((Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
KindArrow Kind
k' [Kind]
ks) a
x
TCEnv -> KCM TCEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (TCEnv -> KCM TCEnv) -> TCEnv -> KCM TCEnv
forall a b. (a -> b) -> a -> b
$ ModuleIdent -> Ident -> TypeInfo -> TCEnv -> TCEnv
bindTypeInfo ModuleIdent
m Ident
tc TypeInfo
ti TCEnv
tcEnv
bindTypeClass :: Ident -> [ClassMethod] -> TCEnv -> KCM TCEnv
bindTypeClass :: Ident -> [ClassMethod] -> TCEnv -> KCM TCEnv
bindTypeClass cls :: Ident
cls ms :: [ClassMethod]
ms tcEnv :: TCEnv
tcEnv = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
Kind
k <- KCM Kind
freshKindVar
let qcls :: QualIdent
qcls = ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
m Ident
cls
ti :: TypeInfo
ti = QualIdent -> Kind -> [ClassMethod] -> TypeInfo
TypeClass QualIdent
qcls Kind
k [ClassMethod]
ms
TCEnv -> KCM TCEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (TCEnv -> KCM TCEnv) -> TCEnv -> KCM TCEnv
forall a b. (a -> b) -> a -> b
$ ModuleIdent -> Ident -> TypeInfo -> TCEnv -> TCEnv
bindTypeInfo ModuleIdent
m Ident
cls TypeInfo
ti TCEnv
tcEnv
bindFreshKind :: TCEnv -> Ident -> KCM TCEnv
bindFreshKind :: TCEnv -> Ident -> KCM TCEnv
bindFreshKind tcEnv :: TCEnv
tcEnv tv :: Ident
tv = do
Kind
k <- KCM Kind
freshKindVar
TCEnv -> KCM TCEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (TCEnv -> KCM TCEnv) -> TCEnv -> KCM TCEnv
forall a b. (a -> b) -> a -> b
$ Ident -> Kind -> TCEnv -> TCEnv
bindTypeVar Ident
tv Kind
k TCEnv
tcEnv
bindTypeVars :: Ident -> [Ident] -> TCEnv -> KCM (Kind, TCEnv)
bindTypeVars :: Ident -> [Ident] -> TCEnv -> KCM (Kind, TCEnv)
bindTypeVars tc :: Ident
tc tvs :: [Ident]
tvs tcEnv :: TCEnv
tcEnv = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
(Kind, TCEnv) -> KCM (Kind, TCEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Kind, TCEnv) -> KCM (Kind, TCEnv))
-> (Kind, TCEnv) -> KCM (Kind, TCEnv)
forall a b. (a -> b) -> a -> b
$ ((Kind, TCEnv) -> Ident -> (Kind, TCEnv))
-> (Kind, TCEnv) -> [Ident] -> (Kind, TCEnv)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(KindArrow k1 :: Kind
k1 k2 :: Kind
k2, tcEnv' :: TCEnv
tcEnv') tv :: Ident
tv ->
(Kind
k2, Ident -> Kind -> TCEnv -> TCEnv
bindTypeVar Ident
tv Kind
k1 TCEnv
tcEnv'))
(ModuleIdent -> QualIdent -> TCEnv -> Kind
tcKind ModuleIdent
m (ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
m Ident
tc) TCEnv
tcEnv, TCEnv
tcEnv)
[Ident]
tvs
bindTypeVar :: Ident -> Kind -> TCEnv -> TCEnv
bindTypeVar :: Ident -> Kind -> TCEnv -> TCEnv
bindTypeVar ident :: Ident
ident k :: Kind
k = Ident -> TypeInfo -> TCEnv -> TCEnv
forall a. Ident -> a -> TopEnv a -> TopEnv a
bindTopEnv Ident
ident (Kind -> TypeInfo
TypeVar Kind
k)
bindClass :: ModuleIdent -> TCEnv -> ClassEnv -> Decl a -> ClassEnv
bindClass :: ModuleIdent -> TCEnv -> ClassEnv -> Decl a -> ClassEnv
bindClass m :: ModuleIdent
m tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv (ClassDecl _ cx :: Context
cx cls :: Ident
cls _ ds :: [Decl a]
ds) =
QualIdent -> ClassInfo -> ClassEnv -> ClassEnv
bindClassInfo QualIdent
qcls ([QualIdent]
sclss, [(Ident, Bool)]
ms) ClassEnv
clsEnv
where qcls :: QualIdent
qcls = ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
m Ident
cls
ms :: [(Ident, Bool)]
ms = (Ident -> (Ident, Bool)) -> [Ident] -> [(Ident, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\f :: Ident
f -> (Ident
f, Ident
f Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Ident]
fs)) ([Ident] -> [(Ident, Bool)]) -> [Ident] -> [(Ident, Bool)]
forall a b. (a -> b) -> a -> b
$ (Decl a -> [Ident]) -> [Decl a] -> [Ident]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Decl a -> [Ident]
forall a. Decl a -> [Ident]
methods [Decl a]
ds
fs :: [Ident]
fs = (Decl a -> [Ident]) -> [Decl a] -> [Ident]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Decl a -> [Ident]
forall a. Decl a -> [Ident]
impls [Decl a]
ds
sclss :: [QualIdent]
sclss = [QualIdent] -> [QualIdent]
forall a. Eq a => [a] -> [a]
nub ([QualIdent] -> [QualIdent]) -> [QualIdent] -> [QualIdent]
forall a b. (a -> b) -> a -> b
$ (Constraint -> QualIdent) -> Context -> [QualIdent]
forall a b. (a -> b) -> [a] -> [b]
map (\(Constraint _ cls' :: QualIdent
cls' _) -> ModuleIdent -> QualIdent -> TCEnv -> QualIdent
getOrigName ModuleIdent
m QualIdent
cls' TCEnv
tcEnv) Context
cx
bindClass _ _ clsEnv :: ClassEnv
clsEnv _ = ClassEnv
clsEnv
instantiateWithDefaultKind :: TypeInfo -> TypeInfo
instantiateWithDefaultKind :: TypeInfo -> TypeInfo
instantiateWithDefaultKind (DataType tc :: QualIdent
tc k :: Kind
k cs :: [DataConstr]
cs) =
QualIdent -> Kind -> [DataConstr] -> TypeInfo
DataType QualIdent
tc (Kind -> Kind
defaultKind Kind
k) [DataConstr]
cs
instantiateWithDefaultKind (RenamingType tc :: QualIdent
tc k :: Kind
k nc :: DataConstr
nc) =
QualIdent -> Kind -> DataConstr -> TypeInfo
RenamingType QualIdent
tc (Kind -> Kind
defaultKind Kind
k) DataConstr
nc
instantiateWithDefaultKind (AliasType tc :: QualIdent
tc k :: Kind
k n :: Int
n ty :: Type
ty) =
QualIdent -> Kind -> Int -> Type -> TypeInfo
AliasType QualIdent
tc (Kind -> Kind
defaultKind Kind
k) Int
n Type
ty
instantiateWithDefaultKind (TypeClass cls :: QualIdent
cls k :: Kind
k ms :: [ClassMethod]
ms) =
QualIdent -> Kind -> [ClassMethod] -> TypeInfo
TypeClass QualIdent
cls (Kind -> Kind
defaultKind Kind
k) [ClassMethod]
ms
instantiateWithDefaultKind (TypeVar _) =
String -> TypeInfo
forall a. String -> a
internalError "Checks.KindCheck.instantiateWithDefaultKind: type variable"
kcDecls :: TCEnv -> ClassEnv -> [Decl a] -> KCM (TCEnv, ClassEnv)
kcDecls :: TCEnv -> ClassEnv -> [Decl a] -> KCM (TCEnv, ClassEnv)
kcDecls tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv ds :: [Decl a]
ds = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
((TCEnv, ClassEnv) -> [Decl a] -> KCM (TCEnv, ClassEnv))
-> (TCEnv, ClassEnv) -> [[Decl a]] -> KCM (TCEnv, ClassEnv)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((TCEnv -> ClassEnv -> [Decl a] -> KCM (TCEnv, ClassEnv))
-> (TCEnv, ClassEnv) -> [Decl a] -> KCM (TCEnv, ClassEnv)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TCEnv -> ClassEnv -> [Decl a] -> KCM (TCEnv, ClassEnv)
forall a. TCEnv -> ClassEnv -> [Decl a] -> KCM (TCEnv, ClassEnv)
kcDeclGroup) (TCEnv
tcEnv, ClassEnv
clsEnv) ([[Decl a]] -> KCM (TCEnv, ClassEnv))
-> [[Decl a]] -> KCM (TCEnv, ClassEnv)
forall a b. (a -> b) -> a -> b
$ (Decl a -> [Ident])
-> (Decl a -> [Ident]) -> [Decl a] -> [[Decl a]]
forall b a. Eq b => (a -> [b]) -> (a -> [b]) -> [a] -> [[a]]
scc Decl a -> [Ident]
forall a. Decl a -> [Ident]
bt (ModuleIdent -> Decl a -> [Ident]
forall a. ModuleIdent -> Decl a -> [Ident]
ft ModuleIdent
m) [Decl a]
ds
kcDeclGroup :: TCEnv -> ClassEnv -> [Decl a] -> KCM (TCEnv, ClassEnv)
kcDeclGroup :: TCEnv -> ClassEnv -> [Decl a] -> KCM (TCEnv, ClassEnv)
kcDeclGroup tcEnv :: TCEnv
tcEnv clsEnv :: ClassEnv
clsEnv ds :: [Decl a]
ds = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
(tcEnv' :: TCEnv
tcEnv', clsEnv' :: ClassEnv
clsEnv') <- ((TCEnv, ClassEnv) -> KCM (TCEnv, ClassEnv))
-> KCM (TCEnv, ClassEnv)
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (\ ~(tcEnv' :: TCEnv
tcEnv', clsEnv' :: ClassEnv
clsEnv') ->
(TCEnv -> ClassEnv -> (TCEnv, ClassEnv))
-> ClassEnv -> TCEnv -> (TCEnv, ClassEnv)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) ((ClassEnv -> Decl a -> ClassEnv)
-> ClassEnv -> [Decl a] -> ClassEnv
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (ModuleIdent -> TCEnv -> ClassEnv -> Decl a -> ClassEnv
forall a. ModuleIdent -> TCEnv -> ClassEnv -> Decl a -> ClassEnv
bindClass ModuleIdent
m TCEnv
tcEnv') ClassEnv
clsEnv [Decl a]
ds) (TCEnv -> (TCEnv, ClassEnv)) -> KCM TCEnv -> KCM (TCEnv, ClassEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(TCEnv -> Decl a -> KCM TCEnv) -> TCEnv -> [Decl a] -> KCM TCEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (ModuleIdent -> TCEnv -> ClassEnv -> TCEnv -> Decl a -> KCM TCEnv
forall a.
ModuleIdent -> TCEnv -> ClassEnv -> TCEnv -> Decl a -> KCM TCEnv
bindKind ModuleIdent
m TCEnv
tcEnv' ClassEnv
clsEnv') TCEnv
tcEnv [Decl a]
ds)
(Decl a -> KCM ()) -> [Decl a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> Decl a -> KCM ()
forall a. TCEnv -> Decl a -> KCM ()
kcDecl TCEnv
tcEnv') [Decl a]
ds
KindSubst
theta <- KCM KindSubst
getKindSubst
(TCEnv, ClassEnv) -> KCM (TCEnv, ClassEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return ((TypeInfo -> TypeInfo) -> TCEnv -> TCEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeInfo -> TypeInfo
instantiateWithDefaultKind (TypeInfo -> TypeInfo)
-> (TypeInfo -> TypeInfo) -> TypeInfo -> TypeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KindSubst -> TypeInfo -> TypeInfo
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
theta) TCEnv
tcEnv', ClassEnv
clsEnv')
kcDecl :: TCEnv -> Decl a -> KCM ()
kcDecl :: TCEnv -> Decl a -> KCM ()
kcDecl _ (InfixDecl _ _ _ _) = KCM ()
ok
kcDecl tcEnv :: TCEnv
tcEnv (DataDecl _ tc :: Ident
tc tvs :: [Ident]
tvs cs :: [ConstrDecl]
cs _) = do
(_, tcEnv' :: TCEnv
tcEnv') <- Ident -> [Ident] -> TCEnv -> KCM (Kind, TCEnv)
bindTypeVars Ident
tc [Ident]
tvs TCEnv
tcEnv
(ConstrDecl -> KCM ()) -> [ConstrDecl] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> ConstrDecl -> KCM ()
kcConstrDecl TCEnv
tcEnv') [ConstrDecl]
cs
kcDecl _ (ExternalDataDecl _ _ _) = KCM ()
ok
kcDecl tcEnv :: TCEnv
tcEnv (NewtypeDecl _ tc :: Ident
tc tvs :: [Ident]
tvs nc :: NewConstrDecl
nc _) = do
(_, tcEnv' :: TCEnv
tcEnv') <- Ident -> [Ident] -> TCEnv -> KCM (Kind, TCEnv)
bindTypeVars Ident
tc [Ident]
tvs TCEnv
tcEnv
TCEnv -> NewConstrDecl -> KCM ()
kcNewConstrDecl TCEnv
tcEnv' NewConstrDecl
nc
kcDecl tcEnv :: TCEnv
tcEnv t :: Decl a
t@(TypeDecl p :: SpanInfo
p tc :: Ident
tc tvs :: [Ident]
tvs ty :: TypeExpr
ty) = do
(k :: Kind
k, tcEnv' :: TCEnv
tcEnv') <- Ident -> [Ident] -> TCEnv -> KCM (Kind, TCEnv)
bindTypeVars Ident
tc [Ident]
tvs TCEnv
tcEnv
TCEnv -> SpanInfo -> String -> Doc -> Kind -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> Kind -> TypeExpr -> KCM ()
kcType TCEnv
tcEnv' SpanInfo
p "type declaration" (Decl a -> Doc
forall a. Decl a -> Doc
ppDecl Decl a
t) Kind
k TypeExpr
ty
kcDecl tcEnv :: TCEnv
tcEnv (TypeSig p :: SpanInfo
p _ qty :: QualTypeExpr
qty) = TCEnv -> SpanInfo -> QualTypeExpr -> KCM ()
forall p. HasPosition p => TCEnv -> p -> QualTypeExpr -> KCM ()
kcTypeSig TCEnv
tcEnv SpanInfo
p QualTypeExpr
qty
kcDecl tcEnv :: TCEnv
tcEnv (FunctionDecl _ _ _ eqs :: [Equation a]
eqs) = (Equation a -> KCM ()) -> [Equation a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> Equation a -> KCM ()
forall a. TCEnv -> Equation a -> KCM ()
kcEquation TCEnv
tcEnv) [Equation a]
eqs
kcDecl _ (ExternalDecl _ _) = KCM ()
ok
kcDecl tcEnv :: TCEnv
tcEnv (PatternDecl _ _ rhs :: Rhs a
rhs) = TCEnv -> Rhs a -> KCM ()
forall a. TCEnv -> Rhs a -> KCM ()
kcRhs TCEnv
tcEnv Rhs a
rhs
kcDecl _ (FreeDecl _ _) = KCM ()
ok
kcDecl tcEnv :: TCEnv
tcEnv (DefaultDecl p :: SpanInfo
p tys :: [TypeExpr]
tys) = do
TCEnv
tcEnv' <- (TCEnv -> Ident -> KCM TCEnv) -> TCEnv -> [Ident] -> KCM TCEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM TCEnv -> Ident -> KCM TCEnv
bindFreshKind TCEnv
tcEnv ([Ident] -> KCM TCEnv) -> [Ident] -> KCM TCEnv
forall a b. (a -> b) -> a -> b
$ [Ident] -> [Ident]
forall a. Eq a => [a] -> [a]
nub ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall a b. (a -> b) -> a -> b
$ [TypeExpr] -> [Ident]
forall e. Expr e => e -> [Ident]
fv [TypeExpr]
tys
(TypeExpr -> KCM ()) -> [TypeExpr] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> SpanInfo -> String -> Doc -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType TCEnv
tcEnv' SpanInfo
p "default declaration" Doc
empty) [TypeExpr]
tys
kcDecl tcEnv :: TCEnv
tcEnv (ClassDecl p :: SpanInfo
p cx :: Context
cx cls :: Ident
cls tv :: Ident
tv ds :: [Decl a]
ds) = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
let tcEnv' :: TCEnv
tcEnv' = Ident -> Kind -> TCEnv -> TCEnv
bindTypeVar Ident
tv (ModuleIdent -> QualIdent -> TCEnv -> Kind
clsKind ModuleIdent
m (ModuleIdent -> Ident -> QualIdent
qualifyWith ModuleIdent
m Ident
cls) TCEnv
tcEnv) TCEnv
tcEnv
TCEnv -> SpanInfo -> Context -> KCM ()
forall p. HasPosition p => TCEnv -> p -> Context -> KCM ()
kcContext TCEnv
tcEnv' SpanInfo
p Context
cx
(Decl a -> KCM ()) -> [Decl a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> Decl a -> KCM ()
forall a. TCEnv -> Decl a -> KCM ()
kcDecl TCEnv
tcEnv') [Decl a]
ds
kcDecl tcEnv :: TCEnv
tcEnv (InstanceDecl p :: SpanInfo
p cx :: Context
cx qcls :: QualIdent
qcls inst :: TypeExpr
inst ds :: [Decl a]
ds) = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
TCEnv
tcEnv' <- (TCEnv -> Ident -> KCM TCEnv) -> TCEnv -> [Ident] -> KCM TCEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM TCEnv -> Ident -> KCM TCEnv
bindFreshKind TCEnv
tcEnv ([Ident] -> KCM TCEnv) -> [Ident] -> KCM TCEnv
forall a b. (a -> b) -> a -> b
$ TypeExpr -> [Ident]
forall e. Expr e => e -> [Ident]
fv TypeExpr
inst
TCEnv -> SpanInfo -> Context -> KCM ()
forall p. HasPosition p => TCEnv -> p -> Context -> KCM ()
kcContext TCEnv
tcEnv' SpanInfo
p Context
cx
TCEnv -> SpanInfo -> String -> Doc -> Kind -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> Kind -> TypeExpr -> KCM ()
kcType TCEnv
tcEnv' SpanInfo
p String
what Doc
doc (ModuleIdent -> QualIdent -> TCEnv -> Kind
clsKind ModuleIdent
m QualIdent
qcls TCEnv
tcEnv) TypeExpr
inst
(Decl a -> KCM ()) -> [Decl a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> Decl a -> KCM ()
forall a. TCEnv -> Decl a -> KCM ()
kcDecl TCEnv
tcEnv') [Decl a]
ds
where
what :: String
what = "instance declaration"
doc :: Doc
doc = Decl Any -> Doc
forall a. Decl a -> Doc
ppDecl (SpanInfo
-> Context -> QualIdent -> TypeExpr -> [Decl Any] -> Decl Any
forall a.
SpanInfo -> Context -> QualIdent -> TypeExpr -> [Decl a] -> Decl a
InstanceDecl SpanInfo
p Context
cx QualIdent
qcls TypeExpr
inst [])
kcConstrDecl :: TCEnv -> ConstrDecl -> KCM ()
kcConstrDecl :: TCEnv -> ConstrDecl -> KCM ()
kcConstrDecl tcEnv :: TCEnv
tcEnv d :: ConstrDecl
d@(ConstrDecl p :: SpanInfo
p _ tys :: [TypeExpr]
tys) = do
(TypeExpr -> KCM ()) -> [TypeExpr] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> SpanInfo -> String -> Doc -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType TCEnv
tcEnv SpanInfo
p String
what Doc
doc) [TypeExpr]
tys
where
what :: String
what = "data constructor declaration"
doc :: Doc
doc = ConstrDecl -> Doc
ppConstr ConstrDecl
d
kcConstrDecl tcEnv :: TCEnv
tcEnv d :: ConstrDecl
d@(ConOpDecl p :: SpanInfo
p ty1 :: TypeExpr
ty1 _ ty2 :: TypeExpr
ty2) = do
TCEnv -> SpanInfo -> String -> Doc -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType TCEnv
tcEnv SpanInfo
p String
what Doc
doc TypeExpr
ty1
TCEnv -> SpanInfo -> String -> Doc -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType TCEnv
tcEnv SpanInfo
p String
what Doc
doc TypeExpr
ty2
where
what :: String
what = "data constructor declaration"
doc :: Doc
doc = ConstrDecl -> Doc
ppConstr ConstrDecl
d
kcConstrDecl tcEnv :: TCEnv
tcEnv (RecordDecl _ _ fs :: [FieldDecl]
fs) = do
(FieldDecl -> KCM ()) -> [FieldDecl] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> FieldDecl -> KCM ()
kcFieldDecl TCEnv
tcEnv) [FieldDecl]
fs
kcFieldDecl :: TCEnv -> FieldDecl -> KCM ()
kcFieldDecl :: TCEnv -> FieldDecl -> KCM ()
kcFieldDecl tcEnv :: TCEnv
tcEnv d :: FieldDecl
d@(FieldDecl p :: SpanInfo
p _ ty :: TypeExpr
ty) =
TCEnv -> SpanInfo -> String -> Doc -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType TCEnv
tcEnv SpanInfo
p "field declaration" (FieldDecl -> Doc
ppFieldDecl FieldDecl
d) TypeExpr
ty
kcNewConstrDecl :: TCEnv -> NewConstrDecl -> KCM ()
kcNewConstrDecl :: TCEnv -> NewConstrDecl -> KCM ()
kcNewConstrDecl tcEnv :: TCEnv
tcEnv d :: NewConstrDecl
d@(NewConstrDecl p :: SpanInfo
p _ ty :: TypeExpr
ty) =
TCEnv -> SpanInfo -> String -> Doc -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType TCEnv
tcEnv SpanInfo
p "newtype constructor declaration" (NewConstrDecl -> Doc
ppNewConstr NewConstrDecl
d) TypeExpr
ty
kcNewConstrDecl tcEnv :: TCEnv
tcEnv (NewRecordDecl p :: SpanInfo
p _ (l :: Ident
l, ty :: TypeExpr
ty)) =
TCEnv -> FieldDecl -> KCM ()
kcFieldDecl TCEnv
tcEnv (SpanInfo -> [Ident] -> TypeExpr -> FieldDecl
FieldDecl SpanInfo
p [Ident
l] TypeExpr
ty)
kcEquation :: TCEnv -> Equation a -> KCM ()
kcEquation :: TCEnv -> Equation a -> KCM ()
kcEquation tcEnv :: TCEnv
tcEnv (Equation _ _ rhs :: Rhs a
rhs) = TCEnv -> Rhs a -> KCM ()
forall a. TCEnv -> Rhs a -> KCM ()
kcRhs TCEnv
tcEnv Rhs a
rhs
kcRhs :: TCEnv -> Rhs a -> KCM ()
kcRhs :: TCEnv -> Rhs a -> KCM ()
kcRhs tcEnv :: TCEnv
tcEnv (SimpleRhs p :: SpanInfo
p e :: Expression a
e ds :: [Decl a]
ds) = do
TCEnv -> SpanInfo -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv SpanInfo
p Expression a
e
(Decl a -> KCM ()) -> [Decl a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> Decl a -> KCM ()
forall a. TCEnv -> Decl a -> KCM ()
kcDecl TCEnv
tcEnv) [Decl a]
ds
kcRhs tcEnv :: TCEnv
tcEnv (GuardedRhs _ es :: [CondExpr a]
es ds :: [Decl a]
ds) = do
(CondExpr a -> KCM ()) -> [CondExpr a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> CondExpr a -> KCM ()
forall a. TCEnv -> CondExpr a -> KCM ()
kcCondExpr TCEnv
tcEnv) [CondExpr a]
es
(Decl a -> KCM ()) -> [Decl a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> Decl a -> KCM ()
forall a. TCEnv -> Decl a -> KCM ()
kcDecl TCEnv
tcEnv) [Decl a]
ds
kcCondExpr :: TCEnv -> CondExpr a -> KCM ()
kcCondExpr :: TCEnv -> CondExpr a -> KCM ()
kcCondExpr tcEnv :: TCEnv
tcEnv (CondExpr p :: SpanInfo
p g :: Expression a
g e :: Expression a
e) = TCEnv -> SpanInfo -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv SpanInfo
p Expression a
g KCM () -> KCM () -> KCM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TCEnv -> SpanInfo -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv SpanInfo
p Expression a
e
kcExpr :: HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr :: TCEnv -> p -> Expression a -> KCM ()
kcExpr _ _ (Literal _ _ _) = KCM ()
ok
kcExpr _ _ (Variable _ _ _) = KCM ()
ok
kcExpr _ _ (Constructor _ _ _) = KCM ()
ok
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (Paren _ e :: Expression a
e) = TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (Typed _ e :: Expression a
e qty :: QualTypeExpr
qty) = do
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
TCEnv -> p -> QualTypeExpr -> KCM ()
forall p. HasPosition p => TCEnv -> p -> QualTypeExpr -> KCM ()
kcTypeSig TCEnv
tcEnv p
p QualTypeExpr
qty
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (Record _ _ _ fs :: [Field (Expression a)]
fs) = (Field (Expression a) -> KCM ())
-> [Field (Expression a)] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> p -> Field (Expression a) -> KCM ()
forall p a.
HasPosition p =>
TCEnv -> p -> Field (Expression a) -> KCM ()
kcField TCEnv
tcEnv p
p) [Field (Expression a)]
fs
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (RecordUpdate _ e :: Expression a
e fs :: [Field (Expression a)]
fs) = do
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
(Field (Expression a) -> KCM ())
-> [Field (Expression a)] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> p -> Field (Expression a) -> KCM ()
forall p a.
HasPosition p =>
TCEnv -> p -> Field (Expression a) -> KCM ()
kcField TCEnv
tcEnv p
p) [Field (Expression a)]
fs
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (Tuple _ es :: [Expression a]
es) = (Expression a -> KCM ()) -> [Expression a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p) [Expression a]
es
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (List _ _ es :: [Expression a]
es) = (Expression a -> KCM ()) -> [Expression a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p) [Expression a]
es
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (ListCompr _ e :: Expression a
e stms :: [Statement a]
stms) = do
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
(Statement a -> KCM ()) -> [Statement a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> p -> Statement a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Statement a -> KCM ()
kcStmt TCEnv
tcEnv p
p) [Statement a]
stms
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (EnumFrom _ e :: Expression a
e) = TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (EnumFromThen _ e1 :: Expression a
e1 e2 :: Expression a
e2) = do
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e1
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e2
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (EnumFromTo _ e1 :: Expression a
e1 e2 :: Expression a
e2) = do
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e1
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e2
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (EnumFromThenTo _ e1 :: Expression a
e1 e2 :: Expression a
e2 e3 :: Expression a
e3) = do
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e1
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e2
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e3
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (UnaryMinus _ e :: Expression a
e) = TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (Apply _ e1 :: Expression a
e1 e2 :: Expression a
e2) = do
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e1
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e2
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (InfixApply _ e1 :: Expression a
e1 _ e2 :: Expression a
e2) = do
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e1
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e2
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (LeftSection _ e :: Expression a
e _) = TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (RightSection _ _ e :: Expression a
e) = TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (Lambda _ _ e :: Expression a
e) = TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (Let _ ds :: [Decl a]
ds e :: Expression a
e) = do
(Decl a -> KCM ()) -> [Decl a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> Decl a -> KCM ()
forall a. TCEnv -> Decl a -> KCM ()
kcDecl TCEnv
tcEnv) [Decl a]
ds
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (Do _ stms :: [Statement a]
stms e :: Expression a
e) = do
(Statement a -> KCM ()) -> [Statement a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> p -> Statement a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Statement a -> KCM ()
kcStmt TCEnv
tcEnv p
p) [Statement a]
stms
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (IfThenElse _ e1 :: Expression a
e1 e2 :: Expression a
e2 e3 :: Expression a
e3) = do
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e1
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e2
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e3
kcExpr tcEnv :: TCEnv
tcEnv p :: p
p (Case _ _ e :: Expression a
e alts :: [Alt a]
alts) = do
TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
(Alt a -> KCM ()) -> [Alt a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> Alt a -> KCM ()
forall a. TCEnv -> Alt a -> KCM ()
kcAlt TCEnv
tcEnv) [Alt a]
alts
kcStmt :: HasPosition p => TCEnv -> p -> Statement a -> KCM ()
kcStmt :: TCEnv -> p -> Statement a -> KCM ()
kcStmt tcEnv :: TCEnv
tcEnv p :: p
p (StmtExpr _ e :: Expression a
e) = TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
kcStmt tcEnv :: TCEnv
tcEnv _ (StmtDecl _ ds :: [Decl a]
ds) = (Decl a -> KCM ()) -> [Decl a] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> Decl a -> KCM ()
forall a. TCEnv -> Decl a -> KCM ()
kcDecl TCEnv
tcEnv) [Decl a]
ds
kcStmt tcEnv :: TCEnv
tcEnv p :: p
p (StmtBind _ _ e :: Expression a
e) = TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
kcAlt :: TCEnv -> Alt a -> KCM ()
kcAlt :: TCEnv -> Alt a -> KCM ()
kcAlt tcEnv :: TCEnv
tcEnv (Alt _ _ rhs :: Rhs a
rhs) = TCEnv -> Rhs a -> KCM ()
forall a. TCEnv -> Rhs a -> KCM ()
kcRhs TCEnv
tcEnv Rhs a
rhs
kcField :: HasPosition p => TCEnv -> p -> Field (Expression a) -> KCM ()
kcField :: TCEnv -> p -> Field (Expression a) -> KCM ()
kcField tcEnv :: TCEnv
tcEnv p :: p
p (Field _ _ e :: Expression a
e) = TCEnv -> p -> Expression a -> KCM ()
forall p a. HasPosition p => TCEnv -> p -> Expression a -> KCM ()
kcExpr TCEnv
tcEnv p
p Expression a
e
kcContext :: HasPosition p => TCEnv -> p -> Context -> KCM ()
kcContext :: TCEnv -> p -> Context -> KCM ()
kcContext tcEnv :: TCEnv
tcEnv p :: p
p = (Constraint -> KCM ()) -> Context -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> p -> Constraint -> KCM ()
forall p. HasPosition p => TCEnv -> p -> Constraint -> KCM ()
kcConstraint TCEnv
tcEnv p
p)
kcConstraint :: HasPosition p => TCEnv -> p -> Constraint -> KCM ()
kcConstraint :: TCEnv -> p -> Constraint -> KCM ()
kcConstraint tcEnv :: TCEnv
tcEnv p :: p
p sc :: Constraint
sc@(Constraint _ qcls :: QualIdent
qcls ty :: TypeExpr
ty) = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
TCEnv -> p -> String -> Doc -> Kind -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> Kind -> TypeExpr -> KCM ()
kcType TCEnv
tcEnv p
p "class constraint" Doc
doc (ModuleIdent -> QualIdent -> TCEnv -> Kind
clsKind ModuleIdent
m QualIdent
qcls TCEnv
tcEnv) TypeExpr
ty
where
doc :: Doc
doc = Constraint -> Doc
ppConstraint Constraint
sc
kcTypeSig :: HasPosition p => TCEnv -> p -> QualTypeExpr -> KCM ()
kcTypeSig :: TCEnv -> p -> QualTypeExpr -> KCM ()
kcTypeSig tcEnv :: TCEnv
tcEnv p :: p
p (QualTypeExpr _ cx :: Context
cx ty :: TypeExpr
ty) = do
TCEnv
tcEnv' <- (TCEnv -> Ident -> KCM TCEnv) -> TCEnv -> [Ident] -> KCM TCEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM TCEnv -> Ident -> KCM TCEnv
bindFreshKind TCEnv
tcEnv [Ident]
free
TCEnv -> p -> Context -> KCM ()
forall p. HasPosition p => TCEnv -> p -> Context -> KCM ()
kcContext TCEnv
tcEnv' p
p Context
cx
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType TCEnv
tcEnv' p
p "type signature" Doc
doc TypeExpr
ty
where
free :: [Ident]
free = (Ident -> Bool) -> [Ident] -> [Ident]
forall a. (a -> Bool) -> [a] -> [a]
filter ([TypeInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TypeInfo] -> Bool) -> (Ident -> [TypeInfo]) -> Ident -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ident -> TCEnv -> [TypeInfo]) -> TCEnv -> Ident -> [TypeInfo]
forall a b c. (a -> b -> c) -> b -> a -> c
flip Ident -> TCEnv -> [TypeInfo]
lookupTypeInfo TCEnv
tcEnv) ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall a b. (a -> b) -> a -> b
$ [Ident] -> [Ident]
forall a. Eq a => [a] -> [a]
nub ([Ident] -> [Ident]) -> [Ident] -> [Ident]
forall a b. (a -> b) -> a -> b
$ TypeExpr -> [Ident]
forall e. Expr e => e -> [Ident]
fv TypeExpr
ty
doc :: Doc
doc = Int -> TypeExpr -> Doc
ppTypeExpr 0 TypeExpr
ty
kcValueType :: HasPosition p => TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType :: TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType tcEnv :: TCEnv
tcEnv p :: p
p what :: String
what doc :: Doc
doc = TCEnv -> p -> String -> Doc -> Kind -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> Kind -> TypeExpr -> KCM ()
kcType TCEnv
tcEnv p
p String
what Doc
doc Kind
KindStar
kcType :: HasPosition p => TCEnv -> p -> String -> Doc -> Kind -> TypeExpr -> KCM ()
kcType :: TCEnv -> p -> String -> Doc -> Kind -> TypeExpr -> KCM ()
kcType tcEnv :: TCEnv
tcEnv p :: p
p what :: String
what doc :: Doc
doc k :: Kind
k ty :: TypeExpr
ty = do
Kind
k' <- TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
kcTypeExpr TCEnv
tcEnv p
p "type expression" Doc
doc' 0 TypeExpr
ty
p -> String -> Doc -> Kind -> Kind -> KCM ()
forall p.
HasPosition p =>
p -> String -> Doc -> Kind -> Kind -> KCM ()
unify p
p String
what (Doc
doc Doc -> Doc -> Doc
$-$ String -> Doc
text "Type:" Doc -> Doc -> Doc
<+> Doc
doc') Kind
k Kind
k'
where
doc' :: Doc
doc' = Int -> TypeExpr -> Doc
ppTypeExpr 0 TypeExpr
ty
kcTypeExpr :: HasPosition p => TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
kcTypeExpr :: TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
kcTypeExpr tcEnv :: TCEnv
tcEnv p :: p
p _ _ n :: Int
n (ConstructorType _ tc :: QualIdent
tc) = do
ModuleIdent
m <- KCM ModuleIdent
getModuleIdent
case QualIdent -> TCEnv -> [TypeInfo]
qualLookupTypeInfo QualIdent
tc TCEnv
tcEnv of
[AliasType _ _ n' :: Int
n' _] -> case Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n' of
True -> Kind -> KCM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> KCM Kind) -> Kind -> KCM Kind
forall a b. (a -> b) -> a -> b
$ ModuleIdent -> QualIdent -> TCEnv -> Kind
tcKind ModuleIdent
m QualIdent
tc TCEnv
tcEnv
False -> do
Message -> KCM ()
report (Message -> KCM ()) -> Message -> KCM ()
forall a b. (a -> b) -> a -> b
$ p -> QualIdent -> Int -> Int -> Message
forall p. HasPosition p => p -> QualIdent -> Int -> Int -> Message
errPartialAlias p
p QualIdent
tc Int
n' Int
n
KCM Kind
freshKindVar
_ -> Kind -> KCM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> KCM Kind) -> Kind -> KCM Kind
forall a b. (a -> b) -> a -> b
$ ModuleIdent -> QualIdent -> TCEnv -> Kind
tcKind ModuleIdent
m QualIdent
tc TCEnv
tcEnv
kcTypeExpr tcEnv :: TCEnv
tcEnv p :: p
p what :: String
what doc :: Doc
doc n :: Int
n (ApplyType _ ty1 :: TypeExpr
ty1 ty2 :: TypeExpr
ty2) = do
(alpha :: Kind
alpha, beta :: Kind
beta) <- TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
kcTypeExpr TCEnv
tcEnv p
p String
what Doc
doc (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) TypeExpr
ty1 KCM Kind
-> (Kind -> StateT KCState Identity (Kind, Kind))
-> StateT KCState Identity (Kind, Kind)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
p -> String -> Doc -> Kind -> StateT KCState Identity (Kind, Kind)
forall p.
HasPosition p =>
p -> String -> Doc -> Kind -> StateT KCState Identity (Kind, Kind)
kcArrow p
p String
what (Doc
doc Doc -> Doc -> Doc
$-$ String -> Doc
text "Type:" Doc -> Doc -> Doc
<+> Int -> TypeExpr -> Doc
ppTypeExpr 0 TypeExpr
ty1)
TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
kcTypeExpr TCEnv
tcEnv p
p String
what Doc
doc 0 TypeExpr
ty2 KCM Kind -> (Kind -> KCM ()) -> KCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
p -> String -> Doc -> Kind -> Kind -> KCM ()
forall p.
HasPosition p =>
p -> String -> Doc -> Kind -> Kind -> KCM ()
unify p
p String
what (Doc
doc Doc -> Doc -> Doc
$-$ String -> Doc
text "Type:" Doc -> Doc -> Doc
<+> Int -> TypeExpr -> Doc
ppTypeExpr 0 TypeExpr
ty2) Kind
alpha
Kind -> KCM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
beta
kcTypeExpr tcEnv :: TCEnv
tcEnv _ _ _ _ (VariableType _ tv :: Ident
tv) = Kind -> KCM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return (Ident -> TCEnv -> Kind
varKind Ident
tv TCEnv
tcEnv)
kcTypeExpr tcEnv :: TCEnv
tcEnv p :: p
p what :: String
what doc :: Doc
doc _ (TupleType _ tys :: [TypeExpr]
tys) = do
(TypeExpr -> KCM ()) -> [TypeExpr] -> KCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType TCEnv
tcEnv p
p String
what Doc
doc) [TypeExpr]
tys
Kind -> KCM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
KindStar
kcTypeExpr tcEnv :: TCEnv
tcEnv p :: p
p what :: String
what doc :: Doc
doc _ (ListType _ ty :: TypeExpr
ty) = do
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType TCEnv
tcEnv p
p String
what Doc
doc TypeExpr
ty
Kind -> KCM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
KindStar
kcTypeExpr tcEnv :: TCEnv
tcEnv p :: p
p what :: String
what doc :: Doc
doc _ (ArrowType _ ty1 :: TypeExpr
ty1 ty2 :: TypeExpr
ty2) = do
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType TCEnv
tcEnv p
p String
what Doc
doc TypeExpr
ty1
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> TypeExpr -> KCM ()
kcValueType TCEnv
tcEnv p
p String
what Doc
doc TypeExpr
ty2
Kind -> KCM Kind
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
KindStar
kcTypeExpr tcEnv :: TCEnv
tcEnv p :: p
p what :: String
what doc :: Doc
doc n :: Int
n (ParenType _ ty :: TypeExpr
ty) = TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
kcTypeExpr TCEnv
tcEnv p
p String
what Doc
doc Int
n TypeExpr
ty
kcTypeExpr tcEnv :: TCEnv
tcEnv p :: p
p what :: String
what doc :: Doc
doc n :: Int
n (ForallType _ vs :: [Ident]
vs ty :: TypeExpr
ty) = do
TCEnv
tcEnv' <- (TCEnv -> Ident -> KCM TCEnv) -> TCEnv -> [Ident] -> KCM TCEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM TCEnv -> Ident -> KCM TCEnv
bindFreshKind TCEnv
tcEnv [Ident]
vs
TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
forall p.
HasPosition p =>
TCEnv -> p -> String -> Doc -> Int -> TypeExpr -> KCM Kind
kcTypeExpr TCEnv
tcEnv' p
p String
what Doc
doc Int
n TypeExpr
ty
kcArrow :: HasPosition p => p -> String -> Doc -> Kind -> KCM (Kind, Kind)
kcArrow :: p -> String -> Doc -> Kind -> StateT KCState Identity (Kind, Kind)
kcArrow p :: p
p what :: String
what doc :: Doc
doc k :: Kind
k = do
KindSubst
theta <- KCM KindSubst
getKindSubst
case KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
theta Kind
k of
KindStar -> do
Message -> KCM ()
report (Message -> KCM ()) -> Message -> KCM ()
forall a b. (a -> b) -> a -> b
$ p -> String -> Doc -> Kind -> Message
forall p. HasPosition p => p -> String -> Doc -> Kind -> Message
errNonArrowKind p
p String
what Doc
doc Kind
KindStar
(,) (Kind -> Kind -> (Kind, Kind))
-> KCM Kind -> StateT KCState Identity (Kind -> (Kind, Kind))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KCM Kind
freshKindVar StateT KCState Identity (Kind -> (Kind, Kind))
-> KCM Kind -> StateT KCState Identity (Kind, Kind)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> KCM Kind
freshKindVar
KindVariable kv :: Int
kv -> do
Kind
alpha <- KCM Kind
freshKindVar
Kind
beta <- KCM Kind
freshKindVar
(KindSubst -> KindSubst) -> KCM ()
modifyKindSubst ((KindSubst -> KindSubst) -> KCM ())
-> (KindSubst -> KindSubst) -> KCM ()
forall a b. (a -> b) -> a -> b
$ Int -> Kind -> KindSubst -> KindSubst
bindVar Int
kv (Kind -> KindSubst -> KindSubst) -> Kind -> KindSubst -> KindSubst
forall a b. (a -> b) -> a -> b
$ Kind -> Kind -> Kind
KindArrow Kind
alpha Kind
beta
(Kind, Kind) -> StateT KCState Identity (Kind, Kind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind
alpha, Kind
beta)
KindArrow k1 :: Kind
k1 k2 :: Kind
k2 -> (Kind, Kind) -> StateT KCState Identity (Kind, Kind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind
k1, Kind
k2)
unify :: HasPosition p => p -> String -> Doc -> Kind -> Kind -> KCM ()
unify :: p -> String -> Doc -> Kind -> Kind -> KCM ()
unify p :: p
p what :: String
what doc :: Doc
doc k1 :: Kind
k1 k2 :: Kind
k2 = do
KindSubst
theta <- KCM KindSubst
getKindSubst
let k1' :: Kind
k1' = KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
theta Kind
k1
let k2' :: Kind
k2' = KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
theta Kind
k2
case Kind -> Kind -> Maybe KindSubst
unifyKinds Kind
k1' Kind
k2' of
Nothing -> Message -> KCM ()
report (Message -> KCM ()) -> Message -> KCM ()
forall a b. (a -> b) -> a -> b
$ p -> String -> Doc -> Kind -> Kind -> Message
forall p.
HasPosition p =>
p -> String -> Doc -> Kind -> Kind -> Message
errKindMismatch p
p String
what Doc
doc Kind
k1' Kind
k2'
Just sigma :: KindSubst
sigma -> (KindSubst -> KindSubst) -> KCM ()
modifyKindSubst (KindSubst -> KindSubst -> KindSubst
forall v e. Ord v => Subst v e -> Subst v e -> Subst v e
compose KindSubst
sigma)
unifyKinds :: Kind -> Kind -> Maybe KindSubst
unifyKinds :: Kind -> Kind -> Maybe KindSubst
unifyKinds KindStar KindStar = KindSubst -> Maybe KindSubst
forall a. a -> Maybe a
Just KindSubst
forall a b. Subst a b
idSubst
unifyKinds (KindVariable kv1 :: Int
kv1) (KindVariable kv2 :: Int
kv2)
| Int
kv1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
kv2 = KindSubst -> Maybe KindSubst
forall a. a -> Maybe a
Just KindSubst
forall a b. Subst a b
idSubst
| Bool
otherwise = KindSubst -> Maybe KindSubst
forall a. a -> Maybe a
Just (Int -> Kind -> KindSubst
forall v e. Ord v => v -> e -> Subst v e
singleSubst Int
kv1 (Int -> Kind
KindVariable Int
kv2))
unifyKinds (KindVariable kv :: Int
kv) k :: Kind
k
| Int
kv Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Kind -> [Int]
kindVars Kind
k = Maybe KindSubst
forall a. Maybe a
Nothing
| Bool
otherwise = KindSubst -> Maybe KindSubst
forall a. a -> Maybe a
Just (Int -> Kind -> KindSubst
forall v e. Ord v => v -> e -> Subst v e
singleSubst Int
kv Kind
k)
unifyKinds k :: Kind
k (KindVariable kv :: Int
kv)
| Int
kv Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Kind -> [Int]
kindVars Kind
k = Maybe KindSubst
forall a. Maybe a
Nothing
| Bool
otherwise = KindSubst -> Maybe KindSubst
forall a. a -> Maybe a
Just (Int -> Kind -> KindSubst
forall v e. Ord v => v -> e -> Subst v e
singleSubst Int
kv Kind
k)
unifyKinds (KindArrow k11 :: Kind
k11 k12 :: Kind
k12) (KindArrow k21 :: Kind
k21 k22 :: Kind
k22) = do
KindSubst
theta <- Kind -> Kind -> Maybe KindSubst
unifyKinds Kind
k11 Kind
k21
KindSubst
theta' <- Kind -> Kind -> Maybe KindSubst
unifyKinds (KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
theta Kind
k12) (KindSubst -> Kind -> Kind
forall a. SubstKind a => KindSubst -> a -> a
subst KindSubst
theta Kind
k22)
KindSubst -> Maybe KindSubst
forall a. a -> Maybe a
Just (KindSubst -> KindSubst -> KindSubst
forall v e. Ord v => Subst v e -> Subst v e -> Subst v e
compose KindSubst
theta' KindSubst
theta)
unifyKinds _ _ = Maybe KindSubst
forall a. Maybe a
Nothing
fresh :: (Int -> a) -> KCM a
fresh :: (Int -> a) -> KCM a
fresh f :: Int -> a
f = Int -> a
f (Int -> a) -> KCM Int -> KCM a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KCM Int
getNextId
freshKindVar :: KCM Kind
freshKindVar :: KCM Kind
freshKindVar = (Int -> Kind) -> KCM Kind
forall a. (Int -> a) -> KCM a
fresh Int -> Kind
KindVariable
typeConstructor :: Decl a -> Ident
typeConstructor :: Decl a -> Ident
typeConstructor (DataDecl _ tc :: Ident
tc _ _ _) = Ident
tc
typeConstructor (ExternalDataDecl _ tc :: Ident
tc _) = Ident
tc
typeConstructor (NewtypeDecl _ tc :: Ident
tc _ _ _) = Ident
tc
typeConstructor (TypeDecl _ tc :: Ident
tc _ _ ) = Ident
tc
typeConstructor _ =
String -> Ident
forall a. String -> a
internalError "Checks.KindCheck.typeConstructor: no type declaration"
isTypeOrNewtypeDecl :: Decl a -> Bool
isTypeOrNewtypeDecl :: Decl a -> Bool
isTypeOrNewtypeDecl (NewtypeDecl _ _ _ _ _) = Bool
True
isTypeOrNewtypeDecl (TypeDecl _ _ _ _) = Bool
True
isTypeOrNewtypeDecl _ = Bool
False
errRecursiveTypes :: [Ident] -> Message
errRecursiveTypes :: [Ident] -> Message
errRecursiveTypes [] = String -> Message
forall a. String -> a
internalError
"KindCheck.errRecursiveTypes: empty list"
errRecursiveTypes [tc :: Ident
tc] = Ident -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage Ident
tc (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text
["Recursive synonym or renaming type", Ident -> String
idName Ident
tc]
errRecursiveTypes (tc :: Ident
tc:tcs :: [Ident]
tcs) = Ident -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage Ident
tc (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$
String -> Doc
text "Mutually recursive synonym and/or renaming types" Doc -> Doc -> Doc
<+>
String -> Doc
text (Ident -> String
idName Ident
tc) Doc -> Doc -> Doc
<> Doc -> [Ident] -> Doc
types Doc
empty [Ident]
tcs
where
types :: Doc -> [Ident] -> Doc
types _ [] = Doc
empty
types del :: Doc
del [tc' :: Ident
tc'] = Doc
del Doc -> Doc -> Doc
<> Doc
space Doc -> Doc -> Doc
<> String -> Doc
text "and" Doc -> Doc -> Doc
<+> Ident -> Doc
typePos Ident
tc'
types _ (tc' :: Ident
tc':tcs' :: [Ident]
tcs') = Doc
comma Doc -> Doc -> Doc
<+> Ident -> Doc
typePos Ident
tc' Doc -> Doc -> Doc
<> Doc -> [Ident] -> Doc
types Doc
comma [Ident]
tcs'
typePos :: Ident -> Doc
typePos tc' :: Ident
tc' =
String -> Doc
text (Ident -> String
idName Ident
tc') Doc -> Doc -> Doc
<+> Doc -> Doc
parens (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Position -> String
showLine (Position -> String) -> Position -> String
forall a b. (a -> b) -> a -> b
$ Ident -> Position
forall a. HasPosition a => a -> Position
getPosition Ident
tc')
errRecursiveClasses :: [Ident] -> Message
errRecursiveClasses :: [Ident] -> Message
errRecursiveClasses [] = String -> Message
forall a. String -> a
internalError
"KindCheck.errRecursiveClasses: empty list"
errRecursiveClasses [cls :: Ident
cls] = Ident -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage Ident
cls (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text
["Recursive type class", Ident -> String
idName Ident
cls]
errRecursiveClasses (cls :: Ident
cls:clss :: [Ident]
clss) = Ident -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage Ident
cls (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$
String -> Doc
text "Mutually recursive type classes" Doc -> Doc -> Doc
<+> String -> Doc
text (Ident -> String
idName Ident
cls) Doc -> Doc -> Doc
<>
Doc -> [Ident] -> Doc
classes Doc
empty [Ident]
clss
where
classes :: Doc -> [Ident] -> Doc
classes _ [] = Doc
empty
classes del :: Doc
del [cls' :: Ident
cls'] = Doc
del Doc -> Doc -> Doc
<> Doc
space Doc -> Doc -> Doc
<> String -> Doc
text "and" Doc -> Doc -> Doc
<+> Ident -> Doc
classPos Ident
cls'
classes _ (cls' :: Ident
cls':clss' :: [Ident]
clss') = Doc
comma Doc -> Doc -> Doc
<+> Ident -> Doc
classPos Ident
cls' Doc -> Doc -> Doc
<> Doc -> [Ident] -> Doc
classes Doc
comma [Ident]
clss'
classPos :: Ident -> Doc
classPos cls' :: Ident
cls' =
String -> Doc
text (Ident -> String
idName Ident
cls') Doc -> Doc -> Doc
<+> Doc -> Doc
parens (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Position -> String
showLine (Position -> String) -> Position -> String
forall a b. (a -> b) -> a -> b
$ Ident -> Position
forall a. HasPosition a => a -> Position
getPosition Ident
cls')
errNonArrowKind :: HasPosition p => p -> String -> Doc -> Kind -> Message
errNonArrowKind :: p -> String -> Doc -> Kind -> Message
errNonArrowKind p :: p
p what :: String
what doc :: Doc
doc k :: Kind
k = p -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage p
p (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
[ String -> Doc
text "Kind error in" Doc -> Doc -> Doc
<+> String -> Doc
text String
what, Doc
doc
, String -> Doc
text "Kind:" Doc -> Doc -> Doc
<+> Kind -> Doc
ppKind Kind
k
, String -> Doc
text "Cannot be applied"
]
errPartialAlias :: HasPosition p => p -> QualIdent -> Int -> Int -> Message
errPartialAlias :: p -> QualIdent -> Int -> Int -> Message
errPartialAlias p :: p
p tc :: QualIdent
tc arity :: Int
arity argc :: Int
argc = p -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage p
p (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep
[ String -> Doc
text "Type synonym", QualIdent -> Doc
ppQIdent QualIdent
tc
, String -> Doc
text "requires at least"
, Int -> Doc
int Int
arity, String -> Doc
text (Int -> String -> String
forall a. (Eq a, Num a) => a -> String -> String
plural Int
arity "argument") Doc -> Doc -> Doc
<> Doc
comma
, String -> Doc
text "but is applied to only", Int -> Doc
int Int
argc
]
where
plural :: a -> String -> String
plural n :: a
n x :: String
x = if a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== 1 then String
x else String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "s"
errKindMismatch :: HasPosition p => p -> String -> Doc -> Kind -> Kind -> Message
errKindMismatch :: p -> String -> Doc -> Kind -> Kind -> Message
errKindMismatch p :: p
p what :: String
what doc :: Doc
doc k1 :: Kind
k1 k2 :: Kind
k2 = p -> Doc -> Message
forall p. HasPosition p => p -> Doc -> Message
posMessage p
p (Doc -> Message) -> Doc -> Message
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
[ String -> Doc
text "Kind error in" Doc -> Doc -> Doc
<+> String -> Doc
text String
what, Doc
doc
, String -> Doc
text "Inferred kind:" Doc -> Doc -> Doc
<+> Kind -> Doc
ppKind Kind
k2
, String -> Doc
text "Expected kind:" Doc -> Doc -> Doc
<+> Kind -> Doc
ppKind Kind
k1
]