GitLab

I originally spotted this in #12102 (closed)##13780 (closed), but I happened to stumble upon it again recently in a separate context, so I though it deserved its own ticket. Here's some code which does not typecheck:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Foo where

data family Sing (a :: k)

data Foo a = a ~ Bool => MkFoo
data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo

In GHC 8.0.1 and 8.0.2, the error message you'd get from this program was reasonable enough:

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

Bug.hs:9:40: error:
    • Expected kind ‘Foo a’, but ‘'MkFoo’ has kind ‘Foo Bool’
    • In the second argument of ‘~’, namely ‘MkFoo’
      In the definition of data constructor ‘SMkFoo’
      In the data instance declaration for ‘Sing’

But in GHC 8.2.1 and HEAD, it's hair-raisingly bad:

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

Bug.hs:9:40: error:
    • Expected kind ‘Foo a’,
        but ‘'MkFoo
               ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind ‘Foo Bool’
    • In the second argument of ‘~’, namely ‘MkFoo’
      In the definition of data constructor ‘SMkFoo’
      In the data instance declaration for ‘Sing’
  |
9 | data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
  |                                        ^^^^^

• *WAT.**

Trac metadata

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