#12564: Type family in type pattern kind -------------------------------------+------------------------------------- Reporter: int-index | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: 14119 | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): * Bizarrely, I don't think we need to do much proving. The type safety proof depends on the non-overlap of axiom LHSs. That's unchanged here -- the overlap check must treat any type family application on an LHS just like it would a variable. The equality constraints serve only to reduce the applicability of axioms, never to increase it. Thus, no threats to safety. * But the evidence ''is'' used: it's passed to the coercion axiom. The evidence is the `coLen` in my example above. * I take back the "evidence may be mentioned" comment. * GHC passes loads of redundant information at every call site (e.g. `id @Bool True`). This is not new. The uniquely-determined check would help those other places too. I think, in the end, that idea is orthogonal to the plan here, which would work for `F x (G x) = True`, should we ever want to support that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12564#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler