[GHC] #12088: Type/data family instances in kind checking

[GHC]

#12088: Type/data family instances in kind checking
-------------------------------------+-------------------------------------
        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, #12239    |  Differential Rev(s):  Phab:D2272
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by int-index):

 Another example, where a newtype complicates things ever further. I tried
 adding TH sections to enforce an order in which type family instances are
 added but it didn't help:

 {{{
 {-# LANGUAGE TemplateHaskell, TypeInType, GADTs, TypeFamilies #-}
 {-# OPTIONS -Wno-unticked-promoted-constructors #-}

 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

 newtype Field (t :: Type) (i :: Fin (FieldCount t)) = Field (FieldType t
 i)

 return [] -- split TH section

 data L

 type instance FieldCount L = S Z

 return [] -- split TH section

 type instance FieldType L FZ = ()

 return [] -- split TH section

 -- newtype not involved, compiles.
 l_fz :: FieldType L FZ
 l_fz = ()

 -- newtype involvoed, doesn't compile.
 field_l_fz  :: Field L FZ
 field_l_fz = Field l_fz
 }}}

 The error I'm getting is:

 {{{
 field.hs:36:20: error:
     • Couldn't match type ‘FieldType L 'FZ’ with ‘()’
     • In the first argument of ‘Field’, namely ‘l_fz’
       In the expression: Field l_fz
       In an equation for ‘field_l_fz’: field_l_fz = Field l_fz
 }}}

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