ddc-core 0.4.2.1 → 0.4.3.1

raw patch · 167 files changed

+11822/−8797 lines, 167 filesdep +filepathdep +inchwormdep +parsecdep −ddc-basedep ~basedep ~mtldep ~transformersPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: filepath, inchworm, parsec, wl-pprint

Dependencies removed: ddc-base

Dependency ranges changed: base, mtl, transformers

API changes (from Hackage documentation)

Files

• DDC/Control/Check.hs +73/−0
• DDC/Control/Panic.hs +23/−0
• DDC/Control/Parser.hs +156/−0
• DDC/Core/Check.hs +67/−6
• DDC/Core/Check/Base.hs +22/−80
• DDC/Core/Check/Config.hs +79/−0
• DDC/Core/Check/Context.hs +78/−0
• DDC/Core/Check/Context/Apply.hs +121/−0
• DDC/Core/Check/Context/Base.hs +433/−0
• DDC/Core/Check/Context/Effect.hs +69/−0
• DDC/Core/Check/Context/Elem.hs +158/−0
• DDC/Core/Check/Context/Mode.hs +42/−0
• DDC/Core/Check/Error.hs +9/−372
• DDC/Core/Check/Error/ErrorData.hs +23/−0
• DDC/Core/Check/Error/ErrorDataMessage.hs +27/−0
• DDC/Core/Check/Error/ErrorExp.hs +383/−0
• DDC/Core/Check/Error/ErrorExpMessage.hs +431/−0
• DDC/Core/Check/Error/ErrorType.hs +94/−0
• DDC/Core/Check/Error/ErrorTypeMessage.hs +107/−0
• DDC/Core/Check/ErrorMessage.hs +0/−427
• DDC/Core/Check/Exp.hs +15/−19
• DDC/Core/Check/Judge/DataDefs.hs +181/−0
• DDC/Core/Check/Judge/Eq.hs +0/−177
• DDC/Core/Check/Judge/EqT.hs +201/−0
• DDC/Core/Check/Judge/Kind.hs +656/−0
• DDC/Core/Check/Judge/Kind/TyCon.hs +67/−0
• DDC/Core/Check/Judge/Module.hs +673/−0
• DDC/Core/Check/Judge/Sub.hs +278/−104
• DDC/Core/Check/Judge/Type/AppT.hs +4/−6
• DDC/Core/Check/Judge/Type/AppX.hs +68/−40
• DDC/Core/Check/Judge/Type/Base.hs +44/−8
• DDC/Core/Check/Judge/Type/Case.hs +80/−42
• DDC/Core/Check/Judge/Type/Cast.hs +22/−20
• DDC/Core/Check/Judge/Type/DaCon.hs +6/−7
• DDC/Core/Check/Judge/Type/LamT.hs +13/−16
• DDC/Core/Check/Judge/Type/LamX.hs +25/−27
• DDC/Core/Check/Judge/Type/Let.hs +10/−14
• DDC/Core/Check/Judge/Type/LetPrivate.hs +21/−18
• DDC/Core/Check/Judge/Type/Sub.hs +130/−13
• DDC/Core/Check/Judge/Type/VarCon.hs +58/−30
• DDC/Core/Check/Judge/Type/Witness.hs +2/−4
• DDC/Core/Check/Judge/Witness.hs +135/−0
• DDC/Core/Check/Module.hs +0/−506
• DDC/Core/Check/Witness.hs +0/−133
• DDC/Core/Collect.hs +10/−4
• DDC/Core/Collect/BindStruct.hs +176/−0
• DDC/Core/Collect/Free.hs +0/−119
• DDC/Core/Collect/Free/Simple.hs +0/−77
• DDC/Core/Collect/FreeT.hs +79/−0
• DDC/Core/Collect/FreeX.hs +120/−0
• DDC/Core/Collect/Support.hs +1/−1
• DDC/Core/Env/EnvT.hs +219/−0
• DDC/Core/Env/EnvX.hs +271/−0
• DDC/Core/Exp/Annot.hs +4/−4
• DDC/Core/Exp/Annot/AnT.hs +1/−1
• DDC/Core/Exp/Annot/AnTEC.hs +2/−3
• DDC/Core/Exp/Annot/Compounds.hs +3/−3
• DDC/Core/Exp/Annot/Context.hs +16/−18
• DDC/Core/Exp/Annot/Ctx.hs +15/−19
• DDC/Core/Exp/Annot/Exp.hs +4/−4
• DDC/Core/Exp/Annot/Predicates.hs +2/−2
• DDC/Core/Exp/Annot/Pretty.hs +324/−0
• DDC/Core/Exp/DaCon.hs +7/−8
• DDC/Core/Exp/Generic.hs +73/−0
• DDC/Core/Exp/Generic/BindStruct.hs +2/−2
• DDC/Core/Exp/Generic/Compounds.hs +4/−3
• DDC/Core/Exp/Generic/Exp.hs +13/−9
• DDC/Core/Exp/Generic/Predicates.hs +2/−2
• DDC/Core/Exp/Generic/Pretty.hs +9/−5
• DDC/Core/Exp/Literal.hs +22/−0
• DDC/Core/Exp/Simple/Compounds.hs +0/−288
• DDC/Core/Exp/Simple/Exp.hs +0/−196
• DDC/Core/Fragment.hs +2/−3
• DDC/Core/Fragment/Profile.hs +8/−4
• DDC/Core/Lexer.hs +114/−237
• DDC/Core/Lexer/Comments.hs +0/−64
• DDC/Core/Lexer/Names.hs +0/−297
• DDC/Core/Lexer/Offside.hs +105/−74
• DDC/Core/Lexer/Token/Builtin.hs +111/−0
• DDC/Core/Lexer/Token/Index.hs +21/−0
• DDC/Core/Lexer/Token/Keyword.hs +139/−0
• DDC/Core/Lexer/Token/Literal.hs +246/−0
• DDC/Core/Lexer/Token/Names.hs +141/−0
• DDC/Core/Lexer/Token/Operator.hs +110/−0
• DDC/Core/Lexer/Token/Symbol.hs +166/−0
• DDC/Core/Lexer/Tokens.hs +113/−268
• DDC/Core/Load.hs +33/−21
• DDC/Core/Module.hs +165/−9
• DDC/Core/Module/Export.hs +5/−6
• DDC/Core/Module/Import.hs +18/−19
• DDC/Core/Module/Name.hs +28/−0
• DDC/Core/Parser.hs +1/−1
• DDC/Core/Parser/Base.hs +32/−35
• DDC/Core/Parser/Context.hs +21/−11
• DDC/Core/Parser/DataDef.hs +9/−8
• DDC/Core/Parser/Exp.hs +85/−79
• DDC/Core/Parser/ExportSpec.hs +19/−13
• DDC/Core/Parser/ImportSpec.hs +75/−35
• DDC/Core/Parser/Module.hs +56/−27
• DDC/Core/Parser/Param.hs +12/−12
• DDC/Core/Parser/Type.hs +36/−25
• DDC/Core/Parser/Witness.hs +7/−7
• DDC/Core/Pretty.hs +57/−331
• DDC/Core/Transform/Annotate.hs +0/−88
• DDC/Core/Transform/Deannotate.hs +0/−75
• DDC/Core/Transform/Reannotate.hs +5/−5
• DDC/Core/Transform/SpreadX.hs +20/−17
• DDC/Core/Transform/SubstituteTX.hs +1/−1
• DDC/Core/Transform/SubstituteWX.hs +1/−1
• DDC/Core/Transform/SubstituteXX.hs +1/−1
• DDC/Data/Canned.hs +13/−0
• DDC/Data/Env.hs +174/−0
• DDC/Data/ListUtils.hs +75/−0
• DDC/Data/Name.hs +25/−0
• DDC/Data/Pretty.hs +139/−0
• DDC/Data/SourcePos.hs +79/−0
• DDC/Type/Check.hs +0/−88
• DDC/Type/Check/Base.hs +0/−75
• DDC/Type/Check/CheckCon.hs +0/−69
• DDC/Type/Check/Config.hs +0/−89
• DDC/Type/Check/Context.hs +0/−610
• DDC/Type/Check/Data.hs +0/−180
• DDC/Type/Check/Error.hs +0/−114
• DDC/Type/Check/ErrorMessage.hs +0/−124
• DDC/Type/Check/Judge/Eq.hs +0/−79
• DDC/Type/Check/Judge/Kind.hs +0/−640
• DDC/Type/Collect.hs +0/−195
• DDC/Type/Collect/FreeT.hs +0/−57
• DDC/Type/Compounds.hs +0/−630
• DDC/Type/DataDef.hs +2/−3
• DDC/Type/Env.hs +9/−15
• DDC/Type/Equiv.hs +0/−302
• DDC/Type/Exp.hs +2/−2
• DDC/Type/Exp/Base.hs +0/−267
• DDC/Type/Exp/Flat.hs +7/−0
• DDC/Type/Exp/Flat/Exp.hs +24/−0
• DDC/Type/Exp/Flat/Pretty.hs +13/−0
• DDC/Type/Exp/Generic.hs +42/−0
• DDC/Type/Exp/Generic/Binding.hs +29/−0
• DDC/Type/Exp/Generic/Compounds.hs +261/−0
• DDC/Type/Exp/Generic/Exp.hs +161/−0
• DDC/Type/Exp/Generic/NFData.hs +38/−0
• DDC/Type/Exp/Generic/Predicates.hs +16/−0
• DDC/Type/Exp/Generic/Pretty.hs +59/−0
• DDC/Type/Exp/NFData.hs +0/−93
• DDC/Type/Exp/Pretty.hs +51/−0
• DDC/Type/Exp/Simple.hs +176/−0
• DDC/Type/Exp/Simple/Compounds.hs +663/−0
• DDC/Type/Exp/Simple/Equiv.hs +339/−0
• DDC/Type/Exp/Simple/Exp.hs +182/−0
• DDC/Type/Exp/Simple/NFData.hs +77/−0
• DDC/Type/Exp/Simple/Predicates.hs +263/−0
• DDC/Type/Exp/Simple/Pretty.hs +144/−0
• DDC/Type/Exp/Simple/Subsumes.hs +26/−0
• DDC/Type/Exp/TyCon.hs +102/−0
• DDC/Type/Predicates.hs +0/−253
• DDC/Type/Pretty.hs +0/−185
• DDC/Type/Subsumes.hs +0/−25
• DDC/Type/Sum.hs +18/−10
• DDC/Type/Transform/BoundT.hs +6/−6
• DDC/Type/Transform/Rename.hs +9/−3
• DDC/Type/Transform/SpreadT.hs +6/−1
• DDC/Type/Transform/SubstituteT.hs +26/−11
• DDC/Type/Universe.hs +29/−5
• DDC/Version.hs +8/−0
• LICENSE +1/−1
• ddc-core.cabal +102/−54

@@ -0,0 +1,73 @@++-- | A simple exception monad.+module DDC.Control.Check+        ( CheckM (..)+        , throw+        , runCheck+        , evalCheck+        , get+        , put)+where+import Control.Monad+++-- | Checker monad maintains some state and manages errors during type checking.+data CheckM s err a+        = CheckM (s -> (s, Either err a))+++instance Functor (CheckM s err) where+ fmap   = liftM+++instance Applicative (CheckM s err) where+ (<*>)  = ap+ pure   = return+++instance Monad (CheckM s err) where+ return !x   +  = CheckM (\s -> (s, Right x))+ {-# INLINE return #-}++ (>>=) !(CheckM f) !g  +  = CheckM $ \s  +  -> case f s of+        (s', Left err)  -> (s', Left err)+        (s', Right x)   -> s `seq` x `seq` runCheck s' (g x)+ {-# INLINE (>>=) #-}+++-- | Run a checker computation,+--      returning the result and new state.+runCheck :: s -> CheckM s err a -> (s, Either err a)+runCheck s (CheckM f)   = f s+{-# INLINE runCheck #-}+++-- | Run a checker computation, +--      ignoreing the final state.+evalCheck :: s -> CheckM s err a -> Either err a+evalCheck s m   = snd $ runCheck s m+{-# INLINE evalCheck #-}+++-- | Throw a type error in the monad.+throw :: err -> CheckM s err a+throw !e        = CheckM $ \s -> (s, Left e)+{-# INLINE throw #-}+++-- | Get the state from the monad.+get :: CheckM s err s+get =  CheckM $ \s -> (s, Right s)+{-# INLINE get #-}+++-- | Put a new state into the monad.+put :: s -> CheckM s err ()+put s + =  CheckM $ \_ -> (s, Right ())+{-# INLINE put #-}++

@@ -0,0 +1,23 @@++module DDC.Control.Panic+        (panic)+where+import DDC.Data.Pretty+++-- | Print an error message and exit the compiler, ungracefully.+--+--   This function should be called when we end up in a state that is definately+--   due to a bug in the compiler. +--+panic   :: String       -- ^ Package name,+        -> String       -- ^ Function name.+        -> Doc          -- ^ Error message that makes some suggestion of what+                        --   caused the error.+        -> a++panic pkg fun msg+        = error $ renderIndent $ vcat+        [ text "PANIC in" <+> text pkg <> text "." <> text fun +        , indent 2 msg +        , empty]

@@ -0,0 +1,156 @@+{-# LANGUAGE TypeFamilies #-}++-- | Parser utilities.+module DDC.Control.Parser+        ( module Text.Parsec+        , Parser+        , ParserState   (..)+        , D.SourcePos   (..)+        , runTokenParser+        , pTokMaybe,    pTokMaybeSP+        , pTokAs,       pTokAsSP+        , pTok,         pTokSP)+where+import DDC.Data.Pretty+import DDC.Data.SourcePos       as D+import Data.Functor.Identity+import Text.Parsec              hiding (SourcePos)+import Text.Parsec              as P  +import Text.Parsec.Error        as P+++-- | A generic parser,+--   parameterised over token and return types.+type Parser k a+        =  Eq k+        => P.ParsecT [Located k] (ParserState k) Identity a+++-- | A parser state that keeps track of the name of the source file.+data ParserState k+        = ParseState+        { stateTokenShow        :: k -> String+        , stateFileName         :: String }+++-- | Run a generic parser, making sure all input is consumed.+runTokenParser+        :: Eq k+        => (k -> String)        -- ^ Show a token.+        -> String               -- ^ File name for error messages.+        -> Parser k a           -- ^ Parser to run.+        -> [Located k]          -- ^ Tokens to parse.+        -> Either P.ParseError a++runTokenParser tokenShow fileName parser + = P.runParser eofParser+        ParseState +        { stateTokenShow        = tokenShow+        , stateFileName         = fileName }+        fileName+ where+  eofParser+   = do r <- parser+        -- We can't use primitive Text.Parsec.eof because it requires+        -- @Show (Token k)@+        (do+                c <- pTokMaybe Just+                unexpected (tokenShow c)) <|> return r+++-------------------------------------------------------------------------------+-- | Accept the given token.+pTok   :: k -> Parser k ()+pTok k  = pTokMaybe $ \k' -> if k == k' then Just () else Nothing+++-- | Accept the given token, returning its source position.+pTokSP :: k -> Parser k D.SourcePos+pTokSP k  + = do   (_, sp) <- pTokMaybeSP +                $ \k' -> if k == k' then Just () else Nothing+        return sp+++-- | Accept a token and return the given value.+pTokAs :: k -> t -> Parser k t+pTokAs k t + = do   pTok k+        return t+++-- | Accept a token and return the given value, +--   along with the source position of the token.+pTokAsSP :: k -> t -> Parser k (t, D.SourcePos)+pTokAsSP k t + = do   sp      <- pTokSP k+        return  (t, sp)+++-- | Accept a token if the function returns `Just`. +pTokMaybe :: (k -> Maybe a) -> Parser k a+pTokMaybe f + = do   state   <- P.getState++        P.token (stateTokenShow state . valueOfLocated)+                (parsecSourcePosOfLocated)+                (f . valueOfLocated)+++-- | Accept a token if the function return `Just`, +--   also returning the source position of that token.+pTokMaybeSP  :: (k -> Maybe a) -> Parser k (a, D.SourcePos)+pTokMaybeSP f+ = do   state   <- P.getState++        let f' token' +                = case f (valueOfLocated token') of+                        Nothing -> Nothing+                        Just x  -> Just (x, sourcePosOfLocated token')++        P.token (stateTokenShow state . valueOfLocated)+                (parsecSourcePosOfLocated)+                f'+++-------------------------------------------------------------------------------+instance Pretty P.ParseError where+ data PrettyMode P.ParseError   = PrettyParseError+ pprDefaultMode                 = PrettyParseError+ ppr err+  = vcat $  [  text "Parse error in" <+> text (show (P.errorPos err)) ]+         ++ (map ppr $ packMessages $ P.errorMessages err)+         +         +instance Pretty P.Message where+ data PrettyMode P.Message      = PrettyMessage+ pprDefaultMode                 = PrettyMessage+ ppr msg+  = case msg of+        SysUnExpect str -> text "Unexpected" <+> text str <> text "."+        UnExpect    str -> text "Unexpected" <+> text str <> text "."+        Expect      str -> text "Expected"   <+> text str <> text "."+        Message     str -> text str+++-- | When we get a parse error, parsec adds multiple 'Unexpected' messages,+--   but we only want to display the first one.+packMessages :: [P.Message] -> [P.Message]+packMessages mm+ = case mm of+        []      -> []+        m1@(P.UnExpect _)   :  (P.UnExpect _)    : rest+                -> packMessages (m1 : rest)++        m1@(P.SysUnExpect _) : (P.SysUnExpect _) : rest+                -> packMessages (m1 : rest)++        m1@(P.SysUnExpect _) : (P.UnExpect _)    : rest+                -> packMessages (m1 : rest)++        m1@(P.UnExpect _)    : (P.SysUnExpect _) : rest+                -> packMessages (m1 : rest)++        m1 : rest+                -> m1 : packMessages rest+

@@ -1,4 +1,3 @@- -- | Type checker for the Disciple Core language. --  --   The functions in this module do not check for language fragment compliance.@@ -15,6 +14,12 @@           -- * Checking Modules         , checkModule         +          -- * Checking Types+        , checkType,    checkTypeM+        , checkSpec+        , kindOfSpec+        , sortOfKind+           -- * Checking Expressions         , Mode   (..)         , Demand (..)@@ -24,16 +29,72 @@         , checkWitness, typeOfWitness         , typeOfWiCon +          -- * Kinds of Constructors+        , takeSortOfKiCon+        , kindOfTwCon+        , kindOfTcCon+           -- * Annotations         , AnTEC(..)            -- * Error messages-        , Error         (..))+        , Error         (..)+        , ErrorType     (..)+        , ErrorData     (..)) where+import DDC.Core.Check.Judge.Kind+import DDC.Core.Check.Judge.Kind.TyCon+import DDC.Core.Check.Judge.Module+import DDC.Core.Check.Judge.Witness import DDC.Core.Check.Error-import DDC.Core.Check.ErrorMessage      ()-import DDC.Core.Check.Module import DDC.Core.Check.Exp-import DDC.Core.Check.Witness import DDC.Core.Check.Base-                +++-- | Check a type in the given universe with the given environment+--   Returns the updated type and its classifier (a kind or sort),+--   depeding on the universe of the type being checked.+checkType  :: (Ord n, Show n, Pretty n)+           => Config n -> Universe -> Type n+           -> Either (Error a n) (Type n, Type n)++checkType config uni tt+ = evalCheck (mempty, 0, 0)+ $ do   (t, k, _) <- checkTypeM config emptyContext uni tt Recon+        return (t, k)+++-- | Check a spec in the given environment, returning an error or its kind.+checkSpec  :: (Ord n, Show n, Pretty n) +           => Config n -> Type n+           -> Either (Error a n) (Type n, Kind n)++checkSpec config tt + = evalCheck (mempty, 0, 0)+ $ do   (t, k, _) <- checkTypeM config emptyContext UniverseSpec tt Recon+        return (t, k)+++-- | Check a spec in an empty environment, returning an error or its kind.+kindOfSpec+        :: (Ord n, Show n, Pretty n) +        => Config n -> Type n +        -> Either (Error a n) (Kind n)++kindOfSpec config tt+ = evalCheck (mempty, 0, 0)+ $ do   (_, k, _) <- checkTypeM config emptyContext UniverseSpec tt Recon+        return k+++-- | Check a kind in an empty environment, returning an error or its sort.+sortOfKind +        :: (Ord n, Show n, Pretty n)+        => Config n -> Kind n+        -> Either (Error a n) (Sort n)++sortOfKind config tt+ = evalCheck (mempty, 0, 0)+ $ do   (_, s, _) <- checkTypeM config emptyContext UniverseKind tt Recon+        return s+

@@ -13,25 +13,20 @@         , CheckTrace (..)         , ctrace -        , checkTypeM-        , checkBindM-           -- Things defined elsewhere.         , throw, runCheck, evalCheck-        , KindEnv, TypeEnv+        , EnvX,  EnvT, TypeEnv, KindEnv         , Set         , module DDC.Core.Check.Error         , module DDC.Core.Collect         , module DDC.Core.Pretty         , module DDC.Core.Exp.Annot-        , module DDC.Type.Check.Context+        , module DDC.Core.Check.Context+         , module DDC.Type.DataDef-        , module DDC.Type.Equiv         , module DDC.Type.Universe-        , module DDC.Type.Compounds-        , module DDC.Type.Predicates-        , module DDC.Type.Exp-        , module DDC.Base.Pretty+        , module DDC.Type.Exp.Simple+        , module DDC.Data.Pretty         , module DDC.Data.ListUtils         , module Control.Monad         , module Data.Maybe)@@ -40,26 +35,26 @@ import DDC.Core.Collect import DDC.Core.Pretty import DDC.Core.Exp.Annot-import DDC.Type.Check.Context-import DDC.Type.Check                           (Config (..), configOfProfile)-import DDC.Type.Env                             (KindEnv, TypeEnv)+import DDC.Core.Check.Context+import DDC.Core.Check.Config+import DDC.Core.Env.EnvT                (EnvT)+import DDC.Core.Env.EnvX                (EnvX)++import DDC.Type.Env                     (TypeEnv, KindEnv) import DDC.Type.DataDef-import DDC.Type.Equiv import DDC.Type.Universe-import DDC.Type.Compounds-import DDC.Type.Predicates-import DDC.Type.Exp-import DDC.Base.Pretty-import DDC.Control.Monad.Check                  (throw, runCheck, evalCheck)+import DDC.Type.Exp.Simple+import DDC.Control.Check                (throw, runCheck, evalCheck)+import DDC.Data.Pretty import DDC.Data.ListUtils+ import Control.Monad-import Data.Monoid                              hiding ((<>))+import Data.Monoid                      hiding ((<>)) import Data.Maybe-import Data.Set                                 (Set)-import qualified Data.Set                       as Set-import qualified DDC.Type.Check                 as T-import qualified DDC.Control.Monad.Check        as G-import Prelude                                  hiding ((<$>))+import Data.Set                         (Set)+import qualified Data.Set               as Set+import qualified DDC.Control.Check      as G+import Prelude                          hiding ((<$>))   -- | Type checker monad.@@ -88,7 +83,7 @@ applyContext ctx tt  = case applyContextEither ctx Set.empty tt of         Left  (tExt, tBind)       -                -> throw $ ErrorType $ T.ErrorInfinite tExt tBind+                -> throw $ ErrorType $ ErrorTypeInfinite tExt tBind         Right t -> return t  @@ -97,7 +92,7 @@ applySolved ctx tt  = case applySolvedEither ctx Set.empty tt of         Left  (tExt, tBind)-                -> throw $ ErrorType $ T.ErrorInfinite tExt tBind+                -> throw $ ErrorType $ ErrorTypeInfinite tExt tBind         Right t -> return t  @@ -126,57 +121,4 @@         let tr' = tr { checkTraceDoc = checkTraceDoc tr <$> doc' }         G.put (tr', ix, pos)         return  ()----- Bind -------------------------------------------------------------------------- | Check the type of a bind.-checkBindM-        :: (Ord n, Show n, Pretty n)-        => Config n             -- ^ Checker configuration.-        -> KindEnv n            -- ^ Global kind environment.-        -> Context n            -- ^ Local context.-        -> Universe             -- ^ Universe for the type of the bind.-        -> Bind n               -- ^ Check this bind.-        -> Mode n               -- ^ Mode for bidirectional checking.-        -> CheckM a n (Bind n, Type n, Context n)--checkBindM config kenv ctx uni bb mode- = do   (t', k, ctx')   <- checkTypeM config kenv ctx uni-                                (typeOfBind bb) mode-        return (replaceTypeOfBind t' bb, k, ctx')----- Type -------------------------------------------------------------------------- | Check a type in the exp checking monad, returning its kind.-checkTypeM-        :: (Ord n, Show n, Pretty n)-        => Config n             -- ^ Checker configuration.-        -> KindEnv n            -- ^ Global kind environment.-        -> Context n            -- ^ Local context.-        -> Universe             -- ^ Universe the type is supposed to be in.-        -> Type n               -- ^ Check this type.-        -> Mode n               -- ^ Mode for bidirectional checking-        -> CheckM a n (Type n, Kind n, Context n)--checkTypeM config kenv ctx uni tt mode- = do-        -- Run the inner type/kind checker computation,-        -- giving it our current values for the existential and position-        -- generators.-        (tr, ix, pos)   <- G.get--        let ((ix', pos'), result)-                = G.runCheck (ix, pos)-                $ T.checkTypeM config kenv ctx uni tt mode--        G.put (tr, ix', pos')--        -- If the type/kind checker returns an error then wrap it-        -- so we can throw it from our exp/type checker.-        case result of-         Left err-          -> throw $ ErrorType err--         Right (t, k, ctx')-          -> return (t, k, ctx') 

@@ -0,0 +1,79 @@++module DDC.Core.Check.Config+        ( Config (..)+        , configOfProfile)+where+import DDC.Type.DataDef+import DDC.Type.Env                     (KindEnv, TypeEnv)+import qualified DDC.Core.Fragment      as F+++-- Config ---------------------------------------------------------------------+-- | Static configuration for the type checker.+--   These fields don't change as we decend into the tree.+--+--   The starting configuration should be converted from the profile that+--   defines the language fragment you are checking. +--   See "DDC.Core.Fragment" and use `configOfProfile` below.+data Config n+        = Config+        { -- | Kinds of primitive types.+          configPrimKinds               :: KindEnv n++          -- | Types of primitive operators.+        , configPrimTypes               :: TypeEnv n++          -- | Data type definitions.+        , configPrimDataDefs            :: DataDefs n  ++          -- | This name represents some hole in the expression that needs+          --   to be filled in by the type checker.+        , configNameIsHole              :: Maybe (n -> Bool) ++          -- | Track effect type information.+        , configTrackedEffects          :: Bool++          -- | Track closure type information.+        , configTrackedClosures         :: Bool ++          -- | Attach effect information to function types.+        , configFunctionalEffects       :: Bool++          -- | Attach closure information to function types.+        , configFunctionalClosures      :: Bool++          -- | Treat effects as capabilities.+        , configEffectCapabilities      :: Bool ++          -- | Allow general let-rec+        , configGeneralLetRec           :: Bool++          -- | Automatically run effectful applications.+        , configImplicitRun             :: Bool++          -- | Automatically box bodies of abstractions.+        , configImplicitBox             :: Bool+        }+++-- | Convert a language profile to a type checker configuration.+configOfProfile :: F.Profile n -> Config n+configOfProfile profile+ = let  features        = F.profileFeatures profile+   in   Config+        { configPrimKinds               = F.profilePrimKinds            profile+        , configPrimTypes               = F.profilePrimTypes            profile+        , configPrimDataDefs            = F.profilePrimDataDefs         profile+        , configNameIsHole              = F.profileNameIsHole           profile +        +        , configTrackedEffects          = F.featuresTrackedEffects      features+        , configTrackedClosures         = F.featuresTrackedClosures     features+        , configFunctionalEffects       = F.featuresFunctionalEffects   features+        , configFunctionalClosures      = F.featuresFunctionalClosures  features+        , configEffectCapabilities      = F.featuresEffectCapabilities  features+        , configGeneralLetRec           = F.featuresGeneralLetRec       features+        , configImplicitRun             = F.featuresImplicitRun         features+        , configImplicitBox             = F.featuresImplicitBox         features+        }+        +

@@ -0,0 +1,78 @@++module DDC.Core.Check.Context+        ( +          -- * Type Checker Mode.+          Mode    (..)++          -- * Positions in the Context.+        , Pos     (..)++          -- * Roles of Type Variable.+        , Role    (..)++          -- * Existentials+        , Exists  (..)+        , typeOfExists+        , takeExists+        , slurpExists++          -- * Context Elements.+        , Elem    (..)++          -- * Checker Context.+        , Context (..)++          -- * Construction+        , emptyContext+        , contextOfEnvT+        , contextOfEnvX+        , contextOfPrimEnvs++          -- * Projection+        , contextEquations+        , contextCapabilities+        , contextDataDefs+        , contextEnvT++          -- * Pushing+        , pushType,   pushTypes+        , pushKind,   pushKinds+        , pushExists, pushExistsBefore, pushExistsScope++          -- * Marking+        , markContext++          -- * Popping+        , popToPos++          -- * Lookup+        , lookupType+        , lookupKind+        , lookupExistsEq++          -- * Membership+        , memberType+        , memberKind+        , memberKindBind++          -- * Existentials+        , locationOfExists+        , updateExists++          -- * Lifting and Lowering+        , liftTypes+        , lowerTypes++          -- * Applying+        , applyContextEither+        , applySolvedEither++          -- * Effects+        , effectSupported)+where+import DDC.Core.Check.Context.Effect+import DDC.Core.Check.Context.Apply+import DDC.Core.Check.Context.Elem+import DDC.Core.Check.Context.Mode+import DDC.Core.Check.Context.Base+

@@ -0,0 +1,121 @@++module DDC.Core.Check.Context.Apply+        ( applyContextEither+        , applySolvedEither)+where+import DDC.Core.Check.Context.Elem+import DDC.Core.Check.Context.Base+import DDC.Type.Exp.Simple+import qualified DDC.Type.Sum           as Sum++import Data.Set                         (Set)+import Data.Maybe+import qualified Data.IntMap.Strict     as IntMap+import qualified Data.Set               as Set++import Prelude                          hiding ((<$>))+++-- | Apply a context to a type, updating any existentials in the type. This+--   uses just the solved constraints on the stack, but not in the solved set.+--+--   If we find a loop through the existential equations then +--   return `Left` the existential and what is was locally bound to.+--+applyContextEither+        :: Ord n +        => Context n    -- ^ Type checker context.+        -> Set Int      -- ^ Indexes of existentials we've already entered.+        -> Type n       -- ^ Type to apply context to.+        -> Either (Type n, Type n) (Type n)++applyContextEither ctx is tt+ = case tt of+        TVar{}          +         ->     return tt++        TCon (TyConExists i k)  +         |  Just t      <- lookupExistsEq (Exists i k) ctx+         -> if Set.member i is +                then Left (tt, t)+                else applyContextEither ctx (Set.insert i is) t++        TCon{}+         ->     return tt++        TAbs b t     +         -> do  tb'     <- applySolvedEither ctx is (typeOfBind b)+                let b'  =  replaceTypeOfBind tb' b+                t'      <- applySolvedEither ctx is t+                return $ TAbs b' t'++        TApp t1 t2+         -> do  t1'     <- applySolvedEither ctx is t1+                t2'     <- applySolvedEither ctx is t2+                return  $ TApp t1' t2'++        TForall b t     +         -> do  tb'     <- applySolvedEither ctx is (typeOfBind b)+                let b'  =  replaceTypeOfBind tb' b+                t'      <- applySolvedEither ctx is t+                return $ TForall b' t'++        TSum ts         +         -> do  tss'    <- mapM (applyContextEither ctx is) +                        $  Sum.toList ts++                return  $ TSum+                        $ Sum.fromList (Sum.kindOfSum ts) tss'+++-- | Like `applyContextEither`, but for the solved types.+applySolvedEither+        :: Ord n +        => Context n    -- ^ Type checker context.+        -> Set Int      -- ^ Indexes of existentials we've already entered.+        -> Type n       -- ^ Type to apply context to.+        -> Either (Type n, Type n) (Type n)++applySolvedEither ctx is tt+ = case tt of+        TVar{}          +         ->     return tt++        TCon (TyConExists i k)+         |  Just t       <- IntMap.lookup i (contextSolved ctx)+         -> if Set.member i is +                then Left (tt, t)+                else applySolvedEither ctx (Set.insert i is) t++         |  Just t       <- lookupExistsEq (Exists i k) ctx+         -> if Set.member i is+                then Left (tt, t)+                else applySolvedEither ctx (Set.insert i is) t++        TCon {}+         ->     return tt++        TAbs b t+         -> do  tb'     <- applySolvedEither ctx is (typeOfBind b)     +                let b'  =  replaceTypeOfBind tb' b+                t'      <- applySolvedEither ctx is t+                return  $ TAbs b' t'++        TApp t1 t2      +         -> do  t1'     <- applySolvedEither ctx is t1+                t2'     <- applySolvedEither ctx is t2+                return  $ TApp t1' t2'++        TForall b t+         -> do  tb'     <- applySolvedEither ctx is (typeOfBind b)     +                let b'  =  replaceTypeOfBind tb' b+                t'      <- applySolvedEither ctx is t+                return  $ TForall b' t'++        TSum ts+         -> do  tss'    <- mapM (applySolvedEither ctx is)+                        $  Sum.toList ts++                return  $  TSum+                        $  Sum.fromList (Sum.kindOfSum ts) tss'+

@@ -0,0 +1,433 @@++module DDC.Core.Check.Context.Base +        ( Context (..)++          -- * Construction+        , emptyContext+        , contextOfEnvT+        , contextOfEnvX+        , contextOfPrimEnvs++          -- * Projection+        , contextEquations+        , contextCapabilities+        , contextDataDefs+        , contextEnvT++          -- * Pushing+        , pushType,   pushTypes+        , pushKind,   pushKinds+        , pushExists+        , pushExistsBefore+        , pushExistsScope++          -- * Marking+        , markContext++          -- * Popping+        , popToPos++          -- * Lookup+        , lookupType+        , lookupKind+        , lookupExistsEq++          -- * Membership+        , memberType+        , memberKind+        , memberKindBind++          -- * Existentials+        , locationOfExists+        , updateExists++          -- * Lifting+        , liftTypes+        , lowerTypes)+where+import DDC.Core.Check.Context.Elem+import DDC.Core.Env.EnvX                (EnvX)+import DDC.Core.Env.EnvX                (EnvT)+import DDC.Type.Transform.BoundT+import DDC.Type.Exp.Simple+import DDC.Type.DataDef+import DDC.Data.Pretty+import qualified DDC.Core.Env.EnvT      as EnvT+import qualified DDC.Core.Env.EnvX      as EnvX+import qualified DDC.Type.Env           as Env++import Data.Maybe+import Data.IntMap.Strict               (IntMap)+import Data.Map                         (Map)+import qualified Data.IntMap.Strict     as IntMap++import Prelude                          hiding ((<$>))++++-- Context --------------------------------------------------------------------+-- | The type checker context.+-- +--   Holds a position counter and a stack of elements. +--   The top of the stack is at the front of the list.+--+data Context n+        = Context +        { -- | Top level environment for terms.+          contextEnvX           :: !(EnvX n)++          -- | Fresh name generator for context positions.+        , contextGenPos         :: !Int++          -- | Fresh name generator for existential variables.+        , contextGenExists      :: !Int ++          -- | The current context stack.+        , contextElems          :: ![Elem n] +        +          -- | Types of solved existentials.+          --   When solved constraints are popped from the main context stack+          --   they are added to this map. The map is used to fill in type +          --   annotations after type inference proper. It's not used as part+          --   of the main algorithm.+        , contextSolved         :: IntMap (Type n) }+++instance (Pretty n, Eq n) => Pretty (Context n) where+ ppr (Context _ genPos genExists ls _solved)+  =   text "Context "+  <$> text "  genPos    = " <> int genPos+  <$> text "  genExists = " <> int genExists+  <$> indent 2 +        (vcat $ [padL 4 (int i)  <+> ppr l+                        | l <- reverse ls+                        | i <- [0..]])++++-- Construction ---------------------------------------------------------------+-- | An empty context.+emptyContext :: Context n+emptyContext +        = Context+        { contextEnvX           = EnvX.empty+        , contextGenPos         = 0+        , contextGenExists      = 0 +        , contextElems          = []+        , contextSolved         = IntMap.empty }+++-- | Wrap an EnvT into a Context.+contextOfEnvT :: EnvT n -> Context n+contextOfEnvT envt+ = let  envx    = EnvX.empty+                { EnvX.envxEnvT = envt }+   in   contextOfEnvX envx+++-- | Wrap an `EnvX` into a context.+contextOfEnvX :: EnvX n -> Context n+contextOfEnvX envx+        = emptyContext { contextEnvX = envx }+++-- | Build a context from prim environments.+contextOfPrimEnvs+        :: Ord n+        => Env.KindEnv n+        -> Env.TypeEnv n+        -> DataDefs n+        -> Context n++contextOfPrimEnvs kenv tenv defs+        = emptyContext +        { contextEnvX = EnvX.fromPrimEnvs kenv tenv defs }+++-- Projection -----------------------------------------------------------------+-- | Take the type equations from a context.+contextEquations :: Context n -> Map n (Type n)+contextEquations ctx+ = EnvT.envtEquations   $ contextEnvT ctx+++-- | Take the capabilities from a context.+contextCapabilities :: Context n -> Map n (Type n)+contextCapabilities ctx+ = EnvT.envtCapabilities $ contextEnvT ctx+++-- | Take the capabilities from a context.+contextDataDefs :: Context n -> DataDefs n+contextDataDefs ctx+ = EnvX.envxDataDefs $ contextEnvX ctx+++-- | Take the top level environment for types from the context.+contextEnvT :: Context n -> EnvT n+contextEnvT ctx+ = EnvX.envxEnvT (contextEnvX ctx)+++-- Push -----------------------------------------------------------------------+-- | Push the type of some value variable onto the context.+pushType  :: Bind n -> Context n -> Context n+pushType b ctx+ = ctx { contextElems = ElemType b : contextElems ctx }+++-- | Push many types onto the context.+pushTypes :: [Bind n] -> Context n -> Context n+pushTypes bs ctx+ = foldl (flip pushType) ctx bs+++-- | Push the kind of some type variable onto the context.+pushKind :: Bind n -> Role -> Context n -> Context n+pushKind b role ctx+ = ctx { contextElems = ElemKind b role : contextElems ctx }+++-- | Push many kinds onto the context.+pushKinds :: [(Bind n, Role)] -> Context n -> Context n+pushKinds brs ctx+ = foldl (\ctx' (b, r) -> pushKind b r ctx') ctx brs+++-- | Push an existential declaration onto the context.+--   If this is not an existential then `error`.+pushExists :: Exists n -> Context n -> Context n+pushExists i ctx+ = ctx { contextElems = ElemExistsDecl i : contextElems ctx }+++-- | Push the first existential into the context just before the+--   declaration of the second one.+pushExistsBefore :: Exists n -> Exists n -> Context n -> Context n+pushExistsBefore i (Exists n _) ctx+ = ctx { contextElems = go (contextElems ctx) }+ where+        go (ElemExistsDecl i'@(Exists n' _)   : es)+         | n' == n      = ElemExistsDecl i'   : ElemExistsDecl i : es++        go (ElemExistsEq   i'@(Exists n' _) t : es)+         | n' == n      = ElemExistsEq   i' t : ElemExistsDecl i : es++        go (e : es)     = e : go es+        go []           = []+++pushExistsScope :: Exists n -> [Exists n] -> Context n -> Context n+pushExistsScope i scope ctx+ = ctx { contextElems +                = go    (ElemExistsDecl i : contextElems ctx) +                        []+                        (contextElems ctx) +       }+ where  +        go cs' acc (e : es)+         | Just i' <- takeExistsOfElem e+         , elem i' scope        +         = go (reverse acc ++ (e : ElemExistsDecl i : es)) (e : acc) es++         | otherwise+         = go cs' (e : acc) es++        go cs' _acc []+         = cs'+++-- Mark / Pop -----------------------------------------------------------------+-- | Mark the context with a new position.+markContext :: Context n -> (Context n, Pos)+markContext ctx+ = let  p       = contextGenPos ctx+        pos     = Pos p+   in   ( ctx   { contextGenPos = p + 1+                , contextElems  = ElemPos pos : contextElems ctx }+        , pos )+++-- | Pop elements from a context to get back to the given position.+popToPos :: Pos -> Context n -> Context n+popToPos pos ctx+ = ctx { contextElems = go $ contextElems ctx }+ where+        go []                  = []++        go (ElemPos pos' : ls)+         | pos' == pos          = ls+         | otherwise            = go ls++        go (_ : ls)             = go ls+++-- Lookup ---------------------------------------------------------------------+-- | Given a bound level-0 (value) variable, lookup its type (level-1) +--   from the context.+lookupType :: Eq n => Bound n -> Context n -> Maybe (Type n)+lookupType u ctx+ = case u of+        UPrim{}         -> Nothing+        UName n         -> goName n    (contextElems ctx)+        UIx   ix        -> goIx   ix 0 (contextElems ctx)+ where+        goName _n []    = Nothing+        goName n  (ElemType (BName n' t) : ls)+         | n == n'      = Just t+         | otherwise    = goName n ls+        goName  n (_ : ls)+         = goName n ls+++        goIx _ix _d []  = Nothing+        goIx ix d  (ElemType (BAnon t) : ls)+         | ix == d      = Just t+         | otherwise    = goIx   ix (d + 1) ls+        goIx ix d  (_ : ls)+         = goIx ix d ls+++-- | Given a bound level-1 (type) variable, lookup its kind (level-2) from+--   the context.+lookupKind :: Eq n => Bound n -> Context n -> Maybe (Kind n, Role)+lookupKind u ctx+ = case u of+        UPrim{}         -> Nothing+        UName n         -> goName n    (contextElems ctx)+        UIx   ix        -> goIx   ix 0 (contextElems ctx)+ where+        goName _n []    = Nothing+        goName n  (ElemKind (BName n' t) role : ls)+         | n == n'      = Just (t, role)+         | otherwise    = goName n ls+        goName  n (_ : ls)+         = goName n ls+++        goIx _ix _d []  = Nothing+        goIx ix d  (ElemKind (BAnon t) role : ls)+         | ix == d      = Just (t, role)+         | otherwise    = goIx   ix (d + 1) ls+        goIx ix d  (_ : ls)+         = goIx ix d ls+++-- | Lookup the type bound to an existential, if any.+lookupExistsEq :: Exists n -> Context n -> Maybe (Type n)+lookupExistsEq i ctx+ = go (contextElems ctx)+ where  go []                           = Nothing+        go (ElemExistsEq i' t : _)+         | i == i'                      = Just t+        go (_ : ls)                     = go ls+++-- Member ---------------------------------------------------------------------+-- | See if this type variable is in the context.+memberType :: Eq n => Bound n -> Context n -> Bool+memberType u ctx = isJust $ lookupType u ctx+++-- | See if this kind variable is in the context.+memberKind :: Eq n => Bound n -> Context n -> Bool+memberKind u ctx = isJust $ lookupKind u ctx+++-- | See if the name on a named binder is in the contexts.+--   Returns False for non-named binders.+memberKindBind :: Eq n => Bind n -> Context n -> Bool+memberKindBind b ctx+ = case b of+        BName n _       -> memberKind (UName n) ctx+        _               -> False+++-- Existentials----------------------------------------------------------------+-- | Get the numeric location of an existential in the context stack,+--   or Nothing if it's not there. Returned value is relative to the TOP+--   of the stack, so the top element has location 0.+locationOfExists +        :: Exists n+        -> Context n+        -> Maybe Int++locationOfExists x ctx+ = go 0 (contextElems ctx)+ where  go !_ix []      = Nothing+        +        go !ix (ElemExistsDecl x'   : moar)+         | x == x'      = Just ix+         | otherwise    = go (ix + 1) moar++        go !ix (ElemExistsEq   x' _ : moar)+         | x == x'      = Just ix+         | otherwise    = go (ix + 1) moar++        go !ix  (_ : moar)+         = go (ix + 1) moar+++-- | Update (solve) an existential in the context stack.+--+--   If the existential is not part of the context then `Nothing`.+updateExists +        :: [Exists n]   -- ^ Other existential declarations to  add before the+                        --   updated one.+        -> Exists n     -- ^ Existential to update.+        -> Type n       -- ^ New monotype.+        -> Context n +        -> Maybe (Context n)++updateExists isMore iEx@(Exists iEx' _) tEx ctx+ = case go $ contextElems ctx of+    Just elems'     +     -> Just $ ctx { contextElems  = elems'+                   , contextSolved = IntMap.insert iEx' tEx (contextSolved ctx) }+    Nothing -> Nothing+ where+        go ll+         = case ll of+                l@ElemPos{}     : ls+                 | Just ls'     <- go ls  -> Just (l : ls')++                l@ElemKind{}    : ls   +                 | Just ls'     <- go ls  -> Just (l : ls')++                l@ElemType{}    : ls+                 | Just ls'     <- go ls  -> Just (l : ls')++                l@(ElemExistsDecl i) : ls+                 | i == iEx             +                 -> let es  =  ElemExistsEq i tEx +                            : [ElemExistsDecl n' | n' <- isMore]+                    in  Just $ es ++ ls++                 | Just ls'     <- go ls  -> Just (l : ls')++                l@ElemExistsEq{} : ls+                 | Just ls'     <- go ls  -> Just (l : ls')++                _ -> Just ll  -- Nothing+++-- Lifting --------------------------------------------------------------------+-- | Lift free debruijn indices in types by the given number of levels.+liftTypes :: Ord n => Int -> Context n -> Context n+liftTypes n ctx+ = ctx { contextElems = go $ contextElems ctx }+ where+        go []                   = []+        go (ElemType b : ls)    = ElemType (liftT n b) : go ls+        go (l:ls)               = l : go ls+++-- Lowering --------------------------------------------------------------------+-- | Lower free debruijn indices in types by the given number of levels.+lowerTypes :: Ord n => Int -> Context n -> Context n+lowerTypes n ctx+ = ctx { contextElems = go $ contextElems ctx }+ where+        go []                   = []+        go (ElemType b : ls)    = ElemType (lowerT n b) : go ls+        go (l:ls)               = l : go ls

@@ -0,0 +1,69 @@++module DDC.Core.Check.Context.Effect+        (effectSupported)+where+import DDC.Core.Check.Context.Base+import DDC.Core.Check.Context.Elem+import DDC.Type.Exp.Simple+import Data.Maybe+import qualified DDC.Core.Env.EnvT      as EnvT+import qualified DDC.Type.Sum           as Sum+import qualified Data.Map.Strict        as Map+++-- | Check whether this effect is supported by the given context.+--   This is used when effects are treated as capabilities.+--+--   The overall function can be passed a compound effect, +--    it returns `Nothing` if the effect is supported, +--    or `Just e`, where `e` is some unsuported atomic effect.+--+effectSupported +        :: (Ord n, Show n)+        => Context n +        -> Effect n +        -> Maybe (Effect n)++effectSupported ctx eff +        -- Check that all the components of a sum are supported.+        | TSum ts       <- eff+        = listToMaybe $ concat [ maybeToList $ effectSupported ctx e+                               | e <- Sum.toList ts ]++        -- Abstract effects are fine.+        --  We'll find out if it is really supported once it's instantiated.+        | TVar {} <- eff+        = Nothing++        -- Abstract global effects are always supported.+        | TCon (TyConBound _ k) <- eff+        , k == kEffect+        = Nothing++        -- For an effects on concrete region,+        -- the capability is supported if it's in the lexical environment.+        | TApp (TCon (TyConSpec tc)) _t2 <- eff+        , elem tc [TcConRead, TcConWrite, TcConAlloc]++        ,   -- Capability in local environment. +            (any  (\b -> equivT (contextEnvT ctx) (typeOfBind b) eff) +                  [ b | ElemType b <- contextElems ctx ] )+   +            -- Capability imported at top level.+         || (any  (\t -> equivT (contextEnvT ctx) t eff)+                  (Map.elems $ EnvT.envtCapabilities $ contextEnvT ctx))+        = Nothing++        -- For an effect on an abstract region, we allow any capability.+        --  We'll find out if it really has this capability when we try+        --  to run the computation.+        | TApp (TCon (TyConSpec tc)) (TVar u) <- eff+        , elem tc [TcConRead, TcConWrite, TcConAlloc]+        = case lookupKind u ctx of+                Just (_, RoleConcrete)  -> Just eff+                Just (_, RoleAbstract)  -> Nothing+                Nothing                 -> Nothing++        | otherwise+        = Just eff+

@@ -0,0 +1,158 @@++module DDC.Core.Check.Context.Elem+        ( -- * Positions in the context.+          Pos    (..)++          -- * Roles of type variables.+        , Role   (..)++          -- * Existentials.+        , Exists (..)+        , typeOfExists+        , takeExists+        , slurpExists++          -- * Context elements.+        , Elem   (..)+        , takeExistsOfElem)+where+import DDC.Type.Exp.Simple+import DDC.Data.Pretty+import qualified DDC.Type.Sum   as Sum+++-- Positions --------------------------------------------------------------------------------------+-- | A position in the type checker context.+--   A position is used to record a particular position in the context stack,+--   so that we can pop elements higher than it.+data Pos+        = Pos !Int+        deriving (Show, Eq)++instance Pretty Pos where+ ppr (Pos p)+        = text "*" <> int p+++-- Role -------------------------------------------------------------------------------------------+-- | The role of some type variable.+data Role+        -- | Concrete type variables are region variables that have been introduced+        --   in an enclosing lexical scope. All the capabilities for these will +        --   also be in the context.+        = RoleConcrete+        +        -- | Abstract type variables are the ones that are bound by type abstraction+        --   Inside the body of a type abstraction we can assume a region supports+        --   any given capability. We only need to worry about if it really does+        --   when we actually run the enclosed computation.+        | RoleAbstract+        deriving (Show, Eq)+++instance Pretty Role where+ ppr role+  = case role of+        RoleConcrete    -> text "Concrete"+        RoleAbstract    -> text "Abstract"+++-- Exists -----------------------------------------------------------------------------------------+-- | An existential variable.+data Exists n+        = Exists !Int !(Kind n)+        deriving (Show)++instance Eq (Exists n) where+ (==)   (Exists i1 _) (Exists i2 _)     = i1 == i2+ (/=)   (Exists i1 _) (Exists i2 _)     = i1 /= i2+++instance Ord (Exists n) where+ compare (Exists i1 _) (Exists i2 _)+        = compare i1 i2+++instance Pretty (Exists n) where+ ppr (Exists i _) = text "?" <> ppr i+++-- | Wrap an existential variable into a type.+typeOfExists :: Exists n -> Type n+typeOfExists (Exists n k)+        = TCon (TyConExists n k)+++-- | Take an Exists from a type.+takeExists :: Type n -> Maybe (Exists n)+takeExists tt+ = case tt of+        TCon (TyConExists n k)  -> Just (Exists n k)+        _                       -> Nothing+++-- | Slurp all the existential variables from this type.+slurpExists :: Type n -> [Exists n]+slurpExists tt+ = case tt of+        TCon (TyConExists n k)  -> [Exists n k]+        TCon _                  -> []+        TVar {}                 -> []+        TAbs b xBody            -> slurpExists (typeOfBind b) ++ slurpExists xBody+        TApp t1 t2              -> slurpExists t1 ++ slurpExists t2+        TForall b xBody         -> slurpExists (typeOfBind b) ++ slurpExists xBody+        TSum ts                 -> concatMap slurpExists $ Sum.toList ts++++-- Elem -------------------------------------------------------------------------------------------+-- | An element in the type checker context.+data Elem n+        -- | A context position marker.+        = ElemPos        !Pos++        -- | Kind of some variable.+        | ElemKind       !(Bind n) !Role++        -- | Type of some variable.+        | ElemType       !(Bind n)++        -- | Existential variable declaration+        | ElemExistsDecl !(Exists n)++        -- | Existential variable solved to some monotype.+        | ElemExistsEq   !(Exists n) !(Type n)+        deriving (Show, Eq)+++instance (Pretty n, Eq n) => Pretty (Elem n) where+ ppr ll+  = case ll of+        ElemPos p+         -> ppr p++        ElemKind b role  +         -> (padL 4 $ ppr (binderOfBind b))+                <+> text ":" +                <+> (ppr $ typeOfBind b)+                <+> text "@" <> ppr role++        ElemType b+         -> (padL 4 $ ppr (binderOfBind b))+                <+> text ":"+                <+> (ppr $ typeOfBind b)++        ElemExistsDecl (Exists i k)+         -> padL 4 (text "?" <> ppr i) <+> text ":" <+> ppr k++        ElemExistsEq (Exists i k) t +         -> padL 4 (text "?" <> ppr i) <+> text ":" <+> ppr k <+> text "=" <+> ppr t+++-- | Take the existential from this context element, if there is one.+takeExistsOfElem :: Elem n -> Maybe (Exists n)+takeExistsOfElem ee+ = case ee of+        ElemExistsDecl i        -> Just i+        ElemExistsEq   i _      -> Just i+        _                       -> Nothing

@@ -0,0 +1,42 @@++module DDC.Core.Check.Context.Mode+        (Mode (..))+where+import DDC.Core.Check.Context.Elem+import DDC.Type.Exp.Simple+import DDC.Data.Pretty+++-- | What mode we're performing type checking/inference in.+data Mode n+        -- | Reconstruct the type of the expression, requiring type annotations+        --   on parameters  as well as type applications to already be present.+        = Recon+        +        -- | The ascending smoke of incense.+        --+        --   Synthesise the type of the expression, producing unification+        --   variables for bidirectional type inference.+        --+        --   Any new unification variables introduced may be used to define the+        --   given existentials, so the need to be declared outside their scopes.+        --   If the list is empty we can add new variables to the inner most scope.+        -- +        | Synth [Exists n]++        -- | The descending tongue of flame.+        --   Check the type of an expression against this expected type, and+        --   unify expected types into unification variables for bidirecional+        --   type inference.+        | Check (Type n)+        deriving (Show, Eq)+++instance (Eq n, Pretty n) => Pretty (Mode n) where+ ppr mode+  = case mode of+        Recon    -> text "RECON"+        Synth is -> text "SYNTH" <+> ppr is+        Check t  -> text "CHECK" <+> parens (ppr t)++

@@ -1,380 +1,17 @@ -- | Errors produced when checking core expressions. module DDC.Core.Check.Error-        (Error(..))+        ( Error         (..)+        , ErrorType     (..)+        , ErrorData     (..)) where-import DDC.Core.Exp-import DDC.Type.Universe-import qualified DDC.Type.Check as T----- | All the things that can go wrong when type checking an expression---   or witness.-data Error a n-        -- Type --------------------------------------------        -- | Found a kind error when checking a type.-        = ErrorType-        { errorTypeError        :: T.Error n }--        -- | Found an error in the data type definitions.-        | ErrorData-        { errorData             :: T.ErrorData n }--        -- Module ------------------------------------------        -- | Exported value is undefined.-        | ErrorExportUndefined-        { errorName             :: n }--        -- | Exported name is exported multiple times.-        | ErrorExportDuplicate-        { errorName             :: n }--        -- | Type signature of exported binding does not match the type at-        --   the definition site.-        | ErrorExportMismatch-        { errorName             :: n-        , errorExportType       :: Type n-        , errorDefType          :: Type n }--        -- | Imported name is imported multiple times.-        | ErrorImportDuplicate-        { errorName             :: n }--        -- | An imported capability that does not have kind Effect.-        | ErrorImportCapNotEffect-        { errorName             :: n }--        -- | An imported value that doesn't have kind Data.-        | ErrorImportValueNotData-        { errorName             :: n }---        -- Exp ---------------------------------------------        -- | Generic mismatch between expected and inferred types.-        | ErrorMismatch-        { errorAnnot            :: a-        , errorInferred         :: Type n-        , errorExpected         :: Type n-        , errorChecking         :: Exp a n }---        -- Var ---------------------------------------------        -- | An undefined type variable.-        | ErrorUndefinedVar-        { errorAnnot            :: a-        , errorBound            :: Bound n-        , errorUniverse         :: Universe }---        -- Con ---------------------------------------------        -- | A data constructor that wasn't in the set of data definitions.-        | ErrorUndefinedCtor-        { errorAnnot            :: a-        , errorChecking         :: Exp a n }---        -- Application -------------------------------------        -- | A function application where the parameter and argument don't match.-        | ErrorAppMismatch-        { errrorAnnot           :: a-        , errorChecking         :: Exp a n-        , errorParamType        :: Type n-        , errorArgType          :: Type n }--        -- | Tried to apply something that is not a function.-        | ErrorAppNotFun-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorNotFunType       :: Type n }--        -- | Cannot infer type of polymorphic expression.-        | ErrorAppCannotInferPolymorphic-        { errorAnnot            :: a-        , errorChecking         :: Exp a n }--        -- Lambda ------------------------------------------        -- | A type abstraction that tries to shadow a type variable that is-        --   already in the environment.-        | ErrorLamShadow-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBind             :: Bind n }--        -- | An abstraction where the body has a visible side effect that-        --   is not supported by the current language fragment.-        | ErrorLamNotPure-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorUniverse         :: Universe-        , errorEffect           :: Effect n }--        -- | A value function where the parameter does not have data-        --   or witness kind.-        | ErrorLamBindBadKind-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorType             :: Type n-        , errorKind             :: Kind n }--        -- | An abstraction where the body does not have data kind.-        | ErrorLamBodyNotData-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBind             :: Bind n-        , errorType             :: Type n-        , errorKind             :: Kind n }--        -- | A function abstraction without a type annotation on the parameter.-        | ErrorLamParamUnannotated-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBind             :: Bind n }--        -- | A type abstraction without a kind annotation on the parameter.-        | ErrorLAMParamUnannotated-        { errorAnnot            :: a-        , errorChecking         :: Exp a n }--        -- | A type abstraction parameter with a bad sort.-        | ErrorLAMParamBadSort-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBind             :: Bind n-        , errorSort             :: Sort n }---        -- Let ---------------------------------------------        -- | A let-expression where the type of the binder does not match the right-        --   of the binding.-        | ErrorLetMismatch-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBind             :: Bind n-        , errorType             :: Type n }--        -- | A let-expression where the right of the binding does not have data kind.-        | ErrorLetBindingNotData-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBind             :: Bind n-        , errorKind             :: Kind n }--        -- | A let-expression where the body does not have data kind.-        | ErrorLetBodyNotData-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorType             :: Type n-        , errorKind             :: Kind n }---        -- Letrec ------------------------------------------        -- | A recursive let-expression where the right of the binding is not-        --   a lambda abstraction.-        | ErrorLetrecBindingNotLambda-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorExp              :: Exp a n }--        -- | A recursive let-binding with a missing type annotation.-        | ErrorLetrecMissingAnnot-        { errorAnnot            :: a-        , errorBind             :: Bind n-        , errorExp              :: Exp a n }--        -- | A recursive let-expression that has more than one binding-        --   with the same name.-        | ErrorLetrecRebound-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBind             :: Bind n }---        -- Letregion ---------------------------------------        -- | A letregion-expression where the some of the bound variables do not-        --   have region kind.-        | ErrorLetRegionsNotRegion-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBinds            :: [Bind n]-        , errorKinds            :: [Kind n] }--        -- | A letregion-expression that tried to shadow some pre-existing named-        --   region variables.-        | ErrorLetRegionsRebound-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBinds            :: [Bind n] }--        -- | A letregion-expression where some of the the bound region variables-        --   are free in the type of the body.-        | ErrorLetRegionFree-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBinds            :: [Bind n]-        , errorType             :: Type n }--        -- | A letregion-expression that tried to create a witness with an-        --   invalid type.-        | ErrorLetRegionWitnessInvalid-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBind             :: Bind n }--        -- | A letregion-expression that tried to create conflicting witnesses.-        | ErrorLetRegionWitnessConflict-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBindWitness1     :: Bind n-        , errorBindWitness2     :: Bind n }--        -- | A letregion-expression where a bound witnesses was not for the-        --   the region variable being introduced.-        | ErrorLetRegionsWitnessOther-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBoundRegions     :: [Bound n]-        , errorBindWitness      :: Bind  n }---        -- Witnesses ---------------------------------------        -- | A witness application where the argument type does not match-        --   the parameter type.-        | ErrorWAppMismatch-        { errorAnnot            :: a-        , errorWitness          :: Witness a n-        , errorParamType        :: Type n-        , errorArgType          :: Type n }--        -- | Tried to perform a witness application with a non-witness.-        | ErrorWAppNotCtor-        { errorAnnot            :: a-        , errorWitness          :: Witness a n-        , errorNotFunType       :: Type n-        , errorArgType          :: Type n }--        -- | A witness provided for a purify cast that does not witness purity.-        | ErrorWitnessNotPurity-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorWitness          :: Witness a n-        , errorType             :: Type n }---        -- Case Expressions --------------------------------        -- | A case-expression where the scrutinee type is not algebraic.-        | ErrorCaseScrutineeNotAlgebraic-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorTypeScrutinee    :: Type n }--        -- | A case-expression where the scrutinee type is not in our set-        --   of data type declarations.-        | ErrorCaseScrutineeTypeUndeclared-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorTypeScrutinee    :: Type n }--        -- | A case-expression with no alternatives.-        | ErrorCaseNoAlternatives-        { errorAnnot            :: a-        , errorChecking         :: Exp a n }--        -- | A case-expression where the alternatives don't cover all the-        --   possible data constructors.-        | ErrorCaseNonExhaustive-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorCtorNamesMissing :: [n] }--        -- | A case-expression where the alternatives don't cover all the-        --   possible constructors, and the type has too many data constructors-        --   to list.-        | ErrorCaseNonExhaustiveLarge-        { errorAnnot            :: a-        , errorChecking         :: Exp a n }--        -- | A case-expression with overlapping alternatives.-        | ErrorCaseOverlapping-        { errorAnnot            :: a-        , errorChecking         :: Exp a n }--        -- | A case-expression where one of the patterns has too many binders.-        | ErrorCaseTooManyBinders-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorCtorDaCon        :: DaCon n-        , errorCtorFields       :: Int-        , errorPatternFields    :: Int }--        -- | A case-expression where the pattern types could not be instantiated-        --   with the arguments of the scrutinee type.-        | ErrorCaseCannotInstantiate-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorTypeScrutinee    :: Type n-        , errorTypeCtor         :: Type n }--        -- | A case-expression where the type of the scrutinee does not match-        --   the type of the pattern.-        | ErrorCaseScrutineeTypeMismatch-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorTypeScrutinee    :: Type n-        , errorTypePattern      :: Type n }--        -- | A case-expression where the annotation on a pattern variable binder-        --   does not match the field type of the constructor.-        | ErrorCaseFieldTypeMismatch-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorTypeAnnot        :: Type n-        , errorTypeField        :: Type n }--        -- | A case-expression where the result types of the alternatives are not-        --   identical.-        | ErrorCaseAltResultMismatch-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorAltType1         :: Type n-        , errorAltType2         :: Type n }---        -- Casts -------------------------------------------        -- | A weakeff-cast where the type provided does not have effect kind.-        | ErrorWeakEffNotEff-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorEffect           :: Effect n-        , errorKind             :: Kind n }--        -- | A run cast applied to a non-suspension.-        | ErrorRunNotSuspension-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorType             :: Type n }--        -- | A run cast where the context does not support the suspended effect.-        | ErrorRunNotSupported-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorEffect           :: Effect n }+import DDC.Core.Check.Error.ErrorExp+import DDC.Core.Check.Error.ErrorExpMessage   () -        -- | A run cast where we cannot infer the type of the suspended computation-        --   and thus cannot check if its effects are suppored by the context.-        | ErrorRunCannotInfer-        { errorAnnot            :: a-        , errorExp              :: Exp a n }+import DDC.Core.Check.Error.ErrorType+import DDC.Core.Check.Error.ErrorTypeMessage  () -        -- Types -------------------------------------------        -- | Found a naked `XType` that wasn't the argument of an application.-        | ErrorNakedType-        { errorAnnot            :: a-        , errorChecking         :: Exp a n }+import DDC.Core.Check.Error.ErrorData+import DDC.Core.Check.Error.ErrorDataMessage  ()  -        -- Witnesses ---------------------------------------        -- | Found a naked `XWitness` that wasn't the argument of an application.-        | ErrorNakedWitness-        { errorAnnot            :: a-        , errorChecking         :: Exp a n }-        deriving (Show) 

@@ -0,0 +1,23 @@++module DDC.Core.Check.Error.ErrorData+        (ErrorData(..))+where+import DDC.Core.Exp+++-- | Things that can go wrong when checking data type definitions.+data ErrorData n+        -- | A duplicate data type constructor name.+        = ErrorDataDupTypeName +        { errorDataDupTypeName          :: n }++        -- | A duplicate data constructor name.+        | ErrorDataDupCtorName+        { errorDataCtorName             :: n }++        -- | A data constructor with the wrong result type.+        | ErrorDataWrongResult+        { errorDataCtorName             :: n+        , errorDataCtorResultActual     :: Type n+        , errorDataCtorResultExpected   :: Type n }+        deriving Show

@@ -0,0 +1,27 @@++module DDC.Core.Check.Error.ErrorDataMessage where+import DDC.Core.Check.Error.ErrorData+import DDC.Data.Pretty+++instance (Eq n, Show n, Pretty n) +       => Pretty (ErrorData n) where+ ppr = ppr'++ppr' (ErrorDataDupTypeName n)+ = vcat [ text "Duplicate data type definition."+        , text "  A constructor with name: "    <> ppr n+        , text "  is already defined." ]++ppr' (ErrorDataDupCtorName n)+ = vcat [ text "Duplicate data constructor definition."+        , text "  A constructor with name: "    <> ppr n+        , text "  is already defined." ]+++ppr' (ErrorDataWrongResult n tActual tExpected)+ = vcat [ text "Invalid result type for data constructor."+        , text "       The data constructor: "  <> ppr n+        , text "            has result type: "  <> ppr tActual+        , text "  but the enclosing type is: "  <> ppr tExpected ]+

@@ -0,0 +1,383 @@++module DDC.Core.Check.Error.ErrorExp+        (Error(..))+where+import DDC.Core.Check.Error.ErrorType+import DDC.Core.Check.Error.ErrorData+import DDC.Core.Exp+import DDC.Type.Universe++-- | All the things that can go wrong when type checking an expression+--   or witness.+data Error a n+        -- Type -------------------------------------------+        -- | Found a kind error when checking a type.+        = ErrorType+        { errorTypeError        :: ErrorType n }++        -- | Found an error in the data type definitions.+        | ErrorData+        { errorData             :: ErrorData n }++        -- Module -----------------------------------------+        -- | Exported value is undefined.+        | ErrorExportUndefined+        { errorName             :: n }++        -- | Exported name is exported multiple times.+        | ErrorExportDuplicate+        { errorName             :: n }++        -- | Type signature of exported binding does not match the type at+        --   the definition site.+        | ErrorExportMismatch+        { errorName             :: n+        , errorExportType       :: Type n+        , errorDefType          :: Type n }++        -- | Imported name is imported multiple times.+        | ErrorImportDuplicate+        { errorName             :: n }++        -- | An imported capability that does not have kind Effect.+        | ErrorImportCapNotEffect+        { errorName             :: n }++        -- | An imported value that doesn't have kind Data.+        | ErrorImportValueNotData+        { errorName             :: n }+++        -- Exp --------------------------------------------+        -- | Generic mismatch between expected and inferred types.+        | ErrorMismatch+        { errorAnnot            :: a+        , errorInferred         :: Type n+        , errorExpected         :: Type n+        , errorChecking         :: Exp a n }+++        -- Var --------------------------------------------+        -- | An undefined type variable.+        | ErrorUndefinedVar+        { errorAnnot            :: a+        , errorBound            :: Bound n+        , errorUniverse         :: Universe }+++        -- Con --------------------------------------------+        -- | A data constructor that wasn't in the set of data definitions.+        | ErrorUndefinedCtor+        { errorAnnot            :: a+        , errorChecking         :: Exp a n }+++        -- Application ------------------------------------+        -- | A function application where the parameter and argument don't match.+        | ErrorAppMismatch+        { errrorAnnot           :: a+        , errorChecking         :: Exp a n+        , errorParamType        :: Type n+        , errorArgType          :: Type n }++        -- | Tried to apply something that is not a function.+        | ErrorAppNotFun+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorNotFunType       :: Type n }++        -- | Cannot infer type of polymorphic expression.+        | ErrorAppCannotInferPolymorphic+        { errorAnnot            :: a+        , errorChecking         :: Exp a n }++        -- Lambda -----------------------------------------+        -- | A type abstraction that tries to shadow a type variable that is+        --   already in the environment.+        | ErrorLamShadow+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBind             :: Bind n }++        -- | An abstraction where the body has a visible side effect that+        --   is not supported by the current language fragment.+        | ErrorLamNotPure+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorUniverse         :: Universe+        , errorEffect           :: Effect n }++        -- | A value function where the parameter does not have data+        --   or witness kind.+        | ErrorLamBindBadKind+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorType             :: Type n+        , errorKind             :: Kind n }++        -- | An abstraction where the body does not have data kind.+        | ErrorLamBodyNotData+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBind             :: Bind n+        , errorType             :: Type n+        , errorKind             :: Kind n }++        -- | A function abstraction without a type annotation on the parameter.+        | ErrorLamParamUnannotated+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBind             :: Bind n }++        -- | A type abstraction without a kind annotation on the parameter.+        | ErrorLAMParamUnannotated+        { errorAnnot            :: a+        , errorChecking         :: Exp a n }++        -- | A type abstraction parameter with a bad sort.+        | ErrorLAMParamBadSort+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBind             :: Bind n+        , errorSort             :: Sort n }+++        -- Let --------------------------------------------+        -- | A let-expression where the type of the binder does not match the right+        --   of the binding.+        | ErrorLetMismatch+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBind             :: Bind n+        , errorType             :: Type n }++        -- | A let-expression where the right of the binding does not have data kind.+        | ErrorLetBindingNotData+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBind             :: Bind n+        , errorKind             :: Kind n }++        -- | A let-expression where the body does not have data kind.+        | ErrorLetBodyNotData+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorType             :: Type n+        , errorKind             :: Kind n }+++        -- Letrec -----------------------------------------+        -- | A recursive let-expression where the right of the binding is not+        --   a lambda abstraction.+        | ErrorLetrecBindingNotLambda+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorExp              :: Exp a n }++        -- | A recursive let-binding with a missing type annotation.+        | ErrorLetrecMissingAnnot+        { errorAnnot            :: a+        , errorBind             :: Bind n+        , errorExp              :: Exp a n }++        -- | A recursive let-expression that has more than one binding+        --   with the same name.+        | ErrorLetrecRebound+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBind             :: Bind n }+++        -- Letregion --------------------------------------+        -- | A letregion-expression where the some of the bound variables do not+        --   have region kind.+        | ErrorLetRegionsNotRegion+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBinds            :: [Bind n]+        , errorKinds            :: [Kind n] }++        -- | A letregion-expression that tried to shadow some pre-existing named+        --   region variables.+        | ErrorLetRegionsRebound+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBinds            :: [Bind n] }++        -- | A letregion-expression where some of the the bound region variables+        --   are free in the type of the body.+        | ErrorLetRegionFree+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBinds            :: [Bind n]+        , errorType             :: Type n }++        -- | A letregion-expression that tried to create a witness with an+        --   invalid type.+        | ErrorLetRegionWitnessInvalid+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBind             :: Bind n }++        -- | A letregion-expression that tried to create conflicting witnesses.+        | ErrorLetRegionWitnessConflict+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBindWitness1     :: Bind n+        , errorBindWitness2     :: Bind n }++        -- | A letregion-expression where a bound witnesses was not for the+        --   the region variable being introduced.+        | ErrorLetRegionsWitnessOther+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorBoundRegions     :: [Bound n]+        , errorBindWitness      :: Bind  n }+++        -- Witnesses --------------------------------------+        -- | A witness application where the argument type does not match+        --   the parameter type.+        | ErrorWAppMismatch+        { errorAnnot            :: a+        , errorWitness          :: Witness a n+        , errorParamType        :: Type n+        , errorArgType          :: Type n }++        -- | Tried to perform a witness application with a non-witness.+        | ErrorWAppNotCtor+        { errorAnnot            :: a+        , errorWitness          :: Witness a n+        , errorNotFunType       :: Type n+        , errorArgType          :: Type n }++        -- | A witness provided for a purify cast that does not witness purity.+        | ErrorWitnessNotPurity+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorWitness          :: Witness a n+        , errorType             :: Type n }+++        -- Case Expressions -------------------------------+        -- | A case-expression where the scrutinee type is not algebraic.+        | ErrorCaseScrutineeNotAlgebraic+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorTypeScrutinee    :: Type n }++        -- | A case-expression where the scrutinee type is not in our set+        --   of data type declarations.+        | ErrorCaseScrutineeTypeUndeclared+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorTypeScrutinee    :: Type n }++        -- | A case-expression with no alternatives.+        | ErrorCaseNoAlternatives+        { errorAnnot            :: a+        , errorChecking         :: Exp a n }++        -- | A case-expression where the alternatives don't cover all the+        --   possible data constructors.+        | ErrorCaseNonExhaustive+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorCtorNamesMissing :: [n] }++        -- | A case-expression where the alternatives don't cover all the+        --   possible constructors, and the type has too many data constructors+        --   to list.+        | ErrorCaseNonExhaustiveLarge+        { errorAnnot            :: a+        , errorChecking         :: Exp a n }++        -- | A case-expression with overlapping alternatives.+        | ErrorCaseOverlapping+        { errorAnnot            :: a+        , errorChecking         :: Exp a n }++        -- | A case-expression where one of the patterns has too many binders.+        | ErrorCaseTooManyBinders+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorCtorDaCon        :: DaCon n (Type n)+        , errorCtorFields       :: Int+        , errorPatternFields    :: Int }++        -- | A case-expression where the pattern types could not be instantiated+        --   with the arguments of the scrutinee type.+        | ErrorCaseCannotInstantiate+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorTypeScrutinee    :: Type n+        , errorTypeCtor         :: Type n }++        -- | A case-expression where the type of the scrutinee does not match+        --   the type of the pattern.+        | ErrorCaseScrutineeTypeMismatch+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorTypeScrutinee    :: Type n+        , errorTypePattern      :: Type n }++        -- | A case-expression where the annotation on a pattern variable binder+        --   does not match the field type of the constructor.+        | ErrorCaseFieldTypeMismatch+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorTypeAnnot        :: Type n+        , errorTypeField        :: Type n }++        -- | A case-expression where the result types of the alternatives are not+        --   identical.+        | ErrorCaseAltResultMismatch+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorAltType1         :: Type n+        , errorAltType2         :: Type n }+++        -- Casts ------------------------------------------+        -- | A weakeff-cast where the type provided does not have effect kind.+        | ErrorWeakEffNotEff+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorEffect           :: Effect n+        , errorKind             :: Kind n }++        -- | A run cast applied to a non-suspension.+        | ErrorRunNotSuspension+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorType             :: Type n }++        -- | A run cast where the context does not support the suspended effect.+        | ErrorRunNotSupported+        { errorAnnot            :: a+        , errorChecking         :: Exp a n+        , errorEffect           :: Effect n }++        -- | A run cast where we cannot infer the type of the suspended computation+        --   and thus cannot check if its effects are suppored by the context.+        | ErrorRunCannotInfer+        { errorAnnot            :: a+        , errorExp              :: Exp a n }++        -- Types ------------------------------------------+        -- | Found a naked `XType` that wasn't the argument of an application.+        | ErrorNakedType+        { errorAnnot            :: a+        , errorChecking         :: Exp a n }+++        -- Witnesses --------------------------------------+        -- | Found a naked `XWitness` that wasn't the argument of an application.+        | ErrorNakedWitness+        { errorAnnot            :: a+        , errorChecking         :: Exp a n }+        deriving (Show)++++

@@ -0,0 +1,431 @@++-- | Errors produced when checking core expressions.+module DDC.Core.Check.Error.ErrorExpMessage+        (Error(..))+where+import DDC.Core.Pretty+import DDC.Core.Check.Error.ErrorExp+import DDC.Core.Check.Error.ErrorTypeMessage      ()+import DDC.Core.Check.Error.ErrorDataMessage      ()+import DDC.Type.Exp.Simple+import DDC.Type.Universe+++instance (Pretty a, Show n, Eq n, Pretty n) +       => Pretty (Error a n) where+ ppr = ppr'+++-- Wrapped Errors -------------------------------------------------------------+ppr' (ErrorType err')+        = ppr err'++ppr' (ErrorData err')+        = ppr err'++-- Modules --------------------------------------------------------------------+ppr' (ErrorExportUndefined n)+ = vcat [ text "Exported name '" <> ppr n <> text "' is undefined." ]++ppr' (ErrorExportDuplicate n)+ = vcat [ text "Duplicate exported name '" <> ppr n <> text "'."]++ppr' (ErrorExportMismatch n tExport tDef)+ = vcat [ text "Type of exported name does not match type of definition."+        , text "             with binding: "   <> ppr n+        , text "           type of export: "   <> ppr tExport+        , text "       type of definition: "   <> ppr tDef ]++ppr' (ErrorImportDuplicate n)+ = vcat [ text "Duplicate imported name '" <> ppr n <> text "'."]++ppr' (ErrorImportCapNotEffect n)+ = vcat [ text "Imported capability '"+                <> ppr n +                <> text "' does not have kind Effect." ]++ppr' (ErrorImportValueNotData n)+ = vcat [ text "Imported value '"+                <> ppr n +                <> text "' does not have kind Data." ]+++-- Exp -------------------------------------------------------------------------+ppr' (ErrorMismatch a tInferred tExpected xx)+ = vcat [ ppr a+        , text "Type mismatch."+        , text "  inferred type: "                     <> ppr tInferred+        , text "  expected type: "                     <> ppr tExpected+        , empty+        , text "with: "                                <> align (ppr xx) ]+++-- Variable -------------------------------------------------------------------+ppr' (ErrorUndefinedVar a u universe)+ = case universe of+        UniverseSpec+          -> vcat  [ ppr a+                   , text "Undefined spec variable: "      <> ppr u ]++        UniverseData+          -> vcat  [ ppr a+                   , text "Undefined value variable: "     <> ppr u ]++        UniverseWitness+          -> vcat  [ ppr a+                   , text "Undefined witness variable: "   <> ppr u ]++        -- Universes other than the above don't have variables,+        -- but let's not worry about that here.+        _ -> vcat  [ ppr a+                   , text "Undefined variable: "           <> ppr u ]+++-- Constructor ----------------------------------------------------------------+ppr' (ErrorUndefinedCtor a xx)+ = vcat [ ppr a+        , text "Undefined data constructor: "  <> ppr xx ]+++-- Application ----------------------------------------------------------------+ppr' (ErrorAppMismatch a xx t1 t2)+ = vcat [ ppr a+        , text "Type mismatch in application."+        , text "     Function expects: "       <> ppr t1+        , text "      but argument is: "       <> ppr t2+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorAppNotFun a xx t1)+ = vcat [ ppr a+        , text "Cannot apply non-function"+        , text "              of type: "       <> ppr t1+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorAppCannotInferPolymorphic a xx)+ = vcat [ ppr a+        , text "Cannot infer the type of a polymorphic expression."+        , text "  Please supply type annotations to constrain the functional"+        , text "  part to have a quantified type."+        , text "with: "                        <> align (ppr xx) ]+++-- Lambda ---------------------------------------------------------------------+ppr' (ErrorLamShadow a xx b)+ = vcat [ ppr a+        , text "Cannot shadow named spec variable."+        , text "  binder: "                    <> ppr b+        , text "  is already in the environment."+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLamNotPure a xx universe eff)+ = vcat [ ppr a+        , text "Impure" <+> ppr universe <+> text "abstraction"+        , text "           has effect: "       <> ppr eff+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLamBindBadKind a xx t1 k1)+ = vcat [ ppr a+        , text "Function parameter has invalid kind."+        , text "    The function parameter: "   <> ppr t1+        , text "                  has kind: "  <> ppr k1+        , text "            but it must be: Data or Witness"+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLamBodyNotData a xx b1 t2 k2)+ = vcat [ ppr a+        , text "Result of function does not have data kind."+        , text "   In function with binder: "  <> ppr b1+        , text "       the result has type: "  <> ppr t2+        , text "                 with kind: "  <> ppr k2+        , text "            but it must be: Data"+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLamParamUnannotated a xx b1)+ = vcat [ ppr a+        , text "Missing type annotation on function parameter."+        , text "             With paramter: " <> ppr b1+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLAMParamUnannotated a xx)+ = vcat [ ppr a+        , text "Type abstraction is missing a kind annotation."+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLAMParamBadSort a xx b s)+ = vcat [ ppr a+        , text "Kind annotation of type parameter has a bad sort."+        , text "                  Parameter: " <> ppr b+        , text "                   has sort: " <> ppr s+        , empty+        , text "with: "                        <> align (ppr xx) ]+++-- Let ------------------------------------------------------------------------+ppr' (ErrorLetMismatch a xx b t)+ = vcat [ ppr a+        , text "Type mismatch in let-binding."+        , text "                The binder: "  <> ppr (binderOfBind b)+        , text "                  has type: "  <> ppr (typeOfBind b)+        , text "     but the body has type: "  <> ppr t+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLetBindingNotData a xx b k)+ = vcat [ ppr a+        , text "Let binding does not have data kind."+        , text "      The binding for: "       <> ppr (binderOfBind b)+        , text "             has type: "       <> ppr (typeOfBind b)+        , text "            with kind: "       <> ppr k+        , text "       but it must be: Data "+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLetBodyNotData a xx t k)+ = vcat [ ppr a+        , text "Let body does not have data kind."+        , text " Body of let has type: "       <> ppr t+        , text "            with kind: "       <> ppr k+        , text "       but it must be: Data "+        , empty+        , text "with: "                        <> align (ppr xx) ]+++-- Letrec ---------------------------------------------------------------------+ppr' (ErrorLetrecRebound a xx b)+ = vcat [ ppr a+        , text "Redefined binder '" <> ppr b <> text "' in letrec."+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLetrecMissingAnnot a b xx)+ = vcat [ ppr a+        , text "Missing or incomplete type annotation on recursive let-binding '"+               <> ppr (binderOfBind b) <> text "'."+        , text "Recursive functions must have full type annotations."+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLetrecBindingNotLambda a xx x)+ = vcat [ ppr a+        , text "Letrec can only bind lambda abstractions."+        , text "      This is not one: "       <> ppr x+        , empty+        , text "with: "                        <> align (ppr xx) ]+++-- Letregion ------------------------------------------------------------------+ppr' (ErrorLetRegionsNotRegion a xx bs ks)+ = vcat [ ppr a+        , text "Letregion binders do not have region kind."+        , text "        Region binders: "       <> (hcat $ map ppr bs)+        , text "             has kinds: "       <> (hcat $ map ppr ks)+        , text "       but they must all be: Region"+        , empty+        , text "with: "                         <> align (ppr xx) ]++ppr' (ErrorLetRegionsRebound a xx bs)+ = vcat [ ppr a+        , text "Region variables shadow existing ones."+        , text "           Region variables: "  <> (hcat $ map ppr bs)+        , text "     are already in environment"+        , empty+        , text "with: "                         <> align (ppr xx) ]++ppr' (ErrorLetRegionFree a xx bs t)+ = vcat [ ppr a+        , text "Region variables escape scope of private."+        , text "       The region variables: "  <> (hcat $ map ppr bs)+        , text "   is free in the body type: "   <> ppr t+        , empty+        , text "with: "                         <> align (ppr xx) ]++ppr' (ErrorLetRegionWitnessInvalid a xx b)+ = vcat [ ppr a+        , text "Invalid witness type with private."+        , text "          The witness: "       <> ppr b+        , text "  cannot be created with a private"+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLetRegionWitnessConflict a xx b1 b2)+ = vcat [ ppr a+        , text "Conflicting witness types with private."+        , text "      Witness binding: "       <> ppr b1+        , text "       conflicts with: "       <> ppr b2+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorLetRegionsWitnessOther a xx bs1 b2)+ = vcat [ ppr a+        , text "Witness type is not for bound regions."+        , text "        private binds: "       <> (hsep $ map ppr bs1)+        , text "  but witness type is: "       <> ppr b2+        , empty+        , text "with: "                        <> align (ppr xx) ]+++-- Witnesses ------------------------------------------------------------------+ppr' (ErrorWAppMismatch a ww t1 t2)+ = vcat [ ppr a+        , text "Type mismatch in witness application."+        , text "  Constructor expects: "       <> ppr t1+        , text "      but argument is: "       <> ppr t2+        , empty+        , text "with: "                        <> align (ppr ww) ]++ppr' (ErrorWAppNotCtor a ww t1 t2)+ = vcat [ ppr a+        , text "Type cannot apply non-constructor witness"+        , text "              of type: "       <> ppr t1+        , text "  to argument of type: "       <> ppr t2+        , empty+        , text "with: "                        <> align (ppr ww) ]++ppr' (ErrorWitnessNotPurity a xx w t)+ = vcat [ ppr a+        , text "Witness for a purify does not witness purity."+        , text "        Witness: "             <> ppr w+        , text "       has type: "             <> ppr t+        , empty+        , text "with: "                        <> align (ppr xx) ]+++-- Case Expressions -----------------------------------------------------------+ppr' (ErrorCaseScrutineeNotAlgebraic a xx tScrutinee)+ = vcat [ ppr a+        , text "Scrutinee of case expression is not algebraic data."+        , text "     Scrutinee type: "         <> ppr tScrutinee+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorCaseScrutineeTypeUndeclared a xx tScrutinee)+ = vcat [ ppr a+        , text "Type of scrutinee does not have a data declaration."+        , text "     Scrutinee type: "         <> ppr tScrutinee+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorCaseNoAlternatives a xx)+ = vcat [ ppr a+        , text "Case expression does not have any alternatives."+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorCaseNonExhaustive a xx ns)+ = vcat [ ppr a+        , text "Case alternatives are non-exhaustive."+        , text " Constructors not matched: "+               <> (sep $ punctuate comma $ map ppr ns)+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorCaseNonExhaustiveLarge a xx)+ = vcat [ ppr a+        , text "Case alternatives are non-exhaustive."+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorCaseOverlapping a xx)+ = vcat [ ppr a+        , text "Case alternatives are overlapping."+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorCaseTooManyBinders a xx uCtor iCtorFields iPatternFields)+ = vcat [ ppr a+        , text "Pattern has more binders than there are fields in the constructor."+        , text "     Contructor: " <> ppr uCtor+        , text "            has: " <> ppr iCtorFields+                                   <+> text "fields"+        , text "  but there are: " <> ppr iPatternFields+                                  <+> text "binders in the pattern"+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorCaseCannotInstantiate a xx tScrutinee tCtor)+ = vcat [ ppr a+        , text "Cannot instantiate constructor type with scrutinee type args."+        , text " Either the constructor has an invalid type,"+        , text " or the type of the scrutinee does not match the type of the pattern."+        , text "        Scrutinee type: "      <> ppr tScrutinee+        , text "      Constructor type: "      <> ppr tCtor+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorCaseScrutineeTypeMismatch a xx tScrutinee tPattern)+ = vcat [ ppr a+        , text "Scrutinee type does not match result of pattern type."+        , text "        Scrutinee type: "      <> ppr tScrutinee+        , text "          Pattern type: "      <> ppr tPattern+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorCaseFieldTypeMismatch a xx tAnnot tField)+ = vcat [ ppr a+        , text "Annotation on pattern variable does not match type of field."+        , text "       Annotation type: "      <> ppr tAnnot+        , text "            Field type: "      <> ppr tField+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorCaseAltResultMismatch a xx t1 t2)+ = vcat [ ppr a+        , text "Mismatch in alternative result types."+        , text "   Type of alternative: "      <> ppr t1+        , text "        does not match: "      <> ppr t2+        , empty+        , text "with: "                        <> align (ppr xx) ]+++-- Casts ----------------------------------------------------------------------+ppr' (ErrorWeakEffNotEff a xx eff k)+ = vcat [ ppr a+        , text "Type provided for a 'weakeff' does not have effect kind."+        , text "           Type: "             <> ppr eff+        , text "       has kind: "             <> ppr k+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorRunNotSuspension a xx t)+ = vcat [ ppr a+        , text "Expression to run is not a suspension."+        , text "          Type: "              <> ppr t+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorRunNotSupported a xx eff)+ = vcat [ ppr a+        , text "Effect of computation not supported by context."+        , text "    Effect:  "                 <> ppr eff+        , empty+        , text "with: "                        <> align (ppr xx) ]++ppr' (ErrorRunCannotInfer a xx)+ = vcat [ ppr a+        , text "Cannot infer type of suspended computation."+        , empty+        , text "with: "                        <> align (ppr xx) ]+++-- Type -----------------------------------------------------------------------+ppr' (ErrorNakedType a xx)+ = vcat [ ppr a+        , text "Found naked type in core program."+        , empty+        , text "with: "                        <> align (ppr xx) ]+++-- Witness --------------------------------------------------------------------+ppr' (ErrorNakedWitness a xx)+ = vcat [ ppr a+        , text "Found naked witness in core program."+        , empty+        , text "with: "                        <> align (ppr xx) ]+

@@ -0,0 +1,94 @@++module DDC.Core.Check.Error.ErrorType where+import DDC.Core.Exp+import DDC.Type.Universe+++-- | Things that can go wrong when checking the kind of at type.+data ErrorType n+        -- Generic Problems ---------------------+        -- | Tried to check a type using the wrong universe, +        --   for example: asking for the kind of a kind.+        = ErrorTypeUniverseMalfunction+        { errorTypeType         :: Type n+        , errorTypeUniverse     :: Universe }++        -- | Generic kind mismatch.+        | ErrorTypeMismatch+        { errorTypeUniverse     :: Universe+        , errorTypeInferred     :: Type n+        , errorTypeExpected     :: Type n+        , errorTypeChecking     :: Type n }++        -- | Cannot construct infinite type.+        | ErrorTypeInfinite+        { errorTypeVar          :: Type n+        , errorTypeBind         :: Type n }++        -- Variables ----------------------------+        -- | An undefined type variable.+        | ErrorTypeUndefined        +        { errorTypeBound        :: Bound n }+++        -- Constructors -------------------------+        -- | Found an unapplied kind function constructor.+        | ErrorTypeUnappliedKindFun ++        -- | Found a naked sort constructor.+        | ErrorTypeNakedSort+        { errorTypeSort         :: Sort n }++        -- | An undefined type constructor.+        | ErrorTypeUndefinedTypeCtor+        { errorTypeBound        :: Bound n }+++        -- Applications -------------------------+        -- | A type application where the thing being applied is not a function.+        | ErrorTypeAppNotFun+        { errorTypeChecking     :: Type n+        , errorTypeFunType      :: Type n+        , errorTypeFunTypeKind  :: Kind n+        , errorTypeArgType      :: Type n }++        -- | A type application where the parameter and argument kinds don't match.+        | ErrorTypeAppArgMismatch   +        { errorTypeChecking     :: Type n+        , errorTypeFunType      :: Type n+        , errorTypeFunKind      :: Kind n+        , errorTypeArgType      :: Type n+        , errorTypeArgKind      :: Kind n }++        -- | A witness implication where the premise or conclusion has an+        --   invalid kind.+        | ErrorTypeWitnessImplInvalid+        { errorTypeChecking     :: Type n+        , errorTypeLeftType     :: Type n+        , errorTypeLeftKind     :: Kind n+        , errorTypeRightType    :: Type n+        , errorTypeRightKind    :: Kind n }+++        -- Quantifiers --------------------------+        -- | A forall where the body does not have data or witness kind.+        | ErrorTypeForallKindInvalid+        { errorTypeChecking     :: Type n+        , errorTypeBody         :: Type n+        , errorTypeKind         :: Kind n }+++        -- Sums ---------------------------------+        -- | A type sum where the components have differing kinds.+        | ErrorTypeSumKindMismatch+        { errorTypeKindExpected :: Kind n+        , errorTypeTypeSum      :: TypeSum n+        , errorTypeKinds        :: [Kind n] }+        +        -- | A type sum that does not have effect or closure kind.+        | ErrorTypeSumKindInvalid+        { errorTypeCheckingSum  :: TypeSum n+        , errorTypeKind         :: Kind n }+        deriving Show++

@@ -0,0 +1,107 @@++-- | Errors produced when checking types.+module DDC.Core.Check.Error.ErrorTypeMessage where+import DDC.Core.Check.Error.ErrorType+import DDC.Type.Exp.Simple+import DDC.Type.Universe+import DDC.Data.Pretty+++instance (Eq n, Show n, Pretty n) +       => Pretty (ErrorType n) where+ ppr = ppr'+++-- Generic Problems -----------------------------------------------------------+ppr' (ErrorTypeUniverseMalfunction t u)+ = vcat [ text "Universe malfunction."+        , text "               Type: "  <> ppr t+        , text " is not in universe: "  <> ppr u ]++ppr' (ErrorTypeMismatch uni tInferred tExpected tt)+ = let (thing, thing')   +        = case uni of+               UniverseSpec    -> ("Kind", "kind")+               UniverseKind    -> ("Sort", "sort")+               _               -> ("Type", "type")+   in vcat +       [ text thing <+> text "mismatch."+       , text "                Expected"+               <+> text thing' <> text ":"      <+> ppr tExpected+       , text " does not match inferred"+               <+> text thing' <> text ":"      <+> ppr tInferred+       , empty+       , text "with: "                          <> align (ppr tt) ]++ppr' (ErrorTypeInfinite tExt tBind)+ = vcat [ text "Cannot construct infinite type."+        , text "  " <> ppr tExt <+> text "=" <+> ppr tBind ]+++-- Variables ------------------------------------------------------------------+ppr' (ErrorTypeUndefined u)+ = text "Undefined type variable: "     <> ppr u+++-- Constructors ---------------------------------------------------------------+ppr' (ErrorTypeUnappliedKindFun)+ = text "Can't take sort of unapplied kind function constructor."++ppr' (ErrorTypeNakedSort s)+ = text "Can't check a naked sort: "    <> ppr s+                +ppr' (ErrorTypeUndefinedTypeCtor u)+ = text "Undefined type constructor: "  <> ppr u+++-- Applications ---------------------------------------------------------------+ppr' (ErrorTypeAppNotFun tt t1 k1 t2)+ = vcat [ text "Type function used in application has invalid kind."+        , text "    In application: "           <> ppr tt+        , text " cannot apply type: "           <> ppr t1+        , text "           of kind: "           <> ppr k1+        , text "           to type: "           <> ppr t2 ]+ +ppr' (ErrorTypeAppArgMismatch tt tFn kFn tArg kArg)+ = vcat [ text "Kind mismatch in type application."+        , text "    In application: "           <> ppr tt+        , text " cannot apply type: "           <> ppr tFn+        , text "         with kind: "           <> ppr kFn+        , text "       to argument: "           <> ppr tArg+        , text "         with kind: "           <> ppr kArg ]         +++ppr' (ErrorTypeWitnessImplInvalid tt t1 k1 t2 k2)+ = vcat [ text "Invalid args for witness implication."+        , text "            left type: "        <> ppr t1+        , text "             has kind: "        <> ppr k1+        , text "           right type: "        <> ppr t2+        , text "             has kind: "        <> ppr k2 +        , text "        when checking: "        <> ppr tt ]+++-- Quantifiers ----------------------------------------------------------------+ppr' (ErrorTypeForallKindInvalid tt t k)+ = vcat [ text "Invalid kind for body of quantified type."+        , text "        the body type: "        <> ppr t+        , text "             has kind: "        <> ppr k+        , text "  but it must be Data or Prop" +        , text "        when checking: "        <> ppr tt ]+++-- Sums -----------------------------------------------------------------------+ppr' (ErrorTypeSumKindMismatch k ts ks)+ = vcat + $      [ text "Kind mismatch in type sum."+        , text " found multiple types: "        <> ppr ts+        , text " with differing kinds: "        <> ppr ks ]+ ++ (if k /= tBot sComp+                then [text "        expected kind: " <> ppr k ]+                else [])+                +ppr' (ErrorTypeSumKindInvalid ts k)+ = vcat [ text "Invalid kind for type sum."+        , text "         the type sum: "        <> ppr ts+        , text "             has kind: "        <> ppr k+        , text "  but it must be Effect or Closure" ]+

@@ -1,427 +0,0 @@--- | Errors produced when checking core expressions.-module DDC.Core.Check.ErrorMessage-        (Error(..))-where-import DDC.Core.Pretty-import DDC.Core.Check.Error-import DDC.Type.Compounds-import DDC.Type.Universe---instance (Pretty a, Show n, Eq n, Pretty n)-       => Pretty (Error a n) where- ppr err-  = case err of-        ErrorType err'-         -> ppr err'--        ErrorData err'-         -> ppr err'--        -- Modules ----------------------------------------        ErrorExportUndefined n-         -> vcat [ text "Exported name '" <> ppr n <> text "' is undefined." ]--        ErrorExportDuplicate n-         -> vcat [ text "Duplicate exported name '" <> ppr n <> text "'."]--        ErrorExportMismatch n tExport tDef-         -> vcat [ text "Type of exported name does not match type of definition."-                 , text "             with binding: "   <> ppr n-                 , text "           type of export: "   <> ppr tExport-                 , text "       type of definition: "   <> ppr tDef ]--        ErrorImportDuplicate n-         -> vcat [ text "Duplicate imported name '" <> ppr n <> text "'."]--        ErrorImportCapNotEffect n-         -> vcat [ text "Imported capability '"-                        <> ppr n -                        <> text "' does not have kind Effect." ]--        ErrorImportValueNotData n-         -> vcat [ text "Imported value '"-                        <> ppr n -                        <> text "' does not have kind Data." ]---        -- Exp ---------------------------------------------        ErrorMismatch a tInferred tExpected xx-         -> vcat [ ppr a-                 , text "Type mismatch."-                 , text "  inferred type: "                     <> ppr tInferred-                 , text "  expected type: "                     <> ppr tExpected-                 , empty-                 , text "with: "                                <> align (ppr xx) ]---        -- Variable ----------------------------------------        ErrorUndefinedVar a u universe-         -> case universe of-             UniverseSpec-               -> vcat  [ ppr a-                        , text "Undefined spec variable: "      <> ppr u ]--             UniverseData-               -> vcat  [ ppr a-                        , text "Undefined value variable: "     <> ppr u ]--             UniverseWitness-               -> vcat  [ ppr a-                        , text "Undefined witness variable: "   <> ppr u ]--             -- Universes other than the above don't have variables,-             -- but let's not worry about that here.-             _ -> vcat  [ ppr a-                        , text "Undefined variable: "           <> ppr u ]---        -- Constructor -------------------------------------        ErrorUndefinedCtor a xx-         -> vcat [ ppr a-                 , text "Undefined data constructor: "  <> ppr xx ]---        -- Application -------------------------------------        ErrorAppMismatch a xx t1 t2-         -> vcat [ ppr a-                 , text "Type mismatch in application."-                 , text "     Function expects: "       <> ppr t1-                 , text "      but argument is: "       <> ppr t2-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorAppNotFun a xx t1-         -> vcat [ ppr a-                 , text "Cannot apply non-function"-                 , text "              of type: "       <> ppr t1-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorAppCannotInferPolymorphic a xx-         -> vcat [ ppr a-                 , text "Cannot infer the type of a polymorphic expression."-                 , text "  Please supply type annotations to constrain the functional"-                 , text "  part to have a quantified type."-                 , text "with: "                        <> align (ppr xx) ]---        -- Lambda ------------------------------------------        ErrorLamShadow a xx b-         -> vcat [ ppr a-                 , text "Cannot shadow named spec variable."-                 , text "  binder: "                    <> ppr b-                 , text "  is already in the environment."-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLamNotPure a xx universe eff-         -> vcat-                [ ppr a-                , text "Impure" <+> ppr universe <+> text "abstraction"-                , text "           has effect: "       <> ppr eff-                , empty-                , text "with: "                        <> align (ppr xx) ]--        ErrorLamBindBadKind a xx t1 k1-         -> vcat [ ppr a-                 , text "Function parameter has invalid kind."-                 , text "    The function parameter: "   <> ppr t1-                 , text "                  has kind: "  <> ppr k1-                 , text "            but it must be: Data or Witness"-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLamBodyNotData a xx b1 t2 k2-         -> vcat [ ppr a-                 , text "Result of function does not have data kind."-                 , text "   In function with binder: "  <> ppr b1-                 , text "       the result has type: "  <> ppr t2-                 , text "                 with kind: "  <> ppr k2-                 , text "            but it must be: Data"-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLamParamUnannotated a xx b1-         -> vcat [ ppr a-                 , text "Missing type annotation on function parameter."-                 , text "             With paramter: " <> ppr b1-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLAMParamUnannotated a xx-         -> vcat [ ppr a-                 , text "Type abstraction is missing a kind annotation."-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLAMParamBadSort a xx b s-         -> vcat [ ppr a-                 , text "Kind annotation of type parameter has a bad sort."-                 , text "                  Parameter: " <> ppr b-                 , text "                   has sort: " <> ppr s-                 , empty-                 , text "with: "                        <> align (ppr xx) ]---        -- Let ---------------------------------------------        ErrorLetMismatch a xx b t-         -> vcat [ ppr a-                 , text "Type mismatch in let-binding."-                 , text "                The binder: "  <> ppr (binderOfBind b)-                 , text "                  has type: "  <> ppr (typeOfBind b)-                 , text "     but the body has type: "  <> ppr t-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLetBindingNotData a xx b k-         -> vcat [ ppr a-                 , text "Let binding does not have data kind."-                 , text "      The binding for: "       <> ppr (binderOfBind b)-                 , text "             has type: "       <> ppr (typeOfBind b)-                 , text "            with kind: "       <> ppr k-                 , text "       but it must be: Data "-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLetBodyNotData a xx t k-         -> vcat [ ppr a-                 , text "Let body does not have data kind."-                 , text " Body of let has type: "       <> ppr t-                 , text "            with kind: "       <> ppr k-                 , text "       but it must be: Data "-                 , empty-                 , text "with: "                        <> align (ppr xx) ]---        -- Letrec ------------------------------------------        ErrorLetrecRebound a xx b-         -> vcat [ ppr a-                 , text "Redefined binder '" <> ppr b <> text "' in letrec."-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLetrecMissingAnnot a b xx-         -> vcat [ ppr a-                 , text "Missing or incomplete type annotation on recursive let-binding '"-                        <> ppr (binderOfBind b) <> text "'."-                 , text "Recursive functions must have full type annotations."-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLetrecBindingNotLambda a xx x-         -> vcat [ ppr a-                 , text "Letrec can only bind lambda abstractions."-                 , text "      This is not one: "       <> ppr x-                 , empty-                 , text "with: "                        <> align (ppr xx) ]---        -- Letregion ---------------------------------------        ErrorLetRegionsNotRegion a xx bs ks-         -> vcat [ ppr a-                 , text "Letregion binders do not have region kind."-                 , text "        Region binders: "       <> (hcat $ map ppr bs)-                 , text "             has kinds: "       <> (hcat $ map ppr ks)-                 , text "       but they must all be: Region"-                 , empty-                 , text "with: "                         <> align (ppr xx) ]--        ErrorLetRegionsRebound a xx bs-         -> vcat [ ppr a-                 , text "Region variables shadow existing ones."-                 , text "           Region variables: "  <> (hcat $ map ppr bs)-                 , text "     are already in environment"-                 , empty-                 , text "with: "                         <> align (ppr xx) ]--        ErrorLetRegionFree a xx bs t-         -> vcat [ ppr a-                 , text "Region variables escape scope of private."-                 , text "       The region variables: "  <> (hcat $ map ppr bs)-                 , text "   is free in the body type: "   <> ppr t-                 , empty-                 , text "with: "                         <> align (ppr xx) ]--        ErrorLetRegionWitnessInvalid a xx b-         -> vcat [ ppr a-                 , text "Invalid witness type with private."-                 , text "          The witness: "       <> ppr b-                 , text "  cannot be created with a private"-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLetRegionWitnessConflict a xx b1 b2-         -> vcat [ ppr a-                 , text "Conflicting witness types with private."-                 , text "      Witness binding: "       <> ppr b1-                 , text "       conflicts with: "       <> ppr b2-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorLetRegionsWitnessOther a xx bs1 b2-         -> vcat [ ppr a-                 , text "Witness type is not for bound regions."-                 , text "        private binds: "       <> (hsep $ map ppr bs1)-                 , text "  but witness type is: "       <> ppr b2-                 , empty-                 , text "with: "                        <> align (ppr xx) ]---        -- Witnesses ---------------------------------------        ErrorWAppMismatch a ww t1 t2-         -> vcat [ ppr a-                 , text "Type mismatch in witness application."-                 , text "  Constructor expects: "       <> ppr t1-                 , text "      but argument is: "       <> ppr t2-                 , empty-                 , text "with: "                        <> align (ppr ww) ]--        ErrorWAppNotCtor a ww t1 t2-         -> vcat [ ppr a-                 , text "Type cannot apply non-constructor witness"-                 , text "              of type: "       <> ppr t1-                 , text "  to argument of type: "       <> ppr t2-                 , empty-                 , text "with: "                        <> align (ppr ww) ]--        ErrorWitnessNotPurity a xx w t-         -> vcat [ ppr a-                 , text "Witness for a purify does not witness purity."-                 , text "        Witness: "             <> ppr w-                 , text "       has type: "             <> ppr t-                 , empty-                 , text "with: "                        <> align (ppr xx) ]---        -- Case Expressions --------------------------------        ErrorCaseScrutineeNotAlgebraic a xx tScrutinee-         -> vcat [ ppr a-                 , text "Scrutinee of case expression is not algebraic data."-                 , text "     Scrutinee type: "         <> ppr tScrutinee-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorCaseScrutineeTypeUndeclared a xx tScrutinee-         -> vcat [ ppr a-                 , text "Type of scrutinee does not have a data declaration."-                 , text "     Scrutinee type: "         <> ppr tScrutinee-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorCaseNoAlternatives a xx-         -> vcat [ ppr a-                 , text "Case expression does not have any alternatives."-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorCaseNonExhaustive a xx ns-         -> vcat [ ppr a-                 , text "Case alternatives are non-exhaustive."-                 , text " Constructors not matched: "-                        <> (sep $ punctuate comma $ map ppr ns)-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorCaseNonExhaustiveLarge a xx-         -> vcat [ ppr a-                 , text "Case alternatives are non-exhaustive."-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorCaseOverlapping a xx-         -> vcat [ ppr a-                 , text "Case alternatives are overlapping."-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorCaseTooManyBinders a xx uCtor iCtorFields iPatternFields-         -> vcat [ ppr a-                 , text "Pattern has more binders than there are fields in the constructor."-                 , text "     Contructor: " <> ppr uCtor-                 , text "            has: " <> ppr iCtorFields-                                            <+> text "fields"-                 , text "  but there are: " <> ppr iPatternFields-                                           <+> text "binders in the pattern"-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorCaseCannotInstantiate a xx tScrutinee tCtor-         -> vcat [ ppr a-                 , text "Cannot instantiate constructor type with scrutinee type args."-                 , text " Either the constructor has an invalid type,"-                 , text " or the type of the scrutinee does not match the type of the pattern."-                 , text "        Scrutinee type: "      <> ppr tScrutinee-                 , text "      Constructor type: "      <> ppr tCtor-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorCaseScrutineeTypeMismatch a xx tScrutinee tPattern-         -> vcat [ ppr a-                 , text "Scrutinee type does not match result of pattern type."-                 , text "        Scrutinee type: "      <> ppr tScrutinee-                 , text "          Pattern type: "      <> ppr tPattern-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorCaseFieldTypeMismatch a xx tAnnot tField-         -> vcat [ ppr a-                 , text "Annotation on pattern variable does not match type of field."-                 , text "       Annotation type: "      <> ppr tAnnot-                 , text "            Field type: "      <> ppr tField-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorCaseAltResultMismatch a xx t1 t2-         -> vcat [ ppr a-                 , text "Mismatch in alternative result types."-                 , text "   Type of alternative: "      <> ppr t1-                 , text "        does not match: "      <> ppr t2-                 , empty-                 , text "with: "                        <> align (ppr xx) ]---        -- Casts -------------------------------------------        ErrorWeakEffNotEff a xx eff k-         -> vcat [ ppr a-                 , text "Type provided for a 'weakeff' does not have effect kind."-                 , text "           Type: "             <> ppr eff-                 , text "       has kind: "             <> ppr k-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorRunNotSuspension a xx t-         -> vcat [ ppr a-                 , text "Expression to run is not a suspension."-                 , text "          Type: "              <> ppr t-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorRunNotSupported a xx eff-         -> vcat [ ppr a-                 , text "Effect of computation not supported by context."-                 , text "    Effect:  "                 <> ppr eff-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--        ErrorRunCannotInfer a xx-         -> vcat [ ppr a-                 , text "Cannot infer type of suspended computation."-                 , empty-                 , text "with: "                        <> align (ppr xx) ]---        -- Type --------------------------------------------        ErrorNakedType a xx-         -> vcat [ ppr a-                 , text "Found naked type in core program."-                 , empty-                 , text "with: "                        <> align (ppr xx) ]---        -- Witness -----------------------------------------        ErrorNakedWitness a xx-         -> vcat [ ppr a-                 , text "Found naked witness in core program."-                 , empty-                 , text "with: "                        <> align (ppr xx) ]-

@@ -46,7 +46,6 @@ import DDC.Core.Check.Judge.Type.Witness import DDC.Core.Check.Judge.Type.Base import DDC.Core.Transform.MapT-import qualified DDC.Type.Env           as Env   -- Wrappers -------------------------------------------------------------------@@ -64,9 +63,8 @@ checkExp         :: (Show a, Ord n, Show n, Pretty n)         => Config n                     -- ^ Static configuration.-        -> KindEnv n                    -- ^ Starting kind environment.-        -> TypeEnv n                    -- ^ Starting type environment.-        -> Mode  n                      -- ^ Check mode.+        -> EnvX n                       -- ^ Environment of expression.+        -> Mode n                       -- ^ Check mode.         -> Demand                       -- ^ Demand placed on the expression.         -> Exp a n                      -- ^ Expression to check.         -> ( Either (Error a n)         --   Type error message.@@ -75,7 +73,7 @@                     , Effect n)         --   Effect of expression.            , CheckTrace)                --   Type checker debug trace. -checkExp !config !kenv !tenv !mode !demand !xx+checkExp !config !env !mode !demand !xx  = (result, ct)  where   ((ct, _, _), result)@@ -84,10 +82,11 @@         -- Check the expression, using the monadic checking function.         (xx', t, effs, ctx)          <- checkExpM-                (makeTable config-                        (Env.union kenv (configPrimKinds config))-                        (Env.union tenv (configPrimTypes config)))-                emptyContext mode demand xx +                (makeTable config)+                (emptyContext { contextEnvX = env })+                mode +                demand +                xx           -- Apply the final context to the annotations in expressions.         -- This ensures that existentials are expanded to solved types.@@ -110,14 +109,13 @@ -- | Like `checkExp`, but only return the value type of an expression. typeOfExp         :: (Show a, Ord n, Pretty n, Show n)-        => Config n                     -- ^ Static configuration.-        -> KindEnv n                    -- ^ Starting Kind environment-        -> TypeEnv n                    -- ^ Starting Type environment.-        -> Exp a n                      -- ^ Expression to check.+        => Config n             -- ^ Static configuration.+        -> EnvX n               -- ^ Environment of expresion.+        -> Exp a n              -- ^ Expression to check.         -> Either (Error a n) (Type n) -typeOfExp !config !kenv !tenv !xx- = case fst $ checkExp config kenv tenv Recon DemandNone xx of+typeOfExp !config !env !xx+ = case fst $ checkExp config env Recon DemandNone xx of         Left err        -> Left err         Right (_, t, _) -> Right t @@ -155,12 +153,10 @@   -- Table -----------------------------------------------------------------------makeTable :: Config n -> KindEnv n -> TypeEnv n -> Table a n-makeTable config kenv tenv+makeTable :: Config n -> Table a n+makeTable config         = Table         { tableConfig           = config-        , tableKindEnv          = kenv-        , tableTypeEnv          = tenv         , tableCheckExp         = checkExpM         , tableCheckVarCon      = checkVarCon         , tableCheckAppT        = checkAppT

@@ -0,0 +1,181 @@++module DDC.Core.Check.Judge.DataDefs+        (checkDataDefs)+where+import DDC.Core.Check.Config+import DDC.Core.Check.Error+import DDC.Type.DataDef+import DDC.Type.Exp.Simple+import DDC.Data.Pretty+import Data.Maybe+import DDC.Core.Env.EnvT                (EnvT)+import Data.Set                         (Set)+import qualified DDC.Type.Env           as Env+import qualified Data.Set               as Set+import qualified Data.Map               as Map+++-------------------------------------------------------------------------------+-- | Check some data type definitions.+checkDataDefs +        :: (Ord n, Show n, Pretty n)+        => Config n+        -> EnvT   n+        -> [DataDef n]+        -> ([ErrorData n], [DataDef n])++checkDataDefs config env defs + = let+        -- Primitive type constructors.+        primTypeCtors+                = Set.fromList+                $ Map.keys $ Env.envMap   $ configPrimKinds config++        -- Primitive data type constructors+        primDataTypeCtors  +                = Set.fromList +                $ Map.keys $ dataDefsTypes $ configPrimDataDefs config++        -- Primitive data constructors+        primDataCtors   +                = Set.fromList +                $ Map.keys $ dataDefsCtors $ configPrimDataDefs config++   in   checkDataDefs' env+                (Set.union primTypeCtors primDataTypeCtors)+                primDataCtors+                [] []+                defs+++checkDataDefs'+        :: (Ord n, Show n, Pretty n)+        => EnvT n               -- ^ Type equations.+        -> Set n                -- ^ Names of existing data types.+        -> Set n                -- ^ Names of existing data constructor.+        -> [ErrorData n]        -- ^ Errors found so far.+        -> [DataDef n]          -- ^ Checked data defs.+        -> [DataDef n]          -- ^ Data defs still to check.+        -> ([ErrorData n], [DataDef n])++checkDataDefs' env nsTypes nsCtors errs dsChecked ds+ -- We've checked all the defs.+ | []   <- ds+ = (reverse errs, reverse dsChecked)+ + -- Keep checking defs.+ | d : ds' <- ds+ = case checkDataDef env nsTypes nsCtors d of++    -- There are errors in this def.+    Left errs' +     -> checkDataDefs' env+                (Set.insert (dataDefTypeName d) nsTypes)+                (Set.fromList $ fromMaybe [] $ dataCtorNamesOfDataDef d)+                (errs ++ errs') dsChecked ds'++    -- This def is ok.+    Right d'   +     -> checkDataDefs' env+                (Set.insert (dataDefTypeName d') nsTypes)+                (Set.fromList $ fromMaybe [] $ dataCtorNamesOfDataDef d)+                errs (d' : dsChecked) ds'++ | otherwise+ = error "ddc-core.checkDataDefs: bogus warning suppression"+++-- DataDef --------------------------------------------------------------------+-- | Check a data type definition.+checkDataDef +        :: (Ord n, Show n, Pretty n)+        => EnvT n               -- ^ Environment of types.+        -> Set n                -- ^ Names of existing data types.+        -> Set n                -- ^ Names of existing data constructors.+        -> DataDef n            -- ^ Data type definition to check.+        -> Either [ErrorData n] (DataDef n)++checkDataDef env nsTypes nsCtors def+        + -- Check the data type name is not already defined.+ | Set.member (dataDefTypeName def) nsTypes+ = Left [ErrorDataDupTypeName (dataDefTypeName def)]++ -- No data constructors to check.+ | Nothing      <- dataDefCtors def+ = Right def++ -- Check the data constructors.+ | Just ctors   <- dataDefCtors def+ = case checkDataCtors env nsCtors [] def [] ctors of+        Left errs       -> Left errs+        Right ctors'    -> Right $ def { dataDefCtors = Just ctors' }++ | otherwise+ = error "ddc-core.checkDataDef: bogus warning suppression"++ +-- Ctors ----------------------------------------------------------------------+-- | Check the data constructor definitions from a single data type.+checkDataCtors+        :: (Ord n, Show n, Pretty n)+        => EnvT n               -- ^ Environment of types+        -> Set n                -- ^ Names of existing data constructors.+        -> [ErrorData n]        -- ^ Errors found so far.+        -> DataDef n            -- ^ The DataDef these constructors relate to.+        -> [DataCtor  n]        -- ^ Checked constructor defs.+        -> [DataCtor  n]        -- ^ Constructor defs still to check.+        -> Either [ErrorData n] [DataCtor n]++checkDataCtors env nsCtors errs def csChecked cs+ -- We've checked all the constructors and there were no errors.+ | []   <- cs, []   <- errs+ = Right (reverse csChecked)++ -- We've checked all the constructors and there were errors with some of them.+ | []   <- cs+ = Left  (reverse errs)++ -- Keep checking constructors.+ | c : cs' <- cs+ = case checkDataCtor env nsCtors def c of+        Left  err -> checkDataCtors env+                        (Set.insert (dataCtorName c) nsCtors)+                        (err : errs) def csChecked cs'+        +        Right c'  -> checkDataCtors env+                        (Set.insert (dataCtorName c') nsCtors)+                        errs         def (c' : csChecked) cs'++ | otherwise+ = error "ddc-core.checkDataCtors: bogus warning suppression"+++-- Ctor -----------------------------------------------------------------------+-- | Check a single data constructor definition.+checkDataCtor +        :: (Ord n, Show n, Pretty n)+        => EnvT n               -- ^ Environment of types.+        -> Set n                -- ^ Names of existing data constructors.+        -> DataDef  n           -- ^ Def of data type for this constructor.+        -> DataCtor n           -- ^ Data constructor to check.+        -> Either (ErrorData n) (DataCtor n)++checkDataCtor env nsCtors def ctor+        + -- Check the constructor name is not already defined.+ | Set.member (dataCtorName ctor) nsCtors + = Left $ ErrorDataDupCtorName (dataCtorName ctor)++ -- Check that the constructor produces a value of the associated data type.+ | not $ equivT env (dataTypeOfDataDef def) (dataCtorResultType ctor)+ = Left $ ErrorDataWrongResult +                (dataCtorName ctor)+                (dataCtorResultType ctor) (dataTypeOfDataDef def)++ -- This constructor looks ok.+ | otherwise+ = Right ctor+++

@@ -1,177 +0,0 @@--module DDC.Core.Check.Judge.Eq-        (makeEq)-where-import DDC.Core.Check.Base-import qualified DDC.Type.Sum   as Sum----- | Make two types equivalent to each other,---   or throw the provided error if this is not possible.-makeEq  :: (Eq n, Ord n, Pretty n, Show n)-        => Config n-        -> a-        -> Context n-        -> Type n-        -> Type n-        -> Error a n-        -> CheckM a n (Context n)--makeEq config a ctx0 tL tR err-- -- EqLSolve- | Just iL <- takeExists tL- , not $ isTExists tR- = do   let Just ctx1   = updateExists [] iL tR ctx0--        ctrace  $ vcat-                [ text "**  EqLSolve"-                , text "    LEFT:  " <> ppr tL-                , text "    RIGHT: " <> ppr tR-                , indent 4 $ ppr ctx0-                , indent 4 $ ppr ctx1-                , empty ]--        return ctx1--- -- EqRSolve- | Just iR <- takeExists tR- , not $ isTExists tL- = do   let Just ctx1   = updateExists [] iR tL ctx0--        ctrace  $ vcat-                [ text "**  EqRSolve"-                , text "    LEFT:  " <> ppr tL-                , text "    RIGHT: " <> ppr tR-                , indent 4 $ ppr ctx0-                , indent 4 $ ppr ctx1-                , empty ]--        return ctx1--- -- EqLReach- --  Both types are existentials, and the left is bound earlier in the stack.- --  CAREFUL: The returned location is relative to the top of the stack,- --           hence we need lL > lR here.- | Just iL <- takeExists tL,    Just lL <- locationOfExists iL ctx0- , Just iR <- takeExists tR,    Just lR <- locationOfExists iR ctx0- , lL > lR- = do   let Just ctx1   = updateExists [] iR tL ctx0--        ctrace  $ vcat-                [ text "**  EqLReach"-                , text "    LEFT:  " <> ppr tL-                , text "    RIGHT: " <> ppr tR-                , indent 4 $ ppr ctx0-                , indent 4 $ ppr ctx1-                , empty ]--        return ctx1-- -- EqRReach- --  Both types are existentials, and the right is bound earlier in the stack.- --  CAREFUL: The returned location is relative to the top of the stack,- --           hence we need lR > lL here.- | Just iL <- takeExists tL,    Just lL <- locationOfExists iL ctx0- , Just iR <- takeExists tR,    Just lR <- locationOfExists iR ctx0- , lR > lL- = do   let Just ctx1   = updateExists [] iL tR ctx0--        ctrace  $ vcat-                [ text "**  EqRReach"-                , text "    LEFT:  " <> ppr tL-                , text "    RIGHT: " <> ppr tR-                , indent 4 $ ppr ctx0-                , indent 4 $ ppr ctx1-                , empty ]--        return ctx1--- -- EqVar- | TVar u1      <- tL- , TVar u2      <- tR- , u1 == u2- = do-        ctrace  $ vcat-                [ text "**  EqVar"-                , text "    LEFT:  " <> ppr tL-                , text "    RIGHT: " <> ppr tR-                , indent 4 $ ppr ctx0-                , empty ]--        return ctx0--- -- EqCon- | TCon tc1     <- tL- , TCon tc2     <- tR- , equivTyCon tc1 tc2- = do-        ctrace  $ vcat-                [ text "**  EqCon"-                , text "    LEFT:  " <> ppr tL-                , text "    RIGHT: " <> ppr tR-                , indent 4 $ ppr ctx0-                , empty ]--        return ctx0--- -- EqApp- | TApp tL1 tL2 <- tL- , TApp tR1 tR2 <- tR- = do-        ctrace  $ vcat-                [ text "*>  EqApp" -                , empty ]--        ctx1    <- makeEq config a ctx0 tL1 tR1 err-        tL2'    <- applyContext ctx1 tL2-        tR2'    <- applyContext ctx1 tR2-        ctx2    <- makeEq config a ctx1 tL2' tR2' err--        ctrace  $ vcat-                [ text "*<  EqApp"-                , text "    LEFT:   " <> ppr tL-                , text "    RIGHT:  " <> ppr tR-                , indent 4 $ ppr ctx0-                , indent 4 $ ppr ctx2-                , empty ]--        return ctx2--- -- EqEquiv- | equivT tL tR - = do   ctrace  $ vcat-                [ text "**  EqEquiv" ]--        return ctx0--- -- Error- | otherwise- = do   let caps = configGlobalCaps config-        let tL'  = crushEffect caps $ unpackSumT tL-        let tR'  = crushEffect caps $ unpackSumT tR--        ctrace  $ vcat-                [ text "DDC.Core.Check.Exp.Inst.makeEq: no match"-                , text "  LEFT:   " <> (text $ show tL)-                , text "  RIGHT:  " <> (text $ show tR)-                , text "  LEFTC:  " <> (text $ show tL')-                , text "  RIGHTC: " <> (text $ show tR')-                , indent 2 $ ppr ctx0 ]--        throw err----- | Unpack single element sums into plain types.-unpackSumT :: Type n -> Type n-unpackSumT (TSum ts)-        | [t]   <- Sum.toList ts = t-unpackSumT tt                    = tt-

@@ -0,0 +1,201 @@++module DDC.Core.Check.Judge.EqT+        (makeEqT)+where+import DDC.Core.Check.Base +import qualified DDC.Core.Env.EnvT      as EnvT+import qualified Data.Map.Strict        as Map+++-- | Make two types equivalent to each other,+--   or throw the provided error if this is not possible.+makeEqT :: (Eq n, Ord n, Pretty n)+        => Config n+        -> Context n+        -> Type n+        -> Type n+        -> Error  a n+        -> CheckM a n (Context n)++makeEqT config ctx0 tL tR err++ -- EqT_SynL+ --   Expand type synonym on the left.+ | TCon (TyConBound (UName n) _) <- tL+ , Just tL' <- Map.lookup n $ EnvT.envtEquations $ contextEnvT ctx0+ = do+        ctrace  $ vcat+                [ text "**  EqT_SynL"+                , text "    tL : " <> ppr tL+                , text "    tL': " <> ppr tL'+                , text "    tR : " <> ppr tR+                , empty ]++        makeEqT config ctx0 tL' tR err+++ -- EqT_SynR+ --   Expand type synonym on the right.+ | TCon (TyConBound (UName n) _) <- tR+ , Just tR' <- Map.lookup n $ EnvT.envtEquations $ contextEnvT ctx0+ = do+        ctrace  $ vcat+                [ text "**  EqT_SynR"+                , text "    tL : " <> ppr tL+                , text "    tR : " <> ppr tR+                , text "    tR': " <> ppr tR'+                , empty ]++        makeEqT config ctx0 tL tR' err++ -- EqT_SolveL+ | Just iL <- takeExists tL+ , not $ isTExists tR+ = do   +        ctrace  $ vcat+                [ text "**  EqT_SolveL"+                , text "    tL:  " <> ppr tL+                , text "    tR:  " <> ppr tR+                , empty ]++        let Just ctx1   = updateExists [] iL tR ctx0+        +        return ctx1+++ -- EqT_SolveR+ | Just iR <- takeExists tR+ , not $ isTExists tL+ = do   +        ctrace  $ vcat+                [ text "**  EqT_SolveR"+                , text "    tL:  " <> ppr tL+                , text "    tR:  " <> ppr tR+                , empty ]+  +        let Just ctx1   = updateExists [] iR tL ctx0+        +        return ctx1+++ -- EqT_EachL+ --  Both types are existentials, and the left is bound earlier in the stack.+ --  CAREFUL: The returned location is relative to the top of the stack,+ --           hence we need lL > lR here.+ | Just iL <- takeExists tL,    Just lL <- locationOfExists iL ctx0+ , Just iR <- takeExists tR,    Just lR <- locationOfExists iR ctx0+ , lL > lR+ = do   let Just ctx1   = updateExists [] iR tL ctx0+        +        ctrace  $ vcat+                [ text "**  EqT_EachL"+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1+                , empty ]++        return ctx1+++ -- EqT_EachR+ --  Both types are existentials, and the right is bound earlier in the stack.+ --  CAREFUL: The returned location is relative to the top of the stack,+ --           hence we need lR > lL here.+ | Just iL <- takeExists tL,    Just lL <- locationOfExists iL ctx0+ , Just iR <- takeExists tR,    Just lR <- locationOfExists iR ctx0+ , lR > lL+ = do   let Just ctx1   = updateExists [] iL tR ctx0++        ctrace  $ vcat+                [ text "**  EqT_EachR"+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1+                , empty ]++        return ctx1+++ -- EqT_Var+ | TVar u1      <- tL+ , TVar u2      <- tR+ , u1 == u2+ = do   +        -- Suppress tracing of boring rule.+        -- ctrace  $ vcat+        --         [ text "**  EqT_Var"+        --         , text "    tL: " <> ppr tL+        --         , text "    tR: " <> ppr tR+        --         , indent 4 $ ppr ctx0+        --         , empty ]++        return ctx0+++ -- EqT_Con+ | TCon tc1     <- tL+ , TCon tc2     <- tR+ , equivTyCon tc1 tc2+ = do+        -- Only trace rule if it's done something interesting.+        when (not $ tc1 == tc2)+         $ ctrace  $ vcat+                [ text "**  EqT_Con"+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , empty ]++        return ctx0+++ -- EqT_App+ | TApp tL1 tL2 <- tL+ , TApp tR1 tR2 <- tR+ = do+        ctrace  $ vcat+                [ text "*>  EqT_App" +                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , empty ]++        ctx1    <- makeEqT config ctx0 tL1  tR1  err+        tL2'    <- applyContext ctx1 tL2+        tR2'    <- applyContext ctx1 tR2+        ctx2    <- makeEqT config ctx1 tL2' tR2' err++        ctrace  $ vcat+                [ text "*<  EqT_App"+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx2+                , empty ]++        return ctx2+++ -- EqT_Equiv+ | equivT (contextEnvT ctx0) tL tR + = do   ctrace  $ vcat+                [ text "**  EqT_Equiv" +                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , empty ]++        return ctx0+++ -- EqT_Fail+ | otherwise+ = do+        ctrace  $ vcat+                [ text "EqT_Fail"+                , text "  tL: " <> ppr tL+                , text "  tR: " <> ppr tR+                , indent 2 $ ppr ctx0+                , empty ]++        throw err+

@@ -0,0 +1,656 @@++module DDC.Core.Check.Judge.Kind+        (checkTypeM)+where+import DDC.Core.Check.Judge.Kind.TyCon+import DDC.Core.Check.Judge.EqT+import DDC.Core.Check.Context+import DDC.Core.Check.Error+import DDC.Core.Check.Config+import DDC.Type.Exp.Simple.Compounds+import DDC.Type.Exp.Simple.Predicates+import DDC.Type.DataDef+import DDC.Type.Universe+import DDC.Type.Exp+import DDC.Data.Pretty+import Control.Monad+import Data.List+import DDC.Core.Check.Base              (CheckM)+import qualified DDC.Core.Check.Base    as C+import qualified DDC.Type.Sum           as TS+import qualified DDC.Core.Env.EnvX      as EnvX+import qualified DDC.Core.Env.EnvT      as EnvT+import qualified Data.Map               as Map++import DDC.Core.Check.Base+        ( throw+        , newExists+        , applyContext)++-- | Check a type returning its kind, or a kind returning its sort.+--+--   The unverse of the thing to check is directly specified, and if the +--   thing is not actually in this universe they you'll get an error.+--+--   We track what universe the provided kind is in for defence against+--   transform bugs. Types like ([a : [b : Data]. b]. a -> a), should not be+--   accepted by the source parser, but may be created by bogus program+--   transformations. Quantifiers cannot be used at the kind level, so it's +--   better to fail early.+---+--   Note that when comparing kinds, we can just use plain equality+--   (==) instead of equivT. This is because kinds do not contain quantifiers+--   that need to be compared up to alpha-equivalence, nor do they contain+--   crushable components terms.+--+checkTypeM +        :: (Ord n, Show n, Pretty n) +        => Config n     -- ^ Type checker configuration.+        -> Context n    -- ^ Context of type to check.+        -> Universe     -- ^ What universe the type to check is in.+        -> Type n       -- ^ The type to check (can be a Spec or Kind)+        -> Mode n       -- ^ Type checker mode.+        -> CheckM a n +                ( Type n+                , Kind n+                , Context n)++-- Variables ------------------------------------+checkTypeM config ctx0 uni tt@(TVar u) mode++ -- Kind holes.+ --   This is some kind that we were explicitly told to infer,+ --   so make a new existential for it.+ | UniverseKind         <- uni+ , Just n               <- takeNameOfBound u+ , Just isHole          <- configNameIsHole config+ , isHole n+ = case mode of+        -- We don't infer kind holes in recon mode.+        -- The program should have complete kind annotations.+        Recon+         -> do  throw $ C.ErrorType $ ErrorTypeUndefined u++        -- Synthesised kinds are assumed to have sort Comp.+        Synth _+         -> do  i        <- newExists sComp+                let t    = typeOfExists i+                let ctx' = pushExists i ctx0+                return (t, sComp, ctx')++        -- We have an expected sort for the existential,+        -- so use that.+        Check sExpected+         -> do  i        <- newExists sExpected+                let t    = typeOfExists i+                let ctx' = pushExists i ctx0+                return (t, sExpected, ctx')++ -- Spec holes.+ --   This is some spec that we were explicitly told to infer,+ --   so make an existential for it.+ | UniverseSpec         <- uni+ , Just n               <- takeNameOfBound u+ , Just isHole          <- configNameIsHole config+ , isHole n+ = case mode of+        -- We don't infer spec holes in recon mode.+        -- The program should have complete spec annotations.+        Recon+         -> do  throw $ C.ErrorType $ ErrorTypeUndefined u++        -- Synthesised types could have an arbitrary kind, +        -- so we need to make two existentials.+        Synth _+         -> do  iK       <- newExists sComp+                let k    =  typeOfExists iK+                let ctx1 =  pushExists iK ctx0++                iT       <- newExists k+                let t    =  typeOfExists iT+                let ctx2 =  pushExists iT ctx1++                return  (t, k, ctx2)++        -- We have an expected kind for the existential,+        -- so use that.+        Check kExpected+         -> do  iT       <- newExists kExpected+                let t    =  typeOfExists iT+                let ctx1 =  pushExists iT ctx0+                return  (t, kExpected, ctx1)+++ -- Some variable defined in an environment, + -- or a primitive variable with its kind directly attached.+ | UniverseSpec          <- uni+ = let  +        -- Get the actual kind of the variable,+        -- according to the kind environment.+        getActual+         -- A variable in the local environment.+         | Just (k, _role) <- lookupKind u ctx0+         = return k++         -- A variable in the global environment.+         | Just k          <- EnvT.lookup u (contextEnvT ctx0)+         = return k++         -- A primitive type variable with its kind directly attached, but where+         -- the variable is not also in the kind environment. This is a hack used+         -- for static used for static region variables in the evaluator.+         -- We make them constructors rather than variables so that we don't need+         -- to have a data constructor definition for each one.+         | UPrim _ k       <- u+         = return k++         -- Type variable is no where to be found.+         | otherwise+         = throw $ C.ErrorType $ ErrorTypeUndefined u++   in do+        kActual  <- getActual+        kActual' <- applyContext ctx0 kActual++        -- In Check mode we check the expected kind against the actual+        -- kind from the environment.+        case mode of+         Check kExpected+          -> do +                kExpected' <- applyContext ctx0 kExpected+                ctx1       <- makeEqT config ctx0 kActual' kExpected'+                           $  C.ErrorType $ ErrorTypeMismatch uni  kActual' kExpected' tt++                return (tt, kActual', ctx1)+ +         _ ->   return (tt, kActual', ctx0)++ -- Type variables are not a part of this universe.+ | otherwise+ = throw $ C.ErrorType $ ErrorTypeUniverseMalfunction tt uni+++-- Constructors ---------------------------------+checkTypeM config ctx0 uni tt@(TCon tc) mode+ = let  +        -- Get the actual kind of the constructor, +        -- according to the constructor definition.+        getActual+         -- Sort constructors don't have a higher classification.+         -- We should never try to check these.+         | TyConSort _          <- tc+         , UniverseSort         <- uni+         = throw $ C.ErrorType $ ErrorTypeNakedSort tt++         -- Baked-in kind constructors.+         -- We can't sort-check a naked kind function constructor because+         -- the sort of a fully applied one depends on the argument kind.+         | TyConKind kc         <- tc+         , UniverseKind         <- uni+         = case takeSortOfKiCon kc of+                Just s   -> return (tt, s)+                Nothing  -> throw $ C.ErrorType $ ErrorTypeUnappliedKindFun++         -- Baked-in witness type constructors.+         | TyConWitness tcw     <- tc+         , UniverseSpec         <- uni+         = return (tt, kindOfTwCon tcw)++         -- Baked-in spec type constructors.+         | TyConSpec    tcc     <- tc+         , UniverseSpec         <- uni+         = return (tt, kindOfTcCon tcc)++         -- Fragment specific, or user defined constructors.+         | TyConBound u k       <- tc+         = case u of+            UName n+             -- User defined data type constructors must be in the set of+             -- data defs. Attach the real kind why we're here.+             | Just def         <- Map.lookup n $ dataDefsTypes +                                                $ EnvX.envxDataDefs +                                                $ contextEnvX ctx0+             , UniverseSpec     <- uni+             -> let k'   = kindOfDataType def+                in  return (TCon (TyConBound u k'), k')++             -- The kinds of abstract imported type constructors are in the+             -- global kind environment.+             | Just k'          <- EnvT.lookupName n (contextEnvT ctx0)+             , UniverseSpec     <- uni+             -> return (TCon (TyConBound u k'), k')++             -- For type synonyms, just re-check the right of the binding.+             | Just t'          <- Map.lookup n $ EnvT.envtEquations+                                                $ contextEnvT ctx0+             -> do  (tt', k', _) <- checkTypeM config ctx0 uni t' mode+                    return (tt', k')++             -- We don't have a type for this constructor.+             | otherwise+             -> throw $ C.ErrorType $ ErrorTypeUndefinedTypeCtor u++            -- The kinds of primitive type constructors are directly attached.+            UPrim{} -> return (tt, k)++            -- Type constructors are always defined at top-level and not+            -- by anonymous debruijn binding.+            UIx{}   -> throw $ C.ErrorType $ ErrorTypeUndefinedTypeCtor u++         -- Existentials can be either in the Spec or Kind universe,+         -- and their kinds/sorts are directly attached.+         | TyConExists _ t       <- tc+         , uni == UniverseSpec || uni == UniverseKind+         = return (tt, t)++         -- Whatever constructor we were given wasn't in the expected universe.+         | otherwise+         = throw $ C.ErrorType $ ErrorTypeUniverseMalfunction tt uni+ in do+        -- Get the actual kind/sort of the constructor according to the +        -- constructor definition.+        (tt', kActual)  <- getActual+        kActual'        <- applyContext ctx0 kActual++        case mode of+         -- If we have an expected kind then make the actual kind the same.+         Check kExpected+           -> do +                 kExpected' <- applyContext ctx0 kExpected+                 ctx1   <- makeEqT config ctx0 kActual' kExpected'+                        $  C.ErrorType $ ErrorTypeMismatch uni  kActual' kExpected' tt+                 return (tt', kActual', ctx1)++         -- In Recon and Synth mode just return the actual kind.+         _ ->    return (tt', kActual', ctx0)+++-- Quantifiers ----------------------------------+checkTypeM config ctx0 uni@UniverseSpec +        tt@(TForall b1 t2) mode+ = case mode of+    Recon+     -> do+        -- Check the binder is well sorted.+        let t1  = typeOfBind b1+        _       <- checkTypeM config ctx0 UniverseKind t1 Recon++        -- Check the body with the binder in scope.+        let (ctx1, pos1) = markContext ctx0+        let ctx2         = pushKind b1 RoleAbstract ctx1+        (t2', k2, ctx3) <- checkTypeM config ctx2 UniverseSpec t2 Recon++        -- The body must have kind Data or Witness.+        k2'             <- applyContext ctx3 k2+        when ( not (isDataKind k2')+            && not (isWitnessKind k2'))+         $ throw $ C.ErrorType $ ErrorTypeForallKindInvalid tt t2 k2'++        -- Pop the quantified type off the context.+        let ctx_cut      = popToPos pos1 ctx3++        return (TForall b1 t2', k2', ctx_cut)++    Synth{}+     -> do+        -- Synthesise a sort for the binder.+        let k1  = typeOfBind b1+        (k1', _s1, ctx1) <- checkTypeM config ctx0 UniverseKind k1 (Synth [])+                +        let b1' = replaceTypeOfBind k1' b1++        -- Check the body with the binder in scope.+        let (ctx2, pos1) = markContext ctx1+        let ctx3         = pushKind b1' RoleAbstract ctx2+        (t2', k2, ctx4) <- checkTypeM config ctx3 UniverseSpec t2 (Synth [])++        -- If the kind of the body is unconstrained then default it to Data.+        -- See [Note: Defaulting the kind of quantified types]+        k2' <- applyContext ctx4 k2+        (k2'', ctx5)+         <- if isTExists k2'+             then do+                ctx5    <- makeEqT config ctx4 k2' kData+                        $  C.ErrorType $ ErrorTypeMismatch uni  k2' kData tt++                k2''    <- applyContext ctx5 k2'+                return (k2'', ctx5)++             else do+                return (k2', ctx4)++        -- The above horror show needs to have worked.+        when ( not (isDataKind k2'')+            && not (isWitnessKind k2''))+         $ throw $ C.ErrorType $ ErrorTypeForallKindInvalid tt t2 k2''++        -- Pop the quantified type off the context.+        let ctx_cut      = popToPos pos1 ctx5++        return (TForall b1' t2', k2'', ctx_cut)++    Check kExpected +     -> do+        -- Synthesise a sort for the binder.+        let k1  = typeOfBind b1+        (k1', _s1, ctx1) <- checkTypeM config ctx0 UniverseKind k1 (Synth [])++        let b1' = replaceTypeOfBind k1' b1++        -- Check the body with the binder in scope.+        let (ctx2, pos1) = markContext ctx1+        let ctx3         = pushKind b1' RoleAbstract ctx2+        (t2', k2, ctx4) <- checkTypeM config ctx3 UniverseSpec t2 (Synth [])++        -- In Check mode if *both* the current kind of the body and the expected+        -- kind are existentials then force them both to be data. Otherwise make+        -- the kind of the body the same as the expected kind.+        -- See [Note: Defaulting the kind of quantified types]+        k2' <- applyContext ctx4 k2+        (k2'', ctx5)+         <- if isTExists k2' && isTExists kExpected+             then do+                ctx'    <- makeEqT config ctx4 k2' kExpected+                        $  C.ErrorType $ ErrorTypeMismatch uni  k2' kExpected tt++                ctx5    <- makeEqT config ctx' k2' kData +                        $  C.ErrorType $ ErrorTypeMismatch uni  k2' kData  tt++                k2''    <- applyContext ctx5 k2'+                return (k2'', ctx5)++             else do+                ctx5    <- makeEqT config ctx4 k2' kExpected+                        $  C.ErrorType $ ErrorTypeMismatch uni  k2' kExpected tt++                k2''    <- applyContext ctx5 k2'+                return (k2'', ctx4)++        -- The above horror show needs to have worked.+        when ( not (isDataKind k2'')+            && not (isWitnessKind k2''))+         $ throw $ C.ErrorType $ ErrorTypeForallKindInvalid tt t2 k2'++        -- Pop the quantified type off the context.+        let ctx_cut      = popToPos pos1 ctx5++        return (TForall b1' t2', k2'', ctx_cut)+++-- Applications ---------------------------------+-- Applications of the kind function constructor are handled directly+-- because the constructor doesn't have a sort by itself.+-- The sort of a kind function is the sort of the result.+checkTypeM config ctx0 uni@UniverseKind +        tt@(TApp (TApp ttFun k1) k2) mode+ | isFunishTCon ttFun+ = case mode of+    Recon+     -> do+        _               <- checkTypeM config ctx0 uni k1 Recon+        (_, s2, _)      <- checkTypeM config ctx0 uni k2 Recon+        return  (tt, s2, ctx0)++    Synth{}+     -> do+        (k1',  _, ctx1) <- checkTypeM config ctx0 uni k1 (Synth [])+        (k2', s2, ctx2) <- checkTypeM config ctx1 uni k2 (Synth [])+        return  (kFun k1' k2', s2, ctx2)++    Check sExpected+     -> do+        (k1',  _, ctx1) <- checkTypeM config ctx0 uni k1 (Synth [])+        (k2', s2, ctx2) <- checkTypeM config ctx1 uni k2 (Check sExpected)+        return  (kFun k1' k2', s2, ctx2)+++-- The implication constructor is overloaded and can have the+-- following kinds:+--   (=>) :: @ ~> @ ~> @,  for witness constructors.+--   (=>) :: @ ~> * ~> *,  for functions that take witnesses.+checkTypeM config ctx0 uni@UniverseSpec +        tt@(TApp (TApp tC@(TCon (TyConWitness TwConImpl)) t1) t2) mode+ = case mode of+    Recon+     -> do+        (t1', k1, ctx1) <- checkTypeM config ctx0 uni t1 Recon+        (t2', k2, ctx2) <- checkTypeM config ctx1 uni t2 Recon++        let tt' = TApp (TApp tC t1') t2'++        if      isWitnessKind k1 && isWitnessKind k2+         then     return (tt', kWitness, ctx2)+        else if isWitnessKind k1 && isDataKind k2+         then     return (tt', kData, ctx2)+        else    throw $ C.ErrorType $ ErrorTypeWitnessImplInvalid tt t1 k1 t2 k2++    Synth{}+     -> do+        (t1', _k1, ctx1) <- checkTypeM config ctx0 uni t1 mode+        (t2', k2,  ctx2) <- checkTypeM config ctx1 uni t2 mode++        return (tImpl t1' t2', k2, ctx2)++    Check kExpected+     -> do+        -- When checking type functions we don't need to worry about scopes.+        (t1', _k1, ctx1) <- checkTypeM config ctx0 uni t1 (Synth [])+        (t2', k2,  ctx2) <- checkTypeM config ctx1 uni t2 (Check kExpected)++        return (tImpl t1' t2', k2, ctx2)+++-- General type application.+checkTypeM config ctx0 UniverseSpec +        tt@(TApp tFn tArg) mode+ = case mode of+    Recon+     -> do+        -- Check the kind of the functional part.+        (tFn',  kFn,  ctx1) +         <- checkTypeM config ctx0 UniverseSpec tFn Recon+        +        -- Check the kind of the argument.+        (tArg', kArg, ctx2) +         <- checkTypeM config ctx1 UniverseSpec tArg Recon++        -- The kind of the parameter must match that of the argument+        case kFn of+         TApp (TApp ttFun kParam) kBody+           |  isFunishTCon ttFun +           ,  C.equivT (contextEnvT ctx2) kParam kArg+           -> return (tApp tFn' tArg', kBody, ctx2)++           | otherwise+           -> throw $ C.ErrorType $ ErrorTypeAppArgMismatch tt tFn' kFn tArg' kArg++         _ -> throw $ C.ErrorType $ ErrorTypeAppNotFun tt tFn' kFn tArg'++    Synth{}+     -> do+        -- Synthesise a kind for the functional part.+        (tFn', kFn, ctx1) +         <- checkTypeM config ctx0 UniverseSpec tFn (Synth [])++        -- Apply the argument to the function.+        kFn'    <- applyContext ctx1 kFn+        (kResult, tArg', ctx2)+         <- synthTAppArg config ctx1 tFn' kFn' tArg++        return (TApp tFn' tArg', kResult, ctx2)++    Check kExpected+     -> do+        -- Synthesise a kind for the overall type.+        (t1', k1, ctx1) +         <- checkTypeM config ctx0 UniverseSpec tt (Synth [])++        -- Force the synthesised kind to be the same as the expected one.+        k1'         <- applyContext   ctx1 k1+        kExpected'  <- applyContext   ctx1 kExpected+        ctx2        <- makeEqT config ctx1 k1' kExpected'+                    $  C.ErrorType $ ErrorTypeMismatch UniverseSpec k1' kExpected' tt++        return (t1', k1', ctx2)+++-- Sums -----------------------------------------+checkTypeM config ctx0 UniverseSpec tt@(TSum ss) mode+ = case mode of+    Recon+     -> do   +        -- Check all the elements,+        --  threading the context from left to right.+        (ts', ks, ctx1) +                <- checkTypesM config ctx0 UniverseSpec Recon+                $  TS.toList ss++        -- Check that all the types in the sum have the same kind.+        let kExpect = TS.kindOfSum ss+        k'      <- case nub ks of     +                     []     -> return $ TS.kindOfSum ss+                     [k]    -> return k+                     _      -> throw $ C.ErrorType $ ErrorTypeSumKindMismatch kExpect ss ks++        -- Check that the kind of the elements is a valid one.+        -- Only effects and closures can be summed.+        if (k' == kEffect || k' == kClosure)+         then return (TSum (TS.fromList k' ts'), k', ctx1)+         else throw $ C.ErrorType $ ErrorTypeSumKindInvalid ss k'++    Synth{}+     -> do+        -- Synthesise a kind for all the elements,+        --  threading the context from left to right.+        (ts, ks, ctx1)+                <- checkTypesM config ctx0 UniverseSpec (Synth [])+                $  TS.toList ss++        case ks of+         -- Force all elements to have the same kind as the first one.+         -- Note that (TS.kindOfSum ts) will be Bot in an unannotated program,+         -- so we can't use that directly.+         k : _ksMore+          -> do +                (ts'', _, ctx2)+                    <- checkTypesM  config ctx1 UniverseSpec (Check k) ts+                k'  <- applyContext ctx2 k+                return  (TSum (TS.fromList k' ts''), k', ctx2)++         -- If the sum does not contain an attached kind, and there are no elements+         -- then default it to Effect kind. This shouldn't happen in a well formed+         -- program, but might in a generated one.+         [] |  isBot (TS.kindOfSum ss)+            -> return   ( TSum (TS.fromList kEffect [])+                        , kEffect, ctx0)+            | otherwise+            -> return   ( TSum (TS.empty (TS.kindOfSum ss))+                        , TS.kindOfSum ss, ctx0)++    Check kExpected+     -> do+        -- Synthesise a kind for the overall type.+        (t1', k1, ctx1)+                <- checkTypeM config ctx0 UniverseSpec tt (Synth [])++        -- Force the synthesised kind to match the expected one.+        k1'         <- applyContext   ctx1 k1+        kExpected'  <- applyContext   ctx1 kExpected+        ctx2        <- makeEqT config ctx1 k1' kExpected'+                    $  C.ErrorType $ ErrorTypeMismatch UniverseSpec k1' kExpected' tt++        return  (t1', k1, ctx2)+++-- Whatever type we were given wasn't in the specified universe.+checkTypeM _ _ uni tt _mode+        = throw $ C.ErrorType $ ErrorTypeUniverseMalfunction tt uni+++-------------------------------------------------------------------------------+-- | Like `checkTypeM` but do several, chaining the contexts appropriately.+checkTypesM +        :: (Ord n, Show n, Pretty n) +        => Config n             -- ^ Type checker configuration.+        -> Context n            -- ^ Local context.+        -> Universe             -- ^ What universe the types to check are in.+        -> Mode n               -- ^ Type checker mode.+        -> [Type n]             -- ^ The types to check.+        -> CheckM a n +                ( [Type n]+                , [Kind n]+                , Context n)++checkTypesM _      ctx0 _   _    []+ = return ([], [], ctx0)++checkTypesM config ctx0 uni mode (t : ts)+ = do   (t',  k',  ctx1)  <- checkTypeM  config ctx0 uni t mode+        (ts', ks', ctx')  <- checkTypesM config ctx1 uni mode ts+        return  (t' : ts', k' : ks', ctx')+++-------------------------------------------------------------------------------+-- | Synthesise the type of a kind function applied to its argument.+synthTAppArg+        :: (Show n, Ord n, Pretty n)+        => Config n+        -> Context n+        -> Type n               -- Type function.+        -> Kind n               -- Kind of functional part.+        -> Type n               -- Type argument.+        -> CheckM a n+                ( Kind n        -- Kind of result.+                , Type n        -- Checked type argument.+                , Context n)    -- Result context. ++synthTAppArg config ctx0 tFn kFn tArg++ | Just iFn     <- takeExists kFn+ = do  +        -- New existential for the kind of the function parameter.+        iParam          <- newExists sComp+        let kParam      = typeOfExists iParam++        -- New existential for the kind of the function body+        iBody           <- newExists sComp+        let kBody       = typeOfExists iBody++        -- Update the context with the new constraint.+        let Just ctx1   = updateExists [iBody, iParam] iFn +                                (kFun kParam kBody) ctx0++        -- Check the argument under the new context.+        (tArg', _kArg, ctx2)+         <- checkTypeM config ctx1 UniverseSpec tArg (Check kParam)++        return (kBody, tArg', ctx2)+++ | TApp (TApp ttFun kParam) kBody <- kFn+ , isFunishTCon ttFun+ = do   +        -- The kind of the argument must match the parameter kind+        (tArg', _kArg, ctx1) +         <- checkTypeM config ctx0 UniverseSpec tArg (Check kParam)++        return (kBody, tArg', ctx1)++ | otherwise+ = throw $ C.ErrorType $ ErrorTypeAppNotFun (TApp tFn tArg) tFn kFn tArg +++-- [Note: Defaulting the kind of quantified types]+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+-- For expressions like:+--   /\a. \(x : [b : Data]. a). ()+--  +-- The kind of 'a' must be Data because 'x' is used as a parameter of a function +-- abstraction. If the kind of the body of a quantified type is unconstrained +-- then we default it to data.+--+-- Although the types of witness constructors have quantified types, +-- those types are primitive, so we never need to do type inference for them.+-- There aren't any cases where defaulting the kind of a quantified type to +-- Data would be the wrong thing to do.+--

@@ -0,0 +1,67 @@++module DDC.Core.Check.Judge.Kind.TyCon+        ( takeKindOfTyCon+        , takeSortOfKiCon+        , kindOfTwCon+        , kindOfTcCon)+where+import DDC.Type.Exp.Simple+++-- | Take the superkind of an atomic kind constructor.+--+--   Yields `Nothing` for the kind function (~>) as it doesn't have a sort+--   without being fully applied.+takeSortOfKiCon :: KiCon -> Maybe (Sort n)+takeSortOfKiCon kc+ = case kc of+        KiConFun        -> Nothing+        KiConData       -> Just sComp+        KiConRegion     -> Just sComp+        KiConEffect     -> Just sComp+        KiConClosure    -> Just sComp+        KiConWitness    -> Just sProp+++-- | Take the kind of a `TyCon`, if there is one.+takeKindOfTyCon :: TyCon n -> Maybe (Kind n)+takeKindOfTyCon tt+ = case tt of        +        -- Sorts don't have a higher classification.+        TyConSort    _   -> Nothing+ +        TyConKind    kc  -> takeSortOfKiCon kc+        TyConWitness tc  -> Just $ kindOfTwCon tc+        TyConSpec    tc  -> Just $ kindOfTcCon tc+        TyConBound   _ k -> Just k+        TyConExists  _ k -> Just k+++-- | Take the kind of a witness type constructor.+kindOfTwCon :: TwCon -> Kind n+kindOfTwCon tc+ = case tc of+        TwConImpl       -> kWitness  `kFun`  kWitness `kFun` kWitness+        TwConPure       -> kEffect   `kFun`  kWitness+        TwConConst      -> kRegion   `kFun`  kWitness+        TwConDeepConst  -> kData     `kFun`  kWitness+        TwConMutable    -> kRegion   `kFun`  kWitness+        TwConDeepMutable-> kData     `kFun`  kWitness+        TwConDisjoint   -> kEffect   `kFun`  kEffect  `kFun`  kWitness+        TwConDistinct n -> (replicate n kRegion)      `kFuns` kWitness        +++-- | Take the kind of a computation type constructor.+kindOfTcCon :: TcCon -> Kind n+kindOfTcCon tc+ = case tc of+        TcConUnit       -> kData+        TcConFun        -> kData    `kFun` kData `kFun` kData+        TcConSusp       -> kEffect  `kFun` kData `kFun` kData+        TcConRead       -> kRegion  `kFun` kEffect+        TcConHeadRead   -> kData    `kFun` kEffect+        TcConDeepRead   -> kData    `kFun` kEffect+        TcConWrite      -> kRegion  `kFun` kEffect+        TcConDeepWrite  -> kData    `kFun` kEffect+        TcConAlloc      -> kRegion  `kFun` kEffect+        TcConDeepAlloc  -> kData    `kFun` kEffect

@@ -0,0 +1,673 @@++module DDC.Core.Check.Judge.Module+        ( checkModule+        , checkModuleM)+where+import DDC.Core.Check.Judge.Type.Base   (checkTypeM)+import DDC.Core.Check.Judge.DataDefs+import DDC.Core.Check.Base+import DDC.Core.Check.Exp+import DDC.Core.Transform.Reannotate+import DDC.Core.Transform.MapT+import DDC.Core.Module+import DDC.Core.Env.EnvX                (EnvX)+import DDC.Control.Check                (runCheck, throw)++import qualified DDC.Type.Env           as Env+import qualified DDC.Core.Env.EnvT      as EnvT+import qualified DDC.Core.Env.EnvX      as EnvX+import qualified Data.Map.Strict        as Map+++-- Wrappers ---------------------------------------------------------------------------------------+-- | Type check a module.+--+--   If it's good, you get a new version with types attached to all the bound+--   variables+--+--   If it's bad, you get a description of the error.+checkModule+        :: (Show a, Ord n, Show n, Pretty n)+        => Config n             -- ^ Static configuration.+        -> Module a n           -- ^ Module to check.+        -> Mode n               -- ^ Type checker mode.+        -> ( Either (Error a n) (Module (AnTEC a n) n)+           , CheckTrace )++checkModule !config !xx !mode+ = let  (s, result)     = runCheck (mempty, 0, 0)+                        $ checkModuleM config xx mode+        (tr, _, _)      = s+   in   (result, tr)+++-- checkModule ------------------------------------------------------------------------------------+-- | Like `checkModule` but using the `CheckM` monad to handle errors.+checkModuleM+        :: (Show a, Ord n, Show n, Pretty n)+        => Config n             -- ^ Static configuration.+        -> Module a n           -- ^ Module to check.+        -> Mode n               -- ^ Type checker mode.+        -> CheckM a n (Module (AnTEC a n) n)++checkModuleM !config mm@ModuleCore{} !mode+ = do+        let envT_prim+                = EnvT.empty+                { EnvT.envtPrimFun      +                        = \n -> Env.lookupName n (configPrimKinds config) }++        -- Check sorts of imported types --------------------------------------+        ctrace  $ vcat+                [ text "* Checking Sorts of Imported Types" ]++        --   These have explicit kind annotations on the type parameters,+        --   which we can sort check directly.+        nitsImportType'+                <- checkImportTypes  config envT_prim mode+                $  moduleImportTypes mm++        let nksImportType' +                = [(n, kindOfImportType i) | (n, i) <- nitsImportType']++        -- Check sorts of imported data types ---------------------------------+        ctrace  $ vcat+                [ text "* Checking Sorts of Imported Data Types." ]++        --   These have explicit kind annotations on the type parameters,+        --   which we can sort check directly.+        nksImportDataDef'   +                <- checkSortsOfDataTypes config mode+                $  moduleImportDataDefs  mm+++        ctrace  $ vcat+                [ text "* Checking Sorts of Local Data Types." ]++        nksLocalDataDef'+                <- checkSortsOfDataTypes config mode+                $  moduleDataDefsLocal   mm++        let envT_dataDefs+                = EnvT.unions+                [ envT_prim+                , EnvT.fromListNT nksImportType'+                , EnvT.fromListNT nksImportDataDef'+                , EnvT.fromListNT nksLocalDataDef' ]++        -- Check kinds of imported type equations -----------------------------+        --   The right of each type equation can mention both imported abstract+        --   types and data type definitions, so we need to include them in+        --   the kind environment as well.+        ctrace  $ vcat+                [ text "* Checking Kinds of Imported Type Equations."]++        -- Imported type equations may mention each other.+        nktsImportTypeDef'+                <- checkKindsOfTypeDefs +                        config +                        envT_dataDefs+                          { EnvT.envtEquations +                          = Map.map snd $ Map.fromList $ moduleImportTypeDefs mm }+                $  moduleImportTypeDefs mm++        let envT_importedTypeDefs+                = EnvT.unions+                [ envT_dataDefs+                , EnvT.fromListNT [ (n, k) | (n, (k, _)) <- nktsImportTypeDef']+                , EnvT.empty +                        { EnvT.envtEquations +                        = Map.fromList    [ (n, t) | (n, (_, t)) <- nktsImportTypeDef']}]+++        -- Check kinds of local type equations --------------------------------+        --   The right of each type equation can mention+        --   imported abstract types, imported and local data type definitions.+        ctrace  $ vcat+                [ text "* Checking Kinds of Local Type Equations."]++        -- Kinds of type constructors in scope in the+        -- locally defined type equations.+        nktsLocalTypeDef'+                <- checkKindsOfTypeDefs+                        config +                        envT_importedTypeDefs+                         { EnvT.envtEquations+                         = Map.map snd $ Map.fromList $ moduleTypeDefsLocal mm }+                $  moduleTypeDefsLocal  mm++        let envT_localTypeDefs+                = EnvT.unions+                [ envT_importedTypeDefs+                , EnvT.fromListNT [ (n, k) | (n, (k, _)) <- nktsLocalTypeDef']+                , EnvT.empty+                        { EnvT.envtEquations+                        = Map.unions+                                [ Map.fromList [ (n, t) | (n, (_, t)) <- nktsLocalTypeDef']+                                , Map.fromList [ (n, t) | (n, (_, t)) <- nktsImportTypeDef' ]]+                        }+                ]+++        -- Check imported data type defs --------------------------------------+        ctrace  $ vcat+                [ text "* Checking Kinds of Imported Data Types."]++        let dataDefsImported = moduleImportDataDefs mm+        dataDefsImported'  +         <- case checkDataDefs config envT_localTypeDefs dataDefsImported of+                (err : _, _)            -> throw $ ErrorData err+                ([], dataDefsImported') -> return dataDefsImported'+++        -- Check the local data defs ------------------------------------------+        ctrace  $ vcat+                [ text "* Checking Kinds of Local Data Types."]++        let dataDefsLocal    = moduleDataDefsLocal mm+        dataDefsLocal'  +         <- case checkDataDefs config envT_localTypeDefs dataDefsLocal of+                (err : _, _)            -> throw $ ErrorData err+                ([], dataDefsLocal')    -> return dataDefsLocal'++        let dataDefs_top    +                = unionDataDefs (configPrimDataDefs config)+                $ unionDataDefs (fromListDataDefs dataDefsImported')+                                (fromListDataDefs dataDefsLocal')+++        -- Check types of imported capabilities -------------------------------+        ctrace  $ vcat+                [ text "* Checking Kinds of Imported Capabilities."]++        ntsImportCap'   +                <- checkImportCaps   config  envT_localTypeDefs mode+                $  moduleImportCaps  mm++        let envT_importCaps+                = EnvT.unions+                [ envT_localTypeDefs+                , EnvT.empty+                        { EnvT.envtCapabilities +                           = Map.fromList +                           $ [ (n, t) | (n, ImportCapAbstract t) <- ntsImportCap'] }]+++        -- Check types of imported values ------------------------------------+        ctrace  $ vcat+                [ text "* Checking Types of Imported Values."]++        ntsImportValue'+                <- checkImportValues  config envT_importCaps mode+                $  moduleImportValues mm++        let envX_importValues+                = (EnvX.fromListNT [(n, typeOfImportValue i) | (n, i) <- ntsImportValue' ])+                {  EnvX.envxEnvT     = envT_importCaps +                ,  EnvX.envxDataDefs = dataDefs_top+                ,  EnvX.envxPrimFun  = \n -> Env.envPrimFun (configPrimTypes config) n }+++        -----------------------------------------------------------------------+        -- Build the top-level config, defs and environments.+        --  These contain names that are visible to bindings in the module.+        let envT_top    = envT_importCaps+        let envX_top    = envX_importValues+        let ctx_top     = emptyContext { contextEnvX = envX_top }+++        -- Check the sigs of exported types ---------------+        esrcsType'  <- checkExportTypes   config envT_top+                    $  moduleExportTypes  mm+++        -- Check the sigs of exported values --------------+        esrcsValue' <- checkExportValues  config envT_top+                    $  moduleExportValues mm+++        -- Check the body of the module -------------------+        (x', _, _effs, ctx)+         <- checkExpM   (makeTable config)+                        ctx_top mode DemandNone (moduleBody mm) ++        -- Apply the final context to the annotations in expressions.+        let applyToAnnot (AnTEC t0 e0 _ x0)+             = do t0' <- applySolved ctx t0+                  e0' <- applySolved ctx e0+                  return $ AnTEC t0' e0' (tBot kClosure) x0++        xx_solved <- mapT (applySolved ctx) x'+        xx_annot  <- reannotateM applyToAnnot xx_solved++        -- Build new module with infered annotations ------+        let mm_inferred+                = mm+                { moduleExportTypes     = esrcsType'+                , moduleImportTypes     = nitsImportType'+                , moduleImportTypeDefs  = nktsImportTypeDef'+                , moduleImportCaps      = ntsImportCap'+                , moduleImportValues    = ntsImportValue'+                , moduleTypeDefsLocal   = nktsLocalTypeDef'+                , moduleBody            = xx_annot }+++        -- Check that each exported signature matches the type of its binding.+        -- This returns an environment containing all the bindings defined+        -- in the module.+        envX_binds+         <- checkModuleBinds envX_top+                (moduleExportTypes  mm_inferred)+                (moduleExportValues mm_inferred) +                xx_annot++        -- Check that all exported bindings are defined by the module,+        --   either directly as bindings, or by importing them from somewhere else.+        --   Header modules don't need to contain the complete set of bindings,+        --   but all other modules do.+        when (not $ moduleIsHeader mm_inferred)+                $ mapM_ (checkBindDefined envX_binds)+                $ map fst $ moduleExportValues mm_inferred++        -- If exported names are missing types then fill them in.+        let updateExportSource e+                | ExportSourceLocalNoType n <- e+                , Just t  <- EnvX.lookupX (UName n) envX_binds+                = ExportSourceLocal n t++                | otherwise = e++        let esrcsValue_updated+                = [ (n, updateExportSource e) | (n, e) <- esrcsValue' ]++        -- Return the checked bindings as they have explicit type annotations.+        let mm_final+                = mm_inferred+                { moduleExportValues    = esrcsValue_updated }++        return mm_final+++---------------------------------------------------------------------------------------------------+-- | Check exported types.+checkExportTypes+        :: (Show n, Pretty n, Ord n)+        => Config  n+        -> EnvT  n+        -> [(n, ExportSource n (Type n))]+        -> CheckM a n [(n, ExportSource n (Type n))]++checkExportTypes config env nesrcs+ = let  +        ctx     = contextOfEnvT env++        check (n, esrc)+         | Just k          <- takeTypeOfExportSource esrc+         = do   (k', _, _) <- checkTypeM config ctx UniverseKind k Recon+                return  $ (n, mapTypeOfExportSource (const k') esrc)++         | otherwise+         = return (n, esrc)+   in do+        -- Check for duplicate exports.+        let dups = findDuplicates $ map fst nesrcs+        (case takeHead dups of+          Just n -> throw $ ErrorExportDuplicate n+          _      -> return ())+++        -- Check the kinds of the export specs.+        mapM check nesrcs+++---------------------------------------------------------------------------------------------------+-- | Check exported types.+checkExportValues+        :: (Show n, Pretty n, Ord n)+        => Config n +        -> EnvT   n+        -> [(n, ExportSource n (Type n))]+        -> CheckM a n [(n, ExportSource n (Type n))]++checkExportValues config env nesrcs+ = let  +        ctx     = contextOfEnvT env++        check (n, esrc)+         | Just t          <- takeTypeOfExportSource esrc+         = do   (t', _, _) <- checkTypeM config ctx UniverseSpec t Recon+                return  $ (n, mapTypeOfExportSource (const t') esrc)++         | otherwise+         = return (n, esrc)++   in do+        -- Check for duplicate exports.+        let dups = findDuplicates $ map fst nesrcs+        (case takeHead dups of+          Just n -> throw $ ErrorExportDuplicate n+          _      -> return ())++        -- Check the types of the exported values.+        mapM check nesrcs+++---------------------------------------------------------------------------------------------------+-- | Check kinds of imported types.+checkImportTypes+        :: (Ord n, Show n, Pretty n)+        => Config n+        -> EnvT   n +        -> Mode   n+        -> [(n, ImportType n (Type n))]+        -> CheckM a n [(n, ImportType n (Type n))]++checkImportTypes config env mode nisrcs+ = let+        ctx     = contextOfEnvT env++        -- Checker mode to use.+        modeCheckImportTypes+         = case mode of+                Recon   -> Recon+                _       -> Synth []++        -- Check an import definition.+        check (n, isrc)+         = do   let k      =  kindOfImportType isrc+                (k', _, _) <- checkTypeM config ctx UniverseKind k modeCheckImportTypes+                return  (n, mapKindOfImportType (const k') isrc)++        -- Pack down duplicate import definitions.+        --   We can import the same value via multiple modules,+        --   which is ok provided all instances have the same kind.+        pack !mm []+         = return $ Map.toList mm++        pack !mm ((n, isrc) : nis)+         = case Map.lookup n mm of+                Just isrc'+                 | compat isrc isrc' -> pack mm nis+                 | otherwise         -> throw $ ErrorImportDuplicate n++                Nothing              -> pack (Map.insert n isrc mm) nis++        -- Check if two import definitions with the same name are compatible.+        -- The same import definition can appear multiple times provided+        -- each instance has the same name and kind.+        compat (ImportTypeAbstract k1) (ImportTypeAbstract k2) +                = equivT env k1 k2++        compat (ImportTypeBoxed    k1) (ImportTypeBoxed    k2)+                = equivT env k1 k2++        compat _ _ = False++   in do+        -- Check all the imports individually.+        nisrcs' <- mapM check nisrcs++        -- Check that exports with the same name are compatable,+        -- and pack down duplicates.+        pack Map.empty nisrcs'+++-------------------------------------------------------------------------------+-- | Check kinds of data type definitions,+--   returning a map of data type constructor constructor name to its kind.+checkSortsOfDataTypes+        :: (Ord n, Show n, Pretty n)+        => Config n +        -> Mode n+        -> [DataDef n]+        -> CheckM a n [(n, Kind n)]++checkSortsOfDataTypes config mode defs+ = let+        -- Checker mode to use.+        modeCheckDataTypes+         = case mode of+                Recon   -> Recon+                _       -> Synth []++        -- Check kind of a data type constructor.+        check def+         = do   let k   = kindOfDataDef def+                (k', _, _) <- checkTypeM config emptyContext UniverseKind k modeCheckDataTypes+                return (dataDefTypeName def, k')++   in do+        -- Check all the imports individually.+        nks     <- mapM check defs+        return  nks+++---------------------------------------------------------------------------------------------------+-- | Check kinds of imported type equations.+checkKindsOfTypeDefs+        :: (Ord n, Show n, Pretty n)+        => Config n+        -> EnvT n+        -> [(n, (Kind n, Type n))]+        -> CheckM a n [(n, (Kind n, Type n))]++checkKindsOfTypeDefs config env nkts+ = let+        ctx     = contextOfEnvT env++        -- Check a single type equation.+        check (n, (_k, t))+         = do   (t', k', _) +                 <- checkTypeM config ctx UniverseSpec t Recon++                -- ISSUE #374: Check specified kinds of type equations against inferred kinds.+                return (n, (k', t'))++   in do+        -- ISSUE #373: Check that type equations are not recursive.+        nkts' <- mapM check nkts+        return nkts'+++---------------------------------------------------------------------------------------------------+-- | Check types of imported capabilities.+checkImportCaps+        :: (Ord n, Show n, Pretty n)+        => Config n +        -> EnvT n+        -> Mode n+        -> [(n, ImportCap n (Type n))]+        -> CheckM a n [(n, ImportCap n (Type n))]++checkImportCaps config env mode nisrcs+ = let+        ctx     = contextOfEnvT env++        -- Checker mode to use.+        modeCheckImportCaps+         = case mode of+                Recon   -> Recon+                _       -> Check kEffect++        -- Check an import definition.+        check (n, isrc)+         = do   let t      =  typeOfImportCap isrc+                (t', k, _) <- checkTypeM config ctx UniverseSpec+                                t modeCheckImportCaps++                -- In Recon mode we need to post-check that the imported+                -- capability really has kind Effect.+                --+                -- In Check mode we pass down the expected kind,+                -- so this is checked locally.+                -- +                when (not $ isEffectKind k)+                 $ throw $ ErrorImportCapNotEffect n++                return (n, mapTypeOfImportCap (const t') isrc)++        -- Pack down duplicate import definitions.+        --   We can import the same capability via multiple modules,+        --   which is ok provided all instances have the same type.+        pack !mm []+         = return $ Map.toList mm++        pack !mm ((n, isrc) : nis)+         = case Map.lookup n mm of+                Just isrc'+                 | compat isrc isrc'    -> pack mm nis+                 | otherwise            -> throw $ ErrorImportDuplicate n++                Nothing                 -> pack (Map.insert n isrc mm) nis++        -- Check if two imported capabilities of the same name are compatiable.+        -- The same import definition can appear multiple times provided each +        -- instance has the same name and type.+        compat (ImportCapAbstract t1) (ImportCapAbstract t2) +                = equivT (contextEnvT ctx) t1 t2++    in do+        -- Check all the imports individually.+        nisrcs' <- mapM check nisrcs++        -- Check that imports with the same name are compatable,+        -- and pack down duplicates.+        pack Map.empty nisrcs'+++---------------------------------------------------------------------------------------------------+-- | Check types of imported values.+checkImportValues+        :: (Ord n, Show n, Pretty n)+        => Config n +        -> EnvT n +        -> Mode n+        -> [(n, ImportValue n (Type n))]+        -> CheckM a n [(n, ImportValue n (Type n))]++checkImportValues config env mode nisrcs+ = let+        ctx = contextOfEnvT env++        -- Checker mode to use.+        modeCheckImportTypes+         = case mode of+                Recon   -> Recon+                _       -> Check kData++        -- Check an import definition.+        check (n, isrc)+         = do   let t      =  typeOfImportValue isrc+                (t', k, _) <- checkTypeM config ctx UniverseSpec+                                         t modeCheckImportTypes++                -- In Recon mode we need to post-check that the imported+                -- value really has kind Data.+                --+                -- In Check mode we pass down the expected kind,+                -- so this is checked locally.+                --+                when (not $ isDataKind k)+                 $ throw $ ErrorImportValueNotData n++                return  (n, mapTypeOfImportValue (const t') isrc)++        -- Pack down duplicate import definitions.+        --   We can import the same value via multiple modules,+        --   which is ok provided all instances have the same type.+        pack !mm []+         = return $ Map.toList mm++        pack !mm ((n, isrc) : nis)+         = case Map.lookup n mm of+                Just isrc'+                  | compat isrc isrc'   -> pack mm nis+                  | otherwise           -> throw $ ErrorImportDuplicate n++                Nothing                 -> pack (Map.insert n isrc mm) nis++        -- Check if two imported values of the same name are compatable.+        compat (ImportValueModule _ _ t1 a1) +               (ImportValueModule _ _ t2 a2)+         = equivT (contextEnvT ctx) t1 t2 && a1 == a2++        compat (ImportValueSea _ t1)+               (ImportValueSea _ t2)+         = equivT (contextEnvT ctx) t1 t2 ++        compat _ _ = False++   in do+        -- Check all the imports individually.+        nisrcs' <- mapM check nisrcs++        -- Check that imports with the same name are compatable,+        -- and pack down duplicates.+        pack Map.empty nisrcs'+++---------------------------------------------------------------------------------------------------+-- | Check that the exported signatures match the types of their bindings.+checkModuleBinds+        :: Ord n+        => EnvX n                               -- ^ Starting environment.+        -> [(n, ExportSource n (Type n))]       -- ^ Exported types.+        -> [(n, ExportSource n (Type n))]       -- ^ Exported values+        -> Exp (AnTEC a n) n+        -> CheckM a n (EnvX n)                  -- ^ Environment of top-level bindings+                                                --   defined by the module++checkModuleBinds !env !ksExports !tsExports !xx+ = case xx of+        XLet _ (LLet b _) x2+         -> do  checkModuleBind (EnvX.envxEnvT env) ksExports tsExports b+                env'    <- checkModuleBinds env ksExports tsExports x2+                return  $ EnvX.extendX b env'++        XLet _ (LRec bxs) x2+         -> do  mapM_ (checkModuleBind (EnvX.envxEnvT env) ksExports tsExports) $ map fst bxs+                env'    <- checkModuleBinds env ksExports tsExports x2+                return  $ EnvX.extendsX (map fst bxs) env'++        XLet _ (LPrivate _ _ _) x2+         ->     checkModuleBinds env ksExports tsExports x2++        _ ->    return env+++-- | If some bind is exported, then check that it matches the exported version.+checkModuleBind+        :: Ord n+        => EnvT n                               -- ^ Environment of types.+        -> [(n, ExportSource n (Type n))]       -- ^ Exported types.+        -> [(n, ExportSource n (Type n))]       -- ^ Exported values.+        -> Bind n+        -> CheckM a n ()++checkModuleBind env !_ksExports !tsExports !b+ | BName n tDef <- b+ = case join $ liftM takeTypeOfExportSource $ lookup n tsExports of+        Nothing                 -> return ()+        Just tExport+         | equivT env tDef tExport  -> return ()+         | otherwise                -> throw $ ErrorExportMismatch n tExport tDef++ -- Only named bindings can be exported,+ --  so we don't need to worry about non-named ones.+ | otherwise+ = return ()+++---------------------------------------------------------------------------------------------------+-- | Check that an exported top-level value is actually defined by the module.+checkBindDefined+        :: Ord n+        => EnvX n               -- ^ Environment containing binds defined by the module.+        -> n                    -- ^ Name of an exported binding.+        -> CheckM a n ()++checkBindDefined envx n+ = case EnvX.lookupX (UName n) envx of+        Just _  -> return ()+        _       -> throw $ ErrorExportUndefined n+