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