Opened 4 months ago

Closed 2 months ago

#13780 closed bug (fixed)

Nightmarish pretty-printing of equality type in GHC 8.2 error message

Reported by: RyanGlScott Owned by: goldfire
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.2.1-rc2
Keywords: TypeInType Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case: dependent/should_fail/T13780a, dependent/should_fail/T13780c
Blocked By: Blocking:
Related Tickets: #13819 Differential Rev(s): Phab:D3794
Wiki Page:

Description

I originally spotted this in https://ghc.haskell.org/trac/ghc/ticket/12102#comment:1, 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.

Change History (8)

comment:1 Changed 4 months ago by RyanGlScott

Cc: simonpj added

This was caused by either commit 77bb09270c70455bbd547470c4e995707d19f37d ( Re-add FunTy (big patch)) or e368f3265b80aeb337fbac3f6a70ee54ab14edfd (Major patch to introduce TyConBinder). I can't know for sure since commit 77bb09270c70455bbd547470c4e995707d19f37d doesn't build properly.

comment:2 Changed 4 months ago by simonpj

Owner: set to goldfire

I think this is another piece of fallout from the horrible uo_thing mess. We are printing a Type in a place where we should printing a HsType.

Richard is planning it investigate and simplify. c.f. #13601, and RichardAndSimon

comment:3 Changed 3 months ago by RyanGlScott

Another occurrence of this bug:

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

data family Sing (a :: k)

data instance Sing (z :: Bool) =
    z ~ False => SFalse
  | z ~ True  => STrue
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind
import Foo

type family ElimBool (p :: Bool -> Type) (b :: Bool) (s :: Sing b)
                     (pFalse :: p False) (pTrue :: p True) :: p b where
  ElimBool _ _ SFalse pFalse _ = pFalse
  ElimBool _ _ STrue  _ pTrue  = pTrue

With GHC 8.0.2, you get this error:

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

Bug.hs:11:16: error:
    • Expected kind ‘Sing _’, but ‘'SFalse’ has kind ‘Sing 'False’
    • In the third argument of ‘ElimBool’, namely ‘SFalse’
      In the type family declaration for ‘ElimBool’

Bug.hs:12:16: error:
    • Expected kind ‘Sing _1’, but ‘'STrue’ has kind ‘Sing 'True’
    • In the third argument of ‘ElimBool’, namely ‘STrue’
      In the type family declaration for ‘ElimBool’

But with 8.2.1, you get this:

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

Bug.hs:11:16: error:
    • Expected kind ‘Sing _’,
        but ‘'SFalse
               ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind ‘Sing
                                                                          'False’
    • In the third argument of ‘ElimBool’, namely ‘SFalse’
      In the type family declaration for ‘ElimBool’
   |
11 |   ElimBool _ _ SFalse pFalse _ = pFalse
   |                ^^^^^^

Bug.hs:12:16: error:
    • Expected kind ‘Sing _1’,
        but ‘'STrue
               ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind ‘Sing
                                                                          'True’
    • In the third argument of ‘ElimBool’, namely ‘STrue’
      In the type family declaration for ‘ElimBool’
   |
12 |   ElimBool _ _ STrue  _ pTrue  = pTrue
   |                ^^^^^

comment:4 Changed 2 months ago by RyanGlScott

This appears to be fixed in GHC HEAD. I need to figure out which commit did the deed.

comment:5 Changed 2 months ago by RyanGlScott

These were fixed in c2417b87ff59c92fbfa8eceeff2a0d6152b11a47 (Fix #13819 by refactoring TypeEqOrigin.uo_thing). TODO Add regression tests.

comment:6 Changed 2 months ago by RyanGlScott

Differential Rev(s): Phab:D3794
Status: newpatch

comment:7 Changed 2 months ago by Ryan Scott <ryan.gl.scott@…>

In 424ecadb/ghc:

Add regression tests for #13601, #13780, #13877

Summary:
Some recent commits happened to fix other issues:

* c2417b87ff59c92fbfa8eceeff2a0d6152b11a47 fixed #13601 and #13780
* 8e15e3d370e9c253ae0dbb330e25b72cb00cdb76 fixed the original program in #13877

Let's add regression tests for each of these to ensure they stay fixed.

Test Plan: make test TEST="T13601 T13780a T13780c T13877"

Reviewers: goldfire, bgamari, austin

Reviewed By: bgamari

Subscribers: rwbarton, thomie

GHC Trac Issues: #13601, #13780, #13877

Differential Revision: https://phabricator.haskell.org/D3794

comment:8 Changed 2 months ago by RyanGlScott

Milestone: 8.4.1
Resolution: fixed
Status: patchclosed
Test Case: dependent/should_fail/T13780a, dependent/should_fail/T13780c
Note: See TracTickets for help on using tickets.