[GHC] #16110: Explicit foralls in associated type family defaults are completely ignored?

[GHC]

#16110: Explicit foralls in associated type family defaults are completely ignored?
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.7
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC accepts
  Unknown/Multiple                   |  invalid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 While playing around with GHC HEAD recently, I noticed some rather bizarre
 behavior when trying to use explicit `forall`s with associated type family
 defaults. Let's pop open GHCi and recreate it:

 {{{
 $ inplace/bin/ghc-stage2 --interactive -XTypeFamilies
 -XScopedTypeVariables
 GHCi, version 8.7.20181215: https://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 λ> class C a where { type T a b; type forall b. T a b = Either a b }
 }}}

 OK, so far, so good. Now let's see what happens when I omit the `b`:

 {{{
 λ> class C a where { type T a b; type forall. T a b = Either a b }
 }}}

 That... works? Wow, I wouldn't have expected that... But it gets even
 worse—I can type in utter nonsense, and GHCi will accept it:

 {{{
 λ> class C a where { type T a b; type forall dup dup dup. T a b = Either a
 b }
 λ> class C a where { type T a b; type forall (a :: a). T a b = Either a b
 }
 λ> class C a where { type T a b; type forall (a :: k) k. T a b = Either a
 b }
 }}}

 How could this possibly happen? After looking at the source code to see
 how associated type family defaults are renamed, it becomes clear why this
 is the case. Here is how they are
 [http://git.haskell.org/ghc.git/blob/ef57272e28f5047599249ae457609a079d8aebef:/compiler/rename/RnSource.hs#l841
 renamed]:

 {{{#!hs
 rnTyFamDefltEqn cls (FamEqn { ...
                             , feqn_bndrs  = bndrs
                             , ... })
   = do { ...
        ; return (FamEqn { ...
                         , feqn_bndrs  = ASSERT( isNothing bndrs )
                                         Nothing
                         , ... }, ...) }
 }}}

 Not only are the type variable binders ignored, there's actually an
 `ASSERT`ion in place which assumes that there will be no binders
 whatsoever! (I haven't checked, but I suspect the code above will trigger
 a failure on that `ASSERT`ion.)

 My questions after seeing all of this are:

 * Should we be accepting explicit `forall`s in associated type family
 defaults at all?
 * If so, should we remove this strange invariant that the binders will
 always be `Nothing`?

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