ddc-core 0.4.1.3 → 0.4.2.1

raw patch · 119 files changed

+7497/−5379 lines, 119 filesdep +textdep ~basedep ~ddc-basedep ~deepseqPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: text

Dependency ranges changed: base, ddc-base, deepseq, mtl

API changes (from Hackage documentation)

Files

• DDC/Core/Annot/AnT.hs +0/−35
• DDC/Core/Annot/AnTEC.hs +0/−50
• DDC/Core/Call.hs +435/−0
• DDC/Core/Check.hs +2/−1
• DDC/Core/Check/Base.hs +42/−23
• DDC/Core/Check/Error.hs +14/−52
• DDC/Core/Check/ErrorMessage.hs +26/−64
• DDC/Core/Check/Exp.hs +57/−63
• DDC/Core/Check/Judge/Eq.hs +73/−68
• DDC/Core/Check/Judge/Inst.hs +49/−49
• DDC/Core/Check/Judge/Sub.hs +107/−78
• DDC/Core/Check/Judge/Type/AppT.hs +26/−34
• DDC/Core/Check/Judge/Type/AppX.hs +160/−109
• DDC/Core/Check/Judge/Type/Base.hs +78/−27
• DDC/Core/Check/Judge/Type/Case.hs +96/−94
• DDC/Core/Check/Judge/Type/Cast.hs +62/−146
• DDC/Core/Check/Judge/Type/DaCon.hs +1/−1
• DDC/Core/Check/Judge/Type/LamT.hs +46/−54
• DDC/Core/Check/Judge/Type/LamX.hs +260/−154
• DDC/Core/Check/Judge/Type/Let.hs +217/−115
• DDC/Core/Check/Judge/Type/LetPrivate.hs +66/−119
• DDC/Core/Check/Judge/Type/Sub.hs +32/−19
• DDC/Core/Check/Judge/Type/VarCon.hs +27/−30
• DDC/Core/Check/Judge/Type/Witness.hs +3/−4
• DDC/Core/Check/Module.hs +262/−102
• DDC/Core/Check/TaggedClosure.hs +0/−234
• DDC/Core/Check/Witness.hs +20/−56
• DDC/Core/Collect/Free.hs +9/−15
• DDC/Core/Collect/Free/Simple.hs +5/−11
• DDC/Core/Collect/Support.hs +37/−22
• DDC/Core/Compounds.hs +0/−7
• DDC/Core/Compounds/Annot.hs +0/−358
• DDC/Core/Compounds/Simple.hs +0/−291
• DDC/Core/Exp.hs +2/−2
• DDC/Core/Exp/Annot.hs +90/−168
• DDC/Core/Exp/Annot/AnT.hs +35/−0
• DDC/Core/Exp/Annot/AnTEC.hs +50/−0
• DDC/Core/Exp/Annot/Compounds.hs +414/−0
• DDC/Core/Exp/Annot/Context.hs +152/−0
• DDC/Core/Exp/Annot/Ctx.hs +235/−0
• DDC/Core/Exp/Annot/Exp.hs +198/−0
• DDC/Core/Exp/Annot/Predicates.hs +162/−0
• DDC/Core/Exp/Generic/BindStruct.hs +86/−0
• DDC/Core/Exp/Generic/Compounds.hs +146/−0
• DDC/Core/Exp/Generic/Exp.hs +162/−0
• DDC/Core/Exp/Generic/Predicates.hs +122/−0
• DDC/Core/Exp/Generic/Pretty.hs +293/−0
• DDC/Core/Exp/Pat.hs +0/−26
• DDC/Core/Exp/Simple.hs +0/−201
• DDC/Core/Exp/Simple/Compounds.hs +288/−0
• DDC/Core/Exp/Simple/Exp.hs +196/−0
• DDC/Core/Exp/WiCon.hs +5/−53
• DDC/Core/Fragment.hs +14/−1
• DDC/Core/Fragment/Compliance.hs +8/−16
• DDC/Core/Fragment/Feature.hs +11/−0
• DDC/Core/Fragment/Profile.hs +25/−2
• DDC/Core/Lexer.hs +209/−125
• DDC/Core/Lexer/Names.hs +16/−28
• DDC/Core/Lexer/Offside.hs +20/−7
• DDC/Core/Lexer/Tokens.hs +59/−22
• DDC/Core/Lexer/Unicode.hs +81/−0
• DDC/Core/Load.hs +3/−3
• DDC/Core/Module.hs +92/−153
• DDC/Core/Module/Export.hs +47/−0
• DDC/Core/Module/Import.hs +157/−0
• DDC/Core/Module/Name.hs +57/−0
• DDC/Core/Parser.hs +3/−2
• DDC/Core/Parser/Base.hs +56/−29
• DDC/Core/Parser/Context.hs +8/−4
• DDC/Core/Parser/DataDef.hs +83/−0
• DDC/Core/Parser/Exp.hs +30/−67
• DDC/Core/Parser/ExportSpec.hs +78/−0
• DDC/Core/Parser/ImportSpec.hs +170/−0
• DDC/Core/Parser/Module.hs +82/−245
• DDC/Core/Parser/Param.hs +5/−11
• DDC/Core/Parser/Type.hs +11/−33
• DDC/Core/Parser/Witness.hs +7/−16
• DDC/Core/Predicates.hs +0/−132
• DDC/Core/Pretty.hs +72/−72
• DDC/Core/Transform/Annotate.hs +4/−8
• DDC/Core/Transform/BoundT.hs +89/−0
• DDC/Core/Transform/BoundX.hs +166/−0
• DDC/Core/Transform/Deannotate.hs +4/−7
• DDC/Core/Transform/LiftT.hs +0/−91
• DDC/Core/Transform/LiftX.hs +0/−170
• DDC/Core/Transform/MapT.hs +84/−56
• DDC/Core/Transform/Reannotate.hs +56/−45
• DDC/Core/Transform/Rename.hs +1/−2
• DDC/Core/Transform/SpreadX.hs +63/−25
• DDC/Core/Transform/SubstituteTX.hs +1/−7
• DDC/Core/Transform/SubstituteWX.hs +2/−8
• DDC/Core/Transform/SubstituteXX.hs +4/−10
• DDC/Core/Transform/Trim.hs +0/−112
• DDC/Type/Check/Base.hs +26/−1
• DDC/Type/Check/CheckCon.hs +1/−11
• DDC/Type/Check/Config.hs +38/−25
• DDC/Type/Check/Context.hs +87/−59
• DDC/Type/Check/Error.hs +4/−0
• DDC/Type/Check/ErrorMessage.hs +3/−0
• DDC/Type/Check/Judge/Eq.hs +4/−4
• DDC/Type/Check/Judge/Kind.hs +29/−25
• DDC/Type/Collect.hs +90/−85
• DDC/Type/Compounds.hs +56/−75
• DDC/Type/DataDef.hs +13/−9
• DDC/Type/Env.hs +1/−1
• DDC/Type/Equiv.hs +173/−9
• DDC/Type/Exp/Base.hs +21/−31
• DDC/Type/Exp/NFData.hs +15/−4
• DDC/Type/Predicates.hs +4/−4
• DDC/Type/Pretty.hs +6/−24
• DDC/Type/Subsumes.hs +4/−11
• DDC/Type/Sum.hs +4/−8
• DDC/Type/Transform/BoundT.hs +109/−0
• DDC/Type/Transform/Crush.hs +0/−185
• DDC/Type/Transform/LiftT.hs +0/−109
• DDC/Type/Transform/SubstituteT.hs +14/−38
• DDC/Type/Transform/Trim.hs +0/−166
• DDC/Type/Universe.hs +0/−1
• ddc-core.cabal +69/−50

@@ -1,35 +0,0 @@--module DDC.Core.Annot.AnT-        (AnT (..))-where-import DDC.Type.Exp-import DDC.Base.Pretty-import Control.DeepSeq-import Data.Typeable----- Annot ------------------------------------------------------------------------- | The type checker for witnesses adds this annotation to every node in the,---   giving the type of each component of the witness.-------   NOTE: We want to leave the components lazy so that the checker---         doesn't actualy need to produce the type components if they're---         not needed.-data AnT a n-        = AnT-        { annotType     :: (Type  n)-        , annotTail     :: a }-        deriving (Show, Typeable)---instance (NFData a, NFData n) => NFData (AnT a n) where- rnf !an-        =     rnf (annotType    an)-        `seq` rnf (annotTail    an)---instance Pretty (AnT a n) where- ppr _ = text "AnT"        ---

@@ -1,50 +0,0 @@--module DDC.Core.Annot.AnTEC-        ( AnTEC (..)-        , fromAnT)-where-import DDC.Type.Compounds-import DDC.Type.Exp-import DDC.Base.Pretty-import Control.DeepSeq-import Data.Typeable-import DDC.Core.Annot.AnT       (AnT)-import qualified DDC.Core.Annot.AnT as AnT----- Annot ------------------------------------------------------------------------- | The type checker adds this annotation to every node in the AST, ---   giving its type, effect and closure.-------   NOTE: We want to leave the components lazy so that the checker---         doesn't actualy need to produce the type components if they're---         not needed.-data AnTEC a n-        = AnTEC-        { annotType     :: (Type    n)-        , annotEffect   :: (Effect  n)-        , annotClosure  :: (Closure n)-        , annotTail     :: a }-        deriving (Show, Typeable)----- | Promote an `AnT` to an `AnTEC` by filling in the effect and closure---   portions with bottoms.-fromAnT :: AnT a n -> AnTEC a n-fromAnT (AnT.AnT t a)-   =    (AnTEC t (tBot kEffect) (tBot kClosure) a)---instance (NFData a, NFData n) => NFData (AnTEC a n) where- rnf !an-        =     rnf (annotType    an)-        `seq` rnf (annotEffect  an)-        `seq` rnf (annotClosure an)-        `seq` rnf (annotTail    an)---instance Pretty (AnTEC a n) where- ppr _ = text "AnTEC"        ---

@@ -0,0 +1,435 @@++-- | Call patterns.+--+--   A call pattern describes the sequence of objects that are eliminated+--   by some object when we apply it, and before it starts constructing+--   new values. +--+-- @+-- Constructor (+ve)             Eliminator (-ve)+--  /\x.  (type   abstraction)    \@'    (type   application)+--   \x.  (object abstraction)    \@     (object application) +--  box   (suspend evaluation)   run   (commence evaluation)+-- @+--   +module DDC.Core.Call +        ( -- * Call constructors+          Cons (..)+        , isConsType+        , isConsValue+        , isConsBox+        , takeCallConsFromExp+        , takeCallConsFromType+        , splitStdCallCons+        , takeStdCallConsFromTypeArity++          -- * Call eliminators+        , Elim (..)+        , isElimType+        , isElimValue+        , isElimRun+        , takeCallElim+        , applyElim+        , splitStdCallElims++          -- * Matching+        , elimForCons+        , dischargeConsWithElims+        , dischargeTypeWithElims)+where+import DDC.Core.Exp.Annot+import DDC.Type.Transform.SubstituteT+++-----------------------------------------------------------------------------+-- | One component of the call pattern of a super.+--   This is the "outer wrapper" of the computation,+-- +--   With @/\(a : k). \(x : t). box (x + 1)@ the call pattern consists of+--   the two lambdas and the box. These three things need to be eliminated+--   before we can construct any new values.+--+data Cons n+        = -- | A type  lambda that needs a type of this kind.+          ConsType    (Bind n)++          -- | A value lambda that needs a value of this type.+        | ConsValue   (Type n)++          -- | A suspended expression that needs to be run.+        | ConsBox+        deriving (Show)+++-- | Check if this is an `ConsType`.+isConsType :: Cons n -> Bool+isConsType cc+ = case cc of+        ConsType{}      -> True+        _               -> False+++-- | Check if this is an `ElimType`.+isConsValue :: Cons n -> Bool+isConsValue cc+ = case cc of+        ConsValue{}     -> True+        _               -> False+++-- | Check if this is an `ElimType`.+isConsBox :: Cons n -> Bool+isConsBox cc+ = case cc of+        ConsBox{}       -> True+        _               -> False+++-- | Get the call pattern of an expression.+takeCallConsFromExp :: Exp a n -> [Cons n]+takeCallConsFromExp xx+ = case xx of+        XLAM _ b x         +         ->     ConsType  b : takeCallConsFromExp x++        XLam _ b x         +         -> let t       = typeOfBind b+            in  ConsValue t : takeCallConsFromExp x++        XCast _ CastBox x+         ->     ConsBox     : takeCallConsFromExp x++        _ -> []+++-- | Infer the call pattern of an expression from its type.+--   If the type has a function constructor then we assume there+--   is a corresponding lambda abstraction in the expression, and so on.+takeCallConsFromType :: Type n -> [Cons n]+takeCallConsFromType tt+        | TForall bParam tBody   <- tt+        = ConsType  bParam : takeCallConsFromType tBody++        | Just (tParam, tResult) <- takeTFun tt+        = ConsValue tParam : takeCallConsFromType tResult++        | Just (_, tResult)      <- takeTSusp tt+        = ConsBox          : takeCallConsFromType tResult++        | otherwise+        = []+++-- | Like `splitStdCallElim`, but for the constructor side.+--+splitStdCallCons+        :: [Cons n]+        -> Maybe ([Cons n], [Cons n], [Cons n])++splitStdCallCons cs+ = eatTypes [] cs+ where+        eatTypes  accTs (e@ConsType{} : es)+         = eatTypes (e : accTs) es++        eatTypes  accTs es+         = eatValues (reverse accTs) [] es++        eatValues accTs accVs (e@ConsValue{} : es)+         = eatValues accTs (e : accVs) es++        eatValues accTs accVs es+         = eatRuns   accTs (reverse accVs) [] es++        eatRuns  accTs accVs accRs (e@ConsBox{} : es)+         = eatRuns   accTs accVs (e : accRs) es++        eatRuns  accTs accVs accRs []+         = Just (accTs, accVs, reverse accRs)++        eatRuns  _accTs _accVs _accRs _+         = Nothing+++-- | Given the type of a super, and the number of type parameters,+--   value parameters and boxings, produce the corresponding list+--   of call constructors.+--+--   Example:+--+-- @+--    takeStdCallConsFromType +--       [| forall (a : k1) (b : k2). a -> b -> S e b |] +--       2 2 1+--    => [ ConsType  [|k1|], ConsType  [|k2|]+--       , ConsValue [|a\],  ConsValue [|b|]+--       , ConsBox ]+-- @+--+--   When we're considering the parts of the type, if the given arity+--   does not match what is in the type then `Nothing`.+--+takeStdCallConsFromTypeArity+        :: Type n       -- ^ Type of super+        -> Int          -- ^ Number of type parameters.+        -> Int          -- ^ Number of value parameters.+        -> Int          -- ^ Number of boxings.+        -> Maybe [Cons n]++takeStdCallConsFromTypeArity tt0 nTypes0 nValues0 nBoxes0+ = eatTypes [] tt0 nTypes0+ where+        -- Consider type parameters.+        eatTypes !accTs !tt !nTypes++         -- The arity information tells us to expect a type parameter.+         | nTypes  > 0+         = case tt of+            -- The super type matches.+            TForall b tBody+             -> eatTypes (ConsType b : accTs) tBody (nTypes - 1)++            -- The super type does not match the arity information.+            _ -> Nothing++         -- No more type parameters expected, so consider the value parameters.+         | otherwise+         = eatValues (reverse accTs) [] tt nValues0+++        -- Consider value parameters.+        eatValues !accTs !accVs !tt !nValues++         -- The arity information tells us to expect a value parameter.+         | nValues > 0+         = case takeTFun tt of+            -- The super type matches.+            Just (t1, t2) +              -> eatValues accTs (ConsValue t1 : accVs) t2 (nValues - 1)++            -- The super type does not match the arity information.+            _ -> Nothing++         -- No more value parameters expect, so consider the boxes.+         | otherwise+         = eatBoxes accTs (reverse accVs) [] tt nBoxes0+++        -- Consider boxes.+        eatBoxes !accTs !accVs !accBs tt nBoxes++         -- The arity information tells us to expect a boxing.+         | nBoxes > 0+         = case takeTSusp tt of+            -- The super type matches.+            Just (_eff, tBody)+              -> eatBoxes accTs accVs (ConsBox : accBs) tBody (nBoxes - 1)++            -- The super type does not match the arity information.+            _ -> Nothing++         -- No more boxings to expect, so we're done.+         | otherwise+         = return (accTs ++ accVs ++ reverse accBs)+++-------------------------------------------------------------------------------+-- | One component of a super call.+data Elim a n+        = -- | Give a type to a type lambda.+          ElimType    a a (Type n)++          -- | Give a value to a value lambda.+        | ElimValue   a (Exp a n)++          -- | Run a suspended computation.+        | ElimRun     a+        deriving (Show)+++-- | Check if this is an `ElimType`.+isElimType :: Elim a n -> Bool+isElimType ee+ = case ee of+        ElimType{}      -> True+        _               -> False+++-- | Check if this is an `ElimType`.+isElimValue :: Elim a n -> Bool+isElimValue ee+ = case ee of+        ElimValue{}     -> True+        _               -> False+++-- | Check if this is an `ElimType`.+isElimRun :: Elim a n -> Bool+isElimRun ee+ = case ee of+        ElimRun{}       -> True+        _               -> False+++-- | Apply an eliminator to an expression.+applyElim :: Exp a n -> Elim a n -> Exp a n+applyElim xx e+ = case e of+        ElimType  a at t -> XApp a xx (XType at t)+        ElimValue a x    -> XApp a xx x+        ElimRun   a      -> XCast a CastRun xx+++-- | Split the application of some object into the object being+--   applied and its eliminators.+takeCallElim :: Exp a n -> (Exp a n, [Elim a n])+takeCallElim xx+ = case xx of+        XApp a x1 (XType at t2)+         -> let (xF, xArgs)     = takeCallElim x1+            in  (xF, xArgs ++ [ElimType a at t2])++        XApp a x1 x2            +         -> let (xF, xArgs)     = takeCallElim x1+            in  (xF, xArgs ++ [ElimValue a x2])++        XCast a CastRun x1+         -> let (xF, xArgs)     = takeCallElim x1+            in  (xF, xArgs ++ [ElimRun a])++        _ -> (xx, [])+++-- | Group eliminators into sets for a standard call.+--+--   The standard call sequence is a list of type arguments, followed+--   by some objects, and optionally running the result suspension.+--+--   @run f [T1] [T2] x1 x2@+--+--   If 'f' is a super, and this is a saturating call then the super header+--   will look like the following:+--+--   @f = (/\t1. /\t2. \v1. \v2. box. body)@++--   If the eliminators are not in the standard call sequence then `Nothing`.+--+splitStdCallElims +        :: [Elim a n] +        -> Maybe ([Elim a n], [Elim a n], [Elim a n])++splitStdCallElims ee+ = eatTypes [] ee+ where+        eatTypes  accTs (e@ElimType{} : es)+         = eatTypes (e : accTs) es++        eatTypes  accTs es+         = eatValues (reverse accTs) [] es++        eatValues accTs accVs (e@ElimValue{} : es)+         = eatValues accTs (e : accVs) es++        eatValues accTs accVs es+         = eatRuns   accTs (reverse accVs) [] es++        eatRuns  accTs accVs accRs (e@ElimRun{} : es)+         = eatRuns   accTs accVs (e : accRs) es++        eatRuns  accTs accVs accRs []+         = Just (accTs, accVs, reverse accRs)++        eatRuns  _accTs _accVs _accRs _+         = Nothing+++-------------------------------------------------------------------------------+-- | Check if this an eliminator for the given constructor.+--   This only checks the general form of the eliminator +--   and constructor, not the exact types or kinds.+elimForCons :: Elim a n -> Cons n -> Bool+elimForCons e c+ = case (e, c) of+        (ElimType{},  ConsType{})       -> True+        (ElimValue{}, ConsValue{})      -> True+        (ElimRun{},   ConsBox{})        -> True+        _                               -> False+++-- | Given lists of constructors and eliminators, check if the+--   eliminators satisfy the constructors, and return any remaining+--   unmatching constructors and eliminators.+--+--   We assume that the application is well typed and that applying+--   the given eliminators will not cause variable capture.+---+--   ISSUE #347: Avoid name capture in dischargeConsWithElims+--   This process doesn't avoid name capture by ConsTypes earlier+--   in the list, but it's only called from the Curry transform+--   where there shouldn't be any shadowed type binders.+--+dischargeConsWithElims+        :: Ord n+        => [Cons n] +        -> [Elim a n] +        -> ([Cons n], [Elim a n])++dischargeConsWithElims (c : cs) (e : es)+ = case (c, e) of+        (ConsType  b1, ElimType  _ _ t2)+          -> dischargeConsWithElims +                (map (instantiateConsT b1 t2) cs) +                es++        (ConsValue _t1, ElimValue _ _x2)+          -> dischargeConsWithElims cs es++        (ConsBox,       ElimRun _)+          -> dischargeConsWithElims cs es++        _ -> (c : cs, e : es)++dischargeConsWithElims cs es+ = (cs, es)+++instantiateConsT :: Ord n => Bind n -> Type n -> Cons n -> Cons n+instantiateConsT b t cc+ = case cc of+        ConsType{}      -> cc+        ConsValue t'    -> ConsValue (substituteT b t t')+        ConsBox{}       -> cc+++-- | Given a type of a function and eliminators, discharge+--   foralls, abstractions and boxes to get the result type+--   of performing the application.+-- +--   We assume that the application is well typed.+--+dischargeTypeWithElims+        :: Ord n+        => Type n+        -> [Elim a n]+        -> Maybe (Type n)++dischargeTypeWithElims tt (ElimType  _ _ tArg : es)+        | TForall b tBody         <- tt+        = dischargeTypeWithElims +                (substituteT b tArg tBody) +                es++dischargeTypeWithElims tt (ElimValue _ _xArg  : es)+        | Just (_tParam, tResult) <- takeTFun tt+        = dischargeTypeWithElims tResult es++dischargeTypeWithElims tt (ElimRun _ : es)+        | Just (_, tBody)         <- takeTSusp tt+        = dischargeTypeWithElims tBody es+ +dischargeTypeWithElims tt []+        = Just tt++dischargeTypeWithElims _tt _es+        = Nothing+

@@ -16,7 +16,8 @@         , checkModule                    -- * Checking Expressions-        , Mode       (..)+        , Mode   (..)+        , Demand (..)         , checkExp,     typeOfExp            -- * Checking Witnesses

@@ -7,6 +7,8 @@         , CheckM         , newExists         , newPos+        , applyContext+        , applySolved          , CheckTrace (..)         , ctrace@@ -20,10 +22,8 @@         , Set         , module DDC.Core.Check.Error         , module DDC.Core.Collect-        , module DDC.Core.Predicates-        , module DDC.Core.Compounds         , module DDC.Core.Pretty-        , module DDC.Core.Exp+        , module DDC.Core.Exp.Annot         , module DDC.Type.Check.Context         , module DDC.Type.DataDef         , module DDC.Type.Equiv@@ -38,10 +38,8 @@ where import DDC.Core.Check.Error import DDC.Core.Collect-import DDC.Core.Predicates-import DDC.Core.Compounds import DDC.Core.Pretty-import DDC.Core.Exp+import DDC.Core.Exp.Annot import DDC.Type.Check.Context import DDC.Type.Check                           (Config (..), configOfProfile) import DDC.Type.Env                             (KindEnv, TypeEnv)@@ -58,13 +56,15 @@ 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 ((<$>))  --- | Type checker monad. +-- | Type checker monad. --   Used to manage type errors.-type CheckM a n   +type CheckM a n         = G.CheckM (CheckTrace, Int, Int) (Error a n)  -- | Allocate a new existential.@@ -83,9 +83,28 @@         return  (Pos pos)  +-- | Apply the checker context to a type.+applyContext :: Ord n => Context n -> Type n -> CheckM a n (Type n)+applyContext ctx tt+ = case applyContextEither ctx Set.empty tt of+        Left  (tExt, tBind)       +                -> throw $ ErrorType $ T.ErrorInfinite tExt tBind+        Right t -> return t+++-- | Substitute solved constraints into a type.+applySolved :: Ord n => Context n -> Type n -> CheckM a n (Type n)+applySolved ctx tt+ = case applySolvedEither ctx Set.empty tt of+        Left  (tExt, tBind)+                -> throw $ ErrorType $ T.ErrorInfinite tExt tBind+        Right t -> return t+++ -- CheckTrace ----------------------------------------------------------------- -- | Human readable trace of the type checker.-data CheckTrace +data CheckTrace         = CheckTrace         { checkTraceDoc :: Doc } @@ -94,9 +113,9 @@  instance Monoid CheckTrace where  mempty = CheckTrace empty- +  mappend ct1 ct2-        = CheckTrace +        = CheckTrace         { checkTraceDoc = checkTraceDoc ct1 <> checkTraceDoc ct2 }  @@ -122,15 +141,15 @@         -> 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 + = 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) +checkTypeM+        :: (Ord n, Show n, Pretty n)         => Config n             -- ^ Checker configuration.         -> KindEnv n            -- ^ Global kind environment.         -> Context n            -- ^ Local context.@@ -140,24 +159,24 @@         -> 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 + = 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 ++        -- 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               +         Left err           -> throw $ ErrorType err -         Right (t, k, ctx')     +         Right (t, k, ctx')           -> return (t, k, ctx') 

@@ -19,7 +19,6 @@         | ErrorData         { errorData             :: T.ErrorData n } -         -- Module -----------------------------------------         -- | Exported value is undefined.         | ErrorExportUndefined@@ -40,6 +39,10 @@         | 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 }@@ -58,7 +61,7 @@         -- | An undefined type variable.         | ErrorUndefinedVar         { errorAnnot            :: a-        , errorBound            :: Bound n +        , errorBound            :: Bound n         , errorUniverse         :: Universe }  @@ -81,7 +84,7 @@         | ErrorAppNotFun         { errorAnnot            :: a         , errorChecking         :: Exp a n-        , errorNotFunType       :: Type n } +        , errorNotFunType       :: Type n }          -- | Cannot infer type of polymorphic expression.         | ErrorAppCannotInferPolymorphic@@ -93,10 +96,10 @@         --   already in the environment.         | ErrorLamShadow         { errorAnnot            :: a-        , errorChecking         :: Exp a n +        , errorChecking         :: Exp a n         , errorBind             :: Bind n } -        -- | An abstraction where the body has a visible side effect that +        -- | An abstraction where the body has a visible side effect that         --   is not supported by the current language fragment.         | ErrorLamNotPure         { errorAnnot            :: a@@ -104,19 +107,11 @@         , errorUniverse         :: Universe         , errorEffect           :: Effect n } -        -- | An abstraction where the body has a visible closure that -        --   is not supported by the current language fragment.-        | ErrorLamNotEmpty-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorUniverse         :: Universe-        , errorClosure          :: Closure n }-         -- | A value function where the parameter does not have data         --   or witness kind.         | ErrorLamBindBadKind         { errorAnnot            :: a-        , errorChecking         :: Exp a n +        , errorChecking         :: Exp a n         , errorType             :: Type n         , errorKind             :: Kind n } @@ -133,7 +128,7 @@         { errorAnnot            :: a         , errorChecking         :: Exp a n         , errorBind             :: Bind n }-        +         -- | A type abstraction without a kind annotation on the parameter.         | ErrorLAMParamUnannotated         { errorAnnot            :: a@@ -176,7 +171,7 @@         --   a lambda abstraction.         | ErrorLetrecBindingNotLambda         { errorAnnot            :: a-        , errorChecking         :: Exp a n +        , errorChecking         :: Exp a n         , errorExp              :: Exp a n }          -- | A recursive let-binding with a missing type annotation.@@ -217,7 +212,7 @@         , errorBinds            :: [Bind n]         , errorType             :: Type n } -        -- | A letregion-expression that tried to create a witness with an +        -- | A letregion-expression that tried to create a witness with an         --   invalid type.         | ErrorLetRegionWitnessInvalid         { errorAnnot            :: a@@ -240,23 +235,6 @@         , errorBindWitness      :: Bind  n }  -        -- Withregion --------------------------------------        -- | A withregion-expression where the handle does not have region kind.-        | ErrorWithRegionNotRegion-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBound            :: Bound n-        , errorKind             :: Kind n }--        -- | A letregion-expression where some of the the bound region variables-        --   are free in the type of the body.-        | ErrorWithRegionFree-        { errorAnnot            :: a-        , errorChecking         :: Exp a n-        , errorBound            :: Bound n-        , errorType             :: Type n }--         -- Witnesses --------------------------------------         -- | A witness application where the argument type does not match         --   the parameter type.@@ -273,15 +251,6 @@         , errorNotFunType       :: Type n         , errorArgType          :: Type n } -        -- | An invalid witness join.-        | ErrorCannotJoin-        { errorAnnot            :: a-        , errorWitness          :: Witness a n-        , errorWitnessLeft      :: Witness a n-        , errorTypeLeft         :: Type n-        , errorWitnessRight     :: Witness a n-        , errorTypeRight        :: Type n }-         -- | A witness provided for a purify cast that does not witness purity.         | ErrorWitnessNotPurity         { errorAnnot            :: a@@ -289,14 +258,7 @@         , errorWitness          :: Witness a n         , errorType             :: Type n } -        -- | A witness provided for a forget cast that does not witness emptiness.-        | ErrorWitnessNotEmpty-        { 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@@ -308,7 +270,7 @@         --   of data type declarations.         | ErrorCaseScrutineeTypeUndeclared         { errorAnnot            :: a-        , errorChecking         :: Exp a n +        , errorChecking         :: Exp a n         , errorTypeScrutinee    :: Type n }          -- | A case-expression with no alternatives.@@ -348,7 +310,7 @@         | ErrorCaseCannotInstantiate         { errorAnnot            :: a         , errorChecking         :: Exp a n-        , errorTypeScrutinee    :: Type n +        , errorTypeScrutinee    :: Type n         , errorTypeCtor         :: Type n }          -- | A case-expression where the type of the scrutinee does not match

@@ -8,16 +8,16 @@ import DDC.Type.Universe  -instance (Pretty a, Show n, Eq n, Pretty n) +instance (Pretty a, Show n, Eq n, Pretty n)        => Pretty (Error a n) where  ppr err   = case err of-        ErrorType err'  +        ErrorType err'          -> ppr err'          ErrorData err'          -> ppr err'-        +         -- Modules ---------------------------------------         ErrorExportUndefined n          -> vcat [ text "Exported name '" <> ppr n <> text "' is undefined." ]@@ -25,7 +25,7 @@         ErrorExportDuplicate n          -> vcat [ text "Duplicate exported name '" <> ppr n <> text "'."] -        ErrorExportMismatch n tExport tDef +        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@@ -34,8 +34,15 @@         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." ]+         -> vcat [ text "Imported value '"+                        <> ppr n +                        <> text "' does not have kind Data." ]           -- Exp --------------------------------------------@@ -78,12 +85,12 @@         -- Application ------------------------------------         ErrorAppMismatch a xx t1 t2          -> vcat [ ppr a-                 , text "Type mismatch in application." +                 , 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"@@ -108,21 +115,13 @@                  , text "with: "                        <> align (ppr xx) ]          ErrorLamNotPure a xx universe eff-         -> vcat +         -> vcat                 [ ppr a                 , text "Impure" <+> ppr universe <+> text "abstraction"                 , text "           has effect: "       <> ppr eff                 , empty                 , text "with: "                        <> align (ppr xx) ] -        ErrorLamNotEmpty a xx universe eff-         -> vcat -                [ ppr a-                , text "Non-empty" <+> ppr universe <+> text "abstraction"-                , text "           has closure: "       <> ppr eff-                , empty-                , text "with: "                        <> align (ppr xx) ]-                          ErrorLamBindBadKind a xx t1 k1          -> vcat [ ppr a                  , text "Function parameter has invalid kind."@@ -145,7 +144,7 @@         ErrorLamParamUnannotated a xx b1          -> vcat [ ppr a                  , text "Missing type annotation on function parameter."-                 , text "             With paramter: " <> ppr b1 +                 , text "             With paramter: " <> ppr b1                  , empty                  , text "with: "                        <> align (ppr xx) ] @@ -203,7 +202,7 @@          ErrorLetrecMissingAnnot a b xx          -> vcat [ ppr a-                 , text "Missing or incomplete type annotation on recursive let-binding '" +                 , text "Missing or incomplete type annotation on recursive let-binding '"                         <> ppr (binderOfBind b) <> text "'."                  , text "Recursive functions must have full type annotations."                  , empty@@ -223,7 +222,7 @@                  , 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" +                 , text "       but they must all be: Region"                  , empty                  , text "with: "                         <> align (ppr xx) ] @@ -242,7 +241,7 @@                  , 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."@@ -255,7 +254,7 @@          -> vcat [ ppr a                  , text "Conflicting witness types with private."                  , text "      Witness binding: "       <> ppr b1-                 , text "       conflicts with: "       <> ppr b2 +                 , text "       conflicts with: "       <> ppr b2                  , empty                  , text "with: "                        <> align (ppr xx) ] @@ -266,27 +265,8 @@                  , text "  but witness type is: "       <> ppr b2                  , empty                  , text "with: "                        <> align (ppr xx) ]-                  -        -- Withregion --------------------------------------        ErrorWithRegionFree a xx u t-         -> vcat [ ppr a-                 , text "Region handle escapes scope of withregion."-                 , text "         The region handle: "   <> ppr u-                 , text "  is used in the body type: "   <> ppr t-                 , empty-                 , text "with: "                         <> align (ppr xx) ] -        ErrorWithRegionNotRegion a xx u k-         -> vcat [ ppr a-                 , text "Withregion handle does not have region kind."-                 , text "   Region var or ctor: "       <> ppr u-                 , text "             has kind: "       <> ppr k-                 , text "       but it must be: Region"-                 , empty-                 , text "with: "                        <> align (ppr xx) ]--         -- Witnesses --------------------------------------         ErrorWAppMismatch a ww t1 t2          -> vcat [ ppr a@@ -304,16 +284,6 @@                  , empty                  , text "with: "                        <> align (ppr ww) ] -        ErrorCannotJoin a ww w1 t1 w2 t2-         -> vcat [ ppr a-                 , text "Cannot join witnesses."-                 , text "          Cannot join: "       <> ppr w1-                 , text "              of type: "       <> ppr t1-                 , text "         with witness: "       <> ppr w2-                 , text "              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."@@ -322,15 +292,7 @@                  , empty                  , text "with: "                        <> align (ppr xx) ] -        ErrorWitnessNotEmpty a xx w t-         -> vcat [ ppr a-                 , text "Witness for a forget does not witness emptiness."-                 , text "        Witness: "             <> ppr w-                 , text "       has type: "             <> ppr t-                 , empty-                 , text "with: "                        <> align (ppr xx) ] -         -- Case Expressions -------------------------------         ErrorCaseScrutineeNotAlgebraic a xx tScrutinee          -> vcat [ ppr a@@ -338,7 +300,7 @@                  , 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."@@ -355,7 +317,7 @@         ErrorCaseNonExhaustive a xx ns          -> vcat [ ppr a                  , text "Case alternatives are non-exhaustive."-                 , text " Constructors not matched: "   +                 , text " Constructors not matched: "                         <> (sep $ punctuate comma $ map ppr ns)                  , empty                  , text "with: "                        <> align (ppr xx) ]@@ -376,10 +338,10 @@          -> vcat [ ppr a                  , text "Pattern has more binders than there are fields in the constructor."                  , text "     Contructor: " <> ppr uCtor-                 , text "            has: " <> ppr iCtorFields      +                 , text "            has: " <> ppr iCtorFields                                             <+> text "fields"-                 , text "  but there are: " <> ppr iPatternFields   -                                           <+> text "binders in the pattern" +                 , text "  but there are: " <> ppr iPatternFields+                                           <+> text "binders in the pattern"                  , empty                  , text "with: "                        <> align (ppr xx) ] @@ -426,7 +388,7 @@                  , 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."

