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?