[GHC] #16139: GHC confused about type synonym kind with QuantifiedConstraints
#16139: GHC confused about type synonym kind with QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Ashley | Owner: (none) Yakeley | Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16139 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16139: GHC confused about type synonym kind with QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ashley Yakeley): Simpler program that is also incorrectly rejected: {{{#!hs {-# LANGUAGE KindSignatures, RankNTypes, ConstraintKinds, QuantifiedConstraints #-} module Bug where import Data.Constraint type E = forall (a :: *). Eq a => Num a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16139#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16139: GHC confused about type synonym kind with QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): You can work around this by annotating the result with a kind signature: {{{#!hs {-# 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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16139#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16139: GHC confused about type synonym kind with QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => QuantifiedConstraints -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16139#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16139: GHC confused about type synonym kind with QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16139#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16139: GHC confused about type synonym kind with QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): See #16148, which I've created to gather these awkward type/constraint issues together. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16139#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16139: GHC confused about type synonym kind with QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #11621, #11715, | Differential Rev(s): #13742, #16148 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #11621, #11715, #13742, #16148 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16139#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16139: GHC confused about type synonym kind with QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #11621, #11715, | Differential Rev(s): #13742, #16148 | Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16139#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC