Dependent type family does not reduce
When a type family is used in a kind of an argument for another type family, it does not reduce. Here's example code:
{-# 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)) = StringUnfortunately, I get these errors during typechecking:
[1 of 1] Compiling Main ( fieldtype.hs, fieldtype.o )
fieldtype.hs:19:27: error:
• Expected kind ‘Fin (FieldCount T)’,
but ‘'FZ’ has kind ‘Fin ('S n0)’
• In the second argument of ‘FieldType’, namely ‘FZ’
In the type instance declaration for ‘FieldType’
fieldtype.hs:20:28: error:
• Expected kind ‘Fin (FieldCount T)’,
but ‘'FS 'FZ’ has kind ‘Fin ('S ('S n0))’
• In the second argument of ‘FieldType’, namely ‘FS FZ’
In the type instance declaration for ‘FieldType’
fieldtype.hs:21:28: error:
• Expected kind ‘Fin (FieldCount T)’,
but ‘'FS ('FS 'FZ)’ has kind ‘Fin ('S ('S ('S n0)))’
• In the second argument of ‘FieldType’, namely ‘FS (FS FZ)’
In the type instance declaration for ‘FieldType’Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |