@@ -74,9 +74,9 @@ elabProvider info syn fc what n
74 (e, et) <- case what of
74 (e, et) <- case what of
75 ProvTerm _ tm -> elabVal info ERHS tm
75 ProvTerm _ tm -> elabVal info ERHS tm
76 ProvPostulate tm -> elabVal info ERHS tm
76 ProvPostulate tm -> elabVal info ERHS tm
77− unless (isProviderOf (normalise ctxt [] ty') et) $
77+ unless (isProviderOf ctxt ty' et) $
78− ifail $ "Expected provider type IO (Provider (" ++
78+ ifail $ "Expected provider type " ++ show (providerOf ty') ++
79− show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
79+ ", got " ++ show et ++ " instead."
81 -- Execute the type provider and normalise the result
81 -- Execute the type provider and normalise the result
82 -- use 'run__provider' to convert to a primitive IO action
82 -- use 'run__provider' to convert to a primitive IO action
@@ -107,11 +107,17 @@ elabProvider info syn fc what n
107 isTType (TType _) = True
107 isTType (TType _) = True
108 isTType _ = False
108 isTType _ = 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)
110− isProviderOf :: TT Name -> TT Name -> Bool
118+ isProviderOf :: Context -> TT Name -> TT Name -> Bool
111− isProviderOf tp prov
119+ isProviderOf ctxt tp prov =
112− | (P _ (UN io) _, [prov']) <- unApply prov
120+ case converts ctxt [] (providerOf tp) prov of
113− , (P _ (NS (UN prov) [provs]) _, [tp']) <- unApply prov'
121+ OK _ -> True
114− , tp == tp', io == txt "IO"
115− , prov == txt "Provider" && provs == txt "Providers" = True
116− isProviderOf _ _ = False
122+ _ -> False