@@ -215,45 +215,47 @@ elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris
215215elabProvider info syn fc n ty tm
216216 = do i <- getIState
217217 -- Ensure that the experimental extension is enabled
218− if not (TypeProviders `elem` idris_language_extensions i)
219− then fail $ "Failed to define type provider \"" ++ show n ++
220− "\".\nYou must turn on the TypeProviders extension."
221− else do ctxt <- getContext
218+ unless (TypeProviders `elem` idris_language_extensions i) $
219+ fail $ "Failed to define type provider \"" ++ show n ++
220+ "\".\nYou must turn on the TypeProviders extension."
222221
223− -- First elaborate the expected type (and check that it's a type)
224− (ty', typ) <- elabVal toplevel False ty
225− unless (isTType typ) $
226− (fail $ "Expected a type, got " ++ show ty' ++ " : " ++ show typ)
222+ ctxt <- getContext
223+
224+ -- First elaborate the expected type (and check that it's a type)
225+ (ty', typ) <- elabVal toplevel False ty
226+ unless (isTType typ) $
227+ (fail $ "Expected a type, got " ++ show ty' ++ " : " ++ show typ)
227228
228− -- Elaborate the provider term to TT and check that the type matches
229− (e, et) <- elabVal toplevel False tm
230− unless (isProviderOf ty' et) $
231− fail $ "Expected provider type IO (Provider (" ++
232− show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
229+ -- Elaborate the provider term to TT and check that the type matches
230+ (e, et) <- elabVal toplevel False tm
231+ unless (isProviderOf ty' et) $
232+ fail $ "Expected provider type IO (Provider (" ++
233+ show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
233234
234− -- Create the top-level type declaration
235− elabType info syn "" fc [] n ty
235+ -- Create the top-level type declaration
236+ elabType info syn "" fc [] n ty
236237
237− -- Execute the type provider and normalise the result
238− rhs <- execute e
239− let rhs' = normalise ctxt [] rhs
240− logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
238+ -- Execute the type provider and normalise the result
239+ rhs <- execute e
240+ let rhs' = normalise ctxt [] rhs
241+ logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
241242
242− -- Extract the provided term from the type provider
243− tm <- getProvided rhs'
243+ -- Extract the provided term from the type provider
244+ tm <- getProvided rhs'
244245
245− -- Finally add a top-level definition of the provided term
246− elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i tm) []]
247− logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
246+ -- Finally add a top-level definition of the provided term
247+ elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i tm) []]
248+ logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
248249
249250 where isTType :: TT Name -> Bool
250251 isTType (TType _) = True
251252 isTType _ = False
252253
253254 isProviderOf :: TT Name -> TT Name -> Bool
254− isProviderOf tp prov | (P _ (UN "IO") _, [prov']) <- unApply prov
255− , (P _ (NS (UN "Provider") ["Providers"]) _, [tp']) <- unApply prov'
256− , tp == tp' = True
255+ isProviderOf tp prov
256+ | (P _ (UN "IO") _, [prov']) <- unApply prov
257+ , (P _ (NS (UN "Provider") ["Providers"]) _, [tp']) <- unApply prov'
258+ , tp == tp' = True
257259 isProviderOf _ _ = False
258260
259261