@@ -117,11 +117,13 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
117117 errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
118118 when (ErrorHandler `elem` opts) $ do
119119 if errorReflection
120− then do
120+ then
121121 -- TODO: Check that the declared type is the correct type for an error handler:
122− -- handler : List (TTName, TT) -> Err -> ErrorReport
123− i <- getIState
124− putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }
122+ -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt
123+ if tyIsHandler nty'
124+ then do i <- getIState
125+ putIState $ i { idris_errorhandlers = n : idris_errorhandlers i }
126+ else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
125127 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
126128 when corec $ do setAccessibility n Frozen
127129 addIBC (IBCAccess n Frozen)
@@ -135,6 +137,16 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
135137 | otherwise = mergeTy sc sc'
136138 mergeTy _ sc = sc
137139
140+ tyIsHandler (Bind _ (Pi (P _ (NS (UN "Err") ns1) _))
141+ (App (P _ (NS (UN "Maybe") ns2) _)
142+ (App (P _ (NS (UN "List") ns3) _)
143+ (P _ (NS (UN "ErrorReportPart") ns4) _))))
144+ | ns1 == ["Errors","Reflection","Language"]
145+ , ns2 == ["Maybe", "Prelude"]
146+ , ns3 == ["List", "Prelude"]
147+ , ns4 == ["Errors","Reflection","Language"] = True
148+ tyIsHandler _ = False
149+
138150
139151elabPostulate :: ElabInfo -> SyntaxInfo -> String ->
140152 FC -> FnOpts -> Name -> PTerm -> Idris ()