Data family with non-Type return kind, can't figure out type despite annotating
{-# Language KindSignatures, DataKinds, TypeFamilyDependencies, GADTs, TypeInType #-}
import Data.Kind
type family
ToNat (n::Type) = (res :: Type) | res -> n where
ToNat Type = Bool
ToNat (Type -> Type) = Maybe Bool
data family FN :: ToNat ty -> ty
data instance
FN :: Bool -> Type where
F :: FN False
T :: FN True
data instance
FN :: Maybe Bool -> (Type -> Type) where
A :: FN (Nothing :: Maybe Bool) a
B :: a -> FN (Just False) a
C :: a -> a -> FN (Just True) a
works on GHC 8.3.20170920, but removing the annotation from (Nothing :: Maybe Bool)
yields
GHCi, version 8.3.20170920: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/Z.hs, interpreted )
/tmp/Z.hs:19:22: error:
• Expected kind ‘ToNat (k0 -> *)’,
but ‘Nothing’ has kind ‘Maybe a0’
• In the first argument of ‘FN’, namely ‘Nothing’
In the type ‘FN Nothing a’
In the definition of data constructor ‘A’
|
19 | A :: FN Nothing a
| ^^^^^^^
Failed, 0 modules loaded.
Prelude>
even though FN
is annotated with the expected kind of Nothing
:
data FN :: Maybe Bool -> ... where
can also be fixed by annotating A :: FN Nothing (a::Type)
.
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | #12369 (closed) |
Blocking | |
CC | |
Operating system | |
Architecture |