## #16123 closed bug (duplicate)

# QuantifiedConstraints fails to deduce trivial constraint

Reported by: | eschnett | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler | Version: | 8.6.3 |

Keywords: | QuantifiedConstraints | Cc: | |

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: |

### Description

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).

### Attachments (1)

### Change History (4)

### Changed 9 months ago by

### comment:1 Changed 9 months ago by

Related Tickets: | → #14680 |
---|---|

Resolution: | → duplicate |

Status: | new → closed |

I'm afraid what you are trying to write just won't work (at least, not today). This quantified constraint:

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 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.

### comment:2 Changed 9 months ago by

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.

### comment:3 Changed 8 months ago by

FWIW, I think I've discovered a way to work around this issue after all. I've written up the trick in full detail here, but in the particular case of your program, the trick is to redefine `Ok`

slightly:

type Ok k :: ObjKind -> Constraint

Once you've done that, you can get the desired superclass for `Functor`

if you write it like this:

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.

**Note:**See TracTickets for help on using tickets.

Source code demonstrating the issue