Re: GHC rewrite rule type-checking failure

2017-10-02 Thread David Feuer
I believe the answer is currently no. As I understand it, the entire instance resolution mechanism drops away after type checking and is therefore not available to the simplifier. So if you need to add a constraint on the RHS of a rule, I think you're mostly out of luck. The only thing I can think

Re: GHC rewrite rule type-checking failure

2017-10-02 Thread Conal Elliott
Thanks very much for the reply, Joachim. Oops! I flubbed the example. I really `morph` to distribute over an application of `comp`. New code below (and attached). You're right that I wouldn't want to restrict the type of `morph`, since each `morph` *rule* imposes its own restrictions. My question

Re: GHC rewrite rule type-checking failure

2017-10-02 Thread 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

GHC rewrite rule type-checking failure

2017-10-02 Thread 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