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 RyanGlScott

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.

comment:2 Changed 7 months ago by goldfire

It does look to me that GHC should do what Ryan asks...

comment:3 Changed 7 months ago by simonpj

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 in reply to:  3 Changed 7 months ago by RyanGlScott

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

Last edited 7 months ago by RyanGlScott (previous) (diff)

comment:5 Changed 7 months ago by simonpj

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.