[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:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I have a very different way of thinking about all of this that may shed
 some light on the matter.

 (Before we get any further, if you'd like my input, do email directly.
 It's only dumb luck that I happened to catch up on this ticket so soon
 after requesting my feedback.)

 Most declarations declare actually ''two'' things: a type and a
 definition. For `data T = MkT Int`, we have the type `T :: Type` and the
 definition, consisting of `MkT`. For `type family F a where F Bool = Int`,
 we get the type `F :: Type -> Type` and the definition `F Bool = Int`.

 What's odd about open families is that the type and definition are
 separated, quite clearly in the code. But when we think about the fact
 that closed definitions are declaring two things at once, perhaps it's the
 ''closed'' definitions that are odd and the open ones are more natural.
 (Indeed, at the term level, we make the type and body separate top-level
 declarations.)

 So, perhaps that's the answer: treat closed declarations as two separate
 pieces, each with its own node in the dependency graph. Now, any
 declaration (where "declaration" means either a type declaration or a
 definition declaration, but not both wrapped together) can depend on any
 other (also separated) declarations.

 (Let's hold off a moment on worrying about how to implement this. I'll get
 to that later. The goal here is simply to describe what programs are
 accepted.)

 Let's review the examples from above:

 ------------------------------------

 '''From the original description:'''

 {{{
 data family T a
 data instance T Int = MkT
 data Proxy (a :: k)
 data S = MkS (Proxy 'MkT)
 }}}

 Here are the dependencies, where I list a declaration and the things it
 depends on (not using transitivity):
 * `T` (type only): nothing
 * `T Int` (defn only): type of `T`
 * type of `Proxy`: nothing
 * defn of `Proxy`: type of `Proxy`
 * type of `S`: nothing
 * defn of `S`: type of `MkT` (= defn of `T Int`)

 In the last bullet, we see that the type of a data constructor is
 considered in the same declaration as the definition of the parent tycon.
 The definition of a constructor is also in this same declaration. (This
 suggests further opportunities for splitting, though. Could one
 constructor mention another constructor, promoted, from the same type? I
 think so.)

 These bullets also show that all definitions automatically depend on their
 own types. No surprise there.

 --------------------------------------
 '''From comment:10:'''

 {{{
 -- module A

 type family Open (t :: Type) :: Type

 data family F (t :: Type) :: Open t -> Type
 }}}

 {{{
 -- module B
 import A

 data Q

 type instance Open Q = Bool

 data instance F Q r where
   F0 :: F Q 'True
 }}}

 * `Open` (type only): nothing
 * `F` (type only): type of `Open`
 * type of `Q`: nothing
 * defn of `Q`: type of `Q`
 * `Open Q` (defn only): type of `Open`, type of `Q`
 * `F Q r` (defn only): type of `F`, type of `Q`, defn of `Open`

 The last bullet above reveals something new: when the type of `A` depends
 on the type of `B`, then the definition of `A` depends on the definition
 of `B`. In this case, the type of `F` depends on the type of `Open`, and
 thus the definition of `F` (that is, `instance F Q r`) depends on the
 definition of `Open`.

 We now have a small conundrum: what on earth is the definition of `Open`,
 an open type family? The only possible answer: all instances that are in
 scope. These instances are considered as an inseparable clump. Any attempt
 to break them up by bizarre mutual dependencies is met with failure. I do
 think there is room to be cleverer here, but I think we'd be too clever by
 half if we tried.

 In this example, it means that we check the `Open Q` instance before the
 `F Q r` instance.

 --------------------------------------------
 '''Also from comment:10:'''

 {{{
 -- module A2

 type family Open1 (t :: Type) :: Type

 type family Open2 (t :: Type) (q :: Open1 t) :: Type
 }}}

 {{{
 -- module B2
 import A2

 type instance Open1 () = Bool
 type instance Open2 () 'True = Char
 }}}

 * `Open1` (type only): nothing
 * `Open2` (type only): type of `Open1`
 * `Open1 ()` (defn only): type of `Open1`
 * `Open2 ()` (defn only): type of `Open2`, defn of `Open1`

 It's now clear that we must check the instance for `Open1` before that of
 `Open2`. No difficulty here.

 -------------------------------------------
 '''From comment:11:'''

 {{{
 data T1 = MkT1 (...something requiring IA...)
 data T2 = MkT2 (...something requiring IB...)
 type instance F1 Int = ...T2...    -- IA
 type instance F2 Int = ...T1...    -- IB
 }}}

 * type of `T1`: nothing
 * defn of `T1`: defn of `F1`
 * type of `T2`: nothing
 * defn of `T2`: defn of `F2`
 * `F1 Int` (defn only): type of `F1`, type of `T2`
 * `F2 Int` (defn only): type of `F2`, type of `T1`

 No problem here either. Go in this order: type of `T1`, type of `T2`, type
 of `F1`, type of `F2`, `F1 Int`, `F2 Int`, defn of `T1`, defn of `T2`.

 The reason there is no problem is that we have separated types from
 definitions.

 ----------------------------------------------
 '''Reactions to comment:12:'''

 * It's hard to bad open type families from appearing somewhere, because
 we'd have to make the ban transitive. We'd thus have two classes of closed
 type families: those that mention open families somewhere (transitively)
 and those that don't. This would be awful.

 * Your "another idea" might be something like what I've proposed here.

 * In answer to your "question": I think only Agda handles this. It's
 induction recursion. And I think it's rather like what I've sketched here.

 -----------------------------------------------
 '''Implementation notes'''

 Checking types and definitions separately is a bit of a bother for
 datatypes, because the datacons and the tycons mutually depend on each
 other. But I think it's possible -- just a little knotty. Let's assume
 that the dependency analysis succeeds and that there is a dependency
 ordering with no (perhaps transitive) self-dependency.

 1. At the beginning of the "type-checking" (ahem, desugaring) pass in
 !TcTyClsDecls, go through the declarations in reverse order and create a
 knot for each definition (with the list of datacons knot-tied) and each
 type (with the tycon knot-tied).

 2. Then check the declarations in order.

    a. When a type declaration is processed, close out the tycon's knot.
 You will now have a tycon usable in every way except to access its
 datacons.

    b. When a definition declaration is processed, close out its knot. The
 datacons will now be untied and usable.

 '''Proposition.''' If the dependency analysis is correct, the above
 algorithm accesses nothing that is knot-tied.

 I propose naming this algorithm the "Celestial Dance of the Black Holes".
 It's as dangerous as it sounds. But I believe it's implementable. Perhaps
 not by humans. :)

 The alternative to the Celestial Dance is to create intermediate
 structures with mutable references and such and then zonk them to get the
 desired outcome. The zonker will have to be creative about knot-tying, but
 that's much simpler. Indeed this may be the better approach, perhaps
 leaning more heavily on the rather new `TcTyCon` than we have been.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12088#comment:13>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler