
#9063: Default associated type instances are too general -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I agree with most of Simon's analysis. The "not OK" instances are definitely not OK, and should be rejected. But, my case is subtly different, in that I'm not asking for magic, just kind-checking. What makes my case different is that the class parameter is a kind variable. Here is how I want GHC to reason, in the example in my original report: - The type family declaration introduces the identifier `(:==)`, with kind `a -> a -> Bool`, where `a` is the class (kind) variable. - When kind-checking the default instance, we kind-check with expected kind `a` for `x` and expected kind `a` for `y`. - The kind-checked, desugared LHS of the default instance indeed does mention a class variable `a`, in exactly the right spot. - Definition accepted. In the instance case, a similar analysis works out: we kind-check the instance for `(:==)` using the instantiated kind (`() -> () -> Bool` in the second instance in my comment above), and everything works out. I ''do'' see the counterargument here, that it seems I'm asking for magic. But, I respectfully disagree with that stance. And, it would seem that the implementation here would be rather straightforward and I'm happy to do it. Regardless of the outcome, we should probably flesh out that manual entry. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9063#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler