Opened 9 months ago

Closed 9 months ago

Last modified 8 months ago

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

CatQC.hs (2.2 KB) - added by eschnett 9 months ago.
Source code demonstrating the issue

Download all attachments as: .zip

Change History (4)

Changed 9 months ago by eschnett

Attachment: CatQC.hs added

Source code demonstrating the issue

comment:1 Changed 9 months ago by RyanGlScott

Resolution: duplicate
Status: newclosed

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

comment:3 Changed 8 months ago 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 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.