positivity checking

src/full/Interaction/CommandLine/CommandLine.hs

@@ -235,7 +235,7 @@ typeOf s =
     do  e  <- parseExpr (unwords s)
         e0 <- typeInCurrent Normalised e
         e1 <- typeInCurrent AsIs e
-	liftIO $ putStrLn $ showA e0
+	liftIO $ putStrLn $ showA e1
 
 typeIn :: [String] -> TCM ()
 typeIn s@(_:_:_) = 

src/full/Interaction/Options.hs

@@ -39,21 +39,22 @@ instance Functor ArgDescr where
     fmap f (OptArg p s) = OptArg (f . p) s
 
 data CommandLineOptions =
-    Options { optProgramName	  :: String
-	    , optInputFile	  :: Maybe FilePath
-	    , optIncludeDirs	  :: [FilePath]
-	    , optShowVersion	  :: Bool
-	    , optShowHelp	  :: Bool
-	    , optInteractive	  :: Bool
-	    , optEmacsMode	  :: Bool
-	    , optVerbose	  :: Int
-	    , optProofIrrelevance :: Bool
-	    , optAllowUnsolved	  :: Bool
-	    , optShowImplicit	  :: Bool
-	    , optRunTests	  :: Bool
-	    , optCompile	  :: Bool
-	    , optGenerateVimFile  :: Bool
-	    , optIgnoreInterfaces :: Bool
+    Options { optProgramName	   :: String
+	    , optInputFile	   :: Maybe FilePath
+	    , optIncludeDirs	   :: [FilePath]
+	    , optShowVersion	   :: Bool
+	    , optShowHelp	   :: Bool
+	    , optInteractive	   :: Bool
+	    , optEmacsMode	   :: Bool
+	    , optVerbose	   :: Int
+	    , optProofIrrelevance  :: Bool
+	    , optAllowUnsolved	   :: Bool
+	    , optShowImplicit	   :: Bool
+	    , optRunTests	   :: Bool
+	    , optCompile	   :: Bool
+	    , optGenerateVimFile   :: Bool
+	    , optIgnoreInterfaces  :: Bool
+	    , optDisablePositivity :: Bool
 	    }
     deriving Show
 
@@ -64,21 +65,22 @@ mapFlag f (Option _ long arg descr) = Option [] (map f long) arg descr
 
 defaultOptions :: CommandLineOptions
 defaultOptions =
-    Options { optProgramName	  = "agda"
-	    , optInputFile	  = Nothing
-	    , optIncludeDirs	  = []
-	    , optShowVersion	  = False
-	    , optShowHelp	  = False
-	    , optInteractive	  = False
-	    , optEmacsMode	  = False
-	    , optVerbose	  = 1
-	    , optProofIrrelevance = False
-	    , optAllowUnsolved	  = False
-	    , optShowImplicit	  = False
-	    , optRunTests	  = False
-	    , optCompile	  = False
-	    , optGenerateVimFile  = False
-	    , optIgnoreInterfaces = False
+    Options { optProgramName	   = "agda"
+	    , optInputFile	   = Nothing
+	    , optIncludeDirs	   = []
+	    , optShowVersion	   = False
+	    , optShowHelp	   = False
+	    , optInteractive	   = False
+	    , optEmacsMode	   = False
+	    , optVerbose	   = 1
+	    , optProofIrrelevance  = False
+	    , optAllowUnsolved	   = False
+	    , optShowImplicit	   = False
+	    , optRunTests	   = False
+	    , optCompile	   = False
+	    , optGenerateVimFile   = False
+	    , optIgnoreInterfaces  = False
+	    , optDisablePositivity = False
 	    }
 
 {- | @f :: Flag opts@  is an action on the option record that results from
@@ -92,14 +94,15 @@ inputFlag f o	    =
 	Nothing  -> return $ o { optInputFile = Just f }
 	Just _	 -> fail "only one input file allowed"
 
-versionFlag	     o = return $ o { optShowVersion	  = True }
-helpFlag	     o = return $ o { optShowHelp	  = True }
-proofIrrelevanceFlag o = return $ o { optProofIrrelevance = True }
-ignoreInterfacesFlag o = return $ o { optIgnoreInterfaces = True }
-allowUnsolvedFlag    o = return $ o { optAllowUnsolved	  = True }
-showImplicitFlag     o = return $ o { optShowImplicit	  = True }
-runTestsFlag	     o = return $ o { optRunTests	  = True }
-vimFlag		     o = return $ o { optGenerateVimFile  = True }
+versionFlag	     o = return $ o { optShowVersion	   = True }
+helpFlag	     o = return $ o { optShowHelp	   = True }
+proofIrrelevanceFlag o = return $ o { optProofIrrelevance  = True }
+ignoreInterfacesFlag o = return $ o { optIgnoreInterfaces  = True }
+allowUnsolvedFlag    o = return $ o { optAllowUnsolved	   = True }
+showImplicitFlag     o = return $ o { optShowImplicit	   = True }
+runTestsFlag	     o = return $ o { optRunTests	   = True }
+vimFlag		     o = return $ o { optGenerateVimFile   = True }
+noPositivityFlag     o = return $ o { optDisablePositivity = True }
 
 interactiveFlag o
     | optEmacsMode o = fail "cannot have both emacs mode and interactive mode"
@@ -153,6 +156,8 @@ pragmaOptions =
 		    "enable proof irrelevance (experimental feature)"
     , Option []	    ["allow-unsolved-metas"] (NoArg allowUnsolvedFlag)
 		    "allow unsolved meta variables (only needed in batch mode)"
+    , Option []	    ["disable-positivity-check"] (NoArg noPositivityFlag)
+		    "disable strict positivity check for datatypes"
     ]
 
 -- | Used for printing usage info.

src/full/Interaction/agda2-mode.el

@@ -63,6 +63,7 @@ effect only after doing 'erase-customization' for `agda2-ghci-options' below"
 
 (defcustom agda2-ghci-options2
   (list
+   "-package Agda"
    "-I."
    "-Wall"
    "-Werror"
@@ -231,7 +232,7 @@ consumed at `agda2-undo'.  It is a list of list
                             mode-name "Agda2 GHCi")
                       (rename-buffer agda2-bufname))))
   (apply 'agda2-go ":set" agda2-ghci-options)
-  (agda2-go ":l" agda2-toplevel-module)
+  (agda2-go ":mod +" agda2-toplevel-module)
   (agda2-text-state))
 
 ;;;; Communicating with Agda2

src/full/TypeChecker.hs

@@ -41,6 +41,7 @@ import TypeChecking.Serialise
 import TypeChecking.Interface
 import TypeChecking.Constraints
 import TypeChecking.Errors
+import TypeChecking.Positivity
 
 import Utils.Monad
 import Utils.List
@@ -109,6 +110,9 @@ checkMutual :: DeclInfo -> [A.TypeSignature] -> [A.Definition] -> TCM ()
 checkMutual i ts ds =
     do	mapM_ checkTypeSignature ts
 	mapM_ checkDefinition ds
+	m <- currentModule
+	whenM positivityCheckEnabled $
+	    checkStrictlyPositive [ qualify m name | A.DataDef _ name _ _ <- ds ]
 
 
 -- | Type check the type signature of an inductive or recursive definition.

src/full/TypeChecking/Monad/Options.hs

@@ -71,6 +71,9 @@ showImplicitArguments = optShowImplicit <$> commandLineOptions
 ignoreInterfaces :: TCM Bool
 ignoreInterfaces = optIgnoreInterfaces <$> commandLineOptions
 
+positivityCheckEnabled :: TCM Bool
+positivityCheckEnabled = not . optDisablePositivity <$> commandLineOptions
+
 getVerbosity :: TCM Int
 getVerbosity = optVerbose <$> commandLineOptions
 

src/full/TypeChecking/Positivity.hs

@@ -0,0 +1,145 @@
+{-# OPTIONS_GHC -cpp -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances #-}
+
+-- | Check that a datatype is strictly positive.
+module TypeChecking.Positivity where
+
+import Prelude hiding (foldr, mapM_, elem, concat)
+
+import Control.Applicative
+import Control.Monad hiding (mapM_)
+import Control.Monad.Trans (liftIO)
+import Control.Monad.State hiding (mapM_)
+import Data.Foldable
+import Data.Set (Set)
+import Data.Monoid
+import qualified Data.Set as Set
+import qualified Data.Map as Map
+
+import Syntax.Common
+import Syntax.Internal
+import TypeChecking.Monad
+import TypeChecking.Substitute
+import TypeChecking.Errors
+
+import Utils.Monad
+
+#include "../undefined.h"
+
+-- | Check that a set of mutually recursive datatypes are strictly positive.
+checkStrictlyPositive :: [QName] -> TCM ()
+checkStrictlyPositive ds = flip evalStateT noAssumptions $ do
+    cs <- concat <$> mapM constructors ds
+    mapM_ (\c -> checkPos ds c =<< lift (typeOfConst c)) cs
+    where
+	constructors d = do
+	    def <- lift $ theDef <$> getConstInfo d
+	    case def of
+		Datatype _ cs _ _ -> return cs
+		_		  -> __IMPOSSIBLE__
+
+-- | Assumptions about arguments to datatypes
+type Assumptions = Set (QName, Int)
+
+noAssumptions :: Assumptions
+noAssumptions = Set.empty
+
+type PosM = StateT Assumptions TCM
+
+isAssumption :: QName -> Int -> PosM Bool
+isAssumption q i = do
+    a <- get
+    return $ Set.member (q,i) a
+
+assume :: QName -> Int -> PosM ()
+assume q i = modify $ Set.insert (q,i)
+
+-- | @checkPos ds c t@: Check that @ds@ only occurs stricly positively in the
+--   type @t@ of the constructor @c@.
+checkPos :: [QName] -> QName -> Type -> PosM ()
+checkPos ds c t = mapM_ check ds
+    where
+	check d = case Map.lookup d defs of
+	    Nothing  -> return ()    -- non-recursive
+	    Just ocs
+		| NonPositive `elem` ocs -> fail $ show d ++ " occurs not strictly positively in the type of the constructor " ++ show c
+		| otherwise		 -> mapM_ (uncurry checkPosArg) args
+		where
+		    args = [ (q, i) | Argument q i <- Set.toList ocs ]
+
+	defs = unMap $ getDefs $ arguments t
+
+	arguments t = case unEl t of
+	    Pi a b  -> a : arguments (absBody b)
+	    Fun a b -> a : arguments b
+	    _	    -> []
+
+-- | Check that a particular argument occurs strictly positively in the
+--   definition of a datatype.
+checkPosArg :: QName -> Int -> PosM ()
+checkPosArg d i = unlessM (isAssumption d i) $ do
+    assume d i
+    def <- lift $ theDef <$> getConstInfo d
+    case def of
+	Datatype _ cs _ _ -> do
+	    xs <- lift $ map (qualify noModuleName) <$>
+		  replicateM (i + 1) (freshName_ "dummy")
+	    let x = xs !! i
+		args = map (Arg NotHidden . flip Def []) xs
+	    let check c = do
+		    t <- lift $ typeOfConst c
+		    checkPos [x] c (t `piApply'` args)
+	    mapM_ check cs
+	_		  -> fail $ "cannot guarantee positivity of argument " ++ show i ++ " to non-datatype " ++ show d
+
+data Occurence = Positive | NonPositive | Argument QName Nat
+    deriving (Show, Eq, Ord)
+
+newtype Map k v = Map { unMap :: Map.Map k v }
+type Defs = Map QName (Set Occurence)
+
+instance (Ord k, Monoid v) => Monoid (Map k v) where
+    mempty = Map Map.empty
+    mappend (Map ds1) (Map ds2) = Map (Map.unionWith mappend ds1 ds2)
+
+instance Ord k => Functor (Map k) where
+    fmap f (Map m) = Map $ fmap f m
+
+makeNegative :: Defs -> Defs
+makeNegative = fmap (const $ Set.singleton NonPositive)
+
+makeArgument :: QName -> Int -> Defs -> Defs
+makeArgument q i = fmap (Set.insert (Argument q i) . Set.delete Positive)
+
+singlePositive :: QName -> Defs
+singlePositive q = Map $ Map.singleton q (Set.singleton Positive)
+
+class HasDefinitions a where
+    getDefs :: a -> Defs
+
+instance HasDefinitions Term where
+    getDefs t = case ignoreBlocking t of
+	Var _ args   -> getDefs args
+	Lam _ t	     -> getDefs t
+	Lit _	     -> mempty
+	Def q args   -> mappend (getDefs q)
+				(mconcat $ zipWith (makeArgument q) [0..] $ map getDefs args)
+	Con q args   -> getDefs (q, args)
+	Pi a b	     -> mappend (makeNegative $ getDefs a) (getDefs b)
+	Fun a b	     -> mappend (makeNegative $ getDefs a) (getDefs b)
+	Sort _	     -> mempty
+	MetaV _ args -> getDefs args
+	BlockedV _   -> __IMPOSSIBLE__
+
+instance HasDefinitions Type where
+    getDefs = getDefs . unEl
+
+instance HasDefinitions QName where
+    getDefs = singlePositive
+
+instance (HasDefinitions a, HasDefinitions b) => HasDefinitions (a,b) where
+    getDefs (x,y) = mappend (getDefs x) (getDefs y)
+
+instance (Functor f, Foldable f, HasDefinitions a) =>
+	 HasDefinitions (f a) where
+    getDefs = foldr mappend mempty . fmap getDefs
+