@@ -3,17 +3,17 @@ --   The algorithm is based on: --    Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism. --    Joshua Dunfield, Neelakantan R. Krishnaswami, ICFP 2013.---  +-- --   Extensions include: --    * Check let-bindings and case-expressions. --    * Allow type annotations on function parameters. --    * Allow explicit type abstraction and application. --    * Infer the kinds of type parameters.---    * Insert type applications in the checked expression, so that the +--    * Insert type applications in the checked expression, so that the --      resulting program can be checked by the standard bottom-up algorithm.---    * Allow explicit hole '?' annotations to indicate a type or kind +--    * Allow explicit hole '?' annotations to indicate a type or kind --      that should be inferred.--- +-- module DDC.Core.Check.Exp         ( -- * Checker configuation.           Config (..)@@ -21,6 +21,7 @@           -- * Pure checking.         , AnTEC         (..)         , Mode          (..)+        , Demand        (..)         , Context         , emptyContext         , checkExp@@ -31,10 +32,7 @@         , makeTable         , CheckM         , checkExpM-        , CheckTrace    (..)--          -- * Tagged closures.-        , TaggedClosure(..))+        , CheckTrace    (..)) where import DDC.Core.Check.Judge.Type.VarCon import DDC.Core.Check.Judge.Type.LamT@@ -48,73 +46,70 @@ import DDC.Core.Check.Judge.Type.Witness import DDC.Core.Check.Judge.Type.Base import DDC.Core.Transform.MapT-import Data.Monoid                      hiding ((<>)) import qualified DDC.Type.Env           as Env   -- Wrappers ---------------------------------------------------------------------- | Type check an expression. +-- | Type check an expression. -----   If it's good, you get a new version with types attached every AST node, +--   If it's good, you get a new version with types attached every AST node, --   as well as every binding occurrence of a variable. -- --   If it's bad, you get a description of the error. -----   The kinds and types of primitives are added to the environments ---   automatically, you don't need to supply these as part of the starting +--   The kinds and types of primitives are added to the environments+--   automatically, you don't need to supply these as part of the starting --   kind and type environment. ---checkExp -        :: (Ord n, Show n, Pretty n)+checkExp+        :: (Show a, Ord n, Show n, Pretty n)         => Config n                     -- ^ Static configuration.         -> KindEnv n                    -- ^ Starting kind environment.         -> TypeEnv n                    -- ^ Starting type environment.-        -> Exp a n                      -- ^ Expression to check.         -> Mode  n                      -- ^ Check mode.-        -> ( Either (Error a n)         --   Type error message. +        -> Demand                       -- ^ Demand placed on the expression.+        -> Exp a n                      -- ^ Expression to check.+        -> ( Either (Error a n)         --   Type error message.                     ( Exp (AnTEC a n) n --   Expression with type annots                     , Type n            --   Type of expression.-                    , Effect n          --   Effect of expression.-                    , Closure n)        --   Closure of expression.+                    , Effect n)         --   Effect of expression.            , CheckTrace)                --   Type checker debug trace. -checkExp !config !kenv !tenv !xx !mode+checkExp !config !kenv !tenv !mode !demand !xx  = (result, ct)- where  + where   ((ct, _, _), result)-   = runCheck (mempty, 0, 0) +   = runCheck (mempty, 0, 0)    $ do         -- Check the expression, using the monadic checking function.-        (xx', t, effs, clos, ctx) -         <- checkExpM +        (xx', t, effs, ctx)+         <- checkExpM                 (makeTable config                         (Env.union kenv (configPrimKinds config))                         (Env.union tenv (configPrimTypes config)))-                emptyContext xx mode-                +                emptyContext mode demand xx +         -- Apply the final context to the annotations in expressions.         -- This ensures that existentials are expanded to solved types.-        let applyToAnnot (AnTEC t0 e0 c0 x0)-                = AnTEC (applySolved ctx t0)-                        (applySolved ctx e0)-                        (applySolved ctx c0)-                        x0+        let applyToAnnot (AnTEC t0 e0 _ x0)+             = do t0' <- applySolved ctx t0+                  e0' <- applySolved ctx e0+                  return $ AnTEC t0' e0' (tBot kClosure) x0 -        let xx'' = reannotate applyToAnnot -                 $ mapT (applySolved ctx) xx'+        xx_solved <- mapT (applySolved ctx) xx'+        xx_annot  <- reannotateM applyToAnnot xx_solved -        -- Also apply the final context to the overall type, +        -- Also apply the final context to the overall type,         -- effect and closure of the expression.-        let t'   = applySolved ctx t-        let e'   = applySolved ctx $ TSum effs-        let c'   = applySolved ctx $ closureOfTaggedSet clos+        t'      <- applySolved ctx t+        e'      <- applySolved ctx $ TSum effs -        return  (xx'', t', e', c')+        return  (xx_annot, t', e')   -- | Like `checkExp`, but only return the value type of an expression.-typeOfExp -        :: (Ord n, Pretty n, Show n)+typeOfExp+        :: (Show a, Ord n, Pretty n, Show n)         => Config n                     -- ^ Static configuration.         -> KindEnv n                    -- ^ Starting Kind environment         -> TypeEnv n                    -- ^ Starting Type environment.@@ -122,42 +117,41 @@         -> Either (Error a n) (Type n)  typeOfExp !config !kenv !tenv !xx- = case fst $ checkExp config kenv tenv xx Recon of-        Left err           -> Left err-        Right (_, t, _, _) -> Right t+ = case fst $ checkExp config kenv tenv Recon DemandNone xx of+        Left err        -> Left err+        Right (_, t, _) -> Right t   -- Monadic Checking ----------------------------------------------------------- -- | Like `checkExp` but using the `CheckM` monad to handle errors.-checkExpM -        :: (Show n, Pretty n, Ord n)+checkExpM+        :: (Show a, Show n, Pretty n, Ord n)         => Table a n                    -- ^ Static config.         -> Context n                    -- ^ Input context.-        -> Exp a n                      -- ^ Expression to check.         -> Mode n                       -- ^ Check mode.-        -> CheckM a n +        -> Demand                       -- ^ Demand placed on the expression.+        -> Exp a n                      -- ^ Expression to check.+        -> CheckM a n                 ( Exp (AnTEC a n) n     -- Annotated expression.                 , Type n                -- Output type.                 , TypeSum n             -- Output effect-                , Set (TaggedClosure n) -- Output closure                 , Context n)            -- Output context.  -- Dispatch to the checker table based on what sort of AST node we're at.-checkExpM !table !ctx !xx !mode+checkExpM !table !ctx !mode !demand !xx   = case xx of-    XVar{}                 -> tableCheckVarCon     table table ctx xx mode-    XCon{}                 -> tableCheckVarCon     table table ctx xx mode-    XApp _ _ XType{}       -> tableCheckAppT       table table ctx xx mode-    XApp{}                 -> tableCheckAppX       table table ctx xx mode-    XLAM{}                 -> tableCheckLamT       table table ctx xx mode-    XLam{}                 -> tableCheckLamX       table table ctx xx mode-    XLet _ LPrivate{} _    -> tableCheckLetPrivate table table ctx xx mode-    XLet _ LWithRegion{} _ -> tableCheckLetPrivate table table ctx xx mode-    XLet{}                 -> tableCheckLet        table table ctx xx mode-    XCase{}                -> tableCheckCase       table table ctx xx mode-    XCast{}                -> tableCheckCast       table table ctx xx mode-    XWitness{}             -> tableCheckWitness    table table ctx xx mode-    XType    a _           -> throw $ ErrorNakedType    a xx +    XVar{}              -> tableCheckVarCon     table table ctx mode demand xx+    XCon{}              -> tableCheckVarCon     table table ctx mode demand xx+    XApp _ _ XType{}    -> tableCheckAppT       table table ctx mode demand xx+    XApp{}              -> tableCheckAppX       table table ctx mode demand xx+    XLAM{}              -> tableCheckLamT       table table ctx mode demand xx+    XLam{}              -> tableCheckLamX       table table ctx mode demand xx+    XLet _ LPrivate{} _ -> tableCheckLetPrivate table table ctx mode demand xx+    XLet{}              -> tableCheckLet        table table ctx mode demand xx+    XCase{}             -> tableCheckCase       table table ctx mode demand xx+    XCast{}             -> tableCheckCast       table table ctx mode demand xx+    XWitness{}          -> tableCheckWitness    table table ctx mode demand xx+    XType    a _        -> throw $ ErrorNakedType    a xx   -- Table ----------------------------------------------------------------------@@ -176,6 +170,6 @@         , tableCheckLet         = checkLet         , tableCheckLetPrivate  = checkLetPrivate         , tableCheckCase        = checkCase-        , tableCheckCast        = checkCast +        , tableCheckCast        = checkCast         , tableCheckWitness     = checkWit } 

@@ -3,12 +3,12 @@         (makeEq) where import DDC.Core.Check.Base-import DDC.Type.Transform.Crush-import DDC.Type.Transform.Trim+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)+makeEq  :: (Eq n, Ord n, Pretty n, Show n)         => Config n         -> a         -> Context n@@ -25,11 +25,11 @@  = do   let Just ctx1   = updateExists [] iL tR ctx0          ctrace  $ vcat-                [ text "* EqLSolve"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1+                [ text "**  EqLSolve"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1                 , empty ]          return ctx1@@ -41,11 +41,11 @@  = do   let Just ctx1   = updateExists [] iR tL ctx0          ctrace  $ vcat-                [ text "* EqRSolve"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1+                [ text "**  EqRSolve"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1                 , empty ]          return ctx1@@ -59,13 +59,13 @@  , 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 2 $ ppr ctx0-                , indent 2 $ ppr ctx1++        ctrace  $ vcat+                [ text "**  EqLReach"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1                 , empty ]          return ctx1@@ -79,12 +79,12 @@  , lR > lL  = do   let Just ctx1   = updateExists [] iL tR ctx0 -        ctrace  $ vcat -                [ text "* EqRReach"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1+        ctrace  $ vcat+                [ text "**  EqRReach"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1                 , empty ]          return ctx1@@ -94,12 +94,12 @@  | TVar u1      <- tL  , TVar u2      <- tR  , u1 == u2- = do   + = do         ctrace  $ vcat-                [ text "* EqVar"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0+                [ text "**  EqVar"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0                 , empty ]          return ctx0@@ -109,64 +109,69 @@  | TCon tc1     <- tL  , TCon tc2     <- tR  , equivTyCon tc1 tc2- = do   + = do         ctrace  $ vcat-                [ text "* EqCon"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0+                [ text "**  EqCon"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0                 , empty ]          return ctx0  - -- EqFun- | Just (tL1, tEffL, tCloL, tL2) <- takeTFunEC tL- , Just (tR1, tEffR, tCloR, tR2) <- takeTFunEC tR- = do   -        ctx1    <- makeEq config a ctx0 tL1 tR1 err-        ctx2    <- makeEq config a ctx1 (crushEffect tEffL) (crushEffect tEffR) err-        -        let Just tCloL' = trimClosure tCloL-        let Just tCloR' = trimClosure tCloR-        ctx3    <- makeEq config a ctx2 tCloL' tCloR' err--        ctx4    <- makeEq config a ctx3 tL2 tR2 err-        return ctx4--  -- EqApp  | TApp tL1 tL2 <- tL  , TApp tR1 tR2 <- tR  = do-        ctx1     <- makeEq config a ctx0 tL1 tR1 err-        let tL2' = applyContext ctx1 tL2-        let tR2' = applyContext ctx1 tR2-        ctx2     <- makeEq config a ctx1 tL2' tR2' err+        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 2 $ ppr ctx0-                , indent 2 $ ppr ctx2+                [ 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- =      return ctx0+ | equivT tL tR + = do   ctrace  $ vcat+                [ text "**  EqEquiv" ] +        return ctx0++  -- Error  | otherwise- = do   ctrace  $ vcat-                [ text "DDC.Core.Check.Exp.Inst.makeEq: no match" -                , text "  LEFT:   " <> ppr tL-                , text "  RIGHT:  " <> ppr tR -                , text "  LEFTC:  " <> (ppr $ crushSomeT tL)-                , text "  RIGHTC: " <> (ppr $ crushSomeT tR)+ = 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 

@@ -24,11 +24,11 @@  = do   let Just ctx1   = updateExists [] iL tR ctx0          ctrace  $ vcat-                [ text "* InstLSolve"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1+                [ text "**  InstLSolve"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1                 , empty ]          return ctx1@@ -42,13 +42,13 @@  , Just iR <- takeExists tR,    Just lR <- locationOfExists iR ctx0  , lL > lR  = do   let Just ctx1   = updateExists [] iR tL ctx0-        -        ctrace  $ vcat -                [ text "* InstLReach"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1++        ctrace  $ vcat+                [ text "**  InstLReach"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1                 , empty ]          return ctx1@@ -62,12 +62,12 @@  , lR > lL  = do   let Just ctx1   = updateExists [] iL tR ctx0 -        ctrace  $ vcat -                [ text "* InstRReach"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1+        ctrace  $ vcat+                [ text "**  InstRReach"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1                 , empty ]          return ctx1@@ -79,30 +79,30 @@  , Just (tR1, tR2)      <- takeTFun tR  = do         -- Make new existentials to match the function type and parameter.-        iL1             <- newExists kData-        let tL1         =  typeOfExists iL1 +        iL1     <- newExists kData+        let tL1 =  typeOfExists iL1 -        iL2             <- newExists kData-        let tL2         =  typeOfExists iL2+        iL2     <- newExists kData+        let tL2 =  typeOfExists iL2          -- Update the context with the new constraint.         let Just ctx1   =  updateExists [iL2, iL1] iL (tFun tL1 tL2) ctx0          -- Instantiate the parameter type.-        ctx2            <- makeInst config a ctx1 tR1 tL1 err+        ctx2    <- makeInst config a ctx1 tR1 tL1 err          -- Substitute into tR2-        let tR2'        =  applyContext ctx2 tR2+        tR2'    <- applyContext ctx2 tR2          -- Instantiate the return type.-        ctx3            <- makeInst config a ctx2 tL2 tR2' err+        ctx3    <- makeInst config a ctx2 tL2 tR2' err          ctrace  $ vcat-                [ text "* InstLArr"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx3 +                [ text "**  InstLArr"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx3                 , empty ]          return ctx3@@ -114,11 +114,11 @@  = do   let Just ctx1   = updateExists [] iR tL ctx0          ctrace  $ vcat-                [ text "* InstRSolve"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1+                [ text "**  InstRSolve"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1                 , empty ]          return ctx1@@ -128,32 +128,32 @@  --  Left is an function arrow, and right is an existential.  | Just (tL1, tL2)      <- takeTFun tL  , Just iR              <- takeExists tR- = do   + = do         -- Make new existentials to match the function type and parameter.-        iR1             <- newExists kData-        let tR1         =  typeOfExists iR1 +        iR1     <- newExists kData+        let tR1 =  typeOfExists iR1 -        iR2             <- newExists kData-        let tR2         =  typeOfExists iR2+        iR2     <- newExists kData+        let tR2 =  typeOfExists iR2          -- Update the context with the new constraint.         let Just ctx1   =  updateExists [iR2, iR1] iR (tFun tR1 tR2) ctx0          -- Instantiate the parameter type.-        ctx2            <- makeInst config a ctx1 tR1 tL1 err+        ctx2    <- makeInst config a ctx1 tR1 tL1 err          -- Substitute into tL2-        let tL2'        = applyContext ctx2 tL2+        tL2'    <- applyContext ctx2 tL2          -- Instantiate the return type.-        ctx3            <- makeInst config a ctx2 tL2' tR2 err+        ctx3    <- makeInst config a ctx2 tL2' tR2 err          ctrace  $ vcat-                [ text "* InstRArr"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx3 +                [ text "**  InstRArr"+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx3                 , empty ]          return ctx3@@ -162,7 +162,7 @@  | otherwise  = do         ctrace  $ vcat-                [ text "DDC.Core.Check.Exp.Inst.inst: no match" +                [ text "DDC.Core.Check.Exp.Inst.inst: no match"                 , text "  LEFT:  " <> ppr tL                 , text "  RIGHT: " <> ppr tR                 , indent 2 $ ppr ctx0

@@ -3,7 +3,7 @@         ( makeSub) where import DDC.Type.Transform.SubstituteT-import DDC.Core.Annot.AnTEC+import DDC.Core.Exp.Annot.AnTEC import DDC.Core.Check.Judge.Eq import DDC.Core.Check.Judge.Inst import DDC.Core.Check.Base@@ -19,7 +19,7 @@         -> Type n         -> Type n         -> Error a n-        -> CheckM a n +        -> CheckM a n                 ( Exp (AnTEC a n) n                 , Context n) @@ -33,12 +33,13 @@  | TCon tc1     <- tL  , TCon tc2     <- tR  , equivTyCon tc1 tc2- = do   + = do         ctrace  $ vcat-                [ text "* SubCon"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0+                [ text "**  SubCon"+                , text "    xL: " <> ppr xL+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , indent 4 $ ppr ctx0                 , empty ]          return (xL, ctx0)@@ -49,12 +50,13 @@  | TVar u1      <- tL  , TVar u2      <- tR  , u1 == u2- = do   + = do         ctrace  $ vcat-                [ text "* SubVar"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0+                [ text "**  SubVar"+                , text "    xL: " <> ppr xL+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , indent 4 $ ppr ctx0                 , empty ]          return (xL, ctx0)@@ -65,32 +67,45 @@  | Just iL <- takeExists tL  , Just iR <- takeExists tR  , iL == iR- = do   + = do         ctrace  $ vcat-                [ text "* SubExVar"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0 +                [ text "**  SubExVar"+                , text "    xL: " <> ppr xL+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , indent 4 $ ppr ctx0                 , empty ]          return (xL, ctx0)  + -- SubEquiv+ --  Both sides are equivalent+ | equivT tL tR+ = do+        ctrace  $ vcat+                [ text "**  SubEquiv"+                , text "    xL: " <> ppr xL+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , indent 4 $ ppr ctx0+                , empty ]++        return (xL, ctx0)++  -- SubInstL  --  Left is an existential.- --- --  ISSUE #326: Do free variables check in new inferencer.- --    check  tL /= FV(tR)- --  | isTExists tL  = do   ctx1    <- makeInst config a ctx0 tR tL err          ctrace  $ vcat-                [ text "* SubInstL"-                , text "  LEFT:   " <> ppr tL-                , text "  RIGHT:  " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1+                [ text "**  SubInstL"+                , text "    xL: " <> ppr xL+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1                 , empty ]          return (xL, ctx1)@@ -98,19 +113,16 @@   -- SubInstR  --  Right is an existential.- --- --  ISSUE #326: Do free variables check in new inferencer.- --     check  tR /= FV(tL)- --  | isTExists tR  = do   ctx1    <- makeInst config a ctx0 tL tR err          ctrace  $ vcat-                [ text "* SubInstR"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1 +                [ text "**  SubInstR"+                , text "    xL: " <> ppr xL+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1                 , empty ]          return (xL, ctx1)@@ -120,42 +132,52 @@  --  Both sides are arrow types.  | Just (tL1, tL2)  <- takeTFun tL  , Just (tR1, tR2)  <- takeTFun tR- = do   -        (_, ctx1)   <- makeSub config a ctx0 xL tR1 tL1 err-        let tL2'    =  applyContext  ctx1    tL2-        let tR2'    =  applyContext  ctx1    tR2-        (_, ctx2)   <- makeSub config a ctx1 xL tL2' tR2' err+ = do+        ctrace  $ vcat+                [ text "*>  SubArr"+                , empty ] +        (_, ctx1) <- makeSub config a ctx0 xL tR1 tL1 err+        tL2'      <- applyContext     ctx1 tL2+        tR2'      <- applyContext     ctx1 tR2+        (_, ctx2) <- makeSub config a ctx1 xL tL2' tR2' err+         ctrace  $ vcat-                [ text "* SubArr"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1-                , indent 2 $ ppr ctx2 +                [ text "*<  SubArr"+                , text "    xL: " <> ppr xL+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1+                , indent 4 $ ppr ctx2                 , empty ]          return (xL, ctx2)  - -- SubApp + -- SubApp  --   Both sides are type applications.  --   Assumes non-function type constructors are invariant.  | TApp tL1 tL2 <- tL  , TApp tR1 tR2 <- tR- = do   -        ctx1     <- makeEq config a ctx0 tL1 tR1 err-        let tL2' =  applyContext ctx1 tL2-        let tR2' =  applyContext ctx1 tR2-        ctx2     <- makeEq config a ctx1 tL2' tR2' err+ = do+        ctrace  $ vcat+                [ text "*>  SubApp"+                , 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 "* SubApp"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1-                , indent 2 $ ppr ctx2 +                [ text "*<  SubApp"+                , text "    xL: " <> ppr xL+                , text "    tL: " <> ppr tL+                , text "    tR: " <> ppr tR+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1+                , indent 4 $ ppr ctx2                 , empty ]          return (xL, ctx2)@@ -164,49 +186,56 @@  -- SubForall  --   Left side is a forall type.  | TForall b t1 <- tL- = do   + = do+        ctrace  $ vcat+                [ text "*>  SubForall"+                , empty ]+         -- Make a new existential to instantiate the quantified-        -- variable and substitute it into the body. +        -- variable and substitute it into the body.         iA        <- newExists (typeOfBind b)         let tA    = typeOfExists iA         let t1'   = substituteT b tA t1 -        -- Check the new body against the right type, +        -- Check the new body against the right type,         -- so that the existential we just made is instantiated         -- to match the right.         let (ctx1, pos1) =  markContext ctx0         let ctx2         =  pushExists  iA ctx1-        (xL1, ctx3)      <- makeSub config a ctx2 xL t1' tR err +        -- Wrap the expression with a type application to cause+        -- the instantiation.+        let AnTEC _ e0 c0 _+                 = annotOfExp xL+        let aFn  = AnTEC t1' (substituteT b tA e0) (substituteT b tA c0) a+        let aArg = AnTEC (typeOfBind b) (tBot kEffect) (tBot kClosure) a+        let xL1  = XApp aFn xL (XType aArg tA)++        (xL2, ctx3) <- makeSub config a ctx2 xL1 t1' tR err+         -- Pop the existential and constraints above it back off         -- the stack.         let ctx4  = popToPos pos1 ctx3          ctrace  $ vcat-                [ text "* SubForall"-                , text "  LEFT:  " <> ppr tL-                , text "  RIGHT: " <> ppr tR-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx4 +                [ text "*<  SubForall"+                , text "    xL:    " <> ppr xL+                , text "    LEFT:  " <> ppr tL+                , text "    RIGHT: " <> ppr tR+                , text "    xL2:   " <> ppr xL2+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx4                 , empty ] -        -- Wrap the expression with a type application to cause-        -- the instantiation.-        let AnTEC _ e0 c0 _    -                 = annotOfExp xL-        let aFn  = AnTEC t1' (substituteT b tA e0) (substituteT b tA c0) a-        let aArg = AnTEC (typeOfBind b) (tBot kEffect) (tBot kClosure) a-        let xL2  = XApp aFn xL1 (XType aArg tA) -         return (xL2, ctx4)    -- Error  | otherwise  = do   ctrace  $ vcat-                [ text "DDC.Core.Check.Exp.Inst.makeSub: no match" -                , text "  LEFT:   " <> text (show tL)-                , text "  RIGHT:  " <> text (show tR) ]+                [ text "DDC.Core.Check.Exp.Inst.makeSub: no match"+                , text "  LEFT:   " <> ppr tL+                , text "  RIGHT:  " <> ppr tR ]          throw err 

@@ -4,27 +4,24 @@ where import DDC.Core.Check.Judge.Type.Sub import DDC.Core.Check.Judge.Type.Base-import qualified Data.Set       as Set   -- | Check a spec application. checkAppT :: Checker a n -checkAppT !table !ctx0 xx@(XApp aApp xFn (XType aArg tArg)) Recon- = do   let config      = tableConfig table+checkAppT !table !ctx0 Recon demand+        xx@(XApp aApp xFn (XType aArg tArg))+ = do   +        let config      = tableConfig table         let kenv        = tableKindEnv table          -- Check the functional expression.-        (xFn', tFn, effsFn, closFn, ctx1) -         <- tableCheckExp table table ctx0 xFn Recon+        (xFn', tFn, effsFn, ctx1)+         <- tableCheckExp table table ctx0 Recon demand xFn          -- Check the argument.         (tArg', kArg, ctx2)-         <- checkTypeM config kenv ctx1 UniverseSpec tArg Recon-                        -        -- Take any Use annots from a region arg.-        --  This always matches because we just checked tArg.-        let Just t2_clo = taggedClosureOfTyArg kenv ctx2 tArg'+         <- checkTypeM    config kenv ctx1 UniverseSpec tArg Recon          -- Determine the type of the result.         --  The function must have a quantified type, which we then instantiate@@ -48,7 +45,7 @@         -- thus we can't be sharing objects that have it in its type.          -- Build an annotated version of the type application.-        let aApp' = AnTEC tResult (TSum effsFn)  (closureOfTaggedSet closFn) aApp  +        let aApp' = AnTEC tResult (TSum effsFn)  (tBot kClosure) aApp         let aArg' = AnTEC kArg    (tBot kEffect) (tBot kClosure) aArg         let xx'   = XApp aApp' xFn' (XType aArg' tArg') @@ -64,27 +61,22 @@          returnX aApp                 (\z -> XApp z xFn' (XType aArg' tArg'))-                tResult effsFn (closFn `Set.union` t2_clo)-                ctx2--checkAppT !table !ctx0 xx@(XApp aApp xFn (XType aArg tArg)) Synth- = do   let kenv        = tableKindEnv table+                tResult effsFn ctx2 +checkAppT !table !ctx0 Synth demand +        xx@(XApp aApp xFn (XType aArg tArg))+ = do         -- Check the functional expression.-        (xFn', tFn, effsFn, closFn, ctx1) -         <- tableCheckExp table table ctx0 xFn Synth+        (xFn', tFn, effsFn, ctx1)+         <- tableCheckExp table table ctx0 Synth demand xFn          -- Apply the type argument to the type of the function.+        tFn' <- applyContext ctx1 tFn         (tResult, tArg', kArg, ctx2)-         <- synthAppArgT table aApp xx ctx1 -                (applyContext ctx1 tFn) tArg-        -        -- Take any Use annots from a region arg.-        --  This always matches because we just checked tArg.-        let Just t2_clo = taggedClosureOfTyArg kenv ctx2 tArg'+             <- synthAppArgT table aApp xx ctx1 tFn' tArg          -- Build an annotated version of the type application.-        let aApp' = AnTEC tResult (TSum effsFn)  (closureOfTaggedSet closFn) aApp  +        let aApp' = AnTEC tResult (TSum effsFn)  (tBot kClosure) aApp         let aArg' = AnTEC kArg    (tBot kEffect) (tBot kClosure) aArg         let xx'   = XApp aApp' xFn' (XType aArg' tArg') @@ -100,14 +92,14 @@          returnX aApp                 (\z -> XApp z xFn' (XType aArg' tArg'))-                tResult effsFn (closFn `Set.union` t2_clo)-                ctx2+                tResult effsFn ctx2  -checkAppT !table !ctx0 xx@(XApp aApp _ (XType _ _)) (Check tExpected)- =      checkSub table aApp ctx0 xx tExpected+checkAppT !table !ctx0 (Check tExpected) demand +        xx@(XApp aApp _ (XType _ _)) + =      checkSub table aApp ctx0 demand xx tExpected -checkAppT _ _ _ _+checkAppT _ _ _ _ _  = error "ddc-core.checkAppT: no match"  @@ -132,7 +124,7 @@  -- Rule (AppT Synth exists)  --  Functional type is an existential.  --- --  Although we know the functional part should have a quantified type, + --  Although we know the functional part should have a quantified type,  --  we can't infer a type for the result because we would need to represent  --  a delayed substitution of a type into an existential. The rule would be  --  as follows:@@ -141,7 +133,7 @@  --   -----------------------------------------------------  --      Env0[?0] |- ?0 * t2 => ?2 [t2/a] -| Env1  --- --  .. but we can't represent the (?2 [t2/a]) part. This is an inherent + --  .. but we can't represent the (?2 [t2/a]) part. This is an inherent  --  limitation of our type inference algorithm.  --  | Just _               <- takeExists tFn@@ -149,7 +141,7 @@    -- Rule (AppT Synth Forall)- --  The function already has a quantified type, so we can instantiate it + --  The function already has a quantified type, so we can instantiate it  --  with the supplied type argument.  | TForall b11 t12      <- tFn  = do   let config      = tableConfig table@@ -157,7 +149,7 @@          -- The kind of the argument must match the annotation on the quantifier.         (tArg', kArg, ctx1)-         <- checkTypeM config kenv ctx0 UniverseSpec tArg +         <- checkTypeM config kenv ctx0 UniverseSpec tArg                 (Check (typeOfBind b11))          -- Instantiate the type of the function with the type argument.

@@ -5,115 +5,130 @@ import DDC.Core.Check.Judge.Type.Sub import DDC.Core.Check.Judge.Type.Base import qualified DDC.Type.Sum   as Sum-import qualified Data.Set       as Set   ------------------------------------------------------------------------------- -- | Check a value expression application. checkAppX :: Checker a n -checkAppX !table !ctx xx@(XApp a xFn xArg) Recon- = do   +checkAppX !table !ctx Recon demand+        xx@(XApp a xFn xArg)+ = do         -- Check the functional expression.-        (xFn',  tFn,  effsFn,  closFn,  ctx1) -         <- tableCheckExp table table ctx  xFn Recon+        (xFn',  tFn,  effsFn, ctx1)+         <- tableCheckExp table table ctx  Recon demand xFn          -- Check the argument.-        (xArg', tArg, effsArg, closArg, ctx2) -         <- tableCheckExp table table ctx1 xArg Recon+        (xArg', tArg, effsArg, ctx2)+         <- tableCheckExp table table ctx1 Recon DemandNone xArg          -- The type of the parameter must match that of the argument.         (tResult, effsLatent)          <- case splitFunType tFn of              Just (tParam, effs, _, tResult)-              | tParam `equivT` tArg +              | tParam `equivT` tArg               -> return (tResult, effs) -              | otherwise           +              | otherwise               -> throw  $ ErrorAppMismatch a xx tParam tArg               Nothing               -> throw  $ ErrorAppNotFun a xx tFn          -- Effect of the overall application.-        let effsResult  = Sum.unions kEffect-                        $ [effsFn, effsArg, Sum.singleton kEffect effsLatent]--        -- Closure of the overall application.-        let closResult  = Set.union  closFn closArg+        let effsResult  +                = Sum.unions kEffect+                $ [effsFn, effsArg, Sum.singleton kEffect effsLatent] -        returnX a +        returnX a                 (\z -> XApp z xFn' xArg')-                tResult effsResult closResult +                tResult effsResult                 ctx2  -checkAppX !table !ctx0 xx@(XApp a xFn xArg) Synth- = do   +checkAppX !table !ctx0 Synth demand +        xx@(XApp a xFn xArg)+ = do+        ctrace  $ vcat+                [ text "*>  App Synth"+                , empty ]+         -- Synth a type for the functional expression.-        (xFn', tFn, effsFn, closFn, ctx1) -         <- tableCheckExp table table ctx0 xFn Synth+        (xFn', tFn, effsFn, ctx1)+         <- tableCheckExp table table ctx0 Synth demand xFn          -- Substitute context into synthesised type.-        let tFn' = applyContext ctx1 tFn+        tFn' <- applyContext ctx1 tFn          -- Synth a type for the function applied to its argument.-        (xFn'', xArg', tResult, effsResult, closResult, ctx2)-         <- synthAppArg table a xx ctx1-                xFn' tFn' effsFn closFn -                xArg+        (xResult, tResult, esResult, ctx2)+         <- synthAppArg table a xx ctx1 demand+                xFn' tFn' effsFn xArg          ctrace  $ vcat-                [ text "* App Synth"-                , indent 2 $ ppr xx-                , text "      tFn:  " <> ppr tFn'-                , text "     xArg:  " <> ppr xArg-                , text "  tResult:  " <> ppr tResult-                , ppr ctx0-                , ppr ctx2+                [ text "*<  App Synth"+                , text "    demand  : " <> (text $ show demand)+                , indent 4 $ ppr xx+                , text "    tFn     : " <> ppr tFn'+                , text "    tArg    : " <> ppr xArg+                , text "    xResult : " <> ppr xResult+                , text "    tResult : " <> ppr tResult+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx2                 , empty ] -        returnX a -                (\z -> XApp z xFn'' xArg')-                tResult effsResult closResult -                ctx2+        return  (xResult, tResult, esResult, ctx2)  -checkAppX !table !ctx xx@(XApp a _ _) (Check tEx)- =      checkSub table a ctx xx tEx+checkAppX !table !ctx (Check tExpected) demand +        xx@(XApp a _ _) + = do   +        ctrace  $ vcat+                [ text "*>  App Check"+                , text "    tExpected: " <> ppr tExpected+                , empty ] +        result  <- checkSub table a ctx demand xx tExpected -checkAppX _ _ _ _+        ctrace  $ vcat+                [ text "*<  App Check"+                , empty ]++        return  result   ++checkAppX _ _ _ _ _  = error "ddc-core.checkApp: no match"   ------------------------------------------------------------------------------- -- | Synthesize the type of a function applied to its argument.-synthAppArg -        :: (Show n, Ord n, Pretty n)+synthAppArg+        :: (Show a, Show n, Ord n, Pretty n)         => Table a n-        -> a                             -- Annot for error messages.-        -> Exp a n                       -- Expression for error messages.-        -> Context n                     -- Current context.-        -> Exp (AnTEC a n) n             -- Checked functional expression.-                -> Type n                -- Type of functional expression.-                -> TypeSum n             -- Effect of functional expression.-                -> Set (TaggedClosure n) -- Closure of functional expression.-        -> Exp a n                       -- Function argument.+        -> a                         -- Annot for error messages.+        -> Exp a n                   -- Expression for error messages.+        -> Context n                 -- Current context.+        -> Demand                    -- Demand placed on result of application.+        -> Exp (AnTEC a n) n         -- Checked functional expression.+                -> Type n            -- Type of functional expression.+                -> TypeSum n         -- Effect of functional expression.+        -> Exp a n                   -- Function argument.         -> CheckM a n-                ( Exp (AnTEC a n) n      -- Checked functional expression.-                , Exp (AnTEC a n) n      -- Checked argument   expression.-                , Type n                 -- Type of result.-                , TypeSum n              -- Effect of result.-                , Set (TaggedClosure n)  -- Closure of result.-                , Context n)             -- Result context.+                ( Exp (AnTEC a n) n  -- Checked application.+                , Type n             -- Type of result.+                , TypeSum n          -- Effect of result.+                , Context n)         -- Result context. -synthAppArg table a xx ctx0 xFn tFn effsFn closFn xArg+synthAppArg table a xx ctx0 demand xFn tFn effsFn xArg   -- Rule (App Synth exists)  --  Functional type is an existential.  | Just iFn      <- takeExists tFn- = do   + = do+        ctrace  $ vcat+                [ text "*>  App Synth Exists"+                , empty ]+         -- New existential for the type of the function parameter.         iA1      <- newExists kData         let tA1  = typeOfExists iA1@@ -126,28 +141,39 @@         let Just ctx1 = updateExists [iA2, iA1] iFn (tFun tA1 tA2) ctx0          -- Check the argument under the new context.-        (xArg', _, effsArg, closArg, ctx2)-         <- tableCheckExp table table ctx1 xArg (Check tA1)+        (xArg', _, effsArg, ctx2)+         <- tableCheckExp table table ctx1 (Check tA1) DemandRun xArg          -- Effect and closure of the overall function application.-        let effsResult = effsFn `Sum.union` effsArg-        let closResult = closFn `Set.union` closArg+        let esResult    = effsFn `Sum.union` effsArg +        -- Result expression.+        let xResult    = XApp  (AnTEC tA2 (TSum esResult) (tBot kClosure) a)+                                xFn xArg'+         ctrace  $ vcat-                [ text "* App Synth exists"-                , indent 2 $ ppr xx-                , indent 2 $ ppr ctx2 +                [ text "*<  App Synth Exists"+                , text "    xFn    :"  <> ppr xFn+                , text "    tFn    :"  <> ppr tFn+                , text "    xArg   :"  <> ppr xArg+                , text "    xArg'  :"  <> ppr xArg'+                , text "    xResult:"  <> ppr xResult+                , indent 4 $ ppr xx+                , indent 4 $ ppr ctx2                 , empty ] -        return  ( xFn, xArg'-                , tA2, effsResult, closResult, ctx2)+        return  (xResult, tA2, esResult, ctx2)    -- Rule (App Synth Forall)  --  Function has a quantified type, but we're applying an expression to it.  --  We need to inject a new type argument.  | TForall b tBody      <- tFn- = do   + = do+        ctrace  $ vcat+                [ text "*>  App Synth Forall"+                , empty ]+         -- Make a new existential for the type of the argument,         -- and push it onto the context.         iA         <- newExists (typeOfBind b)@@ -158,78 +184,106 @@         let tBody' = substituteT b tA tBody          -- Add the missing type application.-        --  Because we were applying a function to an expression argument, +        --  Because we were applying a function to an expression argument,         --  and the type of the function was quantified, we know there should         --  be a type application here.-        let aFn    = AnTEC tFn (TSum effsFn) (closureOfTaggedSet closFn) a+        let aFn    = AnTEC tFn (TSum effsFn) (tBot kClosure) a         let aArg   = AnTEC (typeOfBind b) (tBot kEffect) (tBot kClosure) a         let xFnTy  = XApp aFn xFn (XType aArg tA) -        -- Synthesise the result type of a function being applied to its +        -- Synthesise the result type of a function being applied to its         -- argument. We know the type of the function up-front, but we pass         -- in the whole argument expression.-        (xFnTy', xArg', tResult, effsResult, closResult, ctx2)-         <- synthAppArg table a xx ctx1 xFnTy tBody' effsFn closFn xArg+        (xResult, tResult, esResult, ctx2)+         <- synthAppArg table a xx ctx1 demand xFnTy tBody' effsFn xArg +        -- Result expression.+         ctrace  $ vcat-                [ text "* App Synth Forall"-                , text "      xFn:  " <> ppr xFnTy'-                , text "     tArg:  " <> ppr xArg'-                , text "      tFn:  " <> ppr tFn-                , text "  tResult:  " <> ppr tResult-                , indent 2 $ ppr ctx2+                [ text "*<  App Synth Forall"+                , text "    xFn     : " <> ppr xFn+                , text "    tFn     : " <> ppr tFn+                , text "    xArg    : " <> ppr xArg+                , text "    xResult : " <> ppr xResult+                , text "    tResult : " <> ppr tResult+                , indent 4 $ ppr ctx2                 , empty ] -        return  ( xFnTy'-                , xArg'-                , tResult, effsResult, closResult, ctx2)+        return  (xResult, tResult, esResult, ctx2)    -- Rule (App Synth Fun)  --  Function already has a concrete function type.  | Just (tParam, tResult)   <- takeTFun tFn- = do   + = do+        ctrace  $ vcat+                [ text "*>  App Synth Fun"+                , empty ]+         -- Check the argument.-        (xArg', tArg, effsArg, closArg, ctx1) -         <- tableCheckExp table table ctx0 xArg (Check tParam)+        (xArg', tArg, esArg, ctx1)+         <- tableCheckExp table table ctx0 (Check tParam) DemandRun xArg -        let tFn1     = applyContext ctx1 tFn-        let tArg1    = applyContext ctx1 tArg-        let tResult1 = applyContext ctx1 tResult+        tFn'     <- applyContext ctx1 tFn+        tArg'    <- applyContext ctx1 tArg+        tResult' <- applyContext ctx1 tResult          -- Get the type, effect and closure resulting from the application         -- of a function of this type to its argument.-        effsLatent-         <- case splitFunType tFn1 of+        esLatent+         <- case splitFunType tFn' of              Just (_tParam, effsLatent, _closLatent, _tResult)               -> return effsLatent               -- This shouldn't happen because this rule (App Synth Fun) only-             -- applies when 'tFn' is has a functional type, and applying +             -- applies when 'tFn' is has a functional type, and applying              -- the current context to it as above should not change this.              Nothing               -> error "ddc-core.synthAppArg: unexpected type of function." -        -- Effect of the overall application.-        let effsResult  = Sum.unions kEffect-                        $ [ effsFn, effsArg, Sum.singleton kEffect effsLatent]-        -        -- Closure of the overall application.-        let closResult  = Set.union closFn closArg +        -- Result of evaluating the functional expression applied+        -- to its argument.+        let esExp       = Sum.unions kEffect+                        $ [ effsFn, esArg, Sum.singleton kEffect esLatent]++        -- The checked application.+        let xExp'       = XApp  (AnTEC tResult' (TSum esExp) (tBot kClosure) a)+                                xFn xArg'++        -- If the function returns a suspension then automatically run it.+        let (xExpRun, tExpRun, esExpRun)+                | configImplicitRun (tableConfig table)+                , DemandRun     <- demand+                , Just (eExpRun', tExpRun') <- takeTSusp tResult'+                = let   +                        eTotal  = tSum kEffect [TSum esExp, eExpRun']++                  in    ( XCast (AnTEC tResult' eTotal (tBot kClosure) a)+                                CastRun xExp'+                        , tExpRun'+                        , Sum.fromList kEffect [eTotal])++                | otherwise+                =       ( xExp'+                        , tResult'+                        , esExp)+         ctrace  $ vcat-                [ text "* App Synth Fun"-                , indent 2 $ ppr xx-                , text "      tFn: " <> ppr tFn1-                , text "     tArg: " <> ppr tArg1-                , text "  tResult: " <> ppr tResult1-                , indent 2 $ ppr ctx1+                [ text "*<  App Synth Fun"+                , indent 4 $ ppr xx+                , text "    xArg    : " <> ppr xArg+                , text "    tFn'    : " <> ppr tFn'+                , text "    tArg'   : " <> ppr tArg'+                , text "    xArg'   : " <> ppr xArg'+                , text "    xExpRun : " <> ppr xExpRun+                , text "    tExpRun : " <> ppr tExpRun+                , indent 4 $ ppr ctx1                 , empty ] -        return  ( xFn, xArg'-                , tResult, effsResult, closResult, ctx1)+        return  (xExpRun, tExpRun, esExpRun, ctx1) - +  -- Applied expression is not a function.  | otherwise  =      throw $ ErrorAppNotFun a xx tFn@@ -248,8 +302,5 @@         TApp (TApp (TCon (TyConSpec TcConFun)) t11) t12           -> Just (t11, tBot kEffect, tBot kClosure, t12) -        TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFunEC)) t11) eff) clo) t12-          -> Just (t11, eff, clo, t12)-         _ -> Nothing-         +

@@ -1,62 +1,68 @@ -module DDC.Core.Check.Judge.Type.Base +module DDC.Core.Check.Judge.Type.Base         ( Checker-        , Table (..)+        , Demand (..)+        , Table  (..)         , returnX+        , runForDemand          , module DDC.Core.Check.Base         , module DDC.Core.Check.Judge.Inst         , module DDC.Core.Check.Judge.Sub         , module DDC.Core.Check.Judge.Eq-        , module DDC.Core.Check.TaggedClosure         , module DDC.Core.Check.Witness         , module DDC.Core.Check.Error         , module DDC.Core.Transform.Reannotate         , module DDC.Core.Transform.SubstituteTX-        , module DDC.Core.Annot.AnTEC+        , module DDC.Core.Exp.Annot.AnTEC          , module DDC.Type.Transform.SubstituteT         , module DDC.Type.Transform.Instantiate-        , module DDC.Type.Transform.Crush-        , module DDC.Type.Transform.LiftT-        , module DDC.Type.Transform.Trim)+        , module DDC.Type.Transform.BoundT) where import DDC.Core.Check.Base import DDC.Core.Check.Judge.Inst import DDC.Core.Check.Judge.Sub import DDC.Core.Check.Judge.Eq-import DDC.Core.Check.TaggedClosure import DDC.Core.Check.Witness import DDC.Core.Check.Error import DDC.Core.Transform.Reannotate import DDC.Core.Transform.SubstituteTX-import DDC.Core.Annot.AnTEC+import DDC.Core.Exp.Annot.AnTEC  import DDC.Type.Transform.SubstituteT import DDC.Type.Transform.Instantiate-import DDC.Type.Transform.Crush-import DDC.Type.Transform.LiftT-import DDC.Type.Transform.Trim+import DDC.Type.Transform.BoundT  +-- | Demand placed on suspensions by the surrounding context.+data Demand+        -- | Run suspensions as we encounter them.+        = DemandRun++        -- | Ignore suspensions, don't run them.+        | DemandNone+        deriving Show++ -- | Type of the function that checks some node of the core AST. type Checker a n-        =  (Show n, Ord n, Pretty n)+        =  (Show a, Show n, Ord n, Pretty n)         => Table a n                    -- ^ Static configuration.         -> Context n                    -- ^ Input context.-        -> Exp a n                      -- ^ Expression to check.         -> Mode n                       -- ^ Type checker mode.+        -> Demand                       -- ^ Demand on the expression.+        -> Exp a n                      -- ^ Expression to check.         -> CheckM a n                 ( Exp (AnTEC a n) n     -- Annotated, checked expression.                 , Type n                -- Type of the expression.                 , TypeSum n             -- Effect sum of expression.-                , Set (TaggedClosure n) -- Closure of expression.                 , Context n)            -- Output context.   -- | Table of environment things that do not change during type checking -----   We've got the static config, +--   We've got the static config, --    global kind and type environments, --    and a type checking function for each node of the AST. --@@ -80,33 +86,78 @@         , tableCheckLet         :: Checker a n         , tableCheckLetPrivate  :: Checker a n         , tableCheckCase        :: Checker a n-        , tableCheckCast        :: Checker a n +        , tableCheckCast        :: Checker a n         , tableCheckWitness     :: Checker a n }   -- | Helper function for building the return value of checkExpM' --   It builts the AnTEC annotation and attaches it to the new AST node, --   as well as returning the current effect and closure in the appropriate---   form as part of the tuple. -returnX :: Ord n +--   form as part of the tuple.+returnX :: Ord n         => a                            -- ^ Annotation for the returned expression.-        -> (AnTEC a n +        -> (AnTEC a n                 -> Exp (AnTEC a n) n)   -- ^ Fn to build the returned expression.         -> Type n                       -- ^ Type of expression.         -> TypeSum n                    -- ^ Effect sum of expression.-        -> Set (TaggedClosure n)        -- ^ Closure of expression.         -> Context n                    -- ^ Input context.-        -> CheckM a n +        -> CheckM a n                 ( Exp (AnTEC a n) n     -- Annotated, checked expression.                 , Type n                -- Type of expression.       (id to above)                 , TypeSum n             -- Effect sum of expression. (id to above)-                , Set (TaggedClosure n) -- Closure of expression.    (id to above)                 , Context n)            -- Output context. -returnX !a !f !t !es !cs !ctx+returnX !a !f !t !es !ctx  = let  e       = TSum es-        c       = closureOfTaggedSet cs-   in   return  (f (AnTEC t e c a)-                , t, es, cs, ctx)+   in   return  (f (AnTEC t e (tBot kClosure) a)+                , t, es, ctx) {-# INLINE returnX #-}+++-- Run ------------------------------------------------------------------------+-- | If an expression has suspension type then run it.+runForDemand +        :: Ord n+        => Config n                     -- ^ Type checker config.+        -> a                            -- ^ Annotation for new+        -> Demand                       -- ^ Demand placed on expression.+        -> Exp    (AnTEC a n) n         -- ^ Expression to inspect.+        -> Type   n                     -- ^ Type of the expression.+        -> Effect n                     -- ^ Effect of the expression.+        -> CheckM a n+                ( Exp (AnTEC a n) n     -- New expression, possibly with run cast.+                , Type   n              -- New type of expression.+                , Effect n)             -- New effect of expression.++runForDemand _config _a DemandNone xExp tExp eExp + = return (xExp, tExp, eExp)++runForDemand config a  DemandRun  xExp tExp eExp++ -- If the expression is wrapped in an explicit box or run then+ -- don't run it again. Doing this will just confuse the client+ -- programmer.+ | isXCastBox xExp || isXCastRun xExp+ = return (xExp, tExp, eExp)++ -- Insert an implicit run cast for this suspension.+ | configImplicitRun config+ , Just (eResult, tResult)  <- takeTSusp tExp+ = let+        -- Effect of overall expression is effect of computing+        -- the suspension plus the effect we get by running +        -- that suspension.+        eTotal  = tSum kEffect [eExp, eResult]++        -- Annotation for the cast expression.+        aCast   = AnTEC tResult eTotal (tBot kClosure) a++   in   return  ( XCast aCast CastRun xExp+                , tResult+                , eTotal)++ | otherwise+ = return (xExp, tExp, eExp)++ 

@@ -4,14 +4,15 @@ where import DDC.Core.Check.Judge.Type.Base import qualified DDC.Type.Sum   as Sum-import qualified Data.Set       as Set import qualified Data.Map       as Map import Data.List                as L  --------------------------------------------------------------------------------------------------- checkCase :: Checker a n-checkCase !table !ctx0 xx@(XCase a xDiscrim alts) mode- = do   let config      = tableConfig table+checkCase !table !ctx0 mode demand +        xx@(XCase a xDiscrim alts)+ = do   +        let config      = tableConfig table          -- There must be at least one alternative, even if there are no data         -- constructors. The rest of the checking code assumes this, and will@@ -20,16 +21,19 @@          $ throw $ ErrorCaseNoAlternatives a xx          -- Decide what mode to use when checking the discriminant.-        (modeDiscrim, ctx1)     +        (modeDiscrim, ctx1)          <- takeDiscrimCheckModeFromAlts table a ctx0 mode alts          -- Check the discriminant.-        (xDiscrim', tDiscrim, effsDiscrim, closDiscrim, ctx2) -         <- tableCheckExp table table ctx1 xDiscrim modeDiscrim+        --   We set the demand to 'Run' because if the scrutinee is a+        --   suspension then we won't be able to destruct it, so we+        --   might as well run it to get the result.+        (xDiscrim', tDiscrim, effsDiscrim, ctx2)+         <- tableCheckExp table table ctx1 modeDiscrim DemandRun xDiscrim           -- Split the type into the type constructor names and type parameters.         -- Also check that it's algebraic data, and not a function or effect-        -- type etc. +        -- type etc.         (mDataMode, tsArgs)          <- case takeTyConApps tDiscrim of              Just (tc, ts)@@ -46,7 +50,7 @@               , takeResultKind k == kData               -> return ( lookupModeOfDataType nTyCon (configDataDefs config)                         , ts )-                      +               -- Primitive data types.               | TyConBound (UPrim nTyCon _) k <- tc               , takeResultKind k == kData@@ -55,9 +59,9 @@               _ -> throw $ ErrorCaseScrutineeNotAlgebraic a xx tDiscrim -        -- Get the mode of the data type, +        -- Get the mode of the data type,         --   this tells us how many constructors there are.-        dataMode    +        dataMode          <- case mDataMode of              Nothing -> throw $ ErrorCaseScrutineeTypeUndeclared a xx tDiscrim              Just m  -> return m@@ -68,22 +72,22 @@          <- case mode of                 Recon   -> return (mode, ctx2)                 Check{} -> return (mode, ctx2)-                Synth   +                Synth                  -> do  iA       <- newExists kData                         let tA   = typeOfExists iA                         let ctx3 = pushExists iA ctx2                         return (Check tA, ctx3)          -- Check the alternatives.-        (alts', tsAlts, effss, closs, ctx4)-         <- checkAltsM table a xx tDiscrim tsArgs modeAlts alts ctx3+        (alts', tsAlts, effss, ctx4)+         <- checkAltsM table a xx tDiscrim tsArgs modeAlts demand alts ctx3          -- Check that all the alternatives have the same type.-        --   In Synth mode this is enforced by passing down an existential to +        --   In Synth mode this is enforced by passing down an existential to         --   unifify against, but with Recon and Check modes we might get         --   a different type for each alternative.-        let tsAlts'     = map (applyContext ctx4) tsAlts-        let tAlt : _    = tsAlts'+        tsAlts'         <- mapM (applyContext ctx4) tsAlts+        let tAlt : _    =  tsAlts'         forM_ tsAlts' $ \tAlt'          -> when (not $ equivT tAlt tAlt')           $ throw $ ErrorCaseAltResultMismatch a xx tAlt tAlt'@@ -94,10 +98,17 @@         -- Check that alternatives are exhaustive.         checkAltsExhaustive a xx dataMode alts -        let effsMatch    -                = Sum.singleton kEffect -                $ crushEffect $ tHeadRead tDiscrim+        -- Effect due to inspecting the scrutinee.+        let effsMatch+                = Sum.singleton kEffect+                $ tHeadRead tDiscrim +        -- Effect of overall expression.+        let effTotal+                = crushEffect (configGlobalCaps config)+                $ TSum $ Sum.unions kEffect+                $ effsDiscrim : effsMatch : effss+         ctrace  $ vcat                 [ text "* Case"                 , text "  modeDiscrim"  <+> ppr modeDiscrim@@ -111,21 +122,20 @@         returnX a                 (\z -> XCase z xDiscrim' alts')                 tAlt-                (Sum.unions kEffect (effsDiscrim : effsMatch : effss))-                (Set.unions         (closDiscrim : closs))+                (Sum.fromList kEffect [effTotal])                 ctx4 -checkCase _ _ _ _+checkCase _ _ _ _ _         = error "ddc-core.checkCase: no match"   --------------------------------------------------------------------------------------------------- -- | Decide what type checker mode to use when checking the discriminant---   of a case expression. +--   of a case expression. -- --   With plain type reconstruction then we also reconsruct the discrim type. -----   With bidirectional checking we use the type of the patterns as +--   With bidirectional checking we use the type of the patterns as --   the expected type when checking the discriminant. -- takeDiscrimCheckModeFromAlts@@ -135,7 +145,7 @@         -> Context n          -- ^ Current context.         -> Mode n             -- ^ Mode for checking enclosing case expression.         -> [Alt a n]          -- ^ Alternatives in the case expression.-        -> CheckM a n +        -> CheckM a n                 ( Mode n                 , Context n) @@ -152,25 +162,25 @@         tsPats       <- liftM catMaybes $ mapM (dataTypeOfPat table a) pats          case tsPats of-         -- We only have a default pattern, +         -- We only have a default pattern,          -- so will need to synthesise the type of the discrim without          -- an expected type.-         [] +         []           -> return (Synth, ctx)           -- We have at least one non-default pattern, which we can use to          -- determine how many existentials are needed to instantiate          -- the quantifiers of its type.-         tPat : _    +         tPat : _           | Just (bs, tBody) <- takeTForalls tPat-          -> do  +          -> do                 -- existentials for all of the type parameters.                 is        <- mapM  (\_ -> newExists kData) bs                 let ts     = map typeOfExists is                 let ctx'   = foldl (flip pushExists) ctx is                 let tBody' = substituteTs (zip bs ts) tBody                 return (Check tBody', ctx')-                +           | otherwise           -> return (Check tPat, ctx) @@ -178,26 +188,26 @@ --------------------------------------------------------------------------------------------------- -- | Check some case alternatives. checkAltsM-        :: (Show n, Pretty n, Ord n)+        :: (Show a, Show n, Pretty n, Ord n)         => Table a n            -- ^ Checker table.         -> a                    -- ^ Annotation for error messages.         -> Exp a n              -- ^ Whole case expression, for error messages.         -> Type n               -- ^ Type of discriminant.         -> [Type n]             -- ^ Args to type constructor of discriminant.         -> Mode n               -- ^ Check mode for the alternatives.+        -> Demand               -- ^ Demand on the result of the alternatives.         -> [Alt a n]            -- ^ Alternatives to check.         -> Context n            -- ^ Context to check the alternatives in.         -> CheckM a n                 ( [Alt (AnTEC a n) n]      -- Checked alternatives.                 , [Type n]                 -- Type of alternative results.                 , [TypeSum n]              -- Alternative effects.-                , [Set (TaggedClosure n)]  -- Alternative closures                 , Context n) -checkAltsM !table !a !xx !tDiscrim !tsArgs !mode !alts0 !ctx+checkAltsM !table !a !xx !tDiscrim !tsArgs !mode !demand !alts0 !ctx  = checkAltsM1 alts0 ctx- - where ++ where   -- Whether we're doing bidirectional type inference.   bidir    = case mode of@@ -206,57 +216,57 @@    -- Check all the alternatives monadically.   checkAltsM1 [] ctx0-   =    return ([], [], [], [], ctx0)+   =    return ([], [], [], ctx0)    checkAltsM1 (alt : alts) ctx0-   = do (alt',  tAlt,  eAlt, cAlt, ctx1)+   = do (alt',  tAlt,  eAlt, ctx1)          <- checkAltM   alt ctx0 -        (alts', tsAlts, esAlts, csAlts, ctx2)+        (alts', tsAlts, esAlts, ctx2)          <- checkAltsM1 alts ctx1          return  ( alt'  : alts'                 , tAlt  : tsAlts                 , eAlt  : esAlts-                , cAlt  : csAlts                 , ctx2)    -- Check a single alternative.   checkAltM   (AAlt PDefault xBody) !ctx0-   = do   +   = do         -- Check the right of the alternative.-        (xBody', tBody, effBody, cloBody, ctx1)-                <- tableCheckExp table table ctx0 xBody mode+        (xBody', tBody, effBody, ctx1)+                <- tableCheckExp table table ctx0 mode demand xBody          return  ( AAlt PDefault xBody'                 , tBody                 , effBody-                , cloBody                 , ctx1)    checkAltM alt@(AAlt (PData dc bsArg) xBody) !ctx0-   = do +   = do         -- Get the constructor type associated with this pattern.         Just tCtor <- ctorTypeOfPat table a (PData dc bsArg)-         -        -- Take the type of the constructor and instantiate it with the -        -- type arguments we got from the discriminant. If the ctor type -        -- doesn't instantiate then it won't have enough foralls on the front, ++        -- Take the type of the constructor and instantiate it with the+        -- type arguments we got from the discriminant. If the ctor type+        -- doesn't instantiate then it won't have enough foralls on the front,         -- which should have been checked by the def checker.-        tCtor_inst      -         <- case instantiateTs tCtor tsArgs of-                Nothing -> throw $ ErrorCaseCannotInstantiate a xx tDiscrim tCtor-                Just t  -> return t-        +        tCtor_inst+         <- if equivT tCtor tDiscrim+             then return tCtor+             else case instantiateTs tCtor tsArgs of+                   Nothing -> throw $ ErrorCaseCannotInstantiate a xx tDiscrim tCtor+                   Just t  -> return t+         -- Split the constructor type into the field and result types.-        let (tsFields_ctor, tResult) +        let (tsFields_ctor, tResult)                 = takeTFunArgResult tCtor_inst          -- The result type of the constructor must match the discriminant type.         -- If it doesn't then the constructor in the pattern probably isn't for         -- the discriminant type.         when (not $ equivT tDiscrim tResult)-         $ throw $ ErrorCaseScrutineeTypeMismatch a xx +         $ throw $ ErrorCaseScrutineeTypeMismatch a xx                         tDiscrim tResult          -- There must be at least as many fields as variables in the pattern.@@ -268,28 +278,21 @@         -- Merge the field types we get by instantiating the constructor         -- type with possible annotations from the source program.         -- If the annotations don't match, then we throw an error.-        (tsFields, ctx1) -                <- checkFieldAnnots table bidir a xx       -                        (zip tsFields_ctor (map typeOfBind bsArg))-                        ctx0+        (tsFields, ctx1)+         <- checkFieldAnnots table bidir a xx+                (zip tsFields_ctor (map typeOfBind bsArg))+                ctx0          -- Extend the environment with the field types.         let bsArg'         = zipWith replaceTypeOfBind tsFields bsArg         let (ctx2, posArg) = markContext ctx1         let ctxArg         = pushTypes bsArg' ctx2-        -        -- Check the body in this new environment.-        (xBody', tBody, effsBody, closBody, ctxBody)-                 <- tableCheckExp table table ctxArg xBody mode -        -- Cut closure terms due to locally bound value vars.-        -- This also lowers deBruijn indices in un-cut closure terms.-        let closBody_cut -                = Set.fromList-                $ mapMaybe (cutTaggedClosureXs bsArg')-                $ Set.toList closBody+        -- Check the body in this new environment.+        (xBody', tBody, effsBody, ctxBody)+                <- tableCheckExp table table ctxArg mode demand xBody -        let tBody'      = applyContext ctxBody tBody+        tBody'  <- applyContext ctxBody tBody          -- Pop the argument types from the context.         let ctx_cut     = popToPos posArg ctxBody@@ -305,26 +308,25 @@                 , empty ]          -- We're returning the new context for kicks,-        -- but the caller doesn't use it because we don't want the order of +        -- but the caller doesn't use it because we don't want the order of         -- alternatives to matter for type inference.         return  ( AAlt (PData dc bsArg') xBody'                 , tBody'                 , effsBody-                , closBody_cut                 , ctx_cut)   -- Fields ----------------------------------------------------------------------------------------- -- | Check the inferred type for a field against any annotation for it.-checkFieldAnnots -        :: (Ord n, Pretty n)+checkFieldAnnots+        :: (Show a, Show n, Ord n, Pretty n)         => Table a n            -- ^ Checker table.         -> Bool                 -- ^ Use bi directional type inference.         -> a                    -- ^ Annotation for error messages.         -> Exp a n              -- ^ Whole case expression for error messages.         -> [(Type n, Type n)]   -- ^ List of inferred and annotation types.         -> Context n-        -> CheckM a n +        -> CheckM a n                 ( [Type n]      --   Final types for each field.                 , Context n)    --   Result context. @@ -335,19 +337,19 @@            -> do (tField,   ctx1)  <- checkFieldAnnot tActual tAnnot ctx0                  (tsFields, ctx')  <- checkFieldAnnots table bidir a xx tts' ctx1                  return (tField : tsFields, ctx')-                 +  where checkFieldAnnot tActual tAnnot ctx         -- Annotation is bottom, so use the inferred type of the field.-        | isBot tAnnot      +        | isBot tAnnot         = return (tActual, ctx) -        -- With bidirectional checking, annotations on fields can refine the +        -- With bidirectional checking, annotations on fields can refine the         -- inferred type for the overal expression.         | bidir         = do    ctx'    <- makeEq (tableConfig table) a ctx tAnnot tActual-                        $  ErrorCaseFieldTypeMismatch a xx tAnnot tActual+                        $  ErrorCaseFieldTypeMismatch a xx  tAnnot tActual -                let tField = applyContext ctx' tActual+                tField  <- applyContext ctx' tActual                 return  (tField, ctx')          -- In Recon mode, if there is an annotation on the field then it needs@@ -357,18 +359,18 @@         = return (tAnnot, ctx)          -- Annotation does not match actual type.-        | otherwise       +        | otherwise         = throw $ ErrorCaseFieldTypeMismatch a xx tAnnot tActual   -- Ctor Types ------------------------------------------------------------------------------------- -- | Get the constructor type associated with a pattern, or Nothing for the---   default pattern. If the data constructor isn't defined then the spread +--   default pattern. If the data constructor isn't defined then the spread --   transform won't have given it a proper type. --   Note that we can't simply check whether the constructor is in the ---  environment because literals like 42# never are. ctorTypeOfPat-        :: Ord n +        :: Ord n         => Table a n            -- ^ Checker table.         -> a                    -- ^ Annotation for error messages.         -> Pat n                -- ^ Pattern.@@ -378,11 +380,11 @@  = case dc of         DaConUnit   -> return $ Just $ tUnit         DaConPrim{} -> return $ Just $ daConType dc-     +         DaConBound n          -- Types of algebraic data ctors should be in the defs table.-         |  Just ctor <- Map.lookup n -                                $ dataDefsCtors +         |  Just ctor <- Map.lookup n+                                $ dataDefsCtors                                 $ configDataDefs $ tableConfig table          -> return $ Just $ typeOfDataCtor ctor @@ -399,8 +401,8 @@ --   Yields  the data type with outer quantifiers for its type parametrs. --   For example, given pattern (Cons x xs), return (forall [a : Data]. List a) ---dataTypeOfPat -        :: Ord n +dataTypeOfPat+        :: Ord n         => Table a n            -- ^ Checker table.         -> a                    -- ^ Annotation for error messages.         -> Pat n                -- ^ Pattern.@@ -414,7 +416,7 @@          Just tCtor -> return $ Just $ eat [] tCtor   where  eat bs tt-         = case tt of  +         = case tt of                 TForall b t        -> eat (bs ++ [b]) t                 TApp{}                  |  Just (_t1, t2) <- takeTFun tt@@ -423,7 +425,7 @@   ------------------------------------------------------------------------------------------------------ | Check for overlapping alternatives, +-- | Check for overlapping alternatives, --   and throw an error in the `CheckM` monad if there are any. checkAltsOverlapping         :: Eq n@@ -472,7 +474,7 @@  checkAltsExhaustive a xx mode alts  = do   let nsCtorsMatched      = mapMaybe takeCtorNameOfAlt alts-        +         -- Check that alternatives are exhaustive.         case mode of @@ -489,13 +491,13 @@            -> throw $ ErrorCaseNonExhaustive a xx nsCtorsMissing             -- All constructors were matched.-           | otherwise +           | otherwise            -> return ()            -- Large types have an effectively infinite number of constructors           -- (like integer literals), so there needs to be a default alt.-          DataModeLarge +          DataModeLarge            | any isPDefault [p | AAlt p _ <- alts] -> return ()-           | otherwise  +           | otherwise            -> throw $ ErrorCaseNonExhaustiveLarge a xx 

@@ -1,32 +1,32 @@  module DDC.Core.Check.Judge.Type.Cast-        (checkCast)+        ( checkCast) where import DDC.Core.Check.Judge.Type.Sub import DDC.Core.Check.Judge.Type.Base import qualified DDC.Type.Sum   as Sum-import qualified Data.Set       as Set   checkCast :: Checker a n  -- WeakenEffect --------------------------------------------------------------- -- Weaken the effect of an expression.-checkCast !table !ctx0 xx@(XCast a (CastWeakenEffect eff) x1) mode+checkCast !table !ctx0 mode _demand+        xx@(XCast a (CastWeakenEffect eff) x1)  = do   let config      = tableConfig  table         let kenv        = tableKindEnv table          -- Check the effect term.-        (eff', kEff, ctx1) -         <- checkTypeM config kenv ctx0 UniverseSpec eff +        (eff', kEff, ctx1)+         <- checkTypeM config kenv ctx0 UniverseSpec eff           $ case mode of                 Recon   -> Recon                 Synth   -> Check kEffect                 Check _ -> Check kEffect          -- Check the body.-        (x1', t1, effs, clo, ctx2)-         <- tableCheckExp table table ctx1 x1 mode+        (x1', t1, effs, ctx2)+         <- tableCheckExp table table ctx1 mode DemandNone x1          -- The effect term must have Effect kind.         when (not $ isEffectKind kEff)@@ -36,43 +36,17 @@         let effs'  = Sum.insert eff' effs          returnX a (\z -> XCast z c' x1')-                t1 effs' clo ctx2-                ---- WeakenClosure ----------------------------------------------------------------- Weaken the closure of an expression.------ DEPRECATED: Closures are being removed in the next version,---             so we don't bother doing proper type inference for closure---             weakenings.----checkCast !table !ctx (XCast a (CastWeakenClosure xs) x1) mode- = do   -        -- Check the contained expressions.-        --  Just ditch the resulting contexts because they shouldn't-        --  contain expression that need types infered.-        (xs', closs, _ctx)-                <- liftM unzip3-                $   mapM (\x -> checkArgM table ctx x Recon) xs--        -- Check the body.-        (x1', t1, effs, clos, ctx1)-                <- tableCheckExp table table ctx x1 mode-        -        let c'     = CastWeakenClosure xs'-        let closs' = Set.unions (clos : closs)--        returnX a (\z -> XCast z c' x1')-                t1 effs closs' ctx1+                t1 effs' ctx2   -- Purify --------------------------------------------------------------------- -- Purify the effect of an expression.--- +-- -- EXPERIMENTAL: The Tetra language doesn't have purification casts yet, --               so proper type inference isn't implemented.--- -checkCast !table !ctx xx@(XCast a (CastPurify w) x1) mode+--+checkCast !table !ctx mode _demand +        xx@(XCast a (CastPurify w) x1)  = do   let config      = tableConfig table         let kenv        = tableKindEnv table         let tenv        = tableTypeEnv table@@ -82,8 +56,8 @@         let wTEC  = reannotate fromAnT w'          -- Check the body.-        (x1', t1, effs, clo, ctx1)-         <- tableCheckExp table table ctx x1 mode+        (x1', t1, effs, ctx1)+         <- tableCheckExp table table ctx mode DemandNone x1          -- The witness must have type (Pure e), for some effect e.         effs' <- case tW of@@ -93,135 +67,115 @@          let c'  = CastPurify wTEC         returnX a (\z -> XCast z c' x1')-                t1 effs' clo ctx1----- Forget ------------------------------------------------------------------------ Forget the closure of an expression.------ DEPRECATED: Closures are being removed in the next version,---             so we don't bother doing proper type inference for forget casts.--- -checkCast !table !ctx xx@(XCast a (CastForget w) x1) mode- = do   let config      = tableConfig table-        let kenv        = tableKindEnv table-        let tenv        = tableTypeEnv table--        -- Check the witness.-        (w', tW)  <- checkWitnessM config kenv tenv ctx w-        let wTEC  = reannotate fromAnT w'--        -- Check the body.-        (x1', t1, effs, clos, ctx1)  -         <- tableCheckExp table table ctx x1 mode--        -- The witness must have type (Empty c), for some closure c.-        clos' <- case tW of-                  TApp (TCon (TyConWitness TwConEmpty)) cloMask-                    -> return $ maskFromTaggedSet -                                        (Sum.singleton kClosure cloMask)-                                        clos--                  _ -> throw $ ErrorWitnessNotEmpty a xx w tW--        let c'  = CastForget wTEC-        returnX a (\z -> XCast z c' x1')-                t1 effs clos' ctx1+                t1 effs' ctx1   -- Box ------------------------------------------------------------------------ -- Box a computation, -- capturing its effects in a computation type.-checkCast !table ctx0 xx@(XCast a CastBox x1) mode+checkCast !table ctx0 mode _demand +        xx@(XCast a CastBox x1)  = case mode of     Check tExpected-     -> do      +     -> do         let config      = tableConfig table          -- Check the body.-        (x1', tBody, effs, clos, ctx1)     -         <- tableCheckExp table table ctx0 x1 Synth+        (x1', tBody, effs, ctx1)+         <- tableCheckExp table table ctx0 Synth DemandRun x1 +        let effs_crush +                = Sum.fromList kEffect+                [ crushEffect (configGlobalCaps config) (TSum effs)]+         -- The actual type is (S eff tBody).-        let tBody'      = applyContext ctx1 tBody-        let tActual     = tApps (TCon (TyConSpec TcConSusp)) [TSum effs, tBody']+        tBody'      <- applyContext ctx1 tBody+        let tActual =  tApps (TCon (TyConSpec TcConSusp)) +                             [TSum effs_crush, tBody']          -- The actual type needs to match the expected type.         -- We're treating the S constructor as invariant in both positions,         --  so we use 'makeEq' here instead of 'makeSub'-        let tExpected'  = applyContext ctx1 tExpected-        ctx2    <- makeEq config a ctx1 tActual tExpected'-                $  ErrorMismatch a      tActual tExpected' xx+        tExpected'  <- applyContext ctx1 tExpected+        ctx2        <- makeEq config a ctx1 tActual tExpected'+                    $  ErrorMismatch a      tActual tExpected' xx          returnX a (\z -> XCast z CastBox x1')-                tExpected (Sum.empty kEffect) clos ctx2+                tExpected (Sum.empty kEffect) ctx2      -- Recon and Synth mode.     _      -> do+        let config      = tableConfig table+         -- Check the body.-        (x1', t1, effs, clos, ctx1) -         <- tableCheckExp table table ctx0 x1 mode+        (x1', t1, effs,  ctx1)+         <- tableCheckExp table table ctx0 mode DemandRun x1 +        let effs_crush +                = Sum.fromList kEffect+                [ crushEffect (configGlobalCaps config) (TSum effs)]+         -- The result type is (S effs a).         let tS  = tApps (TCon (TyConSpec TcConSusp))-                        [TSum effs, t1]+                        [TSum effs_crush, t1]          returnX a (\z -> XCast z CastBox x1')-                tS (Sum.empty kEffect) clos ctx1+                tS (Sum.empty kEffect) ctx1   -- Run ------------------------------------------------------------------------ -- Run a suspended computation, -- releasing its effects into the environment.-checkCast !table !ctx0 xx@(XCast a CastRun xBody) mode+checkCast !table !ctx0 mode _demand+        xx@(XCast a CastRun xBody)  = case mode of     Recon      -> do         -- Check the body.-        (xBody', tBody, effs, clos, ctx1)-         <- tableCheckExp table table ctx0 xBody Recon+        (xBody', tBody, effs, ctx1)+         <- tableCheckExp table table ctx0 Recon DemandNone xBody          -- The body must have type (S eff a),         --  and the result has type 'a' while unleashing effect 'eff'.         case tBody of          TApp (TApp (TCon (TyConSpec TcConSusp)) eff2) tResult           -> do-                -- Check that the context has the capability to support +                -- Check that the context has the capability to support                 -- this effect.                 let config      = tableConfig table                 checkEffectSupported config a xx ctx0 eff2                  returnX a                         (\z -> XCast z CastRun xBody')-                        tResult +                        tResult                         (Sum.union effs (Sum.singleton kEffect eff2))-                        clos ctx1+                        ctx1           _ -> throw $ ErrorRunNotSuspension a xx tBody      Synth      -> do         -- Synthesize a type for the body.-        (xBody', tBody, effs, clos, ctx1)-         <- tableCheckExp table table ctx0 xBody Synth+        (xBody', tBody, effs, ctx1)+         <- tableCheckExp table table ctx0 Synth DemandNone xBody          -- Run the body,         -- which needs to have been resolved to a computation type.-        let tBody'      = applyContext ctx1 tBody+        tBody'  <- applyContext ctx1 tBody         (tResult, effsSusp, ctx2)          <- synthRunSusp table a xx ctx1 tBody' -        returnX a +        returnX a                 (\z -> XCast z CastRun xBody')                 tResult                 (Sum.union effs (Sum.singleton kEffect effsSusp))-                clos ctx2+                ctx2      Check tExpected-     -> checkSub table a ctx0 xx tExpected+     -> checkSub table a ctx0 DemandNone xx tExpected -checkCast _ _ _ _+checkCast _ _ _ _ _         = error "ddc-core.checkCast: no match"  @@ -239,8 +193,8 @@                 , Effect n      -- Effects unleashed by running the computation.                 , Context n)    -- Result context. -synthRunSusp table a xx ctx0 tt - +synthRunSusp table a xx ctx0 tt+  -- Rule (Run Synth exists)  -- If the type of the suspension has not been resolved then we don't know  -- what effects it has, and thus cannot check if running them is supported@@ -260,52 +214,13 @@  -- Run expression is not a suspension.  | otherwise  =      throw $ ErrorRunNotSuspension a xx tt-  --- Arg --------------------------------------------------------------------------- | Like `checkExp` but we allow naked types and witnesses.-checkArgM -        :: (Show n, Pretty n, Ord n)-        => Table a n            -- ^ Static config.-        -> Context n            -- ^ Input context.-        -> Exp a n              -- ^ Expression to check.-        -> Mode n               -- ^ Checking mode.-        -> CheckM a n -                ( Exp (AnTEC a n) n-                , Set (TaggedClosure n)-                , Context n) -checkArgM !table !ctx0 !xx !mode- = let  config  = tableConfig  table-        tenv    = tableTypeEnv table-        kenv    = tableKindEnv table-   in case xx of-        XType a t-         -> do  (t', k, ctx1) <- checkTypeM config kenv ctx0 UniverseSpec t Recon-                let Just clo = taggedClosureOfTyArg kenv ctx1 t-                let a'   = AnTEC k (tBot kEffect) (tBot kClosure) a-                return  ( XType a' t'-                        , clo-                        , ctx1)--        XWitness a w-         -> do  (w', t) <- checkWitnessM config kenv tenv ctx0 w-                let a'   = AnTEC t (tBot kEffect) (tBot kClosure) a-                return  ( XWitness a' (reannotate fromAnT w')-                        , Set.empty-                        , ctx0)--        _ -> do-                (xx', _, _, clos, ctx1) -                        <- tableCheckExp table table ctx0 xx mode-                return  (xx', clos, ctx1)-                        - -- Support ----------------------------------------------------------------------- | Check if the provided effect is supported by the context, +-- | Check if the provided effect is supported by the context, --   if not then throw an error.-checkEffectSupported -        :: Ord n +checkEffectSupported+        :: (Show n, Ord n)         => Config n             -- ^ Static config.         -> a                    -- ^ Annotation for error messages.         -> Exp a n              -- ^ Expression for error messages.@@ -317,4 +232,5 @@  = case effectSupported eff ctx of         Nothing         -> return ()         Just effBad     -> throw $ ErrorRunNotSupported a xx effBad- ++

@@ -23,7 +23,7 @@      -> return tUnit      -- Primitive data constructors need to have a corresponding data type,-    -- but there may be too many constructors to list, like with Int literals. +    -- but there may be too many constructors to list, like with Int literals.     --     -- The mode field in the data type declaration says what to expect.     --    If the mode is 'Small' the data constructor needs to be listed,

@@ -5,16 +5,17 @@ import DDC.Core.Check.Judge.Type.Sub import DDC.Core.Check.Judge.Type.Base import qualified DDC.Type.Sum   as Sum-import qualified Data.Set       as Set   -- Check a spec abstraction. checkLamT :: Checker a n-checkLamT !table !ctx xx mode+checkLamT !table !ctx mode _demand xx   = case xx of-        XLAM a b1 x2    -> checkLAM table ctx a b1 x2 mode-        _               -> error "ddc-core.checkLamT: no match."+        XLAM a b1 x2+           -> checkLAM table ctx a b1 x2 mode+        _  -> error "ddc-core.checkLamT: no match." + -- When reconstructing the type of a type abstraction, --  the formal parameter must have a kind annotation: eg (/\v : K. x2) checkLAM !table !ctx0 a b1 x2 Recon@@ -43,19 +44,22 @@         when (not (sA == sComp) && not (sA == sProp))          $ throw $ ErrorLAMParamBadSort a xx b1 sA -        +         -- Check the body -----------------------         let (ctx2, pos1) = markContext ctxA         let ctx3         = pushKind b1' RoleAbstract ctx2         let ctx4         = liftTypes 1  ctx3 -        (x2', t2, e2, c2, ctx5)-         <- tableCheckExp table table ctx4 x2 Recon-        +        -- Set the demand to 'None' because we don't want to force out+        -- suspensions. If the body of a type abstraction has any effects+        -- then this is a type error.+        (x2', t2, e2, ctx5)+         <- tableCheckExp table table ctx4 Recon DemandNone x2 +         -- Reconstruct the kind of the body.-        (t2', k2, ctx6) +        (t2', k2, ctx6)          <- checkTypeM config kenv ctx5 UniverseSpec t2 Recon-        +         -- The type of the body must have data kind.         when (not $ isDataKind k2)          $ throw $ ErrorLamBodyNotData a xx b1 t2' k2@@ -64,15 +68,10 @@         when (e2 /= Sum.empty kEffect)          $ throw $ ErrorLamNotPure a xx UniverseSpec (TSum e2) -        -- Mask closure terms due to locally bound region vars.-        let c2_cut      = Set.fromList-                        $ mapMaybe (cutTaggedClosureT b1)-                        $ Set.toList c2-         -- Cut the bound kind and elems under it from the context.         let ctx_cut     = lowerTypes 1                         $ popToPos pos1 ctx6-                                   +         -- Build the result type.         let tResult     = TForall b1' t2' @@ -81,13 +80,12 @@                 , indent 2 $ ppr (XLAM a b1' x2)                 , text "  OUT: " <> ppr tResult                 , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx_cut +                , indent 2 $ ppr ctx_cut                 , empty ]          returnX a                 (\z -> XLAM z b1' x2')-                tResult (Sum.empty kEffect) c2_cut-                ctx_cut+                tResult (Sum.empty kEffect) ctx_cut   checkLAM !table !ctx0 a b1 x2 Synth@@ -104,8 +102,8 @@         -- If the annotation is missing then make a new existential for it.         let kA  = typeOfBind b1         (kA', sA, ctxA)-         <- if isBot kA -             then do   +         <- if isBot kA+             then do                 iA       <- newExists sComp                 let kA'  = typeOfExists iA                 let ctxA = pushExists   iA ctx0@@ -125,29 +123,27 @@         let ctx3         = pushKind b1' RoleAbstract ctx2         let ctx4         = liftTypes 1  ctx3 -        (x2', t2, e2, c2, ctx5)-         <- tableCheckExp table table ctx4 x2 Synth-        +        -- Set the demand to 'None' because we don't want to force out+        -- suspensions. If the body of a type abstraction has any effects+        -- then this is a type error.+        (x2', t2, e2,ctx5)+         <- tableCheckExp table table ctx4 Synth DemandNone x2 +         -- Force the kind of the body to be data.         --  This is needed when the type of the body is an existential         --  which doesn't yet have a resolved kind.-        (_, _, ctx6) -         <- checkTypeM config kenv ctx5 UniverseSpec -                (applyContext ctx5 t2) (Check kData)-        +        t2'     <- applyContext ctx5 t2+        (_, _, ctx6)+         <- checkTypeM config kenv ctx5 UniverseSpec t2' (Check kData)+         -- The body of a spec abstraction must be pure.         when (e2 /= Sum.empty kEffect)          $ throw $ ErrorLamNotPure a xx UniverseSpec (TSum e2) -        -- Mask closure terms due to locally bound region vars.-        let c2_cut      = Set.fromList-                        $ mapMaybe (cutTaggedClosureT b1)-                        $ Set.toList c2-         -- Cut the bound kind and elems under it from the context.         let ctx_cut     = lowerTypes 1                         $ popToPos pos1 ctx6-        +         -- Build the result type.         let tResult     = TForall b1' t2 @@ -156,13 +152,12 @@                 , indent 2 $ ppr (XLAM a b1' x2)                 , text "  OUT: " <> ppr tResult                 , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx_cut +                , indent 2 $ ppr ctx_cut                 , empty ]          returnX a                 (\z -> XLAM z b1' x2')-                tResult (Sum.empty kEffect) c2_cut-                ctx_cut+                tResult (Sum.empty kEffect) ctx_cut   checkLAM !table !ctx0 a b1 x2 (Check (TForall b tBody))@@ -184,14 +179,14 @@         -- If both the kind annotation is missing and there is no         -- expected kind then we need to make an existential for it.         (kA', sA, ctxA)-         <- if (isBot kParam && isBot kExpected) +         <- if (isBot kParam && isBot kExpected)              then do                 iA       <- newExists sComp                 let kA'  = typeOfExists iA                 let ctxA = pushExists   iA ctx0                 return (kA', sComp, ctxA) -             else if isBot kExpected +             else if isBot kExpected               then do                 checkTypeM config kenv ctx0 UniverseKind kParam Synth @@ -218,9 +213,12 @@                 Nothing -> return tBody                 Just u1 -> return $ substituteT b (TVar u1) tBody -        (x2', t2, e2, c2, ctx5)-         <- tableCheckExp table table ctx4 x2 (Check tBody_skol)-        +        -- Set the demand to 'None' because we don't want to force out+        -- suspensions. If the body of a type abstraction has any effects+        -- then this is a type error.+        (x2', t2, e2, ctx5)+         <- tableCheckExp table table ctx4 (Check tBody_skol) DemandNone x2 +         -- Force the body of the spec abstraction must have data kind.         --  This is needed when the type of the body is an existential         --  which doesn't yet have a resolved kind.@@ -231,21 +229,16 @@         when (e2 /= Sum.empty kEffect)          $ throw $ ErrorLamNotPure a xx UniverseSpec (TSum e2) -        -- Mask closure terms due to locally bound region vars.-        let c2_cut      = Set.fromList-                        $ mapMaybe (cutTaggedClosureT b1)-                        $ Set.toList c2-         -- Apply context to synthesised type.-        -- We're about to pop the context back to how it was before the +        -- We're about to pop the context back to how it was before the         -- type lambda, and want to keep information gained from synthing         -- the body.-        let t2_sub      = applyContext ctx6 t2'+        t2_sub  <- applyContext ctx6 t2'          -- Cut the bound kind and elems under it from the context.         let ctx_cut     = lowerTypes 1                         $ popToPos pos1 ctx6-        +         -- Build the result type.         let tResult     = TForall b1' t2_sub @@ -254,14 +247,13 @@                 , indent 2 $ ppr (XLAM a b1' x2)                 , text "  OUT: " <> ppr tResult                 , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx_cut +                , indent 2 $ ppr ctx_cut                 , empty ]          returnX a                 (\z -> XLAM z b1' x2')-                tResult (Sum.empty kEffect) c2_cut-                ctx_cut+                tResult (Sum.empty kEffect) ctx_cut  checkLAM table ctx0 a b1 x2 (Check tExpected)- = checkSub table a ctx0 (XLAM a b1 x2) tExpected+ = checkSub table a ctx0 DemandNone (XLAM a b1 x2) tExpected 

@@ -5,26 +5,29 @@ import DDC.Core.Check.Judge.Type.Sub import DDC.Core.Check.Judge.Type.Base import qualified DDC.Type.Sum   as Sum-import qualified Data.Set       as Set   -- | Check a lambda abstraction. checkLamX :: Checker a n-checkLamX !table !ctx xx mode++checkLamX !table !ctx mode _demand xx  = case xx of-        XLam a b1 x2    -> checkLam table a ctx b1 x2 mode-        _               -> error "ddc-core.checkLamX: no match."+        XLam a b1 x2+          -> checkLam table a ctx b1 x2 mode+        _ -> error "ddc-core.checkLamX: no match." + -- When reconstructing the type of a lambda abstraction, --  the formal parameter must have a type annotation: eg (\v : T. x2) checkLam !table !a !ctx !b1 !x2 !Recon- = do   let config      = tableConfig table+ = do+        let config      = tableConfig table         let kenv        = tableKindEnv table         let xx          = XLam a b1 x2          -- Check the parameter ------------------         let t1          = typeOfBind b1-        +         -- The formal parameter must have a type annotation.         when (isBot t1)          $ throw $ ErrorLamParamUnannotated a xx b1@@ -38,40 +41,46 @@         let (ctx', pos1) = markContext ctx         let ctx1         = pushType b1 ctx' -        (x2', t2, e2, c2, ctx2)-         <- tableCheckExp table table ctx1 x2 Recon+        -- It doesn't matter what we set the demand to at this point+        -- because the 'Recon' mode doesn't use it. We'll just set it +        -- like the other modes to avoid confusion.+        (x2', t2, e2, ctx2)+         <- tableCheckExp table table ctx1 Recon DemandRun x2  +        let e2_crush +                = Sum.fromList kEffect+                [ crushEffect (configGlobalCaps config) (TSum e2)]+         -- The body of the function must produce data.         (_, k2, _)      <- checkTypeM config kenv ctx2 UniverseSpec t2 Recon         when (not $ isDataKind k2)-         $ throw $ ErrorLamBodyNotData a xx b1 t2 k2 --        -- Cut closure terms due to locally bound value vars.-        -- This also lowers deBruijn indices in un-cut closure terms.-        let c2_cut      = Set.fromList-                        $ mapMaybe (cutTaggedClosureX b1)-                        $ Set.toList c2+         $ throw $ ErrorLamBodyNotData a xx b1 t2 k2          -- Cut the bound type and elems under it from the context.         let ctx_cut     = popToPos pos1 ctx2-        +         -- Build result type --------------------         -- Build the resulting function type.         --   The way the effect and closure term is captured depends on         --   the configuration flags.-        (tResult, cResult)-         <- makeFunctionType config a xx t1 k1 t2 e2 c2_cut-        -        returnX a-                (\z -> XLam z b1' x2')-                tResult (Sum.empty kEffect) cResult-                ctx_cut+        (xAbs', tAbs) +         <- makeFunction config a xx b1' t1 k1 x2' t2 e2_crush +        return  ( xAbs'+                , tAbs+                , Sum.empty kEffect+                , ctx_cut) + -- When synthesizing the type of a lambda abstraction --   we produce a type (?1 -> ?2) with new unification variables. checkLam !table !a !ctx !b1 !x2 !Synth- = do   let config      = tableConfig table     + = do+        ctrace  $ vcat+                [ text "*>  Lam SYNTH"+                , text "    in  bind = " <+> ppr b1 ]++        let config      = tableConfig table         let kenv        = tableKindEnv table         let xx          = XLam a b1 x2 @@ -81,7 +90,7 @@         -- If there isn't an existing annotation then make an existential.         (b1', t1', k1, ctx1)          <- if isBot t1-             then do +             then do                 -- There is no annotation at all, so make an existential.                 -- Missing anotations are assumed to have kind Data.                 i1      <- newExists kData@@ -89,7 +98,7 @@                 let b1'  = replaceTypeOfBind t1' b1                 let ctx1 = pushExists i1 ctx                 return (b1', t1', kData, ctx1)-                     +              else do                 -- Check the existing annotation.                 --   This also turns explit holes ? into existentials.@@ -100,73 +109,78 @@                 let b1' = replaceTypeOfBind t1' b1                 return (b1', t1', k1, ctx1) -        -- Check the body -----------------------        +        -- Check the body -----------------------         -- Make an existential for the result type.         -- The type of a function abstraction has kind Data.         i2              <- newExists kData         let t2          = typeOfExists i2-        -        -- Push the existential for the result, ++        -- Push the existential for the result,         -- and parameter type onto the context.         let (ctx2, pos1) = markContext                           $ pushExists i2 ctx1         let ctx3         = pushType   b1' ctx2          -- Check the body against the existential for it.-        (x2', t2', e2, c2, ctx4)-         <- tableCheckExp table table ctx3 x2 (Check t2)+        --   Set the demand to 'Run' to force out any suspensions.+        --   We'll box them up again just underneath the lambda+        --   so that the effects from multiple computations get combined.+        (x2', t2', e2, ctx4)+         <- tableCheckExp table table ctx3 (Check t2) DemandRun x2  +        let e2_crush +                = Sum.fromList kEffect+                [ crushEffect (configGlobalCaps config) (TSum e2)]+         -- Force the kind of the body to be Data.         --   This constrains the kind of polymorpic variables that are used-        --   as the result of a function, like with (\x. x). +        --   as the result of a function, like with (\x. x).         --   We know \x. can't bind a witness here.-        (_, _, ctx5)    <- checkTypeM config kenv ctx4 UniverseSpec -                                (applyContext ctx4 t2')-                                (Check kData)+        t2''     <- applyContext ctx4 t2'+        (_, _, ctx5)+         <- checkTypeM config kenv ctx4 UniverseSpec t2'' (Check kData)          -- Build the result type -------------         -- If the kind of the parameter is unconstrained then default it         -- to Data. This handles  "/\f. \(a : f Int#). ()"-        let k1'        = applyContext ctx5 k1+        k1'     <- applyContext ctx5 k1         (k1'', ctx6)          <- if isTExists k1'              then do                 ctx6    <- makeEq config a ctx5 k1' kData                         $  ErrorMismatch a k1' kData xx-                return (applyContext ctx6 k1', ctx6) +                k1''    <- applyContext ctx6 k1'++                return (k1'', ctx6)+              else do                 return (k1', ctx5) -        -- Cut closure terms due to locally bound value vars.-        -- This also lowers deBruijn indices in un-cut closure terms.-        let c2_cut      = Set.fromList-                        $ mapMaybe (cutTaggedClosureX b1')-                        $ Set.toList c2-          -- Cut the bound type and elems under it from the context.         let ctx_cut     = popToPos pos1 ctx6          -- Build the resulting function type.         --  This switches on the kind of the argument, so we need to apply         --  the context to 'k1' to ensure it has all available information.-        (tResult, cResult)-         <- makeFunctionType config a (XLam a b1' x2) -                t1' k1''-                t2' e2 c2_cut+        (xAbs', tAbs)+         <- makeFunction +                config a (XLam a b1' x2)+                b1' t1' k1''+                x2' t2' e2_crush          ctrace  $ vcat-                [ text "* Lam Synth"-                , indent 2 $ ppr (XLam a b1' x2)-                , text "  OUT: " <> ppr tResult-                , indent 2 $ ppr ctx-                , indent 2 $ ppr ctx_cut +                [ text "*<  Lam SYNTH"+                , text "    in  bind = " <+> ppr b1+                , text "    out type = " <+> ppr tAbs+                , indent 4 $ ppr ctx+                , indent 4 $ ppr ctx_cut                 , empty ] -        returnX a-                (\z -> XLam z b1' x2')-                tResult (Sum.empty kEffect) cResult-                ctx_cut+        return  ( xAbs'+                , tAbs+                , Sum.empty kEffect+                , ctx_cut)   -- When checking type type of a lambda abstraction against an existing@@ -174,94 +188,157 @@ --   type annotation, and in this case we replace it with the expected type. checkLam !table !a !ctx !b1 !x2 !(Check tExpected)  | Just (tX1, tX2)      <- takeTFun tExpected- = do   let config      = tableConfig table+ = do   +        ctrace  $ vcat+                [ text "*>  Lam CHECK"+                , text "    in bind =" <+> ppr b1+                , text "    in type =" <+> ppr tExpected +                , empty ]++        let config      = tableConfig table         let kenv        = tableKindEnv table         let xx          = XLam a b1 x2          -- Check the parameter ------------------         let t1          = typeOfBind b1 -        -- If the parameter has no type annotation at all then we can use the-        --   expected type we were passed down from above.-        -- If it does have an annotation, then it needs to match the-        --   expected type.-        (b1', t1', ctx0) -         <- if isBot t1             -             then +        -- If the parameter has no type annotation at all then we can+        --   use the expected type we were passed down from above.+        -- If it does have an annotation, then the annotation also needs+        --   to match the expected type.+        (b1', t1', ctx0)+         <- if isBot t1+             then                 return  (replaceTypeOfBind tX1 b1, tX1, ctx)              else do-                ctx0    <- makeEq config a ctx t1 tX1 +                ctx0    <- makeEq config a ctx t1 tX1                         $  ErrorMismatch a t1 tExpected (XLam a b1 x2)                 return  (b1, t1, ctx0)-                        +         -- Check the body ----------------------         -- Check the body of the abstraction under the extended environment.         let (ctx', pos1) = markContext ctx0         let ctx1         = pushType b1' ctx' -        (x2', t2, e2, c2, ctx2)-         <- tableCheckExp table table ctx1 x2 (Check tX2)+        -- Check the body against the type we have for it.+        (x2', t2, e2, ctx2)+         <- case takeTSusp tX2 of +             -- If we're implicitly boxing bodies and we're expecting a+             -- suspension, then check the body against the type of the+             -- result of the suspension.+             Just (e2Expected, t2Expected)+              |  configImplicitBox config+              ,  not $ isXCastBox x2+              -> do +                    -- Check the body against the expected result type of the+                    -- suspension.+                    (x2', t2', es2Actual, ctx2)+                      <- tableCheckExp table table ctx1 (Check t2Expected) DemandRun x2 ++                    let es2Actual_crushed+                          = Sum.fromList kEffect+                          [ crushEffect (configGlobalCaps config) (TSum es2Actual)]++                    -- The expected effect in the suspension could have been an+                    -- existential, so we need to unify it against the reconstructed+                    -- effect to instantiate it.+                    let e2Actual_crushed = TSum es2Actual_crushed+                    ctx2' <- makeEq config a ctx2 e2Expected e2Actual_crushed+                          $  ErrorMismatch a e2Actual_crushed e2Expected x2++                    return (x2', t2', es2Actual_crushed, ctx2')++             _+              -> do+                    (x2', t2', es2Actual, ctx2)+                      <- tableCheckExp table table ctx1 (Check tX2) DemandNone x2++                    let es2Actual_crushed+                          = Sum.fromList kEffect+                          [ crushEffect (configGlobalCaps config) (TSum es2Actual)]++                    return (x2', t2', es2Actual_crushed, ctx2)+         -- Force the kind of the body to be Data.         --   This constrains the kind of polymorpic variables that are used-        --   as the result of a function, like with (\x. x). +        --   as the result of a function, like with (\x. x).         --   We know \x. can't bind a witness here.-        (_, _, ctx3)    <- checkTypeM config kenv ctx2 UniverseSpec -                                (applyContext ctx2 t2) -                                (Check kData)+        t2' <- applyContext ctx2 t2+        (_, _, ctx3)+            <- checkTypeM config kenv ctx2 UniverseSpec t2' (Check kData)          -- Make the result type -----------------         -- If the kind of the parameter is unconstrained then default it         -- to Data. This handles  "/\f. \(a : f Int#). ()"         (_, k1, _)      <- checkTypeM config kenv ctx3 UniverseSpec t1' Synth-        let k1'         = applyContext ctx3 k1+        k1'             <- applyContext ctx3 k1         (k1'', ctx4)          <- if isTExists k1'              then do                 ctx4    <- makeEq config a ctx3 k1' kData                         $  ErrorMismatch a k1' kData xx-                return (applyContext ctx4 k1', ctx4) +                k1''    <- applyContext ctx4 k1'++                return (k1'', ctx4)+              else do                 return (k1', ctx3) -        -- Cut closure terms due to locally bound value vars.-        -- This also lowers deBruijn indices in un-cut closure terms.-        let c2_cut      = Set.fromList-                        $ mapMaybe (cutTaggedClosureX b1)-                        $ Set.toList c2-        -        -- Cut the bound type and elems under it from the context.-        let ctx_cut     = popToPos pos1 ctx4          -- Build the resulting function type.         --  This switches on the kind of the argument, so we need to apply         --  the context to 'k1' to ensure it has all available information.-        (tResult, cResult)-         <- makeFunctionType config a (XLam a b1' x2) -                t1' k1''-                t2 e2 c2_cut+        (xAbs', tAbs)+         <- makeFunction+                config a (XLam a b1' x2)+                b1' t1' k1'' +                x2' t2  e2 -        ctrace  $ vcat -                [ text "* Lam Check"-                , indent 2 $ ppr (XLam a b1' x2)-                , text "  IN:  " <> ppr tExpected-                , text "  OUT: " <> ppr tResult-                , indent 2 $ ppr ctx-                , indent 2 $ ppr ctx_cut++        -- Ensure that the final type matches the one we expected.+        --   The expected type may have had an existential for the parameter,+        --   which we want to unify with any type annotation that was on +        --   the abstraction.+        --   +        --   The `makeFunction` can also insert implicit box casts, so we +        --   need to check that the result of doing this is as expected.+        -- +        ctx5    <- makeEq config a ctx4 tAbs tExpected+                $  ErrorMismatch a tAbs tExpected xx++        tAbs'   <- applyContext ctx4 tAbs++        -- Cut the bound type and elems under it from the context.+        let ctx_cut     = popToPos pos1 ctx5++        ctrace  $ vcat+                [ text "*<  Lam CHECK"+                , text "    in  type: " <> ppr tExpected+                , text "    out type: " <> ppr tAbs'+                , indent 4 $ ppr ctx+                , indent 4 $ ppr ctx_cut                 , empty ] -        returnX a-                (\z -> XLam z b1' x2')-                tResult (Sum.empty kEffect) cResult-                ctx_cut+        return  ( xAbs'+                , tAbs'+                , Sum.empty kEffect+                , ctx_cut) ++-- The expected type is not a functional type, yet we have a lambda+-- abstraction. Fall through to the subsumtion checker which will+-- throw the error message. checkLam !table !a !ctx !b1 !x2 !(Check tExpected)- = checkSub table a ctx (XLam a b1 x2) tExpected+ = do   ctrace  $ vcat+                [ text "*>  Lam Check (not function)" ] +        checkSub table a ctx DemandNone (XLam a b1 x2) tExpected + ---------------------------------------------------------------------------------- | Construct a function-like type with the given effect and closure.+-- | Construct a function type with the given effect and closure. -- --   Whether this is a witness or data abstraction depends on the kind --   of the parameter type.@@ -270,78 +347,107 @@ --   is set by the Config, which depends on the specific language fragment --   that we're checking. ---makeFunctionType +makeFunction         :: (Show n, Ord n)-        => Config n              -- ^ Type checker config.-        -> a                     -- ^ Annotation for error messages.-        -> Exp a n               -- ^ Expression for error messages.-        -> Type n                -- ^ Parameter type of the function.-        -> Kind n                -- ^ Kind of the parameter.-        -> Type n                -- ^ Result type of the function.-        -> TypeSum n             -- ^ Effect sum.-        -> Set (TaggedClosure n) -- ^ Closure terms.-        -> CheckM a n (Type n, Set (TaggedClosure n))+        => Config n             -- ^ Type checker config.+        -> a                    -- ^ Annotation for error messages.+        -> Exp  a n             -- ^ Expression for error messages.+        -> Bind n               -- ^ Binder of the function parameter.+        -> Type n               -- ^ Parameter type of the function.+        -> Kind n               -- ^ Kind of the parameter.+        -> Exp  (AnTEC a n) n   -- ^ Body of the function.+        -> Type n               -- ^ Result type of the function.+        -> TypeSum n            -- ^ Effect sum.+        -> CheckM a n (Exp (AnTEC a n) n, Type n) -makeFunctionType config a xx t1 k1 t2 e2 c2- | isTExists k1- = throw $ ErrorLamBindBadKind a xx t1 k1+makeFunction config a xx bParam tParam kParam xBody tBody eBody+ | isTExists kParam+ = throw $ ErrorLamBindBadKind a xx tParam kParam - | not (k1 == kData) && not (k1 == kWitness)- = throw $ ErrorLamBindBadKind a xx t1 k1+ | not (kParam == kData) && not (kParam == kWitness)+ = throw $ ErrorLamBindBadKind a xx tParam kParam   | otherwise- = do   + = do         -- Get the universe the parameter value belongs to.-        let Just uniParam    = universeFromType2 k1--        -- Trim the closure before we annotate the returned function-        -- type with it. This should always succeed because trimClosure-        -- only returns Nothing if the closure is miskinded, and we've-        -- already already checked that.-        let c2_captured-                -- If we're not tracking closure information then just drop it -                -- on the floor.-                | not  $ configTrackedClosures config   = tBot kClosure-                | otherwise-                = let Just c = trimClosure $ closureOfTaggedSet c2 in c+        let Just uniParam    = universeFromType2 kParam -        let e2_captured-                -- If we're not tracking effect information then just drop it +        -- The effects due to evaluating the body that are +        -- captured by this abstraction.+        let eCaptured+                -- If we're not tracking effect information then just drop it                 -- on the floor.                 | not  $ configTrackedEffects config    = tBot kEffect-                | otherwise                             = TSum e2---        -- Data abstraction where the function type for the language fragment-        -- supports latent effects and closures.-        if      (  k1 == kData-                && configFunctionalEffects  config-                && configFunctionalClosures config)-         then   return  ( tFunEC t1 e2_captured c2_captured t2-                        , c2)+                | otherwise                             = TSum eBody          -- Data abstraction where the function constructor for the language         -- fragment does not suport latent effects or closures.-        else if (  k1 == kData-                && e2_captured == tBot kEffect-                && c2_captured == tBot kClosure)-         then   return  ( tFun t1 t2-                        , Set.empty)+        if (    kParam == kData+                && eCaptured == tBot kEffect)+         then let tAbs  = tFun tParam tBody+                  aAbs  = AnTEC tAbs (tBot kEffect) (tBot kClosure) a+              in  return ( XLam aAbs bParam xBody+                         , tAbs)          -- Witness abstractions must always be pure,         --  but closures are passed through.-        else if (  k1 == kWitness-                && e2_captured == tBot kEffect)-         then   return  ( tImpl t1 t2-                        , c2 )+        else if (  kParam == kWitness+                && eCaptured == tBot kEffect)+         then let tAbs  = tImpl tParam tBody+                  aAbs  = AnTEC tAbs (tBot kEffect) (tBot kClosure) a+              in  return ( XLam aAbs bParam xBody+                         , tAbs) -        -- We don't have a way of forming a function with an impure effect.-        else if (e2_captured /= tBot kEffect)-         then   throw $ ErrorLamNotPure  a xx uniParam e2_captured+        -- Handle ImplicitBoxBodies+        --   Evaluating the given body causes an effect, but the body of an+        --   abstraction must be pure. Automatically box up the body to build+        --   a suspension that we can abstract over. We justify the fact that+        --   inserting this cast is valid because if we didn't the program+        --   would be ill-typed, as the next case it to throw an error.+        else if (   configImplicitBox config+                && (eCaptured /= tBot kEffect))+         then +              case takeTSusp tBody of -        -- We don't have a way of forming a function with an non-empty closure.-        else if (c2_captured /= tBot kClosure)-         then   throw $ ErrorLamNotEmpty a xx uniParam c2_captured+                -- The body itself does not produce another suspension, +                -- so we can just box it up.+                Nothing +                 -> let tBodySusp = tSusp eCaptured tBody+                        aBox      = AnTEC tBodySusp (tBot kEffect) (tBot kClosure) a++                        tAbs      = tFun tParam tBodySusp+                        aAbs      = AnTEC tAbs      (tBot kEffect) (tBot kClosure) a++                    in  return  ( XLam aAbs bParam (XCast aBox CastBox xBody)+                                , tAbs)++                -- The body itself produces another suspension.+                -- Instead boxing this to form a result of type:+                --    S eCaptured (S eResult tResult)+                --+                -- we instead run the inner suspension and re-box it,+                -- so that we have a single suspension that includes both effects:+                --    S (eCaptured + eResult) tResult+                -- +                Just (eSusp, tResult)+                 -> let aRun      = AnTEC tResult eSusp (tBot kClosure) a++                        eTotal    = tSum kEffect [eSusp, eCaptured]+                        tBodySusp = tSusp eTotal tResult+                        aBox      = AnTEC tBodySusp (tBot kEffect) (tBot kClosure) a++                        tAbs      = tFun tParam tBodySusp+                        aAbs      = AnTEC tAbs      (tBot kEffect) (tBot kClosure) a++                    in  return  ( XLam aAbs bParam +                                        $ XCast aBox CastBox +                                        $ XCast aRun CastRun +                                        $ xBody+                                , tAbs)++        -- We don't have a way of forming a function with an impure effect.+        else if (eCaptured /= tBot kEffect)+         then   throw $ ErrorLamNotPure  a xx uniParam eCaptured          -- One of the above error reporting cases should have fired already.         else    error $ "ddc-core.makeFunctionType: is broken."

@@ -4,129 +4,153 @@ where import DDC.Core.Check.Judge.Type.Base import qualified DDC.Type.Sum   as Sum-import qualified Data.Set       as Set import Data.List                as L  +--------------------------------------------------------------------------------------------------- checkLet :: Checker a n  -- let ---------------------------------------------checkLet !table !ctx0 xx@(XLet a lts xBody) mode+checkLet !table !ctx0 mode demand xx@(XLet a lts xBody)  | case lts of         LLet{}  -> True         LRec{}  -> True         _       -> False - = do   let config  = tableConfig table+ = do   ctrace  $ vcat+                [ text "*>  Let" +                , text "    mode   =" <+> ppr mode +                , text "    demand =" <+> (text $ show demand)+                , empty]++        let config  = tableConfig table         let kenv    = tableKindEnv table          -- Check the bindings -------------------         -- Decide whether to use bidirectional type inference when checking         -- the types of the bindings.-        let useBidirChecking   +        let useBidirChecking                 = case mode of                         Recon   -> False                         Check{} -> True                         Synth   -> True-        -        (lts', bs', effsBinds, closBinds, pos1, ctx1)-         <- checkLetsM useBidirChecking xx table ctx0 lts  -        +        (lts', _bs', effsBinds, pos1, ctx1)+         <- checkLetsM useBidirChecking xx table ctx0 demand lts++         -- Check the body -----------------------         -- -- Check the body expression in a context         -- -- extended with the types of the bindings.-        (xBody', tBody, effsBody, closBody, ctx2)-         <- tableCheckExp table table ctx1 xBody mode+        ctrace  $ vcat+                [ text "*.  Let Body " <> ppr mode+                , text "    demand = " <> (text $ show demand)+                , empty] +        (xBody', tBody, effsBody, ctx2)+         <- tableCheckExp table table ctx1 mode demand xBody+         -- The body must have data kind.-        (tBody', kBody, ctx3)      +        (tBodyChecked, kBody, ctx3)          <- checkTypeM config kenv ctx2 UniverseSpec tBody          $  case mode of                 Recon   -> Recon                 _       -> Check kData-        -        let kBody' = applyContext ctx3 kBody++        kBody' <- applyContext ctx3 kBody         when (not $ isDataKind kBody')          $ throw $ ErrorLetBodyNotData a xx tBody kBody' +        tBody' <- applyContext ctx3 tBodyChecked -        -- Build the result ----------------------        -- Mask closure terms due to locally bound value vars.-        let clos_cut    = Set.fromList-                        $ mapMaybe (cutTaggedClosureXs bs')-                        $ Set.toList closBody+        -- Run the body if needed ---------------+        (xBodyRun, tBodyRun, eBodyRun)+         <- case mode of+                Synth   -> runForDemand (tableConfig table) a demand+                                xBody' tBody' (TSum effsBody) +                _       -> return (xBody', tBody', TSum effsBody)+++        -- Build the result ---------------------         -- The new effect and closure.-        let tResult     = applyContext ctx3 tBody'-        let effs'       = effsBinds `Sum.union` effsBody-        let clos'       = closBinds `Set.union` clos_cut+        let eResult     = tSum kEffect [TSum effsBinds, eBodyRun]          -- Pop the elements due to the let-bindings from the context.         let ctx_cut     = popToPos pos1 ctx3          ctrace  $ vcat-                [ text "* Let"-                , indent 2 $ ppr xx-                , text "  tResult:  " <> ppr tResult-                , indent 2 $ ppr ctx3-                , indent 2 $ ppr ctx_cut ]+                [ text "*<  Let " <> ppr mode+                , text "    demand = " <> (text $ show demand)+                , text "    -- EXP IN  ----"+                , indent 4 $ ppr xx+                , text "    -- EXP OUT ----"+                , indent 4 $ ppr (XLet (AnTEC tBodyRun (tBot kEffect) (tBot kClosure) a) +                                        lts' xBodyRun)+                , text "    --"+                , text "    tBodyRun:  " <> ppr tBodyRun+                , indent 4 $ ppr ctx3+                , indent 4 $ ppr ctx_cut +                , empty ] -        returnX a (\z -> XLet z lts' xBody')-                tResult effs' clos' ctx_cut+        returnX a +                (\z -> XLet z lts' xBodyRun)+                tBodyRun +                (Sum.fromList kEffect [eResult])+                ctx_cut   -- others --------------------------------------- -- The dispatcher should only call checkLet with a XLet AST node.-checkLet _ _ _ _-        = error "ddc-core.checkLet: no match"        +checkLet _ _ _ _ _+        = error "ddc-core.checkLet: no match"  --------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------- -- | Check some let bindings, --   and push their binders onto the context.-checkLetsM -        :: (Show n, Pretty n, Ord n)+checkLetsM+        :: (Show a, Show n, Pretty n, Ord n)         => Bool                         -- ^ Use bidirectional inference.         -> Exp a n                      -- ^ Expression for error messages.         -> Table a n                    -- ^ Static configuration.         -> Context n                    -- ^ Input context.+        -> Demand                       -- ^ Demand placed on the bindings.         -> Lets a n                     -- ^ Let-bindings to check.         -> CheckM a n                 ( Lets (AnTEC a n) n    --   Let-bindings annotated with types.                 , [Bind n]              --   Binding occs of vars, with types.                 , TypeSum n             --   Effect of evaluating all the bindings.-                , Set (TaggedClosure n) --   Closure of all the bindings.                 , Pos                   --   Context position with bindings pushed.                 , Context n)            --   Output context. -checkLetsM !bidir xx !table !ctx0 (LLet b xBind)- +checkLetsM !bidir xx !table !ctx0 !demand (LLet b xBind)+  -- Reconstruct the type of a non-recursive let-binding.  | False  <- bidir- = do   + = do         let config      = tableConfig table         let kenv        = tableKindEnv table         let a           = annotOfExp xx          -- Reconstruct the type of the binding.-        (xBind', tBind, effsBind, closBind, ctx1) -         <- tableCheckExp table table ctx0 xBind Recon-        +        (xBind', tBind, effsBind, ctx1)+         <- tableCheckExp table table ctx0 Recon demand xBind+         -- The kind of the binding must be Data.-        (_, kBind', _) +        (_, kBind', _)          <- checkTypeM config kenv ctx1 UniverseSpec tBind Recon          when (not $ isDataKind kBind')          $ throw $ ErrorLetBindingNotData a xx b kBind'-        +         -- If there is a type annotation on the binding then this         -- must match the reconstructed type.         when (not $ isBot (typeOfBind b))          $ if equivT (typeOfBind b) tBind                 then return ()-                else (throw $ ErrorLetMismatch a xx b tBind)          -        +                else (throw $ ErrorLetMismatch a xx b tBind)+         -- Update the annotation on the binder with the actual type of         -- the binding.         let b'  = replaceTypeOfBind tBind b@@ -137,25 +161,26 @@          return  ( LLet b' xBind'                 , [b']-                , effsBind, closBind+                , effsBind                 , pos1, ctx3)   -- Synthesise the type of a non-recursive let-binding,  -- using any annotation on the binder as the expected type.  | True   <- bidir- = do   + = do         let config      = tableConfig table         let kenv        = tableKindEnv table-        +        let a           = annotOfExp xx+         -- If the binder has a type annotation then we use that as the expected         -- type when checking the binding. Any annotation must also have kind         -- Data, which we verify here.         let tAnnot      = typeOfBind b-        (modeCheck, ctx1)+        (mode, ctx1)          <- if isBot tAnnot              -- There is no annotation on the binder.              then return (Synth, ctx0)-             +              -- Check the type annotation on the binder,              -- expecting the kind to be Data.              else do@@ -163,69 +188,105 @@                  <- checkTypeM config kenv ctx0 UniverseSpec tAnnot (Check kData)                 return (Check tAnnot', ctx1) +        ctrace  $ vcat+                [ text "*>  Let Bind"  <+> ppr mode+                , text "    demand = " <> (text $ show demand)+                , text "    bind   = " <> (ppr b)+                , empty ]+         -- Check the expression in the right of the binding.-        (xBind', tBind1, effsBind, closBind, ctx2)-         <- tableCheckExp table table ctx1 xBind modeCheck+        (xBind_raw, tBind_raw, effs_raw, ctx2)+         <- tableCheckExp table table ctx1 mode demand xBind +        tBind_ctx <- applyContext ctx2 tBind_raw++        -- Handle ImplictRunBindings+        --   If the right of the binding is a suspended expression, but there is+        --   no binder then the expression is probably being evaluated for its+        --   effect only. If ImplicitRunBindings is enabled then we automatically+        --   run the suspension to release its effect.+        let (xBind_run, tBind_run, effs_run)+                | configImplicitRun $ tableConfig table +                , not $ isXCastBox xBind_raw+                , not $ isXCastRun xBind_raw+                , Just  (effs_susp, tBind_susp) <- takeTSusp tBind_ctx+                = let   +                        -- Effect of overall expression is effect of computing+                        -- the suspension plus the effect we get by running+                        -- that suspension.+                        effs_result = Sum.insert effs_susp effs_raw++                        -- Annotation for the resulting cast expression.+                        a'          = AnTEC tBind_susp (TSum $ effs_result)+                                            (tBot kClosure) a+                  in    ( XCast a' CastRun xBind_raw+                        , tBind_susp+                        , effs_result)++                | otherwise+                = (xBind_raw, tBind_raw, effs_raw)++         -- Update the annotation on the binder with the actual type of         -- the binding.-        let tBind2      = applyContext ctx2 tBind1-        let b'          = replaceTypeOfBind tBind2 b+        let b'           = replaceTypeOfBind tBind_run b          -- Push the binder on the context.         let (ctx3, pos1) =  markContext ctx2         let ctx4         =  pushType b' ctx3 -        return  ( LLet b' xBind'+        return  ( LLet b' xBind_run                 , [b']-                , effsBind, closBind+                , effs_run                 , pos1, ctx4)   -- letrec ----------------------------------------checkLetsM !bidir !xx !table !ctx0 (LRec bxs)+checkLetsM !bidir !xx !table !ctx0 !demand (LRec bxs)  = do   let (bs, xs)    = unzip bxs         let a           = annotOfExp xx +        ctrace  $ vcat+                [ text "*>  Let Rec"+                , text "    demand = " <> (text $ show demand)+                , text "    binds  = " <> (ppr  $ map fst bxs)+                , empty ]+         -- Named binders cannot be multiply defined.         checkNoDuplicateBindings a xx bs          -- All right hand sides must be syntactic abstractions.-        checkSyntacticLambdas a xx xs+        checkSyntacticLambdas table a xx xs -        -- Check the type annotations on all the binders.       -        (bs', ctx1)      <- checkRecBinds table bidir a xx ctx0 bs+        -- Check the type annotations on all the binders.+        (bs', ctx1)+         <- checkRecBinds table bidir a xx ctx0 bs          -- All variables are in scope in all right hand sides.         let (ctx2, pos1) =  markContext ctx1         let ctx3         =  pushTypes bs' ctx2          -- Check the right hand sides.-        (results, ctx4)  <- checkRecBindExps table bidir a ctx3 (zip bs' xs)--        let (bs'', xsRight', clossBinds)-                = unzip3 results+        (results, ctx4)  +         <- checkRecBindExps table bidir a ctx3 demand (zip bs' xs) -        -- Cut closure terms due to locally bound value vars.-        let clos_cut -                 = Set.fromList-                 $ mapMaybe (cutTaggedClosureXs bs)-                 $ Set.toList $ Set.unions clossBinds+        let (bs'', xsRight')+                = unzip results          return  ( LRec (zip bs'' xsRight')                 , bs''-                , Sum.empty kEffect, clos_cut+                , Sum.empty kEffect                 , pos1, ctx4)   -- others ------------------------------------------ The dispatcher should only call checkLet with LLet and LRec AST nodes, +-- The dispatcher should only call checkLet with LLet and LRec AST nodes, -- so we should not see the others here.-checkLetsM _ _ _ _ _+checkLetsM _ _ _ _ _ _         = error "ddc-core.checkLetsM: no match"  --------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------- -- | Check the annotations on a group of recursive binders. checkRecBinds         :: (Pretty n, Show n, Ord n)@@ -233,9 +294,9 @@         -> Bool                         -- ^ Use bidirectional checking.         -> a                            -- ^ Annotation for error messages.         -> Exp a n                      -- ^ Expression for error messages.-        -> Context n                    -- ^ Original context.                     +        -> Context n                    -- ^ Original context.         -> [Bind n]                     -- ^ Input binding group.-        -> CheckM a n +        -> CheckM a n                 ( [Bind n]              --   Result binding group.                 ,  Context n)           --   Output context. @@ -256,14 +317,14 @@         checkRecBind b ctx          = case bidir of             False-             -> do      +             -> do                 -- In Recon mode, all recursive let-bindings must have full                 -- type annotations.                 when (isBot $ typeOfBind b)                  $ throw $ ErrorLetrecMissingAnnot a b xx                  -- Check the type on the binder.-                (b', k, ctx') +                (b', k, ctx')                  <- checkBindM config kenv ctx UniverseSpec b Recon                  -- The type on the binder must have kind Data.@@ -282,85 +343,121 @@                    let b'   = replaceTypeOfBind t b                    return (b', ctx') -             -- Recursive let-binding has a type annotation, +             -- Recursive let-binding has a type annotation,              -- so check it, expecting it to have kind Data.              | otherwise              -> do-                (b0, _k, ctx1) +                (b0, _k, ctx1)                  <- checkBindM config kenv ctx UniverseSpec b (Check kData) -                let t0  = typeOfBind b0-                let t1  = applyContext ctx1 t0-                let b1  = replaceTypeOfBind t1 b0+                let t0  =  typeOfBind b0+                t1      <- applyContext ctx1 t0+                let b1  =  replaceTypeOfBind t1 b0                  return (b1, ctx1)  --------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------- -- | Check some recursive bindings. --   Doing this won't push any more bindings onto the context, --   though it may solve some existentials in it. checkRecBindExps-        :: (Pretty n, Show n, Ord n)+        :: (Show a, Show n, Ord n, Pretty n)         => Table a n         -> Bool                         -- ^ Use bidirectional checking.         -> a                            -- ^ Annotation for error messages.         -> Context n                    -- ^ Original context.+        -> Demand                       -- ^ Demand placed on bindings.         -> [(Bind n, Exp a n)]          -- ^ Bindings and exps for rec bindings.-        -> CheckM a n +        -> CheckM a n                 ( [ ( Bind n                   -- Result bindiner.-                    , Exp (AnTEC a n) n        -- Result expression.-                    , Set (TaggedClosure n))]  -- Result closure.+                    , Exp (AnTEC a n) n)]      -- Result expression.                 , Context n) -checkRecBindExps table bidir a ctx0 bxs0+checkRecBindExps table False a ctx0 demand bxs0  = go bxs0 ctx0- where  -        go [] ctx       + where+        go [] ctx          = return ([], ctx)-        -        go ((b, x) : bxs) ctx-         = do   (result, ctx')  <- checkRecBindExp b x ctx-                (moar,   ctx'') <- go bxs ctx'-                return (result : moar, ctx'') -        checkRecBindExp b x ctx-         = case bidir of-            False -             -> do+        go ((b, xBind) : bxs) ctx+         = do   +                ctrace  $ vcat+                        [ text "*>  Let Rec Bind RECON"+                        , text "    demand     = " <> (text $ show demand)+                        , text "    in binder  = " <> ppr (binderOfBind b)+                        , text "    in type    = " <> ppr (typeOfBind   b)+                        , empty ]+                 -- Check the right of the binding.                 --  We checked that the expression is a syntactic lambda                 --  abstraction in checkLetsM, so we know the effect is pure.-                (x', t, _effs, clos, ctx')-                 <- tableCheckExp table table ctx x Recon+                (xBind', t, _effs, ctx')+                 <- tableCheckExp table table ctx Recon demand xBind                  -- Check the annotation on the binder matches the reconstructed                 -- type of the binding.                 when (not $ equivT (typeOfBind b) t)-                 $ throw $ ErrorLetMismatch a x b t+                 $ throw $ ErrorLetMismatch a xBind b t                  -- Reconstructing the types of binders adds missing kind info to                 -- constructors etc, so update the binders with this new info.                 let b'  = replaceTypeOfBind t b -                return ( (b', x', clos), ctx')+                ctrace  $ vcat+                        [ text "*<  Let Rec Bind RECON"+                        , text "    demand     =" <+> (text $ show demand)+                        , text "    in  binder =" <+> ppr (binderOfBind b)+                        , text "    in  type   =" <+> ppr (typeOfBind   b)+                        , text "    out type   =" <+> ppr t +                        , empty ] -            True-             -> do+                -- Check the rest of the bindings.+                (moar,   ctx'') <- go bxs ctx'++                return ((b', xBind') : moar, ctx'')++checkRecBindExps table True _a ctx0 demand bxs0+ = go bxs0 ctx0+ where+        go [] ctx+         = return ([], ctx)++        go ((b, xBind) : bxs) ctx+         = do+                ctrace  $ vcat+                        [ text "*>  Let Rec Bind BIDIR"+                        , text "    demand    =" <+> (text $ show demand)+                        , text "    in binder =" <+> ppr (binderOfBind b)+                        , text "    in type   =" <+> ppr (typeOfBind   b)+                        , empty ]+                 -- Check the right of the binding.                 --  We checked that the expression is a syntactic lambda                 --  abstraction in checkLetsM, so we know the effect is pure.-                (x', t, _effs, clos, ctx')-                 <- tableCheckExp table table ctx x (Check (typeOfBind b))+                (xBind', t, _effs, ctx')+                 <- tableCheckExp table table ctx +                        (Check (typeOfBind b)) demand xBind                  -- Reconstructing the types of binders adds missing kind info to                 -- constructors etc, so update the binders with this new info.                 let b'  = replaceTypeOfBind t b -                return ((b', x', clos), ctx')+                ctrace  $ vcat+                        [ text "*<  Let Rec Bind BIDIR"+                        , text "    demand     =" <+> (text $ show demand)+                        , text "    in  binder =" <+> ppr (binderOfBind b)+                        , text "    in  type   =" <+> ppr (typeOfBind   b)+                        , text "    out type   =" <+> ppr t +                        , empty ] +                -- Check the rest of the bindings.+                (moar, ctx'') <- go bxs ctx' --------------------------------------------------------------------------------+                return ((b', xBind') : moar, ctx'')+++--------------------------------------------------------------------------------------------------- -- | Check that the given list of binds does not contain duplicates --   that would conflict if we added them to the environment --   at the same level. If so, then throw and error.@@ -383,20 +480,25 @@ duplicates (x : xs)         | L.elem x xs   = x : duplicates (filter (/= x) xs)         | otherwise     = duplicates xs-         --------------------------------------------------------------------------------++--------------------------------------------------------------------------------------------------- -- | Check that all the bindings in a recursive let are syntactic lambdas. --   We don't support value recursion, so can only define recursive functions. --   If one of the expression is not a lambda then throw an error. checkSyntacticLambdas-        :: a                    -- ^ Annotation for error messages.+        :: Table a n+        -> a                    -- ^ Annotation for error messages.         -> Exp a n              -- ^ Expression for error message.         -> [Exp a n]            -- ^ Expressions to check.         -> CheckM a n () -checkSyntacticLambdas a xx xs- = forM_ xs $ \x -        -> when (not $ (isXLam x || isXLAM x))-        $ throw $ ErrorLetrecBindingNotLambda a xx x+checkSyntacticLambdas table a xx xs+        | configGeneralLetRec $ tableConfig table+        = return ()++        | otherwise+        = forM_ xs $ \x+                -> when (not $ (isXLam x || isXLAM x))+                $  throw $ ErrorLetrecBindingNotLambda a xx x 

@@ -12,25 +12,36 @@ checkLetPrivate :: Checker a n  -- private ---------------------------------------checkLetPrivate !table !ctx -        xx@(XLet a (LPrivate bsRgn mtParent bsWit) x) mode+checkLetPrivate !table !ctx mode demand+        xx@(XLet a (LPrivate bsRgn mtParent bsWit) x)+  = case takeSubstBoundsOfBinds bsRgn of-    []   -> tableCheckExp table table ctx x Recon+    []   -> tableCheckExp table table ctx Recon demand x+     us   -> do         let config      = tableConfig table         let kenv        = tableKindEnv table         let depth       = length $ map isBAnon bsRgn +        ctrace  $ vcat+                [ text "*>  Let Private"+                , text "    mode             =" <+> ppr mode+                , text "    demand           =" <+> text (show demand)+                , text "    in region binds  =" <+> ppr bsRgn+                , text "    in parent bind   =" <+> text (show mtParent)+                , text "    in witness binds =" <+> ppr bsWit+                , empty ]+         -- Check the kinds of the region binders.         -- These must already set to kind Region.-        (bsRgn', _, _)  +        (bsRgn', _, _)          <- liftM unzip3          $  mapM (\b -> checkBindM config kenv ctx UniverseKind b Recon)                  bsRgn         let ksRgn       = map typeOfBind bsRgn'-        +         -- The binders must have region kind.-        when (any (not . isRegionKind) ksRgn) +        when (any (not . isRegionKind) ksRgn)          $ throw $ ErrorLetRegionsNotRegion a xx bsRgn ksRgn          -- We can't shadow region binders because we might have witnesses@@ -38,37 +49,41 @@         let rebounds    = filter (flip memberKindBind ctx) bsRgn'         when (not $ null rebounds)          $ throw $ ErrorLetRegionsRebound a xx rebounds-        +         -- Check the witness binders.         -- These must have full type annotations, as we don't infer         -- the types of introduced witnesses.         let (ctx', pos1) = markContext ctx         let ctx1         = pushKinds [(b, RoleConcrete) | b <- bsRgn] ctx'         let ctx2         = liftTypes depth ctx1-        (bsWit', _, _)   +        (bsWit', _, _)          <- liftM unzip3-         $  mapM (\b -> checkBindM config kenv ctx2 UniverseSpec b Recon) +         $  mapM (\b -> checkBindM config kenv ctx2 UniverseSpec b Recon)                  bsWit-        +         -- Check that the witnesses bound here are for the region,         -- and they don't conflict with each other.         checkWitnessBindsM config a kenv ctx xx us bsWit'          -- Check the body expression.+        --   We always want to do this in 'Synth' mode as the expected+        --   type uses the region names visible from outside, and will+        --   not mention local regions are introduced by the 'private'+        --   construct.         let ctx3        = pushTypes bsWit' ctx2-        (xBody3, tBody3, effs3, clo, ctx4)  -          <- tableCheckExp table table ctx3 x mode+        (xBody3, tBody3, effs3, ctx4)+          <- tableCheckExp table table ctx3 Synth demand x          -- The body type must have data kind.-        (tBody4, kBody4, ctx5)   -         <- checkTypeM config kenv ctx4 UniverseSpec tBody3-         $  case mode of+        (tBody4, kBody4, ctx5)+          <- checkTypeM config kenv ctx4 UniverseSpec tBody3+          $  case mode of                 Recon   -> Recon                 _       -> Check kData -        let tBody5      = applyContext ctx5 tBody4-        let kBody5      = applyContext ctx5 kBody4-        let TSum effs5  = applyContext ctx5 (TSum effs3)+        tBody5      <- applyContext ctx5 tBody4+        kBody5      <- applyContext ctx5 kBody4+        TSum effs5  <- applyContext ctx5 (TSum effs3)         when (not $ isDataKind kBody5)          $ throw $ ErrorLetBodyNotData a xx tBody5 kBody5 @@ -76,13 +91,13 @@         tBody_final          <- case mtParent of                 -- If the bound region variables are children of some parent-                -- region then they are merged into the parent when the +                -- region then they are merged into the parent when the                 -- private/extend construct ends.                 Just tParent-                 -> do  return $ foldl  (\t b -> substituteTX b tParent t) +                 -> do  return $ foldl  (\t b -> substituteTX b tParent t)                                         tBody5 bsRgn -                -- If the bound region variables have no parent then they are +                -- If the bound region variables have no parent then they are                 -- deallocated when the private construct ends.                 -- The bound region variables cannot be free in the body type.                 _@@ -91,17 +106,27 @@                          $ throw $ ErrorLetRegionFree a xx bsRgn tBody5                         return $ lowerT depth tBody5 +        -- Check that the result matches any expected type.+        ctx6    <- case mode of+                    Check tExpected+                     -> do  makeEq config a ctx5 tExpected tBody_final+                             $  ErrorMismatch a tExpected tBody_final xx++                    _ -> return ctx5++        tBody_final' <- applyContext ctx6 tBody_final+         -- Delete effects on the bound region from the result.         let delEff es u = Sum.delete (tRead  (TVar u))                         $ Sum.delete (tWrite (TVar u))                         $ Sum.delete (tAlloc (TVar u))                         $ es-        +         -- The final effect type.         effs_cut          <- case mtParent of                 -- If the bound region variables are children of some parent-                -- region then the overall effect is to allocate into +                -- region then the overall effect is to allocate into                 -- the parent.                 Just tParent                   -> return $ (lowerT depth $ foldl delEff effs5 us)@@ -110,93 +135,27 @@                 -- If the bound region variables have no parent then they                 -- are deallocated when the private construct ends and no                 -- effect on these regions is visible.-                _ -> return $ lowerT depth -                            $ foldl delEff effs5 us --        -- Delete the bound region variable from the closure.-        -- Mask closure terms due to locally bound region vars.-        let cutClo c r  = mapMaybe (cutTaggedClosureT r) c-        let clos_cut    = Set.fromList -                        $ foldl cutClo (Set.toList clo) bsRgn+                _ -> return $ lowerT depth+                            $ foldl delEff effs5 us          -- Cut stack back to the length we started with,         --  remembering to lower to undo the lift we applied previously.         let ctx_cut     = lowerTypes depth-                        $ popToPos pos1 ctx5+                        $ popToPos pos1 ctx6          returnX a                 (\z -> XLet z (LPrivate bsRgn mtParent bsWit) xBody3)-                tBody_final effs_cut clos_cut-                ctx_cut+                tBody_final' effs_cut ctx_cut  --- withregion ------------------------------------checkLetPrivate !table !ctx0-        xx@(XLet a (LWithRegion u) x) mode- = do   let config      = tableConfig table-        let kenv        = tableKindEnv table--        -- The handle must have region kind.-        -- We need to look in the KindEnv as well as the Context here, -        --  because the KindEnv knows the types of primitive variables.-        (case listToMaybe  -                $ catMaybes [ Env.lookup u kenv-                            , liftM fst $ lookupKind u ctx0] of-          Nothing -> throw $ ErrorUndefinedVar a u UniverseSpec--          Just k  |  not $ isRegionKind k-                  -> throw $ ErrorWithRegionNotRegion a xx u k--          _       -> return ())-        -        -- Check the body expression.-        (xBody0, tBody0, effs0, clo, ctx1) -         <- tableCheckExp table table ctx0 x mode--        -- The body type must have data kind.-        (tBody1, kBody1, ctx2) -         <- checkTypeM config kenv ctx1 UniverseSpec tBody0-         $  case mode of-                Recon   -> Recon-                _       -> Check kData--        let tBody2      = applyContext ctx2 tBody1-        let kBody2      = applyContext ctx2 kBody1-        let TSum effs2  = applyContext ctx2 (TSum effs0)-        -        when (not $ isDataKind kBody2)-         $ throw $ ErrorLetBodyNotData a xx tBody2 kBody2-        -        -- The bound region variable cannot be free in the body type.-        let tcs         = supportTyCon-                        $ support Env.empty Env.empty tBody2-        -        when (Set.member u tcs)-         $ throw $ ErrorWithRegionFree a xx u tBody2--        -- Delete effects on the bound region from the result.-        let tu          = TVar u-        let effs_cut    = Sum.delete (tRead  tu)-                        $ Sum.delete (tWrite tu)-                        $ Sum.delete (tAlloc tu)-                        $ effs2-        -        -- Delete the bound region handle from the closure.-        let clos_cut    = Set.delete (GBoundRgnCon u) clo--        returnX a-                (\z -> XLet z (LWithRegion u) xBody0)-                tBody2 effs_cut clos_cut-                ctx2--checkLetPrivate _ _ _ _-        = error "ddc-core.checkLetPrivate: no match"        +checkLetPrivate _ _ _ _ _+        = error "ddc-core.checkLetPrivate: no match"   ------------------------------------------------------------------------------- -- | Check the set of witness bindings bound in a letregion for conflicts.-checkWitnessBindsM -        :: (Show n, Ord n) +checkWitnessBindsM+        :: (Show n, Ord n)         => Config n             -- ^ Type checker config.         -> a                    -- ^ Annotation for error messages.         -> KindEnv n            -- ^ Kind Environment.@@ -214,14 +173,14 @@         -- when using the Eval fragment.         inEnv tt          = case tt of-             TVar u'                +             TVar u'                 | Env.member u' kenv    -> True                 | memberKind u' ctx     -> True-             -             TCon (TyConBound u' _) ++             TCon (TyConBound u' _)                 | Env.member u' kenv    -> True                 | memberKind u' ctx     -> True-             _                          -> False +             _                          -> False           -- Check the argument of a witness type is for the region we're@@ -229,27 +188,25 @@         checkWitnessArg bWit t2          = case t2 of             TVar u'-             |  all (/= u') uRegions +             |  all (/= u') uRegions              -> throw $ ErrorLetRegionsWitnessOther a xx uRegions bWit              | otherwise -> return ()              TCon (TyConBound u' _)-             | all (/= u') uRegions +             | all (/= u') uRegions              -> throw $ ErrorLetRegionsWitnessOther a xx uRegions bWit              | otherwise -> return ()-            -            -- The parser should ensure the right of a witness is a ++            -- The parser should ensure the right of a witness is a             -- constructor or variable.             _            -> throw $ ErrorLetRegionWitnessInvalid a xx bWit-    +         -- Associate each witness binder with its type.         btsWit  = [(typeOfBind b, b) | b <- bsWit]-  +         -- Check a single witness binder for conflicts with other witnesses.         checkWitnessBindM bWit          = case typeOfBind bWit of-            TApp (TCon (TyConWitness TwConGlobal))   t2-             -> checkWitnessArg bWit t2              TApp (TCon (TyConWitness TwConConst))    t2              | Just bConflict <- L.lookup (tMutable t2) btsWit@@ -261,16 +218,6 @@              -> throw $ ErrorLetRegionWitnessConflict a xx bWit bConflict              | otherwise    -> checkWitnessArg bWit t2 -            TApp (TCon (TyConWitness TwConLazy))     t2-             | Just bConflict <- L.lookup (tManifest t2) btsWit-             -> throw $ ErrorLetRegionWitnessConflict a xx bWit bConflict-             | otherwise    -> checkWitnessArg bWit t2--            TApp (TCon (TyConWitness TwConManifest)) t2-             | Just bConflict <- L.lookup (tLazy t2)     btsWit-             -> throw $ ErrorLetRegionWitnessConflict a xx bWit bConflict-             | otherwise    -> checkWitnessArg bWit t2-                      (takeTyConApps -> Just (TyConWitness (TwConDistinct 2), [t1, t2]))              | inEnv t1  -> checkWitnessArg bWit t2              | inEnv t2  -> checkWitnessArg bWit t1

@@ -6,33 +6,46 @@   -- This is the subtyping rule for the type checking judgment.-checkSub table !a ctx0 xx0 tExpect- = do   let config      = tableConfig table- -        (xx1, tSynth, eff, clo, ctx1)-         <- tableCheckExp table table ctx0 xx0 Synth+checkSub table !a ctx0 demand xx0 tExpect+ = do   +        ctrace  $ vcat +                [ text "*>  Sub Check"+                , text "    demand:  " <> (text $ show demand)+                , text "    tExpect: " <> (ppr tExpect) +                , empty ] +        let config      = tableConfig table++        (xx1, tSynth, eff, ctx1)+         <- tableCheckExp table table ctx0 Synth demand xx0 +         -- Substitute context into synthesised and expected types.-        let tSynth'     = applyContext ctx1 tSynth-        let tExpect'    = applyContext ctx1 tExpect-        -        (xx2, ctx2)     <- makeSub config a +        tSynth'  <- applyContext ctx1 tSynth+        tExpect' <- applyContext ctx1 tExpect++        ctrace  $ vcat+                [ text "*.  Sub Check"+                , text "    demand:  " <> (text $ show demand)+                , text "    tExpect: " <> (ppr tExpect) +                , empty ]++        (xx2, ctx2)     <- makeSub config a                                 ctx1 xx1 tSynth' tExpect'                         $  ErrorMismatch a  tSynth' tExpect' xx0          ctrace  $ vcat-                [ text "* Sub"-                , indent 2 $ ppr xx0-                , text "  tExpect:  " <> ppr tExpect-                , text "  tSynth:   " <> ppr tSynth-                , text "  tExpect': " <> ppr tExpect'-                , text "  tSynth':  " <> ppr tSynth'-                , indent 2 $ ppr ctx0-                , indent 2 $ ppr ctx1-                , indent 2 $ ppr ctx2 +                [ text "*<  Sub"+                , indent 4 $ ppr xx0+                , text "    tExpect:  " <> ppr tExpect+                , text "    tSynth:   " <> ppr tSynth+                , text "    tExpect': " <> ppr tExpect'+                , text "    tSynth':  " <> ppr tSynth'+                , indent 4 $ ppr ctx0+                , indent 4 $ ppr ctx1+                , indent 4 $ ppr ctx2                 , empty ]          returnX a                 (\_ -> xx2)                 tExpect-                eff clo ctx2+                eff ctx2

@@ -8,34 +8,32 @@ import qualified DDC.Type.Env   as Env import qualified DDC.Type.Sum   as Sum import qualified Data.Map       as Map-import qualified Data.Set       as Set   checkVarCon :: Checker a n  -- variables -------------------------------------checkVarCon !table !ctx xx@(XVar a u) mode- +checkVarCon !table !ctx mode demand xx@(XVar a u)+  -- Look in the local context.  | Just t       <- lookupType u ctx  = case mode of         -- Check subsumption against an existing type.         -- This may instantiate existentials in the exising type.         Check tExpect-         ->     checkSub table a ctx xx tExpect+         ->     checkSub table a ctx demand xx tExpect          _ -> do ctrace  $ vcat-                        [ text "* Var Local"-                        , indent 2 $ ppr xx-                        , text "  TYPE:  " <> ppr t-                        , indent 2 $ ppr ctx +                        [ text "**  Var Local"+                        , indent 4 $ ppr xx+                        , text "    tVar: " <> ppr t+                        , indent 4 $ ppr ctx                         , empty ]                  returnX a                         (\z -> XVar z u)                         t                         (Sum.empty kEffect)-                        (Set.singleton $ taggedClosureOfValBound t u)                         ctx   -- Look in the global environment.@@ -44,40 +42,40 @@         -- Check subsumption against an existing type.         -- This may instantiate existentials in the exising type.         Check tExpect-         ->     checkSub table a ctx xx tExpect+         ->     checkSub table a ctx demand xx tExpect          _ -> do ctrace  $ vcat-                        [ text "* Var Global"-                        , indent 2 $ ppr xx-                        , text "  TYPE:  " <> ppr t-                        , indent 2 $ ppr ctx+                        [ text "**  Var Global"+                        , indent 4 $ ppr xx+                        , text "    tVar: " <> ppr t+                        , indent 4 $ ppr ctx                         , empty ] -                returnX a +                returnX a                         (\z -> XVar z u)                         t                         (Sum.empty kEffect)-                        (Set.singleton $ taggedClosureOfValBound t u)                         ctx- +  -- Can't find this variable name in the environment.  | otherwise  = throw $ ErrorUndefinedVar a u UniverseData-          + -- constructors ----------------------------------checkVarCon !table !ctx xx@(XCon a dc) mode+checkVarCon !table !ctx mode demand xx@(XCon a dc)   -- For recon and synthesis we already know what type the constructor  -- should have, so we can use that.- | mode == Recon || mode == Synth - = do   let config      = tableConfig table+ | mode == Recon || mode == Synth+ = do+        let config      = tableConfig table         let defs        = configDataDefs config          -- All data constructors need to have valid type annotations.-        tCtor +        tCtor          <- case dc of              DaConUnit   -> return tUnit-             +              DaConPrim{} -> return $ daConType dc               DaConBound n@@ -92,10 +90,10 @@         checkDaConM config xx a dc          ctrace  $ vcat-                [ text "* Con"-                , indent 2 $ ppr xx-                , text "  TYPE:  " <> ppr tCtor-                , indent 2 $ ppr ctx+                [ text "**  Con"+                , indent 4 $ ppr xx+                , text "    tCon: " <> ppr tCtor+                , indent 4 $ ppr ctx                 , empty ]          -- Type of the data constructor.@@ -103,17 +101,16 @@                 (\z -> XCon z dc)                 tCtor                 (Sum.empty kEffect)-                Set.empty                 ctx   -- Check subsumption against an existing type.  -- This may instantiate existentials in the exising type.  | otherwise  , Check tExpect    <- mode- = checkSub table a ctx xx tExpect+ = checkSub table a ctx demand xx tExpect   -- others ----------------------------------------checkVarCon _ _ _ _+checkVarCon _ _ _ _ _  = error "ddc-core.checkVarCon: no match" 

@@ -5,11 +5,11 @@ import DDC.Core.Check.Witness import DDC.Core.Check.Judge.Type.Base import qualified DDC.Type.Sum           as Sum-import qualified Data.Set               as Set   checkWit :: Checker a n-checkWit !table !ctx (XWitness a w1) _+checkWit !table !ctx _mode _demand +        (XWitness a w1)  = do   let config      = tableConfig table         let kenv        = tableKindEnv table         let tenv        = tableTypeEnv table@@ -22,8 +22,7 @@                 (\z -> XWitness z w1TEC)                 t1                 (Sum.empty kEffect)-                Set.empty                 ctx -checkWit _ _ _ _+checkWit _ _ _ _ _  = error "ddc-core.checkWit: no match"

@@ -3,7 +3,7 @@         ( checkModule         , checkModuleM) where-import DDC.Core.Check.Base      (checkTypeM)+import DDC.Core.Check.Base      (checkTypeM, applySolved) import DDC.Core.Check.Exp import DDC.Core.Check.Error import DDC.Core.Transform.Reannotate@@ -20,11 +20,10 @@ import DDC.Base.Pretty import DDC.Type.Env             (KindEnv, TypeEnv) import DDC.Control.Monad.Check  (runCheck, throw)-import Data.Monoid import DDC.Data.ListUtils import Control.Monad-import qualified DDC.Type.Env   as Env-import qualified Data.Map       as Map+import qualified DDC.Type.Env           as Env+import qualified Data.Map.Strict        as Map   -- Wrappers ---------------------------------------------------------------------------------------@@ -35,7 +34,7 @@ -- --   If it's bad, you get a description of the error. checkModule-        :: (Ord n, Show n, Pretty n)+        :: (Show a, Ord n, Show n, Pretty n)         => Config n             -- ^ Static configuration.         -> Module a n           -- ^ Module to check.         -> Mode n               -- ^ Type checker mode.@@ -44,7 +43,7 @@  checkModule !config !xx !mode  = let  (s, result)     = runCheck (mempty, 0, 0)-                        $ checkModuleM config +                        $ checkModuleM config                                 (configPrimKinds config)                                 (configPrimTypes config)                                 xx mode@@ -54,8 +53,8 @@  -- checkModule ------------------------------------------------------------------------------------ -- | Like `checkModule` but using the `CheckM` monad to handle errors.-checkModuleM -        :: (Ord n, Show n, Pretty n)+checkModuleM+        :: (Show a, Ord n, Show n, Pretty n)         => Config n             -- ^ Static configuration.         -> KindEnv n            -- ^ Starting kind environment.         -> TypeEnv n            -- ^ Starting type environment.@@ -64,96 +63,145 @@         -> CheckM a n (Module (AnTEC a n) n)  checkModuleM !config !kenv !tenv mm@ModuleCore{} !mode- = do   + = do         -- Check kinds of imported types -------------------        nksImport'      <- checkImportTypes config mode   +        nksImported'    <- checkImportTypes config mode                         $  moduleImportTypes mm -        -- Build the initial kind environment.-        let kenv'       = Env.union kenv -                        $ Env.fromList  [ BName n (typeOfImportSource isrc)-                                                | (n, isrc) <- nksImport' ] +        -- Check imported data type defs ------------------+        let defsImported = moduleImportDataDefs mm+        defsImported'   <- case checkDataDefs config defsImported of+                                (err : _, _)      -> throw $ ErrorData err+                                ([], defsImported') -> return defsImported' ++        -- Build the imported defs and kind environment.+        --  This contains kinds of type visible in the imported values.+        let config_import = config+                        { configDataDefs = unionDataDefs (configDataDefs config)+                                                         (fromListDataDefs defsImported') }+        let kenv_import = Env.union kenv+                        $ Env.fromList  [ BName n (kindOfImportType isrc)+                                        | (n, isrc) <- nksImported' ]+++        -- Check types of imported capabilities -----------+        ntsImportCap'   <- checkImportCaps config_import kenv_import mode+                        $  moduleImportCaps mm++        let bsImportCap = [ BName n (typeOfImportCap   isrc)+                          | (n, isrc) <- ntsImportCap' ]+         -- Check types of imported values ------------------        ntsImport'      <- checkImportValues config kenv' mode +        ntsImportValue' <- checkImportValues config_import kenv_import mode                         $  moduleImportValues mm-        -        -- Build the initial type environment.-        let tenv'       = Env.union tenv -                        $ Env.fromList  [ BName n (typeOfImportSource isrc)-                                                | (n, isrc) <- ntsImport' ]  +        -- Check the local data type defs -----------------+        let defsLocal   =  moduleDataDefsLocal mm+        defsLocal'      <- case checkDataDefs config defsLocal of+                                (err : _, _)     -> throw $ ErrorData err+                                ([], defsLocal') -> return defsLocal'++++        -- Build the top-level config, defs and environments.+        --  These contain names that are visible to bindings in the module.+        let defs_top    = unionDataDefs (configDataDefs config)+                        $ unionDataDefs (fromListDataDefs defsImported')+                                        (fromListDataDefs defsLocal')++        let caps_top    = Env.fromList+                        $ [BName n t    | (n, ImportCapAbstract t) <- ntsImportCap' ]++        let config_top  = config +                        { configDataDefs        = defs_top +                        , configGlobalCaps      = caps_top }++        let kenv_top    = kenv_import++        let tenv_top    = Env.unions +                        [ tenv+                        , Env.fromList  [ BName n (typeOfImportValue isrc)+                                        | (n, isrc) <- ntsImportValue' ]++                        , Env.fromList  [ BName n (typeOfImportCap   isrc)+                                        | (n, isrc) <- ntsImportCap'   ]+                        ]++        let ctx_top     = pushTypes bsImportCap emptyContext+         -- Check the sigs of exported types ----------------        esrcsType'      <- checkExportTypes config        -                        $ moduleExportTypes mm+        esrcsType'      <- checkExportTypes  config_top+                        $  moduleExportTypes mm +         -- Check the sigs of exported values ---------------        esrcsValue'     <- checkExportValues config kenv' -                        $ moduleExportValues mm-        -        -        -- Check the local data type defs ------------------        defs'           <- case checkDataDefs config (moduleDataDefsLocal mm) of-                                (err : _, _)   -> throw $ ErrorData err-                                ([], defs')    -> return defs'+        esrcsValue'     <- checkExportValues config_top kenv_top+                        $  moduleExportValues mm -        let defs_all =  unionDataDefs (configDataDefs config) -                                      (fromListDataDefs defs')-                                      -        -        -- Check the body of the module --------------------        let bsData      = [BName (dataDefTypeName def) (kindOfDataDef def) | def <- defs' ]-        let kenv_data   = Env.union kenv' (Env.fromList bsData)                    -        let config_data = config { configDataDefs = defs_all } -        (x', _, _effs, _, ctx) -                <- checkExpM -                        (makeTable config_data kenv_data tenv')-                        emptyContext (moduleBody mm) mode+        -- Check the body of the module -------------------+        (x', _, _effs, ctx)+         <- checkExpM   (makeTable config_top kenv_top tenv_top)+                        ctx_top mode DemandNone (moduleBody mm)           -- Apply the final context to the annotations in expressions.-        let applyToAnnot (AnTEC t0 e0 c0 x0)-                = AnTEC (applySolved ctx t0)-                        (applySolved ctx e0)-                        (applySolved ctx c0)-                        x0+        let applyToAnnot (AnTEC t0 e0 _ x0)+             = do t0' <- applySolved ctx t0+                  e0' <- applySolved ctx e0+                  return $ AnTEC t0' e0' (tBot kClosure) x0 -        let x'' = reannotate applyToAnnot -                $ mapT (applySolved ctx) x'+        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     = nksImported'+                , moduleImportCaps      = ntsImportCap'+                , moduleImportValues    = ntsImportValue'+                , moduleBody            = xx_annot } +         -- Check that each exported signature matches the type of its binding.-        envDef  <- checkModuleBinds (moduleExportTypes mm) (moduleExportValues mm) x''+        -- This returns an environment containing all the bindings defined+        -- in the module.+        tenv_binds      <- checkModuleBinds+                                (moduleExportTypes  mm_inferred)+                                (moduleExportValues mm_inferred) +                                xx_annot -        -- Check that all exported bindings are defined by the module.-        mapM_ (checkBindDefined envDef) -                $ map fst $ moduleExportValues mm+        -- Build the environment containing all names that can be exported.+        let tenv_exportable = Env.union tenv_top tenv_binds -        -- If exported names are missing types then fill them in.-        let tsTop       = moduleTopBindTypes mm+        -- 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 tenv_exportable)+                $ map fst $ moduleExportValues mm_inferred +        -- If exported names are missing types then fill them in.         let updateExportSource e                 | ExportSourceLocalNoType n <- e-                , Just t  <- Map.lookup n tsTop   +                , Just t  <- Env.lookup (UName n) tenv_exportable                 = 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' = mm    -                { moduleExportTypes     = esrcsType'-                , moduleExportValues    = esrcsValue_updated-                , moduleImportTypes     = nksImport'-                , moduleImportValues    = ntsImport'-                , moduleBody            = x'' }+        let mm_final+                = mm_inferred+                { moduleExportValues    = esrcsValue_updated } -        return mm'+        return mm_final   ---------------------------------------------------------------------------------------------------@@ -178,12 +226,12 @@         (case takeHead dups of           Just n -> throw $ ErrorExportDuplicate n           _      -> return ())-         +         -- Check the kinds of the export specs.         mapM check nesrcs-  + --------------------------------------------------------------------------------------------------- -- | Check exported types. checkExportValues@@ -217,39 +265,122 @@ checkImportTypes         :: (Ord n, Show n, Pretty n)         => Config n -> Mode n-        -> [(n, ImportSource n)]-        -> CheckM a n [(n, ImportSource n)]+        -> [(n, ImportType n)]+        -> CheckM a n [(n, ImportType n)]  checkImportTypes config mode nisrcs- = let  + = let         -- Checker mode to use.         modeCheckImportTypes          = case mode of                 Recon   -> Recon                 _       -> Synth +        -- Check an import definition.         check (n, isrc)-         = do   let k           =  typeOfImportSource isrc-                (k', _, _)      <- checkTypeM config Env.empty emptyContext UniverseKind+         = do   let k      =  kindOfImportType isrc+                (k', _, _) <- checkTypeM config Env.empty emptyContext UniverseKind                                         k modeCheckImportTypes-                return  (n, mapTypeOfImportSource (const k') isrc)+                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 k1 k2+        compat (ImportTypeBoxed    k1) (ImportTypeBoxed    k2) = equivT k1 k2+        compat _ _ = False+    in do-        -- Check for duplicate imports.-        let dups = findDuplicates $ map fst nisrcs-        (case takeHead dups of-          Just n -> throw $ ErrorImportDuplicate n-          _      -> return ())+        -- Check all the imports individually.+        nisrcs' <- mapM check nisrcs -        mapM check nisrcs+        -- Check that exports with the same name are compatable,+        -- and pack down duplicates.+        pack Map.empty nisrcs'   ---------------------------------------------------------------------------------------------------+-- | Check types of imported capabilities.+checkImportCaps+        :: (Ord n, Show n, Pretty n)+        => Config n -> KindEnv n -> Mode n+        -> [(n, ImportCap n)]+        -> CheckM a n [(n, ImportCap n)]++checkImportCaps config kenv mode nisrcs+ = let+        -- 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 kenv emptyContext 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 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 -> KindEnv n -> Mode n-        -> [(n, ImportSource n)]-        -> CheckM a n [(n, ImportSource n)]+        -> [(n, ImportValue n)]+        -> CheckM a n [(n, ImportValue n)]  checkImportValues config kenv mode nisrcs  = let@@ -259,31 +390,60 @@                 Recon   -> Recon                 _       -> Check kData +        -- Check an import definition.         check (n, isrc)-         = do   let t           = typeOfImportSource isrc-                (t', k, _)      <- checkTypeM config kenv emptyContext UniverseSpec-                                        t modeCheckImportTypes+         = do   let t      =  typeOfImportValue isrc+                (t', k, _) <- checkTypeM config kenv emptyContext UniverseSpec+                                         t modeCheckImportTypes                  -- In Recon mode we need to post-check that the imported-                -- value really has kind data. In inference mode the expected-                -- kind we pass down will handle this.+                -- 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, mapTypeOfImportSource (const t') isrc)+                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 t1 t2 && a1 == a2++        compat (ImportValueSea _ t1)+               (ImportValueSea _ t2)+         = equivT t1 t2 ++        compat _ _ = False+    in do-        -- Check for duplicate imports.-        let dups = findDuplicates $ map fst nisrcs-        (case takeHead dups of-          Just n -> throw $ ErrorImportDuplicate n-          _      -> return ())+        -- Check all the imports individually.+        nisrcs' <- mapM check 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 +checkModuleBinds         :: Ord n         => [(n, ExportSource n)]        -- ^ Exported types.         -> [(n, ExportSource n)]        -- ^ Exported values@@ -293,7 +453,7 @@  checkModuleBinds !ksExports !tsExports !xx  = case xx of-        XLet _ (LLet b _) x2     +        XLet _ (LLet b _) x2          -> do  checkModuleBind  ksExports tsExports b                 env     <- checkModuleBinds ksExports tsExports x2                 return  $ Env.extend b env@@ -310,7 +470,7 @@   -- | If some bind is exported, then check that it matches the exported version.-checkModuleBind +checkModuleBind         :: Ord n         => [(n, ExportSource n)]        -- ^ Exported types.         -> [(n, ExportSource n)]        -- ^ Exported values.@@ -321,22 +481,22 @@  | BName n tDef <- b  = case join $ liftM takeTypeOfExportSource $ lookup n tsExports of         Nothing                 -> return ()-        Just tExport +        Just tExport          | equivT tDef tExport  -> return ()          | otherwise            -> throw $ ErrorExportMismatch n tExport tDef - -- Only named bindings can be exported, + -- Only named bindings can be exported,  --  so we don't need to worry about non-named ones.  | otherwise  = return ()   ------------------------------------------------------------------------------------------------------ | Check that a top-level binding is actually defined by the module.-checkBindDefined +-- | Check that an exported top-level value is actually defined by the module.+checkBindDefined         :: Ord n-        => TypeEnv n                    -- ^ Types defined by the module.-        -> n                            -- ^ Name of an exported binding.+        => TypeEnv n            -- ^ Types defined by the module.+        -> n                    -- ^ Name of an exported binding.         -> CheckM a n ()  checkBindDefined env n