[GHC] #15793: Type family doesn't reduce with visible kind application

[GHC]

#15793: Type family doesn't reduce with visible kind application
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications                   |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 If we un-comment `f2`

 {{{#!hs
 {-# Language RankNTypes       #-}
 {-# Language TypeFamilies     #-}
 {-# Language TypeApplications #-}
 {-# Language PolyKinds        #-}

 import Data.Kind

 type family
   F1 (a :: Type) :: Type where
   F1 a = Maybe a

 f1 :: F1 a
 f1 = Nothing

 type family
   F2 :: forall (a :: Type). Type where
   F2 @a = Maybe a

 -- f2 :: F2 @a
 -- f2 = Nothing
 }}}

 this program fails with

 {{{
        • Couldn't match kind ‘forall a1. *’ with ‘* -> *’
          When matching types
            F2 :: forall a. *
            Maybe :: * -> *
          Expected type: F2
            Actual type: Maybe a
        • In the expression: Nothing
          In an equation for ‘f2’: f2 = Nothing
       |
    20 | f2 = Nothing
       |      ^^^^^^^
    Failed, no modules loaded.
 }}}

 It also succeeds replacing `Nothing` with `undefined`

 {{{#!hs
 f2 :: F2 @a
 f2 = undefined
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15793>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler