[GHC] #13881: Inexplicable error message when using out-of-scope type variable in pattern type signature

[GHC]

#13881: Inexplicable error message when using out-of-scope type variable in pattern
type signature
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Poor/confusing
  Unknown/Multiple                   |  error message
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This code gives an error on any version of GHC since 7.6:

 {{{#!hs
 {-# 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.

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