Opened 7 months ago

Last modified 7 months ago

## #16365 new bug

# Inconsistency in quantified constraint solving

Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler | Version: | 8.6.3 |

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

Consider the following program:

{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind import Data.Proxy class C a where m :: a -> () data Dict c = c => Dict ----- type family F a :: Type -> Type class C (F a b) => CF a b instance C (F a b) => CF a b works1 :: (forall z. CF a z) => Proxy (a, b) -> Dict (CF a b) works1 _ = Dict works2 :: ( CF a b) => Proxy (a, b) -> Dict (C (F a b)) works2 _ = Dict works3, fails :: (forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b)) works3 p | Dict <- works1 p = Dict fails _ = Dict

`fails`

, as its name suggests, fails to typecheck:

$ /opt/ghc/8.6.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:33:11: error: • Could not deduce (C (F a b)) arising from a use of ‘Dict’ from the context: forall z. CF a z bound by the type signature for: fails :: forall a b. (forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b)) at Bug.hs:31:1-71 • In the expression: Dict In an equation for ‘fails’: fails _ = Dict | 33 | fails _ = Dict | ^^^^

But I see no reason why this shouldn't typecheck. After all, the fact that `works1`

typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(forall z. CF a z)`

implies `(CF a b)`

, and the fact that `works2`

typechecks proves that GHC's constraint solver is perfectly capable of deducing that `(CF a b)`

implies that `(C (F a b))`

. Why then can GHC's constraint solver not connect the dots and deduce that `(forall z. CF a z)`

implies `(C (F a b))`

(in the type of `fails`

)?

Note that something with the type `(forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b))`

*can* be made to work if you explicitly guide GHC along with explicit pattern-matching on a `Dict`

, as `works3`

demonstrates. But I claim that this shouldn't be necessary.

Moreover, in this variation of the program above:

-- <as above> ----- data G a :: Type -> Type class C (G a b) => CG a b instance C (G a b) => CG a b works1' :: (forall z. CG a z) => Proxy (a, b) -> Dict (CG a b) works1' _ = Dict works2' :: ( CG a b) => Proxy (a, b) -> Dict (C (G a b)) works2' _ = Dict works3' :: (forall z. CG a z) => Proxy (a, b) -> Dict (C (G a b)) works3' _ = Dict

`works3'`

needs no explicit `Dict`

pattern-matching to typecheck.

### Change History (5)

### comment:1 Changed 7 months ago by

### comment:3 follow-up: 4 Changed 7 months ago by

In `works3`

we get

[G] forall z. CF a z -- From the type signature [W] forall z. CF a z -- from the call of works1

We can solve this no problem.

And we also get

[G] CF a b -- From the pattern match on Dict Dict <- works1 p [W] C (F a b) -- From the call of Dict on the RHS of works3

Now `C (F a b)`

is a superclass of `CF a b`

, so we get

[G] C (F a b) -- Via superclass expansion [W] C (F a b) -- From the call of Dict on the RHS of works3

We can solve this without difficulty.

However, in `fails`

we get this:

[G] forall z. CF a z -- From the type signature on fails [W] C (F a b)

From superclass expansion we get

[G] forall z. C (F a z) -- From superclass expansion [W] C (F a b)

And now we are stuck. What `z`

would make `C (F a z)`

match `C (F a b)`

? Well, yes, `b`

would, but maybe also lots of other things. GHC simply doesn't support matching involving type families.

So, as it stands, this looks reasonable. And I don't see an easy way to improve matters.

### comment:4 Changed 7 months ago by

I'm still not convinced. You say:

Replying to simonpj:

From superclass expansion we get

[G] forall z. C (F a z) -- From superclass expansion [W] C (F a b)And now we are stuck. What

`z`

would make`C (F a z)`

match`C (F a b)`

? Well, yes,`b`

would, but maybe also lots of other things. GHC simply doesn't support matching involving type families.

I don't really see why `F`

being a type family has anything to do with this. Recall the definition of `F`

:

type family F a :: Type -> Type

Note that `F`

's second argument is *matchable*. This means that given an equality between `F`

s, we can easily decompose it into their second type arguments, as demonstrated by the fact that this function typechecks:

f :: Proxy a -> F a b :~: F a c -> b :~: c f _ Refl = Refl

Now recall what things we are trying to solve:

[G] forall z. C (F a z) -- From superclass expansion [W] C (F a b)

These two constraints only differ in the second argument to `F`

. But as we just established above, `F`

is matchable in its second argument. Therefore, GHC should have no trouble concluding that `z`

equals `b`

. In other words, `b`

is the only sensible choice here.

### comment:5 Changed 7 months ago by

Ah! I had not focused on the fact that `F`

only has arity 1. Good point.

Avoiding the issues of superclasses for now, this fails:

fails2 :: (forall z. C (F a z)) => Proxy (a, b) -> Dict (C (F a b)) fails2 _ = Dict

saying (quite helpfully)

T16365.hs:37:11: error: • Illegal type synonym family application ‘F a’ in instance: C (F a z) • In the quantified constraint ‘forall z. C (F a z)’ In the type signature: fails2 :: (forall z. C (F a z)) => Proxy (a, b) -> Dict (C (F a b)) | 37 | fails2 :: (forall z. C (F a z)) => Proxy (a, b) -> Dict (C (F a b)) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

You sneak around that by hiding it under a superclass. I'm not sure how to stop you doing that :-).

But this succeeds:

fails3 :: (F a ~ fa, forall z. C (fa z)) => Proxy (a, b) -> Dict (C (F a b)) fails3 _ = Dict

Alas, I don't see how to use the same trick for `CF`

, with its superclass.

In other tickets we have wondered if this kind of floating could happen automatically. I argued "no" because it's subtle and you can do it manually. But with your superclass thing you can't do it manually (I thihik. So maybe that's an argument in favour.

Hmm. Maybe we could elaboarate the matching process. Usually we match

template: forall a b. [a] -> b target: [(Int,Bool)] -> Char

and produce a substitution

a :-> (Int,Bool) b :-> Char

such that applying the substitution to the template yields the target.

But we could instead additionally produce a list of wanted equalities, and treat a type-family application as a wildcard, something like this:

template: forall a. F a -> a -> Int target: Char -> [Bool] -> Int

then we succeed in matching, thus:

Substitution: a :-> Int Wanted equalities: F a ~ [Bool]

I don't think this would be terribly useful at top level, but in these quantified constraints it really might be.

Interesting.

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

Note that this is quite annoying in practice for the

`singletons`

library, as the existence of this bug prevents it from using`deriving`

to generate its`Show`

instances, instead forcing it to laboriously generate`Show`

instances with Template Haskell.