Merge pull request #860 from david-christiansen/provider-type-normalize
Normalise provider types before checking
commit3dbd8bb5e9976beedc95386050fa631bd6fa69e9
authorEdwin Brady <edwin.brady@gmail.com>
dateThu 6 Feb 2014, 15:11 (13 years ago)
parentf446697be4cff0
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