From 30873a77626705c7ae48c6ac29b5f4748e027b50 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 28 Jun 2019 13:15:05 -0400 Subject: [PATCH] Turn the wheel to maximum fastness. --- semantic-core/src/Data/Core.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/semantic-core/src/Data/Core.hs b/semantic-core/src/Data/Core.hs index 6cceec56f..5fee9a200 100644 --- a/semantic-core/src/Data/Core.hs +++ b/semantic-core/src/Data/Core.hs @@ -255,14 +255,14 @@ efold :: forall l m n z b -> Core (l b) -> n (z b) efold var let' seq' lam app unit bool if' string load edge frame dot assign ann k = eiter var alg - where alg :: forall x l' c z' . Functor c => (forall l'' z'' x . (l'' x -> m (z'' x)) -> c (l'' x) -> n (z'' x)) -> (l' x -> m (z' x)) -> CoreF c (l' x) -> n (z' x) + where alg :: forall x l' c z' . (forall a b . Coercible a b => Coercible (c a) (c b)) => (forall l'' z'' x . (l'' x -> m (z'' x)) -> c (l'' x) -> n (z'' x)) -> (l' x -> m (z' x)) -> CoreF c (l' x) -> n (z' x) alg go h = \case LetF a -> let' a a :>>$ b -> go h a `seq'` go h b LamF b -> lam (coerce (go (coerce (k . fmap (go h)) :: ((Incr :.: c :.: l') x -> m ((Incr :.: n :.: z') x))) - (fmap coerce b))) -- FIXME: can we avoid this fmap and just coerce harder? + (coerce b))) a :$$ b -> go h a `app` go h b UnitF -> unit BoolF b -> bool b @@ -278,7 +278,7 @@ efold var let' seq' lam app unit bool if' string load edge frame dot assign ann -- | Efficient Mendler-style iteration. eiter :: forall l m n z b . (forall a . m a -> n a) - -> (forall a l' c z' . Functor c => (forall l'' z'' x . (l'' x -> m (z'' x)) -> c (l'' x) -> n (z'' x)) -> (l' a -> m (z' a)) -> CoreF c (l' a) -> n (z' a)) + -> (forall a l' c z' . (forall a b . Coercible a b => Coercible (c a) (c b)) => (forall l'' z'' x . (l'' x -> m (z'' x)) -> c (l'' x) -> n (z'' x)) -> (l' a -> m (z' a)) -> CoreF c (l' a) -> n (z' a)) -> (l b -> m (z b)) -> Core (l b) -> n (z b)