<div dir="ltr"><div>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.</div><div><br></div><div>Is GHC's behavior intended (and perhaps necessary), or a bug?</div><div><br></div><div>Thanks,  -- Conal</div><div><br></div><div>Code (also attached):</div><div><br></div><div><br></div><div><div><font face="monospace, monospace">{-# LANGUAGE FlexibleInstances #-}</font></div><div><font face="monospace, monospace">{-# LANGUAGE MultiParamTypeClasses #-}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">{-# OPTIONS_GHC -Wall #-}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">-- Demonstrate a type checking failure with rewrite rules</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">module RuleFail where</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">class C k where comp' :: k b c -> k a b -> k a c</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">instance C (->) where comp' = (.)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">-- Late-inlining version to enable rewriting.</font></div><div><font face="monospace, monospace">comp :: C k => k b c -> k a b -> k a c</font></div><div><font face="monospace, monospace">comp = comp'</font></div><div><font face="monospace, monospace">{-# INLINE [0] comp #-}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">morph :: (a -> b) -> k a b</font></div><div><font face="monospace, monospace">morph = error "morph: undefined"</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">{-# RULES "morph/(.)" morph comp = comp #-}  -- Fine</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">class D k a where addC' :: k (a,a) a</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">instance Num a => D (->) a where addC' = uncurry (+)</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">-- Late-inlining version to enable rewriting.</font></div><div><font face="monospace, monospace">addC :: D k a => k (a,a) a</font></div><div><font face="monospace, monospace">addC = addC'</font></div><div><font face="monospace, monospace">{-# INLINE [0] addC #-}</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">{-# RULES "morph/addC" morph addC = addC #-}  -- Fail</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">-- • Could not deduce (D k b) arising from a use of ‘addC’</font></div><div><font face="monospace, monospace">--   from the context: D (->) b</font></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">-- Why does GHC infer the (C k) constraint for the first rule but not (D k b)</font></div><div><font face="monospace, monospace">-- for the second rule?</font></div></div><div><br></div></div>