[GHC] #14457: Data family with non-Type return kind, can't figure out type despite annotating
#14457: Data family with non-Type return kind, can't figure out type despite annotating -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #12369 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# 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`: {{{#!hs data FN :: Maybe Bool -> ... where }}} can also be fixed by annotating `A :: FN Nothing (a::Type)`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14457 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14457: Data family with non-Type return kind, can't figure out type despite annotating -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12369, #14111 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => duplicate * related: #12369 => #12369, #14111 Comment: This is a duplicate of #14111, so I'll close this ticket in favor of that one. The issue actually has nothing to do with the return kind. We can see this in this stripped-down version of your example: {{{#!hs {-# 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 (a :: k) (b :: Type) :: Type data instance FN (a :: Maybe Bool) (b :: Type) :: Type where A :: FN Nothing a }}} {{{ $ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:14:3: error: • Data constructor ‘A’ returns type ‘FN 'Nothing a1’ instead of an instance of its parent type ‘FN a b’ • In the definition of data constructor ‘A’ In the data instance declaration for ‘FN’ | 14 | A :: FN Nothing a | ^ }}} In principle, there should be enough types here that GHC can figure out what to do, but unfortunately that's not the case at the moment (due to #14111). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14457#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC