
#16116: Explicit foralls in associated type family equations are oblivious to class-bound variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): That's a good point. I think that check is a relic from commit 171101beca39befde191baff5027c417bcc709ee, which made an attempt to reject programs like this one: {{{#!hs instance C ('KProxy :: KProxy o) where type F 'KProxy = NatTr (Proxy :: o -> *) }}} Since `o` isn't //explicitly// bound on the left-hand side. However, we later reversed this policy in commit 0829821a6b886788a3ba6989e57e25a037bb6d05, where it was decided that it was OK to mention type variables on the RHSes of type family instances even if they're implicitly bound (i.e., we should accept `F 'KProxy` above). In light of this, I'd agree that `null bad_tvs` validity check serves no purpose. Removing it does make the program work again, (and validates, aside from some expected error message wibbles in `T5515`) which is an encouraging sign. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16116#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler