@@ -74,9 +74,9 @@ elabProvider info syn fc what n
7474 (e, et) <- case what of
7575 ProvTerm _ tm -> elabVal info ERHS tm
7676 ProvPostulate tm -> elabVal info ERHS tm
77− unless (isProviderOf (normalise ctxt [] ty') et) $
78− ifail $ "Expected provider type IO (Provider (" ++
79− show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
77+ unless (isProviderOf ctxt ty' et) $
78+ ifail $ "Expected provider type " ++ show (providerOf ty') ++
79+ ", got " ++ show et ++ " instead."
8080
8181 -- Execute the type provider and normalise the result
8282 -- use 'run__provider' to convert to a primitive IO action
@@ -107,11 +107,17 @@ elabProvider info syn fc what n
107107 isTType (TType _) = True
108108 isTType _ = False
109109
110− isProviderOf :: TT Name -> TT Name -> Bool
111− isProviderOf tp prov
112− | (P _ (UN io) _, [prov']) <- unApply prov
113− , (P _ (NS (UN prov) [provs]) _, [tp']) <- unApply prov'
114− , tp == tp', io == txt "IO"
115− , prov == txt "Provider" && provs == txt "Providers" = True
116− isProviderOf _ _ = False
110+ -- Note: IO (Providers.Provider ty) is used instead of IO'
111+ -- (MkFFI C_FFI) (Providers.Provider ty) in hopes of better
112+ -- error messages with less normalisation
113+ providerOf :: Type -> Type
114+ providerOf ty = App (P Ref (sUN "IO") Erased) $
115+ App (P Ref (sNS (sUN "Provider") ["Providers"]) Erased)
116+ ty
117+
118+ isProviderOf :: Context -> TT Name -> TT Name -> Bool
119+ isProviderOf ctxt tp prov =
120+ case converts ctxt [] (providerOf tp) prov of
121+ OK _ -> True
122+ _ -> False
117123