Opened 4 years ago

Last modified 7 months ago

#12102 new bug

“Constraints in kinds” illegal family application in instance (+ documentation issues?)

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T12102
Blocked By: Blocking:
Related Tickets: #13780, #15872, #16263 Differential Rev(s): Phab:D5397
Wiki Page:

Description (last modified by Iceland_jack)

GHC 8.0.0.20160511. Example from the user guide: Constraints in kinds

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!"

Deriving a standalone Show instance *without* the constraint (IsTypeLit a ~ 'True) => works fine

deriving instance Show (T a)

but I couldn't define a Show instance given the constraints:

-- • Couldn't match expected kind ‘'True’
--               with actual kind ‘IsTypeLit a0’
--   The type variable ‘a0’ is ambiguous
-- • In the first argument of ‘Show’, namely ‘T a’
--   In the stand-alone deriving instance for ‘Show (T a)’
deriving instance Show (T a)

let's add constraints

-- • Couldn't match expected kind ‘'True’
--               with actual kind ‘IsTypeLit lit’
-- • In the first argument of ‘Show’, namely ‘T (a :: lit)’
--   In the instance declaration for ‘Show (T (a :: lit))’
instance IsTypeLit lit ~ 'True => Show (T (a :: lit)) where

let's derive for a single literal

-- • Illegal type synonym family application in instance:
--     T Nat
--       ('Data.Type.Equality.C:~
--          Bool
--          (IsTypeLit Nat)
--          'True
--          ('GHC.Types.Eq# Bool Bool (IsTypeLit Nat) 'True <>))
--       42
-- • In the stand-alone deriving instance for ‘Show (T (42 :: Nat))’
deriving instance Show (T (42 :: Nat))

same happens with

instance Show (T 42) where

The documentation

Note that explicitly quantifying with forall a is not necessary here.

seems to be wrong since removing it results in

tVDv.hs:10:17-18: error: …
    • Expected kind ‘a’, but ‘42’ has kind ‘Nat’
    • In the first argument of ‘T’, namely ‘42’
      In the type ‘T 42’
      In the definition of data constructor ‘MkNat’
Compilation failed.

Change History (23)

comment:1 Changed 3 years ago by RyanGlScott

Cc: goldfire added

I agree that something is quite fishy is going on here—or perhaps several things? The further I dug into this, the more horrified I became. One thing I tried was seeing what GHCi thinks of this engimatic T type:

$ ghc/inplace/bin/ghc-stage2 --interactive Bug2.hs
GHCi, version 8.3.20170503: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug2.hs, interpreted )
Ok, modules loaded: Main.
λ> :i T
type role T nominal nominal
data T (b :: IsTypeLit a ~ 'True) (c :: a) where
  MkNat :: T ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>)) 42
  MkSymbol :: T ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))
                "Don't panic!"
        -- Defined at Bug2.hs:14:1

...Oh. Oh my goodness. I don't even know how one is supposed to possibly interpret that (perhaps this is related to #13407?).

Something that's particularly strange is that T is reported as having two type parameters, which is certainly not correct. This might help explain all of your attempts to use T were met with confusing errors.

Another thing that perplexes me is—should the definition of T as it's written in the original example even be accepted? We have:

data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where ...

If I'm reading this correctly, this would desugar into something like this, yes?

data (IsTypeLit a ~ 'True) => T (x :: a) = ...

If so, shouldn't that require DatatypeContexts? Also if so, why on earth is something that requires DatatypeContexts in the users' manual?

Perhaps this is my inexperience with this feature bleeding through. After all, I didn't even know "type constraints" were a thing until I stumbled upon this ticket.

comment:2 Changed 3 years ago by Iceland_jack

Description: modified (diff)

comment:3 in reply to:  1 Changed 3 years ago by Iceland_jack

Yeah this is something odd

Replying to RyanGlScott:

Perhaps this is my inexperience with this feature bleeding through. After all, I didn't even know "type constraints" were a thing until I stumbled upon this ticket.

Richard has a paper on Constrained Type Families, which as I understand it might express this with closed type classes

class TypeLit (a :: Type) where
  instance TypeLit Nat
  instance TypeLit Symbol

data T :: forall a. TypeLit a => a -> Type where
  MkNat    :: T 42
  MkSymbol :: T "Don't panic!"  

who knows

Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:4 Changed 3 years ago by Iceland_jack

I think I found a solution for this particular case, using TypeFamilyDependencies, if we make a restricted code

data Code = NAT | SYMBOL

with an injective interpretation

type family
  Interp (a :: Code) = (res :: Type) | res -> a where
  Interp NAT    = Nat
  Interp SYMBOL = Symbol

then you can write

data T :: forall a. Interp a -> Type where
  MkNat    :: T 42
  MkSymbol :: T "Don't panic!"

deriving instance Show (T a)
deriving instance Eq   (T a)
deriving instance Ord  (T a)
-- deriving instance Read (T a)

but using any of those methods causes the error in #13643 :) once that ticket is created

comment:5 Changed 3 years ago by simonpj

I didn't even know we allowed constraints in kinds. We certainly should not allow lifted equality constraints, like T :: forall k. (t1 ~ t2) => blah. Because (t1 ~ t2) is represented by lifted, heap-allocated, possibly-bottom value, and we don't have a case expression in types to unpack it.

Possibly we should allow unlifted equality T :: forall k. (t1 ~# t2) => blah. I'm not sure. But what you have is definitely wrong and should be rejected with a decent error message. (And the user manual should be fixed!)

Richard what do you think?

comment:6 Changed 3 years ago by goldfire

Good questions. Here are my thoughts:

  • Satisfying kind-level equality constraints is implemented in Inst.tcInstBinderX, called when a type is applied to some arguments. The code there handles both unboxed equality and boxed equality.
  • The "no case" problem in Simon's comment:5 is quite true. But this is OK, because such an equality constraint can never be a Given: constraints in types can't be used within the same type, but (I believe) these constraints scope only over a type (never a term).
  • This last point makes these new constraints somewhat like datatype contexts, but one does not desugar into the other.
  • Clearly, the output from :info is horrible.
  • The "no forall needed" is an interaction with CUSKs. This point should be clarified in the manual.
  • "Constrained type families" interacts poorly with today's story for kind families: constrained type families requires the use of class constraints, but class constraints aren't currently allowed in kinds. It would seem that it's best to implement constrained type families in the context of Dependent Haskell.
  • Bottom line: this feature is probably a misfire. It is marginally useful, as I think the example from the manual demonstrates. (That seems useful to me, at least.) But the implementation is very ad-hoc, and the fact that these constraints never appear as Givens take much of the air out of them. It would be easy enough to remove this feature for 8.2.

comment:7 Changed 3 years ago by simonpj

I'm still lost. Even if they are wanteds, that still means we are going to get term-level variables appearing in types, at the occurrences of T.

If you say we can get rid of them, let's get rid of them. Aasp!

comment:8 Changed 3 years ago by simonpj

If you say we can get rid of them, let's get rid of them. Aasp!

Richard agrees.

comment:9 Changed 2 years ago by RyanGlScott

BTW, I've opened #13780 to track the pretty-printing issue observed in comment:1.

comment:10 Changed 2 years ago by goldfire

I was just about to do this. But then I had second thoughts. Right now, we take it as a general rule that the following two declarations are the same:

data G1 a where
  MkG1 :: G1 Bool

data G2 a = (a ~ Bool) => MkG2

and indeed this is true today. But if we throw out ~ in kinds, as proposed here, then only 'MkG1 would be usable in a type. 'MkG2 would be an error, violating our general rule.

About Givens: GADT pattern-matching in terms must be very fancy, because the GADT pattern-match relates a runtime thing to a compile-time thing. Figuring out how to do this time travel required several PhDs to be earned. On the other hand, GADT pattern-matching in types need not be nearly so advanced, because everything is compile-time. Indeed, GHC's current implementation of type-level GADT pattern-matching is somewhat simplistic, not using Givens at all. (More below, as I'm sure you'll be curious.) So, even though a ~ in a kind never gives rise to a Given, they are still useful and can be matched against in a type family.

How type-level GADT pattern matching works: Let's look at an example.

type family F1 (a :: G k) :: k where
  F1 MkG1 = True

This would seem to require fancy GADT pattern matching. After all, we declare that the return kind be k for some unknown k, and yet we return True :: Bool. However, this really works by doing kind-matching. That is, the definition is elaborated to make its kind variables explicit:

type family F1 (k :: Type) (a :: G k) :: k where
  F1 Bool MkG1 = True

Because type families can pattern-match on kinds, this is hunky dory. The caller is responsible for showing that k is really Bool. This sounds terrible, though: what has happened to the expressiveness of GADTs? Nothing bad. Of course the caller can figure out what k should be, because it has the same information this function does. (This is very different in terms, where a GADT parameter is learned by a runtime pattern match. No phase distinction in type families!)

This trick has its limits, of course: you can't usefully use a constraint of the form F a ~ G a in a kind. I do want to fix that some day. But not today. And, in the meantime, it's unclear if I should fix this ticket and violate the general rule at the top of this comment.

comment:11 Changed 2 years ago by RyanGlScott

I'm confused then on what this ticket is about. Is the plan to keep this feature and fix the bugs reported in the original comment?

FWIW, I noticed that even after commit c2417b87ff59c92fbfa8eceeff2a0d6152b11a47, which fixed several ugly pretty-printer bugs that caused things like 'GHC.Types.Eq# to be printed, a similar pretty-printer bug in this ticket is still not fixed on GHC HEAD. For instance, this program:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

import Data.Kind
import GHC.TypeLits hiding (type (*))

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!"

instance Show (T 42) where

Still spits out 'GHC.Types.Eq#:

$ ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20170725: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:21:10: error:
    • Illegal type synonym family application in instance:
        T ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>)) 42
    • In the instance declaration for ‘Show (T 42)’
   |
21 | instance Show (T 42) where
   |          ^^^^^^^^^^^

comment:12 Changed 2 years ago by goldfire

I think we first need to decide on whether to keep the feature. Once that's settled, then we can look at the other issues (mostly pretty-printing) brought up here.

comment:13 Changed 12 months ago by RyanGlScott

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

$ inplace/bin/ghc-stage2 --interactive ../Bug.hs
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:15:1: error:
    • Illegal constraint in a kind: forall a.
                                    (IsTypeLit a ~ 'True) =>
                                    a -> *
    • In the data type declaration for ‘T’
   |
15 | data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Which would suggest that this issue is now moot.

comment:14 Changed 12 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:15 Changed 12 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:16 Changed 12 months ago by RyanGlScott

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

comment:17 Changed 9 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. Here's one example of the bizarre things that equality constraints in kinds cause:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
module T12102 where

import Data.Kind
import GHC.TypeLits

type family IsTypeLit a where
  IsTypeLit Nat    = 'True
  IsTypeLit Symbol = 'True
  IsTypeLit a      = 'False

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

deriving instance Show (T a)
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling T12102           ( Bug.hs, Bug.o )

Bug.hs:21:25: error:
    • Expecting one more argument to ‘T a’
      Expected a type, but ‘T a’ has kind ‘a0 -> *’
    • In the first argument of ‘Show’, namely ‘(T a)’
      In the stand-alone deriving instance for ‘Show (T a)’
   |
21 | deriving instance Show (T a)
   |                         ^^^

Bug.hs:21:27: error:
    • Couldn't match kind ‘*’ with ‘Constraint’
      When matching kinds
        k0 :: *
        IsTypeLit a0 ~ 'True :: Constraint
      Expected kind ‘IsTypeLit a0 ~ 'True’, but ‘a’ has kind ‘k0’
    • In the first argument of ‘T’, namely ‘a’
      In the first argument of ‘Show’, namely ‘(T a)’
      In the stand-alone deriving instance for ‘Show (T a)’
   |
21 | deriving instance Show (T a)
   |                           ^

Huh? Why is GHC claiming that T a has kind a0 -> *? Well, if you ask GHCi:

λ> :k T
T :: (IsTypeLit a ~ 'True) -> a -> *

Yikes. Something is clearly wrong here.

comment:18 Changed 9 months ago by RyanGlScott

comment:19 Changed 9 months ago by simonpj

Ryan, there's now an extensive comment in Note [Constraints in kinds] in TyCoRep that describes what is supposed to happen for equality constraints in kinds.

In the light of that description, could you spare the time to look into this ticket and #15872 to see what needs doing? I think we may need to look at the user manual too.

comment:20 Changed 9 months ago by RyanGlScott

I don't think we're on the same page here. This ticket and #15872 demonstrate that constraints in kinds are horribly broken, and that there's no way to profitably use them. I would think that we should fix GHC's treatment of constraints in kinds before we document how they work in the users' manual.

Unfortunately, fixing that is far beyond my technical expertise.

comment:21 Changed 9 months ago by simonpj

Hang on. The Note explains that

  • equality constraints (~) and (~~) should be fine;
  • other constraints like Eq a should be illegal;
  • (~#) isn't a constraint at all; see Note [Types for coercions, predicates, and evidence] in TyCoRep

We should both make the user manual reflect this, and fix any bugs (which surely exist).

comment:22 in reply to:  21 Changed 9 months ago by RyanGlScott

Replying to simonpj:

We should both make the user manual reflect this, and fix any bugs (which surely exist).

I'm just pointing out that "make the user manual reflect this" and "fix any bugs" are two actions which require very different sets of abilities. I might be able to do the former, but definitely not the latter. Given that, perhaps we should wait until someone with the competency to fix the latter comes along, and then we can update the users' manual at the same time.

comment:23 Changed 7 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.