GHC rewrite rule type-checking failure

[Simon Peyton Jones]

*   Is it feasible for GHC to combine the constraints needed LHS and RHS to form an applicability condition?
I don’t think so.

Remember that a rewrite rule literally rewrites LHS to RHS.  It does not conjure up any new dictionaries out of thin air.  In your example, (D k b) is needed in the result of the rewrite.  Where can it come from?  Only from something matched on the left.

So GHC treats any dictionaries matched on the left as “givens” and tries to solve the ones matched on the left.  If it fails you get the sort of error you see.

One way to see this is to write out the rewrite rule you want, complete with all its dictionary arguments. Can you do that?

Simon

From: Glasgow-haskell-users [mailto:glasgow-haskell-users-bounces at haskell.org] On Behalf Of Conal Elliott
Sent: 03 October 2017 01:03
To: Joachim Breitner <mail at joachim-breitner.de>
Cc: glasgow-haskell-users at haskell.org
Subject: Re: GHC rewrite rule type-checking failure

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<mailto: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<mailto:Glasgow-haskell-users at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-users&data=02%7C01%7Csimonpj%40microsoft.com%7C3da5c75572694bab31aa08d509f25936%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636425858847457302&sdata=6dcqjyAYmKXKwZzQQExmWl1cJlCySmP1EvdjA03O19M%3D&reserved=0>
--
Joachim Breitner
  mail at joachim-breitner.de<mailto:mail at joachim-breitner.de>
  http://www.joachim-breitner.de/<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C3da5c75572694bab31aa08d509f25936%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636425858847457302&sdata=Uoe%2Bw8T3VMFLRsFY%2B8nacXIV0pUQOyCe4iHz%2FS5kGrA%3D&reserved=0>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171003/cda976d6/attachment-0001.html>