[GHC] #12088: Promote data family instance constructors

[GHC]

#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