Visible kind application defeats type family with higher-rank result kind
After #15740 (closed), GHC now (correctly) rejects this program:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Kind
data SBool :: Bool -> Type
type family F :: forall k. k -> Type where
F = SBool
$ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.7.20190115: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:12:7: error:
• Expected kind ‘forall k. k -> *’,
but ‘SBool’ has kind ‘Bool -> *’
• In the type ‘SBool’
In the type family declaration for ‘F’
|
12 | F = SBool
| ^^^^^
However, there's a very simple way to circumvent this: add a visible kind application to F
's equation.
type family F :: forall k. k -> Type where
F @Bool = SBool
If I understand things correctly, GHC shouldn't allow this.
Trac metadata
Trac field | Value |
---|---|
Version | 8.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |