@@ -74,37 +74,50 @@ instance Sized FC where
74instance Show FC where
74instance Show FC where
75 show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c
75 show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c
77+-- | Used for error reflection
78+data ErrorReportPart = TextPart String
84+-- Please remember to keep Err synchronised with
85+-- Language.Reflection.Errors.Err in the stdlib!
87+-- | Idris errors. Used as exceptions in the compiler, but reported to users
88+-- if they reach the top level.
77data Err = Msg String
89data Err = Msg String
78− | InternalMsg String
90+ | InternalMsg String
79− | CantUnify Bool Term Term Err [(Name, Type)] Int
91+ | CantUnify Bool Term Term Err [(Name, Type)] Int
80− -- Int is 'score' - how much we did unify
92+ -- Int is 'score' - how much we did unify
81− -- Bool indicates recoverability, True indicates more info may make
93+ -- Bool indicates recoverability, True indicates more info may make
82− -- unification succeed
94+ -- unification succeed
83− | InfiniteUnify Name Term [(Name, Type)]
95+ | InfiniteUnify Name Term [(Name, Type)]
84− | CantConvert Term Term [(Name, Type)]
96+ | CantConvert Term Term [(Name, Type)]
85− | UnifyScope Name Name Term [(Name, Type)]
97+ | UnifyScope Name Name Term [(Name, Type)]
86− | CantInferType String
98+ | CantInferType String
87− | NonFunctionType Term Term
99+ | NonFunctionType Term Term
88− | NotEquality Term Term
100+ | NotEquality Term Term
89− | TooManyArguments Name
101+ | TooManyArguments Name
90− | CantIntroduce Term
102+ | CantIntroduce Term
91− | NoSuchVariable Name
103+ | NoSuchVariable Name
92− | NoTypeDecl Name
104+ | NoTypeDecl Name
93− | NotInjective Term Term Term
105+ | NotInjective Term Term Term
94− | CantResolve Term
106+ | CantResolve Term
95− | CantResolveAlts [String]
107+ | CantResolveAlts [String]
96− | IncompleteTerm Term
108+ | IncompleteTerm Term
97− | UniverseError
109+ | UniverseError
98− | ProgramLineComment
110+ | ProgramLineComment
99− | Inaccessible Name
111+ | Inaccessible Name
100− | NonCollapsiblePostulate Name
112+ | NonCollapsiblePostulate Name
101− | AlreadyDefined Name
113+ | AlreadyDefined Name
102− | ProofSearchFail Err
114+ | ProofSearchFail Err
103− | NoRewriting Term
115+ | NoRewriting Term
104− | At FC Err
116+ | At FC Err
105− | Elaborating String Name Err
117+ | Elaborating String Name Err
106− | ProviderError String
118+ | ProviderError String
107− | LoadingFailed String Err
119+ | LoadingFailed String Err
120+ | ReflectionError [ErrorReportPart]
108 deriving Eq
121 deriving Eq
110deriving instance NFData Err
123deriving instance NFData Err