Inexplicable error message when using out-of-scope type variable in pattern type signature

This code gives an error on any version of GHC since 7.6:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

data family Sing (a :: k)

data instance Sing (z :: [a]) where
  SNil  :: Sing '[]
  SCons :: Sing x -> Sing xs -> Sing (x ': xs)

fl :: forall (l :: [a]). Sing l -> Sing l
fl (SNil :: Sing (l :: [y])) = SNil
fl (SCons x xs)              = SCons x xs

$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:16:5: error:
    • The type variable ‘y’
      should be bound by the pattern signature ‘Sing l’
      but are actually discarded by a type synonym
      To fix this, expand the type synonym
      [Note: I hope to lift this restriction in due course]
    • In the pattern: SNil :: Sing (l :: [y])
      In an equation for ‘fl’: fl (SNil :: Sing (l :: [y])) = SNil
   |
16 | fl (SNil :: Sing (l :: [y])) = SNil
   |     ^^^^^^^^^^^^^^^^^^^^^^^

I can't wrap my head around the error message, though. It complains about a type synonym discarding y, but there are no type variables in this program! The //real// source of the issue, the fact that y is out of scope (and should actually be a), is obscured.

Trac metadata

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