Type family doesn't reduce with visible kind application

If we un-comment f2

{-# 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

f2 :: F2 @a
f2 = undefined

Trac metadata

Trac field	Value
Version	8.6.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	mnguyen
Operating system
Architecture