GHC rewrite rule type-checking failure

[Conal Elliott]

Thanks very much for the reply, Joachim.

Oops! I flubbed the example. I really `morph` to distribute over an
application of `comp`. New code below (and attached). You're right that I
wouldn't want to restrict the type of `morph`, since each `morph` *rule*
imposes its own restrictions.

My questions:

*   Is it feasible for GHC to combine the constraints needed LHS and RHS to
form an applicability condition?
*   Is there any way I can make the needed constraints explicit in my
rewrite rules?
*   Are there any other work-arounds that would enable writing such
RHS-constrained rules?

Regards, -- Conal

``` haskell
{-# OPTIONS_GHC -Wall #-}
-- Demonstrate a type checking failure with rewrite rules

module RuleFail where

class C k where comp' :: k b c -> k a b -> k a c

instance C (->) where comp' = (.)

-- Late-inlining version to enable rewriting.
comp :: C k => k b c -> k a b -> k a c
comp = comp'
{-# INLINE [0] comp #-}

morph :: (a -> b) -> k a b
morph = error "morph: undefined"

{-# RULES "morph/(.)" forall f g. morph (g `comp` f) = morph g `comp` morph
f #-}

-- • Could not deduce (C k) arising from a use of ‘comp’
--   from the context: C (->)
--     bound by the RULE "morph/(.)"
```


On Mon, Oct 2, 2017 at 3:52 PM, Joachim Breitner <mail at joachim-breitner.de>
wrote:

> Hi Conal,
>
> The difference is that the LHS of the first rule is mentions the `C k`
> constraint (probably unintentionally):
>
> *RuleFail> :t morph comp
> morph comp :: C k => k1 (k b c) (k a b -> k a c)
>
> but the LHS of the second rule side does not:
>
> *RuleFail> :t morph addC
> morph addC :: Num b => k (b, b) b
>
>
>
> A work-around is to add the constraint to `morph`:
>
>     morph :: D k b => (a -> b) -> k a b
>     morph = error "morph: undefined"
>
>     but I fear that this work-around is not acceptable to you.
>
>     Joachim
>
>     Am Montag, den 02.10.2017, 14:25 -0700 schrieb Conal Elliott:
>     > -- Demonstrate a type checking failure with rewrite rules
> >
> > module RuleFail where
> >
> > class C k where comp' :: k b c -> k a b -> k a c
> >
> > instance C (->) where comp' = (.)
> >
> > -- Late-inlining version to enable rewriting.
> > comp :: C k => k b c -> k a b -> k a c
> > comp = comp'
> > {-# INLINE [0] comp #-}
> >
> > morph :: (a -> b) -> k a b
> > morph = error "morph: undefined"
> >
> > {-# RULES "morph/(.)" morph comp = comp #-}  -- Fine
>
>
>
> > class D k a where addC' :: k (a,a) a
> >
> > instance Num a => D (->) a where addC' = uncurry (+)
> >
> > -- Late-inlining version to enable rewriting.
> > addC :: D k a => k (a,a) a
> > addC = addC'
> > {-# INLINE [0] addC #-}
> >
> > {-# RULES "morph/addC" morph addC = addC #-}  -- Fail
> >
> > -- • Could not deduce (D k b) arising from a use of ‘addC’
> > --   from the context: D (->) b
> >
> > -- Why does GHC infer the (C k) constraint for the first rule but not (D
> k b)
> > -- for the second rule?
> >
> > _______________________________________________
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
> --
> Joachim Breitner
>   mail at joachim-breitner.de
>   http://www.joachim-breitner.de/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171002/03062b62/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: RuleFail.hs
Type: application/octet-stream
Size: 590 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171002/03062b62/attachment-0001.obj>