Opened 8 months ago

Last modified 8 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 8 months ago by Ashley Yakeley

Simpler program that is also incorrectly rejected:

{-# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints #-}
module Bug where
import Data.Constraint

type E = forall (a :: *). Eq a => Num a

comment:2 Changed 8 months ago by RyanGlScott

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 8 months ago by RyanGlScott

Keywords: QuantifiedConstraints added

comment:4 Changed 8 months ago by simonpj

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 8 months ago by simonpj

See #16148, which I've created to gather these awkward type/constraint issues together.

comment:6 Changed 8 months ago by RyanGlScott

comment:7 Changed 8 months ago by goldfire

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.

Note: See TracTickets for help on using tickets.