{- |
    Module      :  $Header$
    Description :  Checks type kinds
    Copyright   :  (c) 2016 - 2017 Finn Teegen
    License     :  BSD-3-clause

    Maintainer  :  bjp@informatik.uni-kiel.de
    Stability   :  experimental
    Portability :  portable

   After the type syntax has been checked und nullary type constructors and
   type variables have been disambiguated, the compiler infers kinds for all
   type constructors and type classes defined in the current module and
   performs kind checking on all type definitions and type signatures.
-}
{-# 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

-- In order to infer kinds for type constructors and type classes, the
-- compiler sorts the module's type and class declarations into minimal
-- recursive binding groups and then applies kind inference to each
-- declaration group. Besides inferring kinds for the type constructors
-- and type classes of a group, the compiler also checks that there are
-- no mutually recursive type synonym definitions and that the super class
-- hierarchy is acyclic. The former allows entering fully expanded type
-- synonyms into the type constructor environment.

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 []

-- Kind Check Monad
type KCM = S.State KCState

-- |Internal state of the Kind Check
data KCState = KCState
  { KCState -> ModuleIdent
moduleIdent :: ModuleIdent -- read only
  , KCState -> KindSubst
kindSubst   :: KindSubst
  , KCState -> Int
nextId      :: Int         -- automatic counter
  , 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 ()

-- Minimal recursive declaration groups are computed using the sets of bound
-- and free type constructor and type class identifiers of the declarations.

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)

-- When types are entered into the type constructor environment, all type
-- synonyms occuring in the definitions are fully expanded (except for
-- record types) and all type constructors and type classes are qualified
-- with the name of the module in which they are defined. This is possible
-- because Curry does not allow (mutually) recursive type synonyms or
-- newtypes, which is checked in the function 'checkNonRecursiveTypes' below.

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"

-- The function 'checkAcyclicSuperClasses' checks that the super class
-- hierarchy is acyclic.

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"

-- For each declaration group, the kind checker first enters new
-- assumptions into the type constructor environment. For a type
-- constructor with arity n, we enter kind k_1 -> ... -> k_n -> k,
-- where k_i are fresh kind variables and k is * for data and newtype
-- type constructors and a fresh kind variable for type synonym type
-- constructors. For a type class we enter kind k, where k is a fresh
-- kind variable. We also add a type class to the class environment.
-- Next, the kind checker checks the declarations of the group within
-- the extended environment, and finally the kind checker instantiates
-- all remaining free kind variables to *.

-- As noted above, type synonyms are fully expanded while types are
-- entered into the type constructor environment. Furthermore, we uses
-- original names for classes and super classes in the class environment.
-- Unfortunately, both of this requires either sorting type declarations
-- properly or using the final type constructor environment for the expansion
-- and original names. We have chosen the latter option here, which requires
-- recursive monadic bindings which are supported using the 'mfix' method
-- from the 'MonadFix' type class.

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')

-- After adding new assumptions to the environment, kind inference is
-- applied to all declarations. The type environment may be extended
-- temporarily with bindings for type variables occurring in the left
-- hand side of type declarations and free type variables of type
-- signatures. While the kinds of the former are determined already by
-- the kinds of their type constructors and type classes, respectively,
-- fresh kind variables are added for the latter.

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)

-- ---------------------------------------------------------------------------
-- Unification
-- ---------------------------------------------------------------------------

-- The unification uses Robinson's algorithm.
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 variables
-- ---------------------------------------------------------------------------

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

-- ---------------------------------------------------------------------------
-- Auxiliary definitions
-- ---------------------------------------------------------------------------

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

-- ---------------------------------------------------------------------------
-- Error messages
-- ---------------------------------------------------------------------------

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
  ]