Opened 3 years ago
Last modified 5 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 )
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 follow-up: 3 Changed 2 years ago by
Cc: | goldfire added |
---|
comment:2 Changed 2 years ago by
Description: | modified (diff) |
---|
comment:3 Changed 2 years ago by
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
comment:4 Changed 2 years ago by
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 2 years ago by
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 2 years ago by
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 2 years ago by
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 2 years ago by
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
Related Tickets: | → #13780 |
---|
comment:10 Changed 2 years ago by
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
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
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 10 months ago by
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 10 months ago by
Differential Rev(s): | → Phab:D5397 |
---|---|
Related Tickets: | #13780 → #13780, #15872 |
Status: | new → patch |
Phab:D5397 wraps things up by removing the outdated users' guide text about this feature, and adding a regression test.
comment:16 Changed 9 months ago by
Milestone: | → 8.8.1 |
---|---|
Resolution: | → fixed |
Status: | patch → closed |
Test Case: | → typecheck/should_fail/T12102 |
comment:17 Changed 7 months ago by
Milestone: | 8.8.1 |
---|---|
Resolution: | fixed |
Status: | closed → new |
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 7 months ago by
Related Tickets: | #13780, #15872 → #13780, #15872, #16263 |
---|
comment:19 Changed 7 months ago by
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 7 months ago by
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 follow-up: 22 Changed 7 months ago by
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; seeNote [Types for coercions, predicates, and evidence]
inTyCoRep
We should both make the user manual reflect this, and fix any bugs (which surely exist).
comment:22 Changed 7 months ago by
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.
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:...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 useT
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:If I'm reading this correctly, this would desugar into something like this, yes?
If so, shouldn't that require
DatatypeContexts
? Also if so, why on earth is something that requiresDatatypeContexts
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.