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 |