[GHC] #16123: QuantifiedConstraints fails to deduce trivial constraint
#16123: QuantifiedConstraints fails to deduce trivial constraint -------------------------------------+------------------------------------- Reporter: eschnett | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- While experimenting with quantified constraints, I find I need to explicitly specify a quantified constraint in an instance declaration that I think should be deduced automatically. When I leave it out, GHC complains that it cannot deduce {{{Num (f a)}}} in the code below. The full source code is attached. The relevant lines are {{{ instance ( Functor f, Dom f ~ NFun, Cod f ~ NFun , forall a. Ok NFun a => Num a -- I don't want to write this constraint ) => Functor (NIdF f) where type Dom (NIdF f) = Dom f type Cod (NIdF f) = Cod f fmap f = NFun \(NIdF xs) -> NIdF (neval (fmap f) xs) }}} where the line marked "I don't want to write ..." points to the constraint I don't want to have to write manually. The definition of the {{{NFun}}} is {{{ instance Category NFun where type Ok NFun a = Num a id = NFun P.id NFun g . NFun f = NFun (g P.. f) }}} Note that the constraint in question does not involve the type {{{NIdF}}} for which the instance is declared – it is a generic condition that is always true, given the instance declaration of {{{NFun}}} (see the definition of {{{Ok}}} there). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16123 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16123: QuantifiedConstraints fails to deduce trivial constraint -------------------------------------+------------------------------------- Reporter: eschnett | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by eschnett): * Attachment "CatQC.hs" added. Source code demonstrating the issue -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16123 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16123: QuantifiedConstraints fails to deduce trivial constraint -------------------------------------+------------------------------------- Reporter: eschnett | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: duplicate | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14680 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => duplicate * related: => #14680 Comment: I'm afraid what you are trying to write just won't work (at least, not today). This quantified constraint: {{{#!hs forall a. Ok (Dom f) a => Ok (Cod f) (f a) }}} Uses a type family in the head of the constraint, which GHC doesn't support. (See [https://ghc.haskell.org/trac/ghc/ticket/14860 this Trac ticket].) The fact that GHC 8.6 somehow accepts this as a superclass constraint for `Functor` is a bug, and as you've discovered, GHC won't actually use that constraint in any instances. On GHC HEAD, your (unmodified) code is rejected with an error message: {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling CatQC ( Bug.hs, Bug.o ) Bug.hs:32:1: error: • Quantified predicate must have a class or type variable head: forall (a :: ObjKind). Ok (Dom f) a => Ok (Cod f) (f a) • In the quantified constraint ‘forall (a :: ObjKind). Ok (Dom f) a => Ok (Cod f) (f a)’ In the context: (Category (Dom f), Category (Cod f), forall (a :: ObjKind). Ok (Dom f) a => Ok (Cod f) (f a)) While checking the super-classes of class ‘Functor’ In the class declaration for ‘Functor’ | 32 | class ( Category (Dom f), Category (Cod f) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... }}} There is a workaround (described in https://ghc.haskell.org/trac/ghc/ticket/14860#comment:19) that can sometimes be used. Unfortunately, this workaround doesn't work here, because you're trying to use a quantified constraint in a superclass position. #14860 is tracking this infelicity already, so I'll close this ticket in favor of that one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16123#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16123: QuantifiedConstraints fails to deduce trivial constraint -------------------------------------+------------------------------------- Reporter: eschnett | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: duplicate | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14680 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by eschnett): For the record: I have a working work-around using {{{Data.Constraint}}}. The {{{functor}}} class then reads {{{ -- | A functor class (Category (Dom f), Category (Cod f)) => Functor f where -- | Prove that this functor maps from its domain to its codomain proveFunctor :: Ok (Dom f) a => Ok (Dom f) a :- Ok (Cod f) (f a) type Dom f :: CatKind type Cod f :: CatKind fmap :: (Ok (Dom f) a, Ok (Dom f) b) => Dom f a b -> Cod f (f a) (f b) }}} and the previously-failing instance declaration becomes {{{ instance (Functor f, Dom f ~ NFun, Cod f ~ NFun) => Functor (NIdF f) where type Dom (NIdF f) = Dom f type Cod (NIdF f) = Cod f proveFunctor :: forall a. Ok (Dom (NIdF f)) a => Ok (Dom (NIdF f)) a :- Ok (Cod (NIdF f)) ((NIdF f) a) proveFunctor = Sub Dict \\ (proveFunctor @f :: Ok (Dom f) a :- Ok (Cod f) (f a)) fmap f = NFun \(NIdF xs) -> NIdF (neval (fmap f) xs) }}} The disadvantage is that {{{proveFunctor}}} is now an explicit function, and using {{{fmap}}} now might require calling {{{proveFunctor}}} explicitly to invoke it as proof. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16123#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16123: QuantifiedConstraints fails to deduce trivial constraint -------------------------------------+------------------------------------- Reporter: eschnett | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: duplicate | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14680 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): FWIW, I think I've discovered a way to work around this issue after all. I've written up the trick in full detail [https://ghc.haskell.org/trac/ghc/ticket/14860#comment:23 here], but in the particular case of your program, the trick is to redefine `Ok` slightly: {{{#!hs type Ok k :: ObjKind -> Constraint }}} Once you've done that, you can get the desired superclass for `Functor` if you write it like this: {{{#!hs class ( Category (Dom f), Category (Cod f) -- | Prove that this functor maps from its domain to its codomain , forall okCodF a. (okCodF ~ Ok (Cod f), Ok (Dom f) a) => okCodF (f a) ) => Functor f where }}} If you do this, then the rest of the module typechecks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16123#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC