Norman Ramsey wrote:
compile1 :: (Builder b box) => t -> Name -> Ir.ANF -> b t compile1 f x body = do env <- compile body empty wire (Arg W) (env x) return f class (Monad b) => Builder b box where wire :: Source box -> Sink box -> b () This program is rejected by GHC with the following message:
Ccomp.hs:54:23: Could not deduce (Builder b box1) from the context (Builder b box) arising from use of `wire' at Ccomp.hs:54:23-42
He continued, [paraphrase] however, compile1 is accepted if the signature is removed. Furthermore, the inferred signature seems identical to the one given above. That is not a bug. We observe that in the explicitly given signature of compile1
compile1 :: (Builder b box) => t -> Name -> Ir.ANF -> b t
the type variable 'box' occurs only in the constraint Builder. The use of `wire' in the body of compile1 entails the constraint `Builder b1 box1' (we alpha-renamed the type variables). Now, we know that the result of the wire is the monadic value 'b1 ()', and compile1, according to the signature, produces the monadic value 'b t. So, the typechecker concludes that b = b1. However, there is nothing in the code that lets the typechecker conclude that box1 is the same as box. Hence the error: the given constraint (Builder b box) differs from the required (Builder b box1). What to do? If applicable, add a functional dependency (either per class or per instance) so to tell the typechecker that a particular 'b' (always, or in some cases) entails the particular 'box'. That will provide the missing improvement equation `box = box1'. Or, one may use the local type variable to the same end
compile1 :: forall b t box. (Builder b box) => t -> Name -> Ir.ANF -> b t compile1 f x body = do env <- compile body empty wire ((Arg W)::Source box) (env x) return f
the explicit `forall' binder is required.