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 )
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 follow-up: 3 Changed 3 months ago by
Cc: | goldfire added |
---|
comment:2 Changed 3 months ago by
Description: | modified (diff) |
---|
comment:3 Changed 3 months 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 3 months 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 3 months 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 3 months 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 3 months 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 3 months ago by
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
Related Tickets: | → #13780 |
---|
comment:10 Changed 5 days 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.
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.