No reduction of "kind families"
Summary
If a type family application is in kind position, GHC doesn't seem to reduce it even if it's defined
Steps to reproduce
Try to compile this:
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
module Test where
type SubTagKind :: forall k . k -> *
type family SubTagKind tag
type SubTag :: forall tag -> SubTagKind tag
type family SubTag tag
type Tag :: *
data Tag
type instance SubTagKind Tag = *
type instance SubTag Tag = Tag
This gives:
Test.hs:18:28: error:
• Expected kind ‘SubTagKind Tag’, but ‘Tag’ has kind ‘*’
• In the type ‘Tag’
In the type instance declaration for ‘SubTag’
|
18 | type instance SubTag Tag = Tag
| ^^^
Expected behavior
This should typecheck, as SubTagKind Tag
is already defined to be *
Environment
- GHC version used: 8.10.7, 9.2.1