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?