Opened 11 months ago
Last modified 11 months ago
#16139 new bug
GHC confused about type synonym kind with QuantifiedConstraints
Reported by: | Ashley Yakeley | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.6.3 |
Keywords: | QuantifiedConstraints | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #11621, #11715, #13742, #16148 | Differential Rev(s): | |
Wiki Page: |
Description
{-# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints #-} module Bug where import Data.Constraint type E (c :: * -> Constraint) = forall (a :: *). Eq a => c a
Bug.hs:5:58: error: • Expected a type, but ‘c a’ has kind ‘Constraint’ • In the type ‘forall (a :: *). Eq a => c a’ In the type declaration for ‘E’ | 5 | type E (c :: * -> Constraint) = forall (a :: *). Eq a => c a | ^^^
Note that GHC accepts the program when the Eq a
constraint is removed.
Change History (7)
comment:1 Changed 11 months ago by
comment:2 Changed 11 months ago by
You can work around this by annotating the result with a kind signature:
{-# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints #-} module Bug where import Data.Kind type E = (forall (a :: *). Eq a => Num a :: Constraint)
(FWIW, I am also confused as to why GHC doesn't just accept your definition as-is.)
comment:3 Changed 11 months ago by
Keywords: | QuantifiedConstraints added |
---|
comment:4 Changed 11 months ago by
This is more fall-out from the Constraint
vs Type
distinction. The kinding rules are
ty : TYPE rep `a` is not free in rep (FORALL1) ----------------------- forall a. ty : TYPE rep ty : Constraint (FORALL2) ------------------------- forall a. ty : Constraint
How do we know which of these rules to use? Currently we do it by looking at the "expected kind", using FORALL2
is the expected kind is Constraint
. That's why it works if you give a kind signature.
You could say "infer the kind of the body type, and use that to choose"; but that's vulnerable to exactly what constraints are solved when.
Or perhaps you could do both.
It's very uncomfortable having two different rules. I've often wondered about defining
type Constraint = TYPE ConstraintRep
in which case one rule would do. Richard thinks this won't work but I forget why.
comment:5 Changed 11 months ago by
See #16148, which I've created to gather these awkward type/constraint issues together.
comment:6 Changed 11 months ago by
Related Tickets: | → #11621, #11715, #13742, #16148 |
---|
comment:7 Changed 11 months ago by
type Constraint = TYPE ConstraintRep
won't work because levity-polymorphic functions would have an unknowable number of explicit arguments. Take something like absX :: forall (r :: RuntimeRep) (a :: TYPE r). NumX a => a -> a
. (This is possible if NumX
is levity polymorphic.) How many explicit arguments does absX
take? It depends on the choice of r
, because what looks like the one explicit argument becomes implicit if r
is ConstraintRep
. Even worse, this function would return a constraint, something we don't currently allow for normal functions.
What would work is type Constraint = TYPE LiftedRep YesIsConstraint
, where we index TYPE
by yet another flag. That's the most principled answer here, but it seems like using a sledgehammer to tap in a nail.
Simpler program that is also incorrectly rejected: