Normalise provider types before checking
This ensures, among other things, that:
* Namespaces don't get in the way
* Type synonyms get expanded
commitbe4cff079ac34004cb21957179ed44e0e62fee12
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateThu 6 Feb 2014, 10:49 (13 years ago)
parent138d35e
src/Idris/ElabDecls.hs+1−1
@@ -630,7 +630,7 @@ elabProvider info syn fc n ty tm
630630
631631 -- Elaborate the provider term to TT and check that the type matches
632632 (e, et) <- elabVal toplevel False tm
633− unless (isProviderOf ty' et) $
633+ unless (isProviderOf (normalise ctxt [] ty') et) $
634634 ifail $ "Expected provider type IO (Provider (" ++
635635 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
636636