[GHC] #14457: Data family with non-Type return kind, can't figure out type despite annotating

[GHC]

#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