Explicit foralls in associated type family defaults are completely ignored?

While playing around with GHC HEAD recently, I noticed some rather bizarre behavior when trying to use explicit foralls 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 renamed:

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 ASSERTion 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 ASSERTion.)

My questions after seeing all of this are:

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

Trac metadata

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