GHC rewrite rule type-checking failure

[Conal Elliott]

I'm running into type checking problem with GHC rewrite rules in GHC 8.0.2,
illustrated in the code below. The first rule type-checks, but the second
triggers the type error mentioned in the comment following the rule
definition. I'd expect both rules to type-check, adding the needed
constraints to the applicability condition for the rule.

Is GHC's behavior intended (and perhaps necessary), or a bug?

Thanks,  -- Conal

Code (also attached):


{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-# 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/(.)" 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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171002/c60de4cb/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: RuleFail.hs
Type: application/octet-stream
Size: 965 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171002/c60de4cb/attachment.obj>