Opened 14 months ago

Last modified 5 days 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:
Blocked By: Blocking:
Related Tickets: #13780 Differential Rev(s):
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 (10)

comment:1 Changed 3 months 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 months ago by Iceland_jack

Description: modified (diff)

comment:3 in reply to:  1 Changed 3 months 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 months ago by Iceland_jack (previous) (diff)

comment:4 Changed 3 months 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 months 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 months 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 months 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 months ago by simonpj

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

Richard agrees.

comment:9 Changed 7 weeks ago by RyanGlScott

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

comment:10 Changed 5 days 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.

Note: See TracTickets for help on using tickets.