GHC rewrite rule type-checking failure

[Joachim Breitner]

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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171002/13eda560/attachment.sig>