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

 Replying to [comment:14 simonpj]:
 > I don't really understand your suggestion Richard.
 >
 > Firstly, we often infer the kind of a data type, so it's hard to
 separate dependence on its kind from dependendence on its definition.  I
 din't undersand the precise dependency analysis that you informally
 propose.

 Yes, of course. But I think this is easily dispatched: if we are inferring
 the kind, then use this rule:

 * If a datatype's definition depends on the definition of `X`, then its
 type depends on the type of `X`.

 I haven't dwelt on this very long, but that seems to capture the nature of
 types that can be inferred.

 Here is something toward a specification of my idea:

 1. In a datatype definition for `T`:
    a. Let `X` be a tycon mentioned in `T`'s kind signature or in kind
 signatures of type variables to `T`. Then `T`'s type depends on `X`'s type
 and `T`'s definition depends on `X`'s definition.
    b. Let `K` be a datacon mentioned in `T`'s kind signature or in kind
 signatures of type variables to `T`. Let `S` be the tycon containing `K`.
 (`S` might be a data family ''instance'' tycon, too.) Then `T`'s type
 depends on the definition of `S`.
    c. Let `X` be a tycon mentioned in the type signature of a datacon in
 `T`. Then the definition of `T` depends on the type of `X`. In addition,
 if `T` does not have CUSK, then the type of `T` depends on the type of
 `X`.
    d. Let `K` be a datacon (belonging to tycon `S`) mentioned in the type
 signature of a datacon in `T`. Then the definition of `T` depends on the
 definition of `S`. In addition, if `T` does not have a CUSK, then the type
 of `T` depends on the type of `S`. (If `S` is a data family instance
 tycon, then this last sentence refers to the family for `S`, not the
 instance tycon, which has no type declaration to depend on.)

 2. In a closed type family definition for `C`:
     a. Let `X` be a tycon mentioned in any kind signature in the head of
 `C`. Then `C`'s type depends on `X`'s type and `C`'s definition depends on
 `X`'s definition.
     b. Let `K` be a datacon (belonging to tycon `S`) mentioned in any kind
 signature in the head of `C`. Then `C`'s type depends on `X`'s definition.
     c. Let `X` be a tycon mentioned in any equation for `C`. Then `C`'s
 definition depends on `X`'s type. In addition, if `C` does not have a
 CUSK, then `C`'s type depends on `X`s type.
     d. Let `K` be a datacon (belonging to tycon `S`) mentioned in any
 equation for `C`. Then `C`'s definition depends on `S`'s definition. In
 addition, if `C` does not have a CUSK, then `C`'s type depends on `S`'s
 type. (Or `S`'s family's type, as above.)

 3. In the declaration of an open type family `F`:
     a. Let `X` be a tycon mentioned in any kind signature in the
 declaration for `F`. Then `F`'s type depends on `X`'s type and `F`'s
 instance block depends on `X`'s definition.
     b. Let `K` be a datacon (belonging to tycon `S`) mentioned in the
 declaration for `F`. then `F`'s type depends on `S`'s type and `F`'s
 instance block depends on `S`'s definition.

 4. In a type family instance for `F`:
     a. Let `X` by a tycon mentioned in the instance. Then `F`'s instance
 block depends on `X`'s type.
     b. Let `K` be a datacon (belonging to tycon `S`) mentioned in the
 instance. Then `F`'s instance block depends on `S`'s definition.

 5. In the declaration of an open data family `D`:
     a. Let `X` be a tycon mentioned in any kind signature in the
 declaration for `D`. Then `D`'s type depends on `X`'s type.
     b. Let `K` be a datacon (belonging to tycon `S`) mentioned in the
 declaration for `D`. then `D`'s type depends on `S`'s type.

 6. In the declaration of a data instance: as for a regular datatype, where
 the kind signatures are inherited from the data family declaration.

 Left for another time: classes.

 Question raised: Data families always have a CUSK because a data family is
 always open. But might a data family instance ''not'' have a CUSK? What
 happens then? Perhaps we need to have CUSK analysis on data family
 instances, too.

 >
 > Secondly, I think that open type families are indeed the odd one out, as
 you acknowledge in the "odd conundrum".  I don't see what's gained by
 separating types from defns even if we could.

 We gain induction recursion, #11962. Even before this whole discussion, I
 had the general idea of this separation. See
 [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions
 this wiki page], written some time ago, on this idea.

 >
 > Thirdly, you suggest kind-checking all equations for a type family
 together as a single group.  But you can't do that if they mention data
 types that have not yet been defined.  Yet we can't delay too long ...
 getting those instances into play early is the whole point.

 It's true that my approach will sometimes fail when a finer-grained
 approach would succeed. But I don't think we're trying to get ''every''
 use case. We're trying to get a predictable approach that works just about
 all the time. Here is an example that would fail:

 {{{
 type family F a = r | r -> a
 data T :: F a -> Type where
   MkT :: T False
 type instance F Int = Bool
 type instance F Char = Proxy MkT
 }}}

 The definition of `T` depends on the first instance while the second
 instance depends on the definition of `T`. I'm not bothered rejecting
 this.

 >
 > Fourth, the dependence may be indirect.  In the example, Open2 mentions
 Open1 directly. But it could instead mention F directly, where F is an
 open family that has an equation like `type instance F [t] = Open1 t`.
 Now the dependence on Open1 is hidden.
 >

 Isn't this just transitivity? Depending on the "definition" of a type
 family means dependency on the block of instances -- all of them. So
 anything an instance depends on is transitively reachable.

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