{-# LANGUAGE CPP, ExistentialQuantification, FlexibleContexts, Rank2Types, TypeSynonymInstances, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving #-} module Agda.TypeChecking.Monad.Base where import Control.Exception as E import Control.Monad.Error import Control.Monad.State import Control.Monad.Reader import Control.Applicative import Data.Int import Data.Map as Map import Data.Set as Set import Data.Generics import Data.Foldable import Data.Traversable import System.Time import Agda.Syntax.Common import qualified Agda.Syntax.Concrete as C import qualified Agda.Syntax.Concrete.Definitions as D import qualified Agda.Syntax.Abstract as A import Agda.Syntax.Internal import Agda.Syntax.Position import Agda.Syntax.Scope.Base import Agda.TypeChecking.CompiledClause import Agda.Interaction.Exceptions import {-# SOURCE #-} Agda.Interaction.FindFile import Agda.Interaction.Options import qualified Agda.Interaction.Highlighting.Range as R import Agda.Interaction.Highlighting.Precise (HighlightingInfo) import Agda.Utils.FileName import Agda.Utils.Fresh import Agda.Utils.Monad import Agda.Utils.Permutation #include "../../undefined.h" import Agda.Utils.Impossible --------------------------------------------------------------------------- -- * Type checking state --------------------------------------------------------------------------- data TCState = TCSt { stFreshThings :: FreshThings , stMetaStore :: MetaStore , stInteractionPoints :: InteractionPoints , stConstraints :: Constraints , stSignature :: Signature , stImports :: Signature , stImportedModules :: Set ModuleName , stModuleToSource :: ModuleToSource , stVisitedModules :: VisitedModules , stDecodedModules :: DecodedModules , stCurrentModule :: Maybe ModuleName -- ^ The current module is available after it has been type -- checked. , stScope :: ScopeInfo , stPersistentOptions :: CommandLineOptions -- ^ Options which apply to all files, unless overridden. , stPragmaOptions :: PragmaOptions -- ^ Options applying to the current file. @OPTIONS@ -- pragmas only affect this field. , stStatistics :: Statistics , stMutualBlocks :: Map MutualId (Set QName) , stLocalBuiltins :: BuiltinThings PrimFun , stImportedBuiltins :: BuiltinThings PrimFun , stHaskellImports :: Set String -- ^ Imports that should be generated by the compiler (this -- includes imports from imported modules). } data FreshThings = Fresh { fMeta :: MetaId , fInteraction :: InteractionId , fMutual :: MutualId , fName :: NameId , fCtx :: CtxId , fInteger :: Integer -- ^ Can be used for various things. } deriving (Show) initState :: TCState initState = TCSt { stFreshThings = Fresh 0 0 0 (NameId 0 0) 0 0 , stMetaStore = Map.empty , stInteractionPoints = Map.empty , stConstraints = [] , stSignature = emptySignature , stImports = emptySignature , stImportedModules = Set.empty , stModuleToSource = Map.empty , stVisitedModules = Map.empty , stDecodedModules = Map.empty , stCurrentModule = Nothing , stScope = emptyScopeInfo , stPersistentOptions = defaultOptions , stPragmaOptions = optPragmaOptions $ defaultOptions , stStatistics = Map.empty , stMutualBlocks = Map.empty , stLocalBuiltins = Map.empty , stImportedBuiltins = Map.empty , stHaskellImports = Set.empty } stBuiltinThings :: TCState -> BuiltinThings PrimFun stBuiltinThings s = stLocalBuiltins s `Map.union` stImportedBuiltins s instance HasFresh MetaId FreshThings where nextFresh s = (i, s { fMeta = i + 1 }) where i = fMeta s instance HasFresh MutualId FreshThings where nextFresh s = (i, s { fMutual = i + 1 }) where i = fMutual s instance HasFresh InteractionId FreshThings where nextFresh s = (i, s { fInteraction = i + 1 }) where i = fInteraction s instance HasFresh NameId FreshThings where nextFresh s = (i, s { fName = succ i }) where i = fName s instance HasFresh CtxId FreshThings where nextFresh s = (i, s { fCtx = succ i }) where i = fCtx s instance HasFresh Integer FreshThings where nextFresh s = (i, s { fInteger = succ i }) where i = fInteger s instance HasFresh i FreshThings => HasFresh i TCState where nextFresh s = ((,) $! i) $! s { stFreshThings = f } where (i, f) = nextFresh $ stFreshThings s --------------------------------------------------------------------------- -- ** Interface --------------------------------------------------------------------------- data ModuleInfo = ModuleInfo { miInterface :: Interface , miWarnings :: Bool -- ^ 'True' if warnings were encountered when the module was type -- checked. , miTimeStamp :: ClockTime -- ^ The modification time stamp of the interface file when the -- interface was read or written. Alternatively, if warnings were -- encountered (in which case there may not be any up-to-date -- interface file), the time at which the interface was produced -- (approximately). } -- Note that the use of 'C.TopLevelModuleName' here is a potential -- performance problem, because these names do not contain unique -- identifiers. type VisitedModules = Map C.TopLevelModuleName ModuleInfo type DecodedModules = Map C.TopLevelModuleName (Interface, ClockTime) data Interface = Interface { iImportedModules :: [ModuleName] , iModuleName :: ModuleName , iScope :: Map ModuleName Scope , iInsideScope :: ScopeInfo , iSignature :: Signature , iBuiltin :: BuiltinThings String , iHaskellImports :: Set String -- ^ Haskell imports listed in -- (transitively) imported modules are -- not included here. , iHighlighting :: HighlightingInfo , iPragmaOptions :: [OptionsPragma] -- ^ Pragma options set in the file. } deriving (Typeable, Data, Show) --------------------------------------------------------------------------- -- ** Closure --------------------------------------------------------------------------- data Closure a = Closure { clSignature :: Signature , clEnv :: TCEnv , clScope :: ScopeInfo , clValue :: a } deriving (Typeable, Data) instance Show a => Show (Closure a) where show cl = "Closure " ++ show (clValue cl) instance HasRange a => HasRange (Closure a) where getRange = getRange . clValue buildClosure :: MonadTCM tcm => a -> tcm (Closure a) buildClosure x = liftTCM $ do env <- ask sig <- gets stSignature scope <- gets stScope return $ Closure sig env scope x --------------------------------------------------------------------------- -- ** Constraints --------------------------------------------------------------------------- type ConstraintClosure = Closure Constraint data Constraint = ValueCmp Comparison Type Term Term | ArgsCmp [Polarity] Type Args Args | TypeCmp Comparison Type Type | TelCmp Comparison Telescope Telescope | SortCmp Comparison Sort Sort | LevelCmp Comparison Term Term | UnBlock MetaId | Guarded Constraint Constraints | IsEmpty Type deriving (Typeable, Show) data Comparison = CmpEq | CmpLeq deriving (Eq, Typeable, Show) type Constraints = [ConstraintClosure] --------------------------------------------------------------------------- -- * Open things --------------------------------------------------------------------------- -- | A thing tagged with the context it came from. data Open a = OpenThing [CtxId] a deriving (Typeable, Data, Show) --------------------------------------------------------------------------- -- * Judgements --------------------------------------------------------------------------- data Judgement t a = HasType a t | IsSort a deriving (Typeable, Data) instance (Show t, Show a) => Show (Judgement t a) where show (HasType a t) = show a ++ " : " ++ show t show (IsSort a) = show a ++ " sort" instance Functor (Judgement t) where fmap f (HasType x t) = HasType (f x) t fmap f (IsSort x) = IsSort (f x) instance Foldable (Judgement t) where foldr f z (HasType x _) = f x z foldr f z (IsSort x) = f x z instance Traversable (Judgement t) where traverse f (HasType x t) = flip HasType t <$> f x traverse f (IsSort x) = IsSort <$> f x --------------------------------------------------------------------------- -- ** Meta variables --------------------------------------------------------------------------- data MetaVariable = MetaVar { mvInfo :: MetaInfo , mvPriority :: MetaPriority -- ^ some metavariables are more eager to be instantiated , mvPermutation :: Permutation -- ^ a metavariable doesn't have to depend on all variables -- in the context, this "permutation" will throw away the -- ones it does not depend on , mvJudgement :: Judgement Type MetaId , mvInstantiation :: MetaInstantiation , mvListeners :: Set MetaId -- ^ metavariables interested in what happens to this guy } deriving (Typeable) data MetaInstantiation = InstV Term | InstS Term -- should be Lam .. Sort s | Open | BlockedConst Term | PostponedTypeCheckingProblem (Closure (A.Expr, Type, TCM Bool)) deriving (Typeable) instance Show MetaInstantiation where show (InstV t) = "InstV (" ++ show t ++ ")" show (InstS s) = "InstS (" ++ show s ++ ")" show Open = "Open" show (BlockedConst t) = "BlockedConst (" ++ show t ++ ")" show (PostponedTypeCheckingProblem{}) = "PostponedTypeCheckingProblem (...)" newtype MetaPriority = MetaPriority Int deriving (Eq, Ord, Show) -- | TODO: Not so nice. type MetaInfo = Closure Range type MetaStore = Map MetaId MetaVariable instance HasRange MetaVariable where getRange m = getRange $ getMetaInfo m instance SetRange MetaVariable where setRange r (MetaVar mi p perm j inst ls) = MetaVar (mi {clValue = r}) p perm j inst ls normalMetaPriority :: MetaPriority normalMetaPriority = MetaPriority 0 lowMetaPriority :: MetaPriority lowMetaPriority = MetaPriority (-10) highMetaPriority :: MetaPriority highMetaPriority = MetaPriority 10 getMetaInfo :: MetaVariable -> MetaInfo getMetaInfo = mvInfo getMetaScope :: MetaVariable -> ScopeInfo getMetaScope m = clScope $ getMetaInfo m getMetaEnv :: MetaVariable -> TCEnv getMetaEnv m = clEnv $ getMetaInfo m getMetaSig :: MetaVariable -> Signature getMetaSig m = clSignature $ getMetaInfo m --------------------------------------------------------------------------- -- ** Interaction meta variables --------------------------------------------------------------------------- type InteractionPoints = Map InteractionId MetaId newtype InteractionId = InteractionId Nat deriving (Eq,Ord,Num,Integral,Real,Enum) instance Show InteractionId where show (InteractionId x) = "?" ++ show x --------------------------------------------------------------------------- -- ** Signature --------------------------------------------------------------------------- data Signature = Sig { sigSections :: Sections , sigDefinitions :: Definitions } deriving (Typeable, Data, Show) type Sections = Map ModuleName Section type Definitions = Map QName Definition data Section = Section { secTelescope :: Telescope , secFreeVars :: Nat -- ^ This is the number of parameters when -- we're inside the section and 0 -- outside. It's used to know how much of -- the context to apply function from the -- section to when translating from -- abstract to internal syntax. } deriving (Typeable, Data, Show) emptySignature :: Signature emptySignature = Sig Map.empty Map.empty data DisplayForm = Display Nat [Term] DisplayTerm -- ^ The three arguments are: -- -- * @n@: number of free variables; -- -- * Patterns for arguments, one extra free var which -- represents pattern vars. There should @n@ of them. -- -- * Display form. @n@ free variables. deriving (Typeable, Data, Show) data DisplayTerm = DWithApp [DisplayTerm] Args | DTerm Term deriving (Typeable, Data, Show) defaultDisplayForm :: QName -> [Open DisplayForm] defaultDisplayForm c = [] data Definition = Defn { defName :: QName , defType :: Type -- type of the lifted definition , defDisplay :: [Open DisplayForm] , defMutual :: MutualId , theDef :: Defn } deriving (Typeable, Data, Show) type HaskellCode = String type HaskellType = String data HaskellRepresentation = HsDefn HaskellType HaskellCode | HsType HaskellType deriving (Typeable, Data, Show) data Polarity = Covariant | Contravariant | Invariant deriving (Typeable, Data, Show, Eq) -- | 'Positive' means strictly positive and 'Negative' means not strictly -- positive. data Occurrence = Positive | Negative | Unused deriving (Typeable, Data, Show, Eq, Ord) data Defn = Axiom { axHsDef :: Maybe HaskellRepresentation } | Function { funClauses :: [Clauses] , funCompiled :: CompiledClauses , funInv :: FunctionInverse , funPolarity :: [Polarity] , funArgOccurrences :: [Occurrence] , funAbstr :: IsAbstract , funDelayed :: Delayed -- ^ Are the clauses of this definition delayed? } | Datatype { dataPars :: Nat -- nof parameters , dataIxs :: Nat -- nof indices , dataInduction :: Induction -- data or codata? , dataClause :: (Maybe Clause) -- this might be in an instantiated module , dataCons :: [QName] -- constructor names , dataSort :: Sort , dataPolarity :: [Polarity] , dataArgOccurrences :: [Occurrence] , dataHsType :: Maybe HaskellType , dataAbstr :: IsAbstract } | Record { recPars :: Nat , recClause :: Maybe Clause , recCon :: QName -- ^ Constructor name. , recNamedCon :: Bool , recConType :: Type -- ^ The record constructor's type. , recFields :: [Arg A.QName] , recTel :: Telescope , recPolarity :: [Polarity] , recArgOccurrences :: [Occurrence] , recEtaEquality :: Bool , recAbstr :: IsAbstract } | Constructor { conPars :: Nat -- nof parameters , conSrcCon :: QName -- original constructor (this might be in a module instance) , conData :: QName -- name of datatype or record type , conHsCode :: Maybe (HaskellType, HaskellCode) -- used by the compiler , conAbstr :: IsAbstract , conInd :: Induction -- ^ Inductive or coinductive? } -- ^ Note that, currently, the sharp constructor is -- represented as a definition ('Def'), but if you look -- up the name you will get a @Constructor@. | Primitive { primAbstr :: IsAbstract , primName :: String , primClauses :: Maybe [Clauses] -- ^ 'Nothing' for primitive functions, @'Just' -- something@ for builtin functions. } -- ^ Primitive or builtin functions. deriving (Typeable, Data, Show) defIsRecord :: Defn -> Bool defIsRecord Record{} = True defIsRecord _ = False newtype Fields = Fields [(C.Name, Type)] deriving (Typeable, Data) data Reduced no yes = NoReduction no | YesReduction yes deriving (Typeable) data PrimFun = PrimFun { primFunName :: QName , primFunArity :: Arity , primFunImplementation :: MonadTCM tcm => [Arg Term] -> tcm (Reduced [Arg Term] Term) } deriving (Typeable) defClauses :: Definition -> [Clauses] defClauses Defn{theDef = Function{funClauses = cs}} = cs defClauses Defn{theDef = Primitive{primClauses = Just cs}} = cs defClauses Defn{theDef = Datatype{dataClause = Just c}} = [Clauses Nothing c] defClauses Defn{theDef = Record{recClause = Just c}} = [Clauses Nothing c] defClauses _ = [] defCompiled :: Definition -> Maybe CompiledClauses defCompiled Defn{theDef = Function{funCompiled = cc}} = Just cc defCompiled _ = Nothing -- | Used to specify whether something should be delayed. data Delayed = Delayed | NotDelayed deriving (Typeable, Data, Show, Eq) -- | Are the clauses of this definition delayed? defDelayed :: Definition -> Delayed defDelayed Defn{theDef = Function{funDelayed = d}} = d defDelayed _ = NotDelayed defAbstract :: Definition -> IsAbstract defAbstract d = case theDef d of Axiom{} -> AbstractDef Function{funAbstr = a} -> a Datatype{dataAbstr = a} -> a Record{recAbstr = a} -> a Constructor{conAbstr = a} -> a Primitive{primAbstr = a} -> a --------------------------------------------------------------------------- -- ** Injectivity --------------------------------------------------------------------------- data FunctionInverse = NotInjective | Inverse (Map TermHead Clause) deriving (Typeable, Data, Show) data TermHead = SortHead | PiHead | ConHead QName deriving (Typeable, Data, Eq, Ord, Show) --------------------------------------------------------------------------- -- ** Mutual blocks --------------------------------------------------------------------------- newtype MutualId = MutId Int32 deriving (Typeable, Data, Eq, Ord, Show, Num) --------------------------------------------------------------------------- -- ** Statistics --------------------------------------------------------------------------- type Statistics = Map String Int --------------------------------------------------------------------------- -- ** Trace --------------------------------------------------------------------------- data Call = CheckClause Type A.Clause (Maybe Clause) | forall a. CheckPattern A.Pattern Telescope Type (Maybe a) | CheckLetBinding A.LetBinding (Maybe ()) | InferExpr A.Expr (Maybe (Term, Type)) | CheckExpr A.Expr Type (Maybe Term) | CheckDotPattern A.Expr Term (Maybe Constraints) | CheckPatternShadowing A.Clause (Maybe ()) | IsTypeCall A.Expr Sort (Maybe Type) | IsType_ A.Expr (Maybe Type) | InferVar Name (Maybe (Term, Type)) | InferDef Range QName (Maybe (Term, Type)) | CheckArguments Range [NamedArg A.Expr] Type Type (Maybe (Args, Type, Constraints)) | CheckDataDef Range Name [A.LamBinding] [A.Constructor] (Maybe ()) | CheckRecDef Range Name [A.LamBinding] [A.Constructor] (Maybe ()) | CheckConstructor QName Telescope Sort A.Constructor (Maybe ()) | CheckFunDef Range Name [A.Clause] (Maybe ()) | CheckPragma Range A.Pragma (Maybe ()) | CheckPrimitive Range Name A.Expr (Maybe ()) | CheckSectionApplication Range ModuleName A.Telescope ModuleName [NamedArg A.Expr] (Maybe ()) | ScopeCheckExpr C.Expr (Maybe A.Expr) | ScopeCheckDeclaration D.NiceDeclaration (Maybe [A.Declaration]) | ScopeCheckLHS C.Name C.Pattern (Maybe A.LHS) | ScopeCheckDefinition D.NiceDefinition (Maybe A.Definition) | forall a. TermFunDef Range Name [A.Clause] (Maybe a) | forall a. SetRange Range (Maybe a) -- ^ used by 'setCurrentRange' -- actually, 'a' is Agda.Termination.TermCheck.CallGraph -- but I was to lazy to import the stuff here --Andreas,2007-5-29 deriving (Typeable) -- Dummy instance instance Data Call where dataTypeOf _ = mkDataType "Call" [] toConstr x = mkConstr (dataTypeOf x) "Dummy" [] Prefix gunfold k z _ = __IMPOSSIBLE__ instance HasRange Call where getRange (CheckClause _ c _) = getRange c getRange (CheckPattern p _ _ _) = getRange p getRange (InferExpr e _) = getRange e getRange (CheckExpr e _ _) = getRange e getRange (CheckLetBinding b _) = getRange b getRange (IsTypeCall e s _) = getRange e getRange (IsType_ e _) = getRange e getRange (InferVar x _) = getRange x getRange (InferDef _ f _) = getRange f getRange (CheckArguments r _ _ _ _) = r getRange (CheckDataDef i _ _ _ _) = getRange i getRange (CheckRecDef i _ _ _ _) = getRange i getRange (CheckConstructor _ _ _ c _) = getRange c getRange (CheckFunDef i _ _ _) = getRange i getRange (CheckPragma r _ _) = r getRange (CheckPrimitive i _ _ _) = getRange i getRange (ScopeCheckExpr e _) = getRange e getRange (ScopeCheckDeclaration d _) = getRange d getRange (ScopeCheckLHS _ p _) = getRange p getRange (ScopeCheckDefinition d _) = getRange d getRange (CheckDotPattern e _ _) = getRange e getRange (CheckPatternShadowing c _) = getRange c getRange (TermFunDef i _ _ _) = getRange i getRange (SetRange r _) = r getRange (CheckSectionApplication r _ _ _ _ _) = r --------------------------------------------------------------------------- -- ** Builtin things --------------------------------------------------------------------------- type BuiltinThings pf = Map String (Builtin pf) data Builtin pf = Builtin Term | Prim pf deriving (Typeable, Data, Show) instance Functor Builtin where fmap f (Builtin t) = Builtin t fmap f (Prim x) = Prim $ f x instance Foldable Builtin where foldr f z (Builtin t) = z foldr f z (Prim x) = f x z instance Traversable Builtin where traverse f (Builtin t) = pure $ Builtin t traverse f (Prim x) = Prim <$> f x --------------------------------------------------------------------------- -- * Type checking environment --------------------------------------------------------------------------- data TCEnv = TCEnv { envContext :: Context , envLetBindings :: LetBindings , envCurrentModule :: ModuleName , envAnonymousModules :: [(ModuleName, Nat)] -- ^ anonymous modules and their number of free variables , envImportPath :: [C.TopLevelModuleName] -- ^ to detect import cycles , envMutualBlock :: Maybe MutualId -- ^ the current (if any) mutual block , envAbstractMode :: AbstractMode -- ^ When checking the typesignature of a public definition -- or the body of a non-abstract definition this is true. -- To prevent information about abstract things leaking -- outside the module. , envReplace :: Bool -- ^ Coinductive constructor applications @c args@ get -- replaced by a function application @f tel@, where -- tel corresponds to the current telescope and @f@ is -- defined as @f tel = c args@. The initial occurrence -- of @c@ in the body of @f@ should not be replaced by -- yet another function application, though. To avoid -- that this happens the @envReplace@ flag is set to -- 'False' when @f@ is checked. , envDisplayFormsEnabled :: Bool -- ^ Sometimes we want to disable display forms. , envReifyInteractionPoints :: Bool -- ^ should we try to recover interaction points when reifying? -- disabled when generating types for with functions , envEtaContractImplicit :: Bool -- ^ it's safe to eta contract implicit lambdas as long as we're -- not going to reify and retypecheck (like when doing with -- abstraction) , envRange :: Range , envCall :: Maybe (Closure Call) -- ^ what we're doing at the moment } deriving (Typeable, Data) initEnv :: TCEnv initEnv = TCEnv { envContext = [] , envLetBindings = Map.empty , envCurrentModule = noModuleName , envAnonymousModules = [] , envImportPath = [] , envMutualBlock = Nothing , envAbstractMode = AbstractMode , envReplace = True , envDisplayFormsEnabled = True , envReifyInteractionPoints = True , envEtaContractImplicit = True , envRange = noRange , envCall = Nothing } --------------------------------------------------------------------------- -- ** Context --------------------------------------------------------------------------- type Context = [ContextEntry] data ContextEntry = Ctx { ctxId :: CtxId , ctxEntry :: Arg (Name, Type) } deriving (Typeable, Data) newtype CtxId = CtxId Nat deriving (Typeable, Data, Eq, Ord, Show, Enum, Real, Integral, Num) --------------------------------------------------------------------------- -- ** Let bindings --------------------------------------------------------------------------- type LetBindings = Map Name (Open (Term, Arg Type)) --------------------------------------------------------------------------- -- ** Abstract mode --------------------------------------------------------------------------- data AbstractMode = AbstractMode -- ^ abstract things in the current module can be accessed | ConcreteMode -- ^ no abstract things can be accessed | IgnoreAbstractMode -- ^ all abstract things can be accessed deriving (Typeable, Data) --------------------------------------------------------------------------- -- * Type checking errors --------------------------------------------------------------------------- -- Occurence of a name in a datatype definition data Occ = OccCon { occDatatype :: QName , occConstructor :: QName , occPosition :: OccPos } | OccClause { occFunction :: QName , occClause :: Int , occPosition :: OccPos } data OccPos = NonPositively | ArgumentTo Nat QName data TypeError = InternalError String | NotImplemented String | NotSupported String | CompilationError String | TerminationCheckFailed [([QName], [R.Range])] -- ^ Parameterised on functions which failed to termination -- check (grouped if they are mutual), along with ranges -- for problematic call sites. | PropMustBeSingleton | DataMustEndInSort Term | ShouldEndInApplicationOfTheDatatype Type -- ^ The target of a constructor isn't an application of its -- datatype. The 'Type' records what it does target. | ShouldBeAppliedToTheDatatypeParameters Term Term -- ^ The target of a constructor isn't its datatype applied to -- something that isn't the parameters. First term is the correct -- target and the second term is the actual target. | ShouldBeApplicationOf Type QName -- ^ Expected a type to be an application of a particular datatype. | ConstructorPatternInWrongDatatype QName QName -- ^ constructor, datatype | DoesNotConstructAnElementOf QName Term -- ^ constructor, type | DifferentArities -- ^ Varying number of arguments for a function. | WrongHidingInLHS Type -- ^ The left hand side of a function definition has a hidden argument -- where a non-hidden was expected. | WrongHidingInLambda Type -- ^ Expected a non-hidden function and found a hidden lambda. | WrongHidingInApplication Type -- ^ A function is applied to a hidden argument where a non-hidden was expected. | NotInductive Term -- ^ The term does not correspond to an inductive data type. | UninstantiatedDotPattern A.Expr | IlltypedPattern A.Pattern Type | TooManyArgumentsInLHS Nat Type | WrongNumberOfConstructorArguments QName Nat Nat | ShouldBeEmpty Type [Pattern] | ShouldBeASort Type -- ^ The given type should have been a sort. | ShouldBePi Type -- ^ The given type should have been a pi. | ShouldBeRecordType Type | NotAProperTerm | SplitOnIrrelevant A.Pattern (Arg Type) | VariableIsIrrelevant Name | UnequalLevel Comparison Term Term | UnequalTerms Comparison Term Term Type | UnequalTypes Comparison Type Type | UnequalTelescopes Comparison Telescope Telescope | UnequalRelevance Type Type -- ^ The two function types have different relevance. | UnequalHiding Type Type -- ^ The two function types have different hiding. | UnequalSorts Sort Sort | NotLeqSort Sort Sort | MetaCannotDependOn MetaId [Nat] Nat -- ^ The arguments are the meta variable, the parameters it can -- depend on and the paratemeter that it wants to depend on. | MetaOccursInItself MetaId | GenericError String | BuiltinMustBeConstructor String A.Expr | NoSuchBuiltinName String | DuplicateBuiltinBinding String Term Term | NoBindingForBuiltin String | NoSuchPrimitiveFunction String | ShadowedModule [A.ModuleName] | BuiltinInParameterisedModule String | NoRHSRequiresAbsurdPattern [NamedArg A.Pattern] | AbsurdPatternRequiresNoRHS [NamedArg A.Pattern] | TooFewFields QName [C.Name] | TooManyFields QName [C.Name] | DuplicateFields [C.Name] | DuplicateConstructors [C.Name] | UnexpectedWithPatterns [A.Pattern] | WithClausePatternMismatch A.Pattern Pattern | FieldOutsideRecord | ModuleArityMismatch A.ModuleName Telescope [NamedArg A.Expr] -- Coverage errors | IncompletePatternMatching Term Args -- can only happen if coverage checking is switched off | CoverageFailure QName [[Arg Pattern]] | UnreachableClauses QName [[Arg Pattern]] | CoverageCantSplitOn QName | CoverageCantSplitType Type -- Positivity errors | NotStrictlyPositive QName [Occ] -- Import errors | LocalVsImportedModuleClash ModuleName | UnsolvedMetas [Range] | UnsolvedConstraints Constraints | CyclicModuleDependency [C.TopLevelModuleName] | FileNotFound C.TopLevelModuleName [AbsolutePath] | OverlappingProjects AbsolutePath C.TopLevelModuleName C.TopLevelModuleName | AmbiguousTopLevelModuleName C.TopLevelModuleName [AbsolutePath] | ModuleNameDoesntMatchFileName C.TopLevelModuleName [AbsolutePath] | ClashingFileNamesFor ModuleName [AbsolutePath] | ModuleDefinedInOtherFile C.TopLevelModuleName AbsolutePath AbsolutePath -- ^ Module name, file from which it was loaded, file which -- the include path says contains the module. -- Scope errors | BothWithAndRHS | NotInScope [C.QName] | NoSuchModule C.QName | AmbiguousName C.QName [A.QName] | AmbiguousModule C.QName [A.ModuleName] | UninstantiatedModule C.QName | ClashingDefinition C.QName A.QName | ClashingModule A.ModuleName A.ModuleName | ClashingImport C.Name A.QName | ClashingModuleImport C.Name A.ModuleName | PatternShadowsConstructor A.Name A.QName | ModuleDoesntExport C.QName [C.ImportedName] | DuplicateImports C.QName [C.ImportedName] | InvalidPattern C.Pattern | RepeatedVariablesInPattern [C.Name] -- Concrete to Abstract errors | NotAModuleExpr C.Expr -- ^ The expr was used in the right hand side of an implicit module -- definition, but it wasn't of the form @m Delta@. | NotAnExpression C.Expr | NotAValidLetBinding D.NiceDeclaration | NothingAppliedToHiddenArg C.Expr -- Operator errors | NoParseForApplication [C.Expr] | AmbiguousParseForApplication [C.Expr] [C.Expr] | NoParseForLHS C.Pattern | AmbiguousParseForLHS C.Pattern [C.Pattern] -- Usage errors deriving (Typeable) instance Show TypeError where show _ = "" -- TODO: more info? instance Error TypeError where noMsg = strMsg "" strMsg = GenericError -- | Type-checking errors. data TCErr' = TypeError TCState (Closure TypeError) | Exception Range String | IOException Range E.IOException | PatternErr TCState -- ^ for pattern violations | AbortAssign TCState -- ^ used to abort assignment to meta when there are instantiations deriving (Typeable) -- | Type-checking errors, potentially paired with relevant syntax -- highlighting information. data TCErr = TCErr { errHighlighting :: Maybe (HighlightingInfo, ModuleToSource) -- ^ The 'ModuleToSource' can be used to map the module -- names in the 'HighlightingInfo' to file names. , errError :: TCErr' } deriving (Typeable) instance Error TCErr where noMsg = strMsg "" strMsg = TCErr Nothing . Exception noRange . strMsg instance Show TCErr where show = show . errError instance Show TCErr' where show (TypeError _ e) = show (envRange $ clEnv e) ++ ": " ++ show (clValue e) show (Exception r s) = show r ++ ": " ++ s show (IOException r e) = show r ++ ": " ++ show e show (PatternErr _) = "Pattern violation (you shouldn't see this)" show (AbortAssign _) = "Abort assignment (you shouldn't see this)" instance HasRange TCErr' where getRange (TypeError _ cl) = envRange $ clEnv cl getRange (Exception r _) = r getRange (IOException r _) = r getRange (PatternErr s) = noRange getRange (AbortAssign s) = noRange instance HasRange TCErr where getRange = getRange . errError instance Exception TCErr --------------------------------------------------------------------------- -- * Type checking monad transformer --------------------------------------------------------------------------- newtype TCMT m a = TCM { unTCM :: TCState -> TCEnv -> m (a, TCState) } instance MonadIO m => MonadReader TCEnv (TCMT m) where ask = TCM $ \s e -> return (e, s) local f (TCM m) = TCM $ \s e -> m s (f e) instance MonadIO m => MonadState TCState (TCMT m) where get = TCM $ \s _ -> return (s, s) put s = TCM $ \_ _ -> return ((), s) type TCM = TCMT IO class ( Applicative tcm, MonadIO tcm , MonadReader TCEnv tcm , MonadState TCState tcm ) => MonadTCM tcm where liftTCM :: TCM a -> tcm a instance MonadError TCErr (TCMT IO) where throwError = liftIO . throwIO catchError m h = TCM $ \s e -> unTCM m s e `E.catch` \err -> unTCM (h err) s e catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a catchError_ m h = TCM $ \s e -> unTCM m s e `E.catch` \err -> unTCM (h err) (error "catchError_") e mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a mapTCMT f (TCM m) = TCM $ \s e -> f (m s e) pureTCM :: Monad m => (TCState -> TCEnv -> a) -> TCMT m a pureTCM f = TCM $ \s e -> return (f s e, s) instance MonadIO m => MonadTCM (TCMT m) where liftTCM = mapTCMT liftIO instance (Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm) where liftTCM = lift . liftTCM instance MonadTrans TCMT where lift m = TCM $ \s _ -> m >>= \x -> return (x, s) -- We want a special monad implementation of fail. {-# SPECIALIZE instance Monad TCM #-} instance MonadIO m => Monad (TCMT m) where return x = TCM $ \s _ -> return (x, s) m >>= k = TCM $ \s e -> do (x, s') <- unTCM m s e unTCM (k x) s' e fail = internalError instance MonadIO m => Functor (TCMT m) where fmap = liftM instance MonadIO m => Applicative (TCMT m) where pure = return (<*>) = ap instance MonadIO m => MonadIO (TCMT m) where liftIO m = TCM $ \s e -> do let r = envRange e liftIO $ wrap r $ do x <- m x `seq` return (x, s) where wrap r m = failOnException handleException $ E.catch m (handleIOException r) handleIOException r e = throwIO $ TCErr Nothing $ IOException r e handleException r s = throwIO $ TCErr Nothing $ Exception r s patternViolation :: MonadTCM tcm => tcm a patternViolation = liftTCM $ do s <- get throwError $ TCErr Nothing $ PatternErr s internalError :: MonadTCM tcm => String -> tcm a internalError s = typeError $ InternalError s typeError :: MonadTCM tcm => TypeError -> tcm a typeError err = liftTCM $ do cl <- buildClosure err s <- get throwError $ TCErr Nothing $ TypeError s cl -- | Running the type checking monad runTCM :: TCMT IO a -> IO (Either TCErr a) runTCM m = (Right <$> runTCM' m) `E.catch` (return . Left) runTCM' :: Monad m => TCMT m a -> m a runTCM' m = liftM fst (unTCM m initState initEnv)