[GHC] #16356: Unexpected type application in default declaration

[GHC]

#16356: Unexpected type application in default declaration
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.6.3
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 The
 [https://downloads.haskell.org/~ghc/8.6.3/docs/html/users_guide/glasgow_exts.html
 #associated-type-synonym-defaults users' guide section] on associated type
 family defaults is probably the closest thing to a specification of how
 they must be structured:

 > Note the following points:
 >
 > * The `instance` keyword is optional.
 > * There can be at most one default declaration for an associated type
 synonym.
 > * A default declaration is not permitted for an associated //data//
 type.
 > * The default declaration must mention only type //variables// on the
 left hand side, and the right hand side must mention only type variables
 that are explicitly bound on the left hand side. This restriction is
 relaxed for //kind variables//, however, as the right hand side is allowed
 to mention kind variables that are implicitly bound on the left hand side.
 > * Unlike the associated type family declaration itself, the type
 variables of the default instance are independent of those of the parent
 class.
 >
 > Here are some examples:
 >
 > {{{
 > class C (a :: Type) where
 >   type F1 a :: Type
 >   type instance F1 a = [a]     -- OK
 >   type instance F1 a = a->a    -- BAD; only one default instance is
 allowed
 >
 >   type F2 b a                  -- OK; note the family has more type
 >                                --     variables than the class
 >   type instance F2 c d = c->d  -- OK; you don't have to use 'a' in the
 type instance
 >
 >   type F3 a
 >   type F3 [b] = b              -- BAD; only type variables allowed on
 the LHS
 >
 >   type F4 a
 >   type F4 b = a                -- BAD; 'a' is not in scope  in the RHS
 >
 >   type F5 a :: [k]
 >   type F5 a = ('[] :: [x])     -- OK; the kind variable x is implicitly
 >                                       bound by an invisible kind pattern
 >                                       on the LHS
 >
 >   type F6 a
 >   type F6 a =
 >     Proxy ('[] :: [x])         -- BAD; the kind variable x is not bound,
 >                                        even by an invisible kind pattern
 >
 >   type F7 (x :: a) :: [a]
 >   type F7 x = ('[] :: [a])     -- OK; the kind variable a is implicitly
 >                                       bound by the kind signature of the
 >                                       LHS type pattern
 > }}}

 Unless I'm missing something, I don't see anything in here which would
 explicitly forbid `type FAssocDefault @k = B @k`. I'm inclined to support
 allowing it.

 In fact, the only reason GHC disallows it at the moment it due to a
 [https://gitlab.haskell.org/ghc/ghc/blob/04b7f4c1c6ea910ab378f27c5f9efd6c88f65425/compiler/parser/RdrHsSyn.hs#L836-841
 validity check] in in `RdrHsSyn.checkTyVars`. It might be interesting to
 see what happens if you remove that validity check. Well, to be more
 precise, if you remove that validity check for associated type family
 defaults—we can't just remove the check entirely, since `checkTyVars` is
 also used to check the type variable binders for classes, data types, type
 synonyms, and type family declarations, where we currently disallow
 visible kind applications (#15782).

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