Opened 11 months ago

Last modified 5 months ago

#15872 new bug

Odd pretty printing of equality constraint in kind ('GHC.Types.Eq# <>)

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.2
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case: typecheck/should_fail/T12102
Blocked By: Blocking:
Related Tickets: #12102, #13933, #16263 Differential Rev(s): Phab:D5397
Wiki Page:

Description

Maybe indicative of deeper issues:

{-# Language RankNTypes #-}
{-# Language DataKinds  #-}
{-# Language PolyKinds  #-}
{-# Language GADTs      #-}

import Data.Kind

data WHICH = OP | OPOP

data Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where
  MkFun :: (a -> b) -> Fun a b

There are some artifacts Fun ('GHC.Type.Eq# <>) in the type of MkFun that shouldn't be there

$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci ~/hs/655_bug.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /home/baldur/hs/655_bug.hs, interpreted )
Ok, one module loaded.
*Main> :t MkFun
MkFun :: (a -> b) -> Fun ('GHC.Types.Eq# <>) a b
*Main> :k Fun
Fun :: (a ~ 'OP) => * -> * -> *
*Main>

Tangent: Omitting {-# Language GADTs #-} we get the term "equational constraint" which is not the term I have seen in the wild

$ latestbug 655_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 655_bug.hs, interpreted )

655_bug.hs:9:1: error:
    Illegal equational constraint a ~ 'OP
    (Use GADTs or TypeFamilies to permit this)
  |
9 | data Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Failed, no modules loaded.
Prelude>

Change History (10)

comment:1 Changed 11 months ago by goldfire

Keywords: TypeInType added

comment:2 Changed 11 months ago by RyanGlScott

See #13933 for another way to trigger the pretty-printing oddities uncovered here.

comment:3 Changed 11 months ago by RyanGlScott

I wonder if these ('GHC.Types.Eq# <>) coercion arguments should just be suppressed by default unless -fprint-explicit-coercions is enabled?

comment:4 Changed 10 months ago by RyanGlScott

In GHC HEAD (as of commit 2257a86daa72db382eb927df12a718669d5491f8), you get the following error when compiling the original program:

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

../Bug.hs:10:1: error:
    • Illegal constraint in a kind: forall (a :: WHICH).
                                    (a ~ 'OP) =>
                                    * -> * -> *
    • In the data type declaration for ‘Fun’
   |
10 | data Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Which would suggest that this issue is now moot.

comment:5 Changed 10 months ago by RyanGlScott

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

Phab:D5397 wraps things up by removing the outdated users' guide text about this feature, and adding a regression test.

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

In 73cce63f/ghc:

Fix #12102/#15872 by removing outdated users' guide prose

Summary:
In the beginning, #12102 (and #15872, which is of a similar
ilk) were caused by a poor, confused user trying to use code that
looks like this (with a constraint in the kind of a data type):

```lang=haskell
type family IsTypeLit a where
  IsTypeLit Nat    = 'True
  IsTypeLit Symbol = 'True
  IsTypeLit a      = 'False

data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
  MkNat    :: T 42
  MkSymbol :: T "Don't panic!"
```

Many bizarre GHC quirks (documented in those tickets) arose from
this sort of construction. Ultimately, the use of constraints in
data type kinds like this has made a lot of people very confused and
been widely regarded as a bad move.

Commit 2257a86daa72db382eb927df12a718669d5491f8 finally put this
feature out of its misery, so now the code above simply errors with
`Illegal constraint in a kind`. As a result, the aforementioned
tickets are moot, so this patch wraps a bow on the whole thing by:

1. Removing the (now outdated) section on constraints in data type
   kinds from the users' guide, and
2. Adding a test case to test this code path.

Test Plan: make test TEST=T12102

Reviewers: goldfire, simonpj, bgamari, tdammers

Reviewed By: tdammers

Subscribers: tdammers, rwbarton, carter

GHC Trac Issues: #12102, #15872

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

comment:7 Changed 10 months ago by RyanGlScott

Milestone: 8.8.1
Resolution: fixed
Status: patchclosed
Test Case: typecheck/should_fail/T12102

comment:8 Changed 7 months ago by RyanGlScott

Milestone: 8.8.1
Resolution: fixed
Status: closednew

Commit 6cce36f83aec33d33545e0ef2135894d22dff5ca (Add AnonArgFlag to FunTy) added back the ability to have equality constraints in kinds. Unfortunately, the issues in the original description persist:

GHCi, version 8.9.20190224: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :i MkFun
type role Fun nominal representational representational
data Fun (a1 :: a ~ 'OP) b c where
  MkFun :: b -> c -> Fun 'GHC.Types.Eq# <> b c
        -- Defined at Bug.hs:11:3
λ> :k Fun
Fun :: (a ~ 'OP) -> * -> * -> *

In fact, the situation is arguably worse now, since :k Fun reports the entirely bogus kind Fun :: (a ~ 'OP) -> * -> * -> *. (See also #12102.)

comment:9 Changed 7 months ago by RyanGlScott

comment:10 Changed 5 months ago by Ömer Sinan Ağacan <omeragacan@…>

In cc495d5/ghc:

Make equality constraints in kinds invisible

Issues #12102 and #15872 revealed something strange about the way GHC
handles equality constraints in kinds: it treats them as _visible_
arguments! This causes a litany of strange effects, from strange
error messages
(https://gitlab.haskell.org/ghc/ghc/issues/12102#note_169035)
to bizarre `Eq#`-related things leaking through to GHCi output, even
without any special flags enabled.

This patch is an attempt to contain some of this strangeness.
In particular:

* In `TcHsType.etaExpandAlgTyCon`, we propagate through the
  `AnonArgFlag`s of any `Anon` binders. Previously, we were always
  hard-coding them to `VisArg`, which meant that invisible binders
  (like those whose kinds were equality constraint) would mistakenly
  get flagged as visible.
* In `ToIface.toIfaceAppArgsX`, we previously assumed that the
  argument to a `FunTy` always corresponding to a `Required`
  argument. We now dispatch on the `FunTy`'s `AnonArgFlag` and map
  `VisArg` to `Required` and `InvisArg` to `Inferred`. As a
  consequence, the iface pretty-printer correctly recognizes that
  equality coercions are inferred arguments, and as a result,
  only displays them in `-fprint-explicit-kinds` is enabled.
* Speaking of iface pretty-printing, `Anon InvisArg` binders were
  previously being pretty-printed like `T (a :: b ~ c)`, as if they
  were required. This seemed inconsistent with other invisible
  arguments (that are printed like `T @{d}`), so I decided to switch
  this to `T @{a :: b ~ c}`.

Along the way, I also cleaned up a minor inaccuracy in the users'
guide section for constraints in kinds that was spotted in
https://gitlab.haskell.org/ghc/ghc/issues/12102#note_136220.

Fixes #12102 and #15872.
Note: See TracTickets for help on using tickets.