
#12088: Promote data family instance constructors -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #11348 | Differential Rev(s): Phab:D2272 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: goldfire (added) Comment: Sorry to be slow... I'm on holiday. You give a great example. The key point is that to ''kind-check'' the `data instance F Q r` declaration, we need to have completely processed the `type instance Open Q` declaration. So even instance declarations can have dependencies! I'd like Richard E's opinion on all this; hence cc'ing goldfire. To me your example raises the question of whether it's even ''possible'' to figure out the dependencies. You probably believe that your "add extra edges" does so. But I still don't know exactly what those edges are. Maybe you could take a comment in this ticket to explain your algorithm precisely? Meanwhile, here's a new hypothesis. The only instances we must have in hand to do kind-checking are `type instance`s, because they give rise to implicit nominal type/kind equalities (e.g. `F Int ~ Bool`) that the kind checker must solve. But `data instance`s are different: they do not give rise to implicit nominal type/kind equalities. So in that way they behave more like data type declarations. Indeed, I think that the only way that type/class declaration T can depend on a `data instance` declaration D is if T mentions one of D's promoted data constructors. This will be sorted out by the ordinary SCC analysis. So perhaps this small modification to my algorithm will work: in the step "Partition the `InstDecl` nodes from the `TyClDecl` nodes", instead partition the `type instance` decls from the `TyClDecl` and `data instance` decls. Then your example will work just fine, because the `type instance Open Q` will be dealt with as soon as `data Q` is done. The worry in my mind is whether you could have two `type instance` declarations, D1 and D2, where it was essential to process D1 before D2, or vice versa. I can't come up with an example, but neither can I see how to prove that there is no such example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12088#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler