ddc-core 0.2.0.2 → 0.2.1.1

raw patch · 13 files changed

+240/−126 lines, 13 filesdep ~ddc-basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: ddc-base

API changes (from Hackage documentation)

Files

• DDC/Core/Check/CheckExp.hs +76/−46
• DDC/Core/Check/CheckWitness.hs +34/−23
• DDC/Core/Check/Error.hs +5/−0
• DDC/Core/Check/ErrorMessage.hs +5/−0
• DDC/Core/Compounds.hs +1/−1
• DDC/Core/DataDef.hs +1/−1
• DDC/Core/Parser.hs +16/−6
• DDC/Type/Check.hs +55/−24
• DDC/Type/Check/CheckError.hs +10/−3
• DDC/Type/Env.hs +14/−0
• DDC/Type/Pretty.hs +8/−17
• LICENSE +11/−1
• ddc-core.cabal +4/−4

@@ -21,6 +21,7 @@ import DDC.Type.Transform.Trim import DDC.Type.Transform.Instantiate import DDC.Type.Transform.LiftT+import DDC.Type.Transform.LowerT import DDC.Type.Equiv import DDC.Type.Universe import DDC.Type.Compounds@@ -33,6 +34,7 @@ import qualified DDC.Type.Env           as Env import qualified DDC.Type.Check         as T import qualified Data.Set               as Set+import qualified Data.Map               as Map import Control.Monad import Data.List                        as L import Data.Maybe@@ -165,18 +167,33 @@   -- constructors ----------------------------------checkExpM' _defs _kenv _tenv (XCon a u)-      = return  ( XCon a u-                , typeOfBound u-                , Sum.empty kEffect-                , Set.empty)+checkExpM' defs _kenv _tenv xx@(XCon a u)+        | UName n _     <- u+        = case Map.lookup n (dataDefsCtors defs) of+           Nothing -> throw $ ErrorUndefinedCtor xx+           Just _  +            -> return  +                  ( XCon a u+                  , typeOfBound u+                  , Sum.empty kEffect+                  , Set.empty) +        | UPrim{}       <- u+        = return  ( XCon a u+                  , typeOfBound u+                  , Sum.empty kEffect+                  , Set.empty) +        -- Constructors can't be locally bound.+        | otherwise+        = throw $ ErrorMalformedExp xx++ -- application ------------------------------------ -- value-type application. checkExpM' defs kenv tenv xx@(XApp a x1 (XType t2))  = do   (x1', t1, effs1, clos1) <- checkExpM  defs kenv tenv x1-        k2                      <- checkTypeM kenv t2+        k2                      <- checkTypeM defs kenv t2         case t1 of          TForall b11 t12           | typeOfBind b11 == k2@@ -192,7 +209,7 @@ -- value-witness application. checkExpM' defs kenv tenv xx@(XApp a x1 (XWitness w2))  = do   (x1', t1, effs1, clos1) <- checkExpM     defs kenv tenv x1-        t2                      <- checkWitnessM      kenv tenv w2+        t2                      <- checkWitnessM defs kenv tenv w2         case t1 of          TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12           | t11 `equivT` t2   @@ -209,6 +226,9 @@ checkExpM' defs kenv tenv xx@(XApp a x1 x2)  = do   (x1', t1, effs1, clos1)    <- checkExpM defs kenv tenv x1         (x2', t2, effs2, clos2)    <- checkExpM defs kenv tenv x2++        -- Note: we don't need to use the closure of the function because+        --       all of its components will already be part of clos1 above.         case t1 of          TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t11) eff) _clo) t12           | t11 `equivT` t2   @@ -225,12 +245,13 @@ -- spec abstraction ----------------------------- checkExpM' defs kenv tenv xx@(XLAM a b1 x2)  = do   let t1          = typeOfBind b1-        _               <- checkTypeM kenv t1+        _               <- checkTypeM defs kenv t1          -- Check the body-        let kenv'         =  Env.extend b1 kenv-        (x2', t2, e2, c2) <- checkExpM defs kenv' tenv x2-        k2                <- checkTypeM kenv' t2+        let kenv'         = Env.extend b1 kenv+        let tenv'         = Env.lift   1  tenv+        (x2', t2, e2, c2) <- checkExpM  defs kenv' tenv' x2+        k2                <- checkTypeM defs kenv' t2          when (Env.memberBind b1 kenv)          $ throw $ ErrorLamShadow xx b1@@ -256,13 +277,13 @@  -- function abstractions ------------------------ checkExpM' defs kenv tenv xx@(XLam a b1 x2)- = do   let t1          =  typeOfBind b1-        k1              <- checkTypeM kenv t1+ = do   let t1               =  typeOfBind b1+        k1                   <- checkTypeM defs kenv t1          -- Check the body.         let tenv'            =  Env.extend b1 tenv         (x2', t2, e2, c2)    <- checkExpM  defs kenv tenv' x2   -        k2                   <- checkTypeM kenv t2+        k2                   <- checkTypeM defs kenv t2          -- The form of the function constructor depends on what universe the          -- binder is in.@@ -311,7 +332,7 @@          -- Check binder annotation against the type we inferred for the right.         (b11', k11')    -         <- checkLetBindOfTypeM xx kenv tenv t12 b11+         <- checkLetBindOfTypeM xx defs kenv tenv t12 b11          -- The right of the binding should have data kind.         when (not $ isDataKind k11')@@ -322,7 +343,7 @@         (x2', t2, effs2, c2)    <- checkExpM defs kenv tenv1 x2          -- The body should have data kind.-        k2 <- checkTypeM kenv t2+        k2 <- checkTypeM defs kenv t2         when (not $ isDataKind k2)          $ throw $ ErrorLetBodyNotData xx t2 k2 @@ -351,7 +372,7 @@           LetLazy Nothing            -> do case takeDataTyConApps t12 of                   Just (_tc, t1 : _)-                   ->  do k1 <- checkTypeM kenv t1+                   ->  do k1 <- checkTypeM defs kenv t1                           when (isRegionKind k1)                            $ throw $ ErrorLetLazyNoWitness xx b11 t12 @@ -360,7 +381,7 @@           -- Type of lazy binding might have a head region,           -- so we need a Lazy witness for it.           LetLazy (Just wit)-           -> do tWit        <- checkWitnessM kenv tenv wit+           -> do tWit        <- checkWitnessM defs kenv tenv wit                  let tWitExp =  case takeDataTyConApps t12 of                                  Just (_tc, tR : _ts) -> tLazy tR                                  _                    -> tHeadLazy t12@@ -382,7 +403,8 @@         let (bs, xs)    = unzip bxs          -- Check all the annotations.-        ks              <- mapM (checkTypeM kenv) $ map typeOfBind bs+        ks              <- mapM (checkTypeM defs kenv) +                        $  map typeOfBind bs          -- Check all the annots have data kind.         zipWithM_ (\b k@@ -414,7 +436,7 @@                 <- checkExpM defs kenv tenv' xBody          -- The body type must have data kind.-        kBody   <- checkTypeM kenv tBody+        kBody   <- checkTypeM defs kenv tBody         when (not $ isDataKind kBody)          $ throw $ ErrorLetBodyNotData xx tBody kBody @@ -440,7 +462,7 @@       -> do         -- Check the type on the region binder.         let k   = typeOfBind b-        checkTypeM kenv k+        checkTypeM defs kenv k          -- The binder must have region kind.         when (not $ isRegionKind k)@@ -452,19 +474,20 @@          $ throw $ ErrorLetRegionRebound xx b                  -- Check the witness types.-        let kenv'         = Env.extend b kenv-        mapM_ (checkTypeM kenv') $ map typeOfBind bs+        let kenv'       = Env.extend b kenv+        let tenv'       = Env.lift 1 tenv+        mapM_ (checkTypeM defs kenv') $ map typeOfBind bs          -- Check that the witnesses bound here are for the region,         -- and they don't conflict with each other.         checkWitnessBindsM xx u bs          -- Check the body expression.-        let tenv'       = Env.extends bs tenv-        (xBody', tBody, effs, clo)  <- checkExpM defs kenv' tenv' x+        let tenv2       = Env.extends bs tenv'+        (xBody', tBody, effs, clo)  <- checkExpM defs kenv' tenv2 x          -- The body type must have data kind.-        kBody           <- checkTypeM kenv' tBody+        kBody           <- checkTypeM defs kenv' tBody         when (not $ isDataKind kBody)          $ throw $ ErrorLetBodyNotData xx tBody kBody @@ -480,20 +503,22 @@                         $ effs          -- Delete the bound region variable from the closure.-        let clo_masked  = Set.delete (GBoundRgnVar u) -                        $ clo-        +        -- Mask closure terms due to locally bound region vars.+        let c2_cut      = Set.fromList+                        $ mapMaybe (cutTaggedClosureT b)+                        $ Set.toList clo+         return  ( XLet a (LLetRegion b bs) xBody'-                , tBody-                , effs'-                , clo_masked)+                , lowerT 1 tBody+                , lowerT 1 effs'+                , c2_cut)   -- withregion ----------------------------------- checkExpM' defs kenv tenv xx@(XLet a (LWithRegion u) x)  = do   -- Check the type on the region handle.         let k   = typeOfBound u-        checkTypeM kenv k+        checkTypeM defs kenv k          -- The handle must have region kind.         when (not $ isRegionKind k)@@ -504,7 +529,7 @@                <- checkExpM defs kenv tenv x          -- The body type must have data kind.-        kBody  <- checkTypeM kenv tBody+        kBody  <- checkTypeM defs kenv tBody         when (not $ isDataKind kBody)          $ throw $ ErrorLetBodyNotData xx tBody kBody         @@ -634,7 +659,7 @@ checkExpM' defs kenv tenv xx@(XCast a c@(CastWeakenEffect eff) x1)  = do            -- Check the effect term.-        kEff    <- checkTypeM kenv eff+        kEff    <- checkTypeM defs kenv eff         when (not $ isEffectKind kEff)          $ throw $ ErrorMaxeffNotEff xx eff kEff @@ -651,7 +676,7 @@ checkExpM' defs kenv tenv xx@(XCast a c@(CastWeakenClosure clo2) x1)  = do            -- Check the closure term.-        kClo    <- checkTypeM kenv clo2+        kClo    <- checkTypeM defs kenv clo2         when (not $ isClosureKind kClo)          $ throw $ ErrorMaxcloNotClo xx clo2 kClo @@ -673,8 +698,8 @@  -- Purify an effect, given a witness that it is pure. checkExpM' defs kenv tenv xx@(XCast a c@(CastPurify w) x1)- = do   tW                   <- checkWitnessM  kenv tenv w-        (x1', t1, effs, clo) <- checkExpM defs kenv tenv x1+ = do   tW                   <- checkWitnessM defs kenv tenv w+        (x1', t1, effs, clo) <- checkExpM     defs kenv tenv x1                          effs' <- case tW of                   TApp (TCon (TyConWitness TwConPure)) effMask@@ -689,8 +714,8 @@  -- Forget a closure, given a witness that it is empty. checkExpM' defs kenv tenv xx@(XCast a c@(CastForget w) x1)- = do   tW                    <- checkWitnessM  kenv tenv w-        (x1', t1, effs, clos) <- checkExpM defs kenv tenv x1+ = do   tW                    <- checkWitnessM defs kenv tenv w+        (x1', t1, effs, clos) <- checkExpM     defs kenv tenv x1          clos' <- case tW of                   TApp (TCon (TyConWitness TwConEmpty)) cloMask@@ -877,10 +902,14 @@  ------------------------------------------------------------------------------- -- | Check a type in the exp checking monad.-checkTypeM :: (Ord n, Pretty n) => Env n -> Type n -> CheckM a n (Kind n)+checkTypeM :: (Ord n, Pretty n) +           => DataDefs n +           -> Env n +           -> Type n +           -> CheckM a n (Kind n) -checkTypeM kenv tt- = case T.checkType kenv tt of+checkTypeM defs kenv tt+ = case T.checkType defs kenv tt of         Left err        -> throw $ ErrorType err         Right k         -> return k @@ -893,16 +922,17 @@ checkLetBindOfTypeM          :: (Eq n, Ord n, Pretty n)          => Exp a n +        -> DataDefs n           -- Data type definitions.         -> Env n                -- Kind environment.          -> Env n                -- Type environment.         -> Type n          -> Bind n          -> CheckM a n (Bind n, Kind n) -checkLetBindOfTypeM xx kenv _tenv tRight b+checkLetBindOfTypeM xx defs kenv _tenv tRight b         -- If the annotation is Bot then just replace it.         | isBot (typeOfBind b)-        = do    k       <- checkTypeM kenv tRight+        = do    k       <- checkTypeM defs kenv tRight                 return  ( replaceTypeOfBind tRight b                          , k) @@ -911,6 +941,6 @@         = throw $ ErrorLetMismatch xx b tRight          | otherwise-        = do    k       <- checkTypeM kenv (typeOfBind b)+        = do    k       <- checkTypeM defs kenv (typeOfBind b)                 return (b, k) 

@@ -9,6 +9,7 @@         , CheckM         , checkWitnessM) where+import DDC.Core.DataDef import DDC.Core.Exp import DDC.Core.Pretty import DDC.Core.Check.Error@@ -45,13 +46,14 @@ -- checkWitness         :: (Ord n, Pretty n)-        => Env n                -- ^ Kind Environment.+        => DataDefs n           -- ^ Data type definitions.+        -> Env n                -- ^ Kind Environment.         -> Env n                -- ^ Type Environment.         -> Witness n            -- ^ Witness to check.         -> Either (Error a n) (Type n) -checkWitness kenv tenv xx-        = result $ checkWitnessM kenv tenv xx+checkWitness defs kenv tenv xx+        = result $ checkWitnessM defs kenv tenv xx   -- | Like `checkWitness`, but check in an empty environment.@@ -62,23 +64,26 @@ -- typeOfWitness          :: (Ord n, Pretty n) -        => Witness n +        => DataDefs n+        -> Witness n          -> Either (Error a n) (Type n)-typeOfWitness ww ++typeOfWitness defs ww          = result -        $ checkWitnessM Env.empty Env.empty ww+        $ checkWitnessM defs Env.empty Env.empty ww   ------------------------------------------------------------------------------ -- | Like `checkWitness` but using the `CheckM` monad to manage errors. checkWitnessM          :: (Ord n, Pretty n)-        => Env n                -- ^ Kind environment.+        => DataDefs n           -- ^ Data type definitions.+        -> Env n                -- ^ Kind environment.         -> Env n                -- ^ Type environment.         -> Witness n            -- ^ Witness to check.         -> CheckM a n (Type n) -checkWitnessM _kenv tenv (WVar u)+checkWitnessM _defs _kenv tenv (WVar u)  = do   let tBound      = typeOfBound u         let mtEnv       = Env.lookup u tenv @@ -122,14 +127,14 @@         return tResult  -checkWitnessM _kenv _tenv (WCon wc)+checkWitnessM _defs _kenv _tenv (WCon wc)  = return $ typeOfWiCon wc     -- value-type application-checkWitnessM kenv tenv ww@(WApp w1 (WType t2))- = do   t1      <- checkWitnessM  kenv tenv w1-        k2      <- checkTypeM     kenv t2+checkWitnessM defs kenv tenv ww@(WApp w1 (WType t2))+ = do   t1      <- checkWitnessM  defs kenv tenv w1+        k2      <- checkTypeM     defs kenv t2         case t1 of          TForall b11 t12           |  typeOfBind b11 == k2@@ -139,9 +144,9 @@          _              -> throw $ ErrorWAppNotCtor  ww t1 t2  -- witness-witness application-checkWitnessM kenv tenv ww@(WApp w1 w2)- = do   t1      <- checkWitnessM kenv tenv w1-        t2      <- checkWitnessM kenv tenv w2+checkWitnessM defs kenv tenv ww@(WApp w1 w2)+ = do   t1      <- checkWitnessM defs kenv tenv w1+        t2      <- checkWitnessM defs kenv tenv w2         case t1 of          TApp (TApp (TCon (TyConWitness TwConImpl)) t11) t12           |  t11 == t2   @@ -151,9 +156,9 @@          _              -> throw $ ErrorWAppNotCtor  ww t1 t2  -- witness joining-checkWitnessM kenv tenv ww@(WJoin w1 w2)- = do   t1      <- checkWitnessM kenv tenv w1-        t2      <- checkWitnessM kenv tenv w2+checkWitnessM defs kenv tenv ww@(WJoin w1 w2)+ = do   t1      <- checkWitnessM defs kenv tenv w1+        t2      <- checkWitnessM defs kenv tenv w2         case (t1, t2) of          (  TApp (TCon (TyConWitness TwConPure)) eff1           , TApp (TCon (TyConWitness TwConPure)) eff2)@@ -168,8 +173,8 @@          _ -> throw $ ErrorCannotJoin ww w1 t1 w2 t2  -- embedded types-checkWitnessM kenv _tenv (WType t)- = checkTypeM kenv t+checkWitnessM defs kenv _tenv (WType t)+ = checkTypeM defs kenv t           -- | Take the type of a witness constructor.@@ -193,9 +198,15 @@  -- checkType ------------------------------------------------------------------ -- | Check a type in the exp checking monad.-checkTypeM :: (Ord n, Pretty n) => Env n -> Type n -> CheckM a n (Kind n)-checkTypeM kenv tt- = case T.checkType kenv tt of+checkTypeM +        :: (Ord n, Pretty n) +        => DataDefs n +        -> Env n +        -> Type n +        -> CheckM a n (Kind n)++checkTypeM defs kenv tt+ = case T.checkType defs kenv tt of         Left err        -> throw $ ErrorType err         Right k         -> return k 

@@ -39,6 +39,11 @@         { errorBound            :: Bound n         , errorTypeEnv          :: Type n } +        -- Con --------------------------------------------+        -- | A data constructor that wasn't in the set of data definitions.+        | ErrorUndefinedCtor+        { errorChecking         :: Exp a n }+         -- Application ------------------------------------         -- | A function application where the parameter and argument don't match.         | ErrorAppMismatch

@@ -40,6 +40,11 @@                  , text "     from environment." ]  +        -- Constructor ------------------------------------+        ErrorUndefinedCtor xx+         -> vcat [ text "Undefined data constructor: "  <> ppr xx ]++         -- Application ------------------------------------         ErrorAppMismatch xx t1 t2          -> vcat [ text "Type mismatch in application." 

@@ -122,7 +122,7 @@  = foldr (\(f, b) x'            -> if f then XLAM a b x'                    else XLam a b x')-                x (reverse fbs)+                x fbs   -- Applications ---------------------------------------------------------------

@@ -30,7 +30,7 @@           -- | Kinds of type parameters.         , dataDefParamKinds     :: [Kind n] -          -- | Constructors of is data type, or Nothing if there are+          -- | Constructors of the data type, or Nothing if there are           --   too many to list (like with `Int`).         , dataDefCtors          :: Maybe [(n, [Type n])] } 

@@ -68,15 +68,25 @@         x2              <- pExp         return  $ XLet () (LLet mode1 b1 x1) x2 +         -- letrec expression  , do   pTok KLetRec-        pTok KBraceBra-        lets    <- P.sepEndBy1 pLetRecBinding (pTok KSemiColon)-        pTok KBraceKet-        pTok KIn-        x       <- pExp -        return  $ XLet () (LRec lets) x+        P.choice+         -- Multiple bindings in braces+         [ do   pTok KBraceBra+                lets    <- P.sepEndBy1 pLetRecBinding (pTok KSemiColon)+                pTok KBraceKet+                pTok KIn+                x       <- pExp+                return  $ XLet () (LRec lets) x++         -- A single binding without braces.+         , do   ll      <- pLetRecBinding+                pTok KIn+                x       <- pExp+                return  $ XLet () (LRec [ll]) x+         ]                 -- Local region binding.

@@ -17,6 +17,7 @@ import DDC.Type.Compounds import DDC.Type.Predicates import DDC.Type.Transform.LiftT+import DDC.Core.DataDef import DDC.Type.Exp import DDC.Base.Pretty import Data.List@@ -27,6 +28,7 @@ import qualified DDC.Type.Sum           as TS import qualified DDC.Type.Env           as Env import qualified DDC.Type.Check.Monad   as G+import qualified Data.Map               as Map   -- | The type checker monad.@@ -35,15 +37,26 @@  -- Wrappers ------------------------------------------------------------------- -- | Check a type in the given environment, returning an error or its kind.-checkType  :: (Ord n, Pretty n) => Env n -> Type n -> Either (Error n) (Kind n)-checkType env tt = result $ checkTypeM env tt+checkType  :: (Ord n, Pretty n) +           => DataDefs n +           -> Env n +           -> Type n +           -> Either (Error n) (Kind n) +checkType defs env tt +        = result $ checkTypeM defs env tt + -- | Check a type in an empty environment, returning an error or its kind.-kindOfType :: (Ord n, Pretty n) => Type n -> Either (Error n) (Kind n)-kindOfType tt = result $ checkTypeM Env.empty tt+kindOfType :: (Ord n, Pretty n) +           => DataDefs n+           -> Type n +           -> Either (Error n) (Kind n) +kindOfType defs tt+        = result $ checkTypeM defs Env.empty tt + -- checkType ------------------------------------------------------------------ -- | Check a type, returning its kind. ---@@ -51,13 +64,19 @@ --   (==) instead of equivT. This is because kinds do not contain quantifiers --   that need to be compared up to alpha-equivalence, nor do they contain --   crushable components terms.-checkTypeM :: (Ord n, Pretty n) => Env n -> Type n -> CheckM n (Kind n)-checkTypeM env tt+checkTypeM +        :: (Ord n, Pretty n) +        => DataDefs n+        -> Env n+        -> Type n +        -> CheckM n (Kind n)++checkTypeM defs env tt         = -- trace (pretty $ text "checkTypeM:" <+> ppr tt) $-          checkTypeM' env tt+          checkTypeM' defs env tt  -- Variables -------------------checkTypeM' env (TVar u)+checkTypeM' _defs env (TVar u)  = do   let tBound      = typeOfBound u         let mtEnv       = Env.lookup u env @@ -97,7 +116,7 @@         mkResult  -- Constructors ----------------checkTypeM' _env tt@(TCon tc)+checkTypeM' defs _env tt@(TCon tc)  = case tc of         -- Sorts don't have a higher classification.         TyConSort _      -> throw $ ErrorNakedSort tt@@ -111,13 +130,25 @@          TyConWitness tcw -> return $ kindOfTwCon tcw         TyConSpec    tcc -> return $ kindOfTcCon tcc-        TyConBound    u  -> return $ typeOfBound u +        -- User defined type constructors need to be in the set of data defs.+        TyConBound    u  +         -> case u of+                UName n _+                 | Just _ <- Map.lookup n (dataDefsTypes defs)+                 -> return $ typeOfBound u +                 | otherwise+                 -> throw $ ErrorUndefinedCtor u++                UPrim{} -> return $ typeOfBound u+                UIx{}   -> error "sorry"++ -- Quantifiers -----------------checkTypeM' env tt@(TForall b1 t2)- = do   _       <- checkTypeM env (typeOfBind b1)-        k2      <- checkTypeM (Env.extend b1 env) t2+checkTypeM' defs env tt@(TForall b1 t2)+ = do   _       <- checkTypeM defs env (typeOfBind b1)+        k2      <- checkTypeM defs (Env.extend b1 env) t2          -- The body must have data or witness kind.         when (  (not $ isDataKind k2)@@ -129,18 +160,18 @@ -- Applications --------------- -- Applications of the kind function constructor are handled directly -- because the constructor doesn't have a sort by itself.-checkTypeM' env (TApp (TApp (TCon (TyConKind KiConFun)) k1) k2)- = do   _       <- checkTypeM env k1-        s2      <- checkTypeM env k2+checkTypeM' defs env (TApp (TApp (TCon (TyConKind KiConFun)) k1) k2)+ = do   _       <- checkTypeM defs env k1+        s2      <- checkTypeM defs env k2         return  s2  -- The implication constructor is overloaded and can have the -- following kinds: --   (=>) :: @ ~> @ ~> @,  for witness implication. --   (=>) :: @ ~> * ~> *,  for a context.-checkTypeM' env tt@(TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2)- = do   k1      <- checkTypeM env t1-        k2      <- checkTypeM env t2+checkTypeM' defs env tt@(TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2)+ = do   k1      <- checkTypeM defs env t1+        k2      <- checkTypeM defs env t2         if      isWitnessKind k1 && isWitnessKind k2          then     return kWitness         else if isWitnessKind k1 && isDataKind k2@@ -148,9 +179,9 @@         else    throw $ ErrorWitnessImplInvalid tt t1 k1 t2 k2  -- Type application.-checkTypeM' env tt@(TApp t1 t2)- = do   k1      <- checkTypeM env t1-        k2      <- checkTypeM env t2+checkTypeM' defs env tt@(TApp t1 t2)+ = do   k1      <- checkTypeM defs env t1+        k2      <- checkTypeM defs env t2         case k1 of          TApp (TApp (TCon (TyConKind KiConFun)) k11) k12           | k11 == k2   -> return k12@@ -159,8 +190,8 @@          _              -> throw $ ErrorAppNotFun tt t1 k1 t2 k2  -- Sums ------------------------checkTypeM' env (TSum ts)- = do   ks      <- mapM (checkTypeM env) $ TS.toList ts+checkTypeM' defs env (TSum ts)+ = do   ks      <- mapM (checkTypeM defs env) $ TS.toList ts          -- Check that all the types in the sum have a single kind,          -- and return that kind.

@@ -16,6 +16,10 @@         = ErrorUndefined                 { errorBound            :: Bound n } +        -- | An undefined type constructor.+        | ErrorUndefinedCtor+        { errorBound            :: Bound n }+         -- | The kind annotation on the variables does not match the one in the environment.         | ErrorVarAnnotMismatch         { errorBound            :: Bound n@@ -72,14 +76,17 @@ instance (Eq n, Pretty n) => Pretty (Error n) where  ppr err   = case err of+        ErrorUndefined u+         -> text "Undefined type variable:  " <> ppr u++        ErrorUndefinedCtor u+         -> text "Undefined type constructor:  " <> ppr u+         ErrorUnappliedKindFun           -> text "Can't take sort of unapplied kind function constructor."                  ErrorNakedSort s          -> text "Can't check a naked sort: " <> ppr s--        ErrorUndefined u-         -> text "Undefined type variable:  " <> ppr u                  ErrorVarAnnotMismatch u t          -> vcat [ text "Type mismatch in annotation."

@@ -16,9 +16,11 @@         , member,       memberBind         , lookup,       lookupName         , depth+        , lift         , wrapTForalls) where import DDC.Type.Exp+import DDC.Type.Transform.LiftT import Data.Maybe import Data.Map                 (Map) import Prelude                  hiding (lookup)@@ -139,6 +141,18 @@ -- | Yield the total depth of the deBruijn stack. depth :: Env n -> Int depth env       = envStackLength env+++-- | Lift all free deBruijn indices in the environment by the given number of steps.+--   TODO: Delay this, only lift when we extract the final type.+--         will also need to update the 'member' function.+lift  :: Ord n => Int -> Env n -> Env n+lift n env+        = Env+        { envMap         = Map.map (liftT n) (envMap env)+        , envStack       = map (liftT n) (envStack env)+        , envStackLength = envStackLength env+        , envPrimFun     = envPrimFun     env }   -- | Wrap locally bound (non primitive) variables defined in an environment

@@ -67,21 +67,20 @@          -> pprParen (d > 5)          $  ppr k1 <+> text "~>" <+> ppr k2 -        TApp (TApp (TCon (TyConWitness TwConImpl)) k1) k2+        TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2          -> pprParen (d > 5)-         $  ppr k1 <+> text "=>" </> pprPrec 6 k2+         $  pprPrec 6 t1 <+> text "=>" </> pprPrec 5 t2          TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) t1) eff) clo) t2          | isBot eff, isBot clo          -> pprParen (d > 5)-         $  (if isTFun t1 then pprPrec 6 t1 else pprPrec 5 t1)-                   <+> text "->" </> ppr t2+         $  pprPrec 6 t1 <+> text "->"  </> pprPrec 5 t2           | otherwise          -> pprParen (d > 5)-         $  (if isTFun t1 then pprPrec 6 t1 else pprPrec 5 t1)-                   <+> text "-(" <> ppr eff <> text " | " <> ppr clo <> text ")>" -                   </> ppr t2+         $  pprPrec 6 t1+                <+> text "-(" <> ppr eff <> text " | " <> ppr clo <> text ")>" +                </> pprPrec 5 t2                             -- Standard types.         TCon tc    -> ppr tc@@ -90,11 +89,11 @@         TForall b t          | Just (bsMore, tBody) <- takeTForalls t          -> let groups  = partitionBindsByType (b:bsMore)-            in  pprParen (d > 1) +            in  pprParen (d > 5)                   $ (cat $ map pprBinderGroup groups) <> ppr tBody                                   | otherwise-         -> pprParen (d > 1)+         -> pprParen (d > 5)                 $ brackets (ppr b) <> dot <> ppr t          TApp t1 t2@@ -107,14 +106,6 @@                    | otherwise          -> pprParen (d > 9) $  ppr ts---isTFun :: Type n -> Bool-isTFun tt- = case tt of-         TApp (TApp (TApp (TApp (TCon (TyConSpec TcConFun)) _) _) _) _-                -> True-         _      -> False   instance (Pretty n, Eq n) => Pretty (TypeSum n) where

@@ -1,7 +1,8 @@ -------------------------------------------------------------------------------- The Disciplined Disciple Compiler License (MIT style) -Copyright (c) 2008-2011 Benjamin Lippmeier+Copyrite (K) 2007-2012 The Disciplined Disciple Compiler Strike Force+All rights reversed.  Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal@@ -12,6 +13,15 @@  The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.++-------------------------------------------------------------------------------+Under Australian law copyright is free and automatic.+By contributing to DDC authors grant all rights they have regarding their+contributions to the other members of the Disciplined Disciple Compiler Strike+Force, past, present and future, as well as placing their contributions under+the above license.++Use "darcs show authors" to get a list of Strike Force members.  -------------------------------------------------------------------------------- Redistributions of libraries in ./external are governed by their own licenses:

@@ -1,9 +1,9 @@ Name:           ddc-core-Version:        0.2.0.2+Version:        0.2.1.1 License:        MIT License-file:   LICENSE-Author:         Ben Lippmeier-Maintainer:     benl@ouroborus.net+Author:         The Disciplined Disciple Compiler Strike Force+Maintainer:     Ben Lippmeier <benl@ouroborus.net> Build-Type:     Simple Cabal-Version:  >=1.6 Stability:      experimental@@ -29,7 +29,7 @@         array           == 0.4.*,         transformers    == 0.2.*,         mtl             == 2.0.*,-        ddc-base        == 0.2.0.*+        ddc-base        == 0.2.1.*    Exposed-modules:         DDC.Core.Check.CheckExp