[GHC] #12088: Promote type/data family instance constructors (was: Promote data family instance constructors)

[GHC]

#12088: Promote type/data family instance constructors
-------------------------------------+-------------------------------------
        Reporter:  alexvieth         |                Owner:
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.1
       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 int-index):

 * priority:  normal => high
 * type:  feature request => bug
 * milestone:   => 8.2.1


Comment:

 So it turns out that https://ghc.haskell.org/trac/ghc/ticket/12239 is a
 manifestation of the same issue. Copying the example from it for
 completeness:

 {{{
 {-# LANGUAGE TypeInType, GADTs, TypeFamilies #-}

 import Data.Kind (Type)

 data N = Z | S N

 data Fin :: N -> Type where
   FZ :: Fin (S n)
   FS :: Fin n -> Fin (S n)

 type family FieldCount (t :: Type) :: N

 type family FieldType (t :: Type) (i :: Fin (FieldCount t)) :: Type

 data T

 type instance FieldCount T = S (S (S Z))

 type instance FieldType T FZ = Int
 type instance FieldType T (FS FZ) = Bool
 type instance FieldType T (FS (FS FZ)) = String
 }}}

 Reordering the declarations slightly makes it compile:

 {{{

 {-# LANGUAGE TypeInType, GADTs, TypeFamilies #-}

 import Data.Kind (Type)

 data N = Z | S N

 data Fin :: N -> Type where
   FZ :: Fin (S n)
   FS :: Fin n -> Fin (S n)

 type family FieldType (t :: Type) (i :: Fin (FieldCount t)) :: Type

 data T

 -- Note that 'FieldCount' is now declared after 'FieldType' and 'T'.
 type family FieldCount (t :: Type) :: N

 type instance FieldCount T = S (S (S Z))

 type instance FieldType T FZ = Int
 type instance FieldType T (FS FZ) = Bool
 type instance FieldType T (FS (FS FZ)) = String

 }}}

 Hope it helps.

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