Opened 15 months ago

Last modified 14 months ago

#15347 new bug

QuantifiedConstraints: Implication constraints with type families don't work

Reported by: aaronvargo Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.5
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by aaronvargo)

This may be related to #14860, but I think it's different.

The following code fails to compile:

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}

import Prelude()
import Data.Kind

data Dict c = c => Dict

type family F a :: Constraint

foo :: forall a b. (a => F b, a) => Dict (F b)
foo = Dict
• Could not deduce: F b arising from a use of ‘Dict’
  from the context: (a => F b, a)

Yet the following all do compile:

bar :: forall a. F a => Dict (F a)
bar = Dict

baz :: forall a b. (a => b, a) => Dict b
baz = Dict

qux :: forall a b c. (a => c, a, c ~ F b) => Dict (F b)
qux = Dict

It seems that a wanted F b can be solved with a given F b, but not with a given a => F b, which is bizarre. The fact that qux still works is also strange, as it means that you get a different result if you first simplify by substituting c = F b.

As a more practical example, the following similarly fails to compile, due to the Cod f type family:

-- in addition to the above extensions
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}

class Ob p a

class (forall a. Ob (Dom f) a => Ob (Cod f) (f a)) => Functor f where
  type Dom f
  type Cod f

liftOb :: forall f a. (Functor f, Ob (Dom f) a) => Dict (Ob (Cod f) (f a))
liftOb = Dict

While a version which uses fundeps instead does compile:

class (forall a. Ob dom a => Ob cod (f a)) => Functor dom cod f | f -> dom cod

liftOb :: forall f a dom cod. (Functor dom cod f, Ob dom a) => Dict (Ob cod (f a))
liftOb = Dict

Change History (21)

comment:1 Changed 15 months ago by aaronvargo

Description: modified (diff)

Actually, the Functor example with type families can be fixed by replacing:

forall a. Ob (Dom f) a => Ob (Cod f) (f a)

with

forall a cod. (Ob (Dom f) a, cod ~ Cod f) => Ob cod (f a)

Perhaps the compiler could do this rewrite automatically? It rightly doesn't in the case of instance declarations, but perhaps it's fine for quantified constraints?

Edit: Never mind. I guess the latter constraint isn't the same, as it overlaps more (just as with instance declarations), and GHC apparently gives up when faced with overlapping quantified constraints.

Last edited 15 months ago by aaronvargo (previous) (diff)

comment:2 Changed 15 months ago by aaronvargo

So I guess what I want is for the given a => F b (in foo) to be replaced with the givens:

a => x
x ~ F b

(as in qux) and for the given

forall a. Ob (Dom f) a => Ob (Cod f) (f a)

to be replaced with:

forall a. Ob (Dom f) a => Ob x (f a)
x ~ Cod f

or something like that.

comment:3 Changed 15 months ago by goldfire

I don't see how this is different from #14860. It looks the same to me.

But I think (x ~ F b, forall a. a => x) and forall a. a => F b really are different. It's all about shadowing. The first casts a much bigger shadow, one whose shape can be specified. The second's shadow is too oddly shaped to be predictable.

comment:4 Changed 15 months ago by aaronvargo

Sorry, ignore comment:1, which was stupid. This situation is different from #14860 in that the quantified variable doesn't appear in the application of the type family. As a result, it should be possible to pull the application out, replacing it with a variable, as I've described in comment:2. That is, the application F b can just be treated as if it's a variable c, allowing it to be matched. Then everything seems to work, as demonstrated by both qux and the example which uses fundeps.

Not doing this seems to undermine the usefulness of type families as an alternative to fundeps.

comment:5 Changed 15 months ago by aaronvargo

To clarify, this also compiles:

class Functor (f :: * -> *) where
  type Dom f
  type Cod f

liftOb :: ( Functor f, cod ~ Cod f
          , forall a. Ob (Dom f) a => Ob cod (f a)
          , Ob (Dom f) a
          ) => Dict (Ob (Cod f) (f a))
liftOb = Dict
Last edited 15 months ago by aaronvargo (previous) (diff)

comment:6 Changed 15 months ago by goldfire

OK. I see how this is different than #14860. But I still claim that GHC should not do this rewriting, because having a variable in a quantified constraint head casts a longer shadow than having a type family. And it's all about that shadow.

comment:7 Changed 15 months ago by aaronvargo

Not if the variable is a skolem (is that the right terminology?), which is what I intended. I should have been clearer.

comment:8 Changed 15 months ago by aaronvargo

This demonstrates there's no shadowing (it compiles):

liftOb :: forall f cod other a.
  ( Functor f, cod ~ Cod f, Ob (Dom f) a
  , forall a. Ob (Dom f) a => Ob cod (f a)
  , forall a. Ob (Dom f) a => Ob other (f a)
  ) => Dict (Ob cod (f a), Ob other (f a))
liftOb = Dict

comment:9 Changed 15 months ago by aaronvargo

Or to give the simpler example, this does too:

wibble :: forall a b fb c. (a, fb ~ F b, a => fb, a => c) => Dict (F b, c)
wibble = Dict

comment:10 Changed 15 months ago by simonpj

Consider this:

type family F a
type instance F Int = Bool

instance Eq a => Eq (F a) where ...

Should we allow this? Obviously not. It's like allowing

map f (xs ++ ys) = map f xs ++ map f ys
map f []         = []

where we have a function call in the pattern match. All manner of overlaps a chaos would result. So generally GHC does not allow type family calls in the head of an instance declaration. And I've made that same rule apply to quantified constraints, which are really just local instance declarations.

But, you say, how are these two different?

foo :: forall a b.   (a => F b,        a) => Dict (F b)
qux :: forall a b c. (a => c, c ~ F b, a) => Dict (F b)

Very different, I say! Suppose that quantified constraint had looked like this

foo :: forall a b.   (forall t. a => F t b,  ...) => Dict (F b)

Notice that the locally-quantified t is one of the arguments to F. Now, all the bad things could happen. What is different about your example is that the function call is independent of any of the forall'd variables of the quantified constraint. You expressed that by floating it out of the quantified constraint with you c ~ F b. And because it is independent of the forall'd variables, it is really constant so far as the instance is concerned, and doesn't lead to problems.

Here's another variant:

foo :: forall b. (forall t. C b t => C (F b) [t],  ...) => Dict (F b)

Now the head of the quantified constraint does mention the forall'd t, but the call to F does not, so we can float thus:

foo :: forall b c. (c ~ F b, forall t. C b t => C c [t],  ...) => Dict (F b)

This directly expresses the fact that the first parameter to C in the head of the quantified constraint is independent of t.

Now, you want this floating business to happen automatically, but I think it is much too complicated to do behind the scenes. If that's what you want, you can say it. I would be reluctant to introduce a significant (and unprecedented) implicit translation, based on a free-variable analysis, without plenty of evidence that it was going to have major benefit for a significant constituency. I don't think we are close to that point yet.

But it is a nice observation that, by expressing the independence with an equality constraint, you can say just what you mean, and get just what you want. (I doubt that fundeps would be any help here.)

PS: I have no idea what this "shadow" language is all about.

Last edited 15 months ago by simonpj (previous) (diff)

comment:11 Changed 15 months ago by aaronvargo

Yes, that's what I want, though I wonder if there may be other ways to achieve the same effect, without actually implementing the described translation.

I'll try and write out a better example of how it might be useful, and experiment with how painful it is to do the transformation manually.

Edit: Everything else I had originally written in this comment was dumb. Sorry, ignore it!

Last edited 15 months ago by aaronvargo (previous) (diff)

comment:12 Changed 15 months ago by aaronvargo

Edit: Everything I wrote in this comment was really stupid. Sorry, ignore it!

Last edited 15 months ago by aaronvargo (previous) (diff)

comment:13 in reply to:  10 Changed 14 months ago by aaronvargo

Replying to simonpj:

A few things:

First, there's probably another way to do this without a free-variable analysis: float type families out when they appear in wanted constraints. E.g. in foo, the floating would happen because F b appears in the wanted constraint, not because it's independent of the forall'd variables in the given quantified constraint. Would something like that be more feasible?

Second,

Consider this:

type family F a
type instance F Int = Bool

instance Eq a => Eq (F a) where ...

Should we allow this? Obviously not. It's like allowing...

Indeed, but this is an argument for disallowing ambiguity, not for disallowing type families. In your Eq example, a is ambiguous since F may not be injective. (likewise, xs and ys are ambiguous in the map example since (++) isn't injective). Not all uses of type families cause such ambiguity, and the compiler already has a perfectly good ambiguity check which can determine whether they do. Some cases where they don't are:

  1. The type family is independent of the quantified variables
  2. The type family is injective
  3. The type family can be reduced to an expression which is unambiguous (this is #13262)
  4. The quantified variables appear ambiguously in the type family, but are still made unambiguous by the rest of the instance head, e.g. forall a. C (F a) [a]

For top-level instances there may be coherence issues with allowing type families even when they don't cause ambiguity, but such issues don't apply to QCs, which can't introduce incoherence.

So why not allow type families in QCs, but require that the quantified variables be unambiguous?

Third, working around this by manually floating out type families can be hugely painful, as it requires sacrificing one of the major benefits of type families, namely the ability to avoid passing around extra class parameters which are already determined by other parameters. The basic problem is this: suppose we have a class:

class (forall a. Eq a => Eq (f a)) => C f t | t -> f

Currently, the parameter f can never be instantiated with a type family without breaking the quantified constraint. This means the extra parameter needs to be repeated throughout the code for the QC to continue to work, despite the fact that f is already determined by t.

Consider the following encoding of categories and functors, which makes use of type families:

type Hom k = k -> k -> Type

-- Natural transformations
data (==>) (p :: Hom i) (q :: Hom j) (f :: i -> j) (g :: i -> j)

class ( Category (Op p)
      , Op (Op p) ~ p
      , Ob (Op p) ~ Ob p
      , FunctorOf' (Op p) (p ==> (->)) p
      , forall a. Ob p a => FunctorOf' p (->) (p a)
      ) => Category (p :: Hom k) where
  type Ob p :: k -> Constraint
  type Op p :: Hom k

-- FunctorOf without superclasses, to work around issues with UndecidableSuperClasses
class FunctorOf' (p :: Hom i) (q :: Hom j) (f :: i -> j) | f -> p q

-- FunctorOf' with proper superclasses
class ( FunctorOf' p q f
      , Category p
      , Category q
      , forall a. Ob p a => Ob q (f a)
      ) => FunctorOf p q f
instance ( FunctorOf' p q f
         , Category p
         , Category q
         , forall a. Ob p a => Ob q (f a)
         ) => FunctorOf p q f

Note that Category p has a superclass Category (Op p), which has a superclass:

-- noting that Ob (Op p) ~ Ob p
forall a. Ob p a => FunctorOf' (Op p) (->) (Op p a)

and that the superclasses of FunctorOf p q f include:

forall a. Ob p a => Ob q (f a)
forall a. Ob p a => FunctorOf' (Op p) (->) (Op p a)
forall a. Ob q a => FunctorOf' (Op q) (->) (Op q a)

All of these have independent type families in the heads. Floating them out manually requires doubling the number of class parameters for both Category and FunctorOf:

class (..., op ~ Op p) => Category op (p :: Hom k) where ...

class ( FunctorOf' p q f
      , Category opP p
      , Category opQ q
      , obQ ~ Ob q
      , forall a. Ob p a => obQ (f a)
      ) => FunctorOf opP p opQ q obQ f

These parameters will spread throughout all of the code. Subclasses will add yet more parameters, and will never be able to use type families for anything which is a functor or a category, without sacrificing some QCs. Types will be lost in a sea of parameters.

This ends up being more painful than just using Dicts.

Last edited 14 months ago by aaronvargo (previous) (diff)

comment:14 Changed 14 months ago by simonpj

Third, working around this by manually floating out type families can be hugely painful, as it requires sacrificing one of the major benefits of type families, namely the ability to avoid passing around extra class parameters which are already determined by other parameters

Would it be possible to distil the example into a smaller form that still illustrates your key point, in italics. My example in comment:10 did not substantiate this point. Can you give a small example that does? The Category example is so big that I lost the wood for the trees. That is, so far I do not understand why floating out type families (a straightforward source-to-source transformation that does not change the number of class parameters) would sacrifice a major benefit. Thanks!

comment:15 in reply to:  14 Changed 14 months ago by aaronvargo

Replying to simonpj:

Yes, sorry!

That is, so far I do not understand why floating out type families (a straightforward source-to-source transformation that does not change the number of class parameters) would sacrifice a major benefit.

It requires changing the number of class parameters when the quantified constraint appears as a superclass. Suppose we would like to write:

class (forall a. Eq a => Eq (F t a)) => C t where
  type F t :: * -> *

where the type family F t in the quantified constraint is independent of the quantified a. In order to float this type family out, we need to add a new parameter to the class, ft, and make it equal to F t:

class (ft ~ F t, forall a. Eq a => Eq (ft a)) => C ft t where
  type F t :: * -> *

Furthermore, this parameter can never be instantiated with a type family without once again breaking the quantified constraint. E.g. if we write

class C (F t) t => D t

then the inherited quantified constraint will contain a type family, and will no longer work.

comment:16 Changed 14 months ago by simonpj

In order to float this type family out, we need to add a new parameter to the class,

Really? What wrong with this?

class (ft ~ F t, forall a. Eq a => Eq (ft a)) => C t where

No extra parameter.

comment:17 in reply to:  16 Changed 14 months ago by aaronvargo

Replying to simonpj:

Really? What wrong with this?

Not in scope: type variable ‘ft’

The superclass isn't allowed to mention variables which don't appear in the head, even if they're already determined by other parameters. The solution to this limitation has been "use type families", which leads us to this issue.

comment:18 Changed 14 months ago by aaronvargo

I don't see why that is though. Why can't ft be made an implicit parameter to the class?

If it were possible to explicitly bind the implicit parameters of a class, perhaps we could write something like:

class forall ft. (ft ~ F t, forall a. Eq a => Eq (ft a)) => C t

Hmm, it is possible to make ft implicit using a proxy though:

class (ft ~ F t, forall a. Eq a => Eq (ft a)) => C (p :: Proxy ft) t where
  type F t :: * -> *

-- this works
foo :: forall t a. (C 'Proxy t, Eq a) => Dict (Eq (F t a))
foo = Dict

This still requires adding a parameter, but would only require adding one to each class rather than potentially several, as we can use a single proxy for all of the extra parameters.

comment:19 in reply to:  16 Changed 14 months ago by aaronvargo

Replying to simonpj:

I thought I'd once seen a ticket for this, and I've managed to find it: see #3490, where you write:

The easiest way forward is to re-express your program using type functions

Also, on second thought, what I said in comment:18 won't work.

comment:20 Changed 14 months ago by simonpj

The superclass isn't allowed to mention variables which don't appear in the head,

Ah, I was thinking "instance decl" but actually we have a class decl. My mistake.

Not allowing functions in the instance head not to do with ambiguity; it's to do with coherence'. Consider, at the term level

f [x]           = x-1
f (reverse [x]) = x+1

reverse is perfectly injective, but we don't want (f e) to return different answers depending on the evaluated-ness of e.

Can you distil a small example that shows the utility of having a function in the head?


Guessing, maybe what you want is this:

class (forall a. Eq a => Eq (F t a)) => C t where
  type F t :: * -> *

instance C Int where
  F Int = Maybe

f1 :: C t => ...
f1 = e1

f2 :: C Int => ...
f2 = e2

In f1 we have the quantified constraint available but with a function in the head, so it's unusuable. But in f2 the quantified constraint becomes

forall a. Eq a => Eq (F Int a)

which rewrites (via the type instance) to

forall a. Eq a => Eq (Maybe a)

and this is usable.

So, maybe a quantified constraints with a function in the head is just "parked", but it wakes up if the function can be reduced.

This all seems complicated to specify, let alone implement, but it's the closest I can get.

comment:21 in reply to:  20 Changed 14 months ago by aaronvargo

Replying to simonpj:

Not allowing functions in the instance head not to do with ambiguity; it's to do with coherence

But is this an issue for QCs, which can't introduce incoherence? Does it matter if two QCs might overlap, as long as locally we can't tell that they do? Suppose we had:

type family F a = r | r -> a
type family G a = r | r -> a

foo :: forall b. (forall a. Eq (F a), forall a. Eq (G a)) => Dict (Eq (F b))
foo = Dict

While F b and G b might overlap for some particular b, locally only one instance can be used to solve Eq (F b), since we don't know whether G b ~ F b. Since the two instances are guaranteed to be coherent, wouldn't it be fine to simply pick the one that matches? (If both were to match then the program would still be rejected).

Likewise for the case with non-injective independent type families:

foo :: forall b. (forall t. C (F b) [t], forall t. C (G b) [t]) => Dict (C (F b) [Int])

The first instance should just be used, since it's the only one that matches given the knowledge available locally.

How does the compiler currently deal with type families in non-quantified constraints? What makes it more difficult to allow them in QCs?

Can you distil a small example that shows the utility of having a function in the head?

For now I have no use case for the injective type family case, and only really care about the independent family case. I'll try and come up with a simpler example than the category one.

So, maybe a quantified constraint with a function in the head is just "parked", but it wakes up if the function can be reduced.

This is much less useful than what I want, though I suppose it might help in some small minority of cases.

Note: See TracTickets for help on using tickets.