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 )

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

Description: | modified (diff) |
---|

### comment:2 Changed 15 months ago by

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

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

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

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

### comment:6 Changed 15 months ago by

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

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

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

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 follow-up: 13 Changed 15 months ago by

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.

### comment:11 Changed 15 months ago by

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!

### comment:12 Changed 15 months ago by

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

### comment:13 Changed 14 months ago by

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:

- The type family is independent of the quantified variables
- The type family is injective
- The type family can be reduced to an expression which is unambiguous (this is #13262)
- 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 `Dict`

s.

### comment:14 follow-up: 15 Changed 14 months ago by

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 Changed 14 months ago by

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 follow-ups: 17 19 Changed 14 months ago by

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 Changed 14 months ago by

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

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 Changed 14 months ago by

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 follow-up: 21 Changed 14 months ago by

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 Changed 14 months ago by

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.

Actually, the

`Functor`

example with type families can be fixed by replacing:with

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.