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

 Some thoughts, after discussion with my son Michael.

 * This entire problem arises only because of ''open'' type families; I
 think closed type families are fine.  We could simply ban the use of open
 type families in the kind signature of an open type family.  Or possibly
 all type families, I'm not sure.

 * Another idea: when we have a group of `type instance` decls, suppose we
 kind check them, but do not yet solve the kind equalities that arise; but
 add them to the instance environment anyway.  Now solve all the kind
 equalities.   In our example, we'd add both instances for `Open1` and
 `Open2` before trying to solve their kind equalities.  Seems a bit scary
 somehow.

 * Question: how do dependently typed languages deal with this?  For
 example, what if typechecking the defintion of a function `f` requires the
 type checker to evaluate calls to `f`?  In Haskell-land you could imagine
 {{{
 type family Id (a :: *) :: Id *
 }}}
   We reject this at the moment, but the idea is to get into a situation
 where, before having typechecked `f` we need to evaluate `f`.  That's
 rather like the situation with `Open1/2`.

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