#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