[WIP] Implement QuantifiedConstraints
AbandonedPublic

Authored by bgamari on Jan 29 2018, 12:31 PM.

Details

Reviewers
goldfire
Trac Issues
#2893
Summary

We have wanted quantified constraints for ages and, as I hoped,
they proved remarkably simple to implement. All the machinery was
already in place.

The main ticket is Trac Trac #2893, but also relevant are

#5927
#8516
#9123 (especially!  higher kinded roles)
#14070
#14317

The wiki page is

https://ghc.haskell.org/trac/ghc/wiki/QuantifiedContexts

Here is the relevant Note:

Note [Quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The -XQuantifiedConstraints extension allows type-class contexts like this:

data Rose f x = Rose x (f (Rose f x))

instance (Eq a, forall b. Eq b => Eq (f b))
      => Eq (Rose f a)  where
  (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2

Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
This quantified constraint is needed to solve the

  • (Eq (f (Rose f x)))

constraint which arises form the (==) definition.

Here are the moving parts

  • Language extension {-# LANGUAGE QuantifiedConstraints #-} and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension
  • A new form of evidence, EvDFun, that is used to discharge such wanted constraints
  • checkValidType gets some changes to accept forall-constraints only in the right places.
  • Type.PredTree gets a new constructor ForAllPred, and and classifyPredType analyses a PredType to decompose the new forall-constraints
  • TcSMonad.InertCans gets an extra field, inert_insts, which holds all the Given forall-constraints. In effect, such Given constraints are like local instance decls.
  • When trying to solve a class constraint, via TcInteract.matchInstEnv, use the InstEnv from inert_insts so that we include the local Given forall-constraints in the lookup. (See TcSMonad.getInstEnvs.)
  • TcCanonical.canForAll deals with solving a forall-constraint. See Note [Solving a Wanted forall-constraint] Note [Solving a Wanted forall-constraint]
  • We augment the kick-out code to kick out an inert forall constraint if it can be rewritten by a new type equality; see TcSMonad.kick_out_rewritable

Still to come

  • User manual documentation
  • A GHC Proposal

This is Simon's patch, part of his wip/T2893 branch.

Test Plan

Validate

bgamari created this revision.Jan 29 2018, 12:31 PM

This Diff doesn't have all of the commits from the wip/T2893 branch, does it? For instance, it seems to be lacking this commit.

Below is an assortment of observations I've made about this patch:

  • Currently, this is the error message you get when you use a quantified context without -XQuantifiedConstraints on:
• Illegal polymorphic type: forall b. Foo [b]
  A constraint must be a monotype
• In the type signature: g :: (forall b. Foo [b]) => String

This should suggest turning on -XQuantifiedConstraints.

  • I'm quite confused as to when a quantified constraint requires the use of UndecidableInstances or not. For instance, this program:
{-# LANGUAGE QuantifiedConstraints  #-}
module T2893 where

f :: forall b c. (Eq b, forall a. Eq a => Eq (c a)) => c b -> Bool
{-# NOINLINE f #-}
f x = x==x

g x = f [x]

data Rose f x = Rose x (f (Rose f x))

instance (Eq a, forall b. Eq b => Eq (f b))
      => Eq (Rose f a)  where
  (Rose x1 rs1) == (Rose x2 rs2)
    = x1==x2 && rs1 == rs2

Works without UndecidableInstances, but the following program does require UndecidableInstances:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving #-}
module Bug where

data Some f where
  Some :: f a -> Some f

deriving instance (forall a. Show (f a)) => Show (Some f)
Bug.hs:9:19: error:
    • The constraint ‘forall a. Show (f a)’
        is no smaller than the instance head
      (Use UndecidableInstances to permit this)
    • In the stand-alone deriving instance for
        ‘(forall a. Show (f a)) => Show (Some f)’
  |
9 | deriving instance (forall a. Show (f a)) => Show (Some f)
  |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It's hard for me to tell why the former doesn't require it, but the latter does. If there is some rhyme or reason behind it, perhaps we should spell it out in the users' guide somewhere.

  • This gives a rather confusing error message:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

data Some f where
  Some :: f a -> Some f

deriving instance (forall a. (Show a, Show (f a))) => Show (Some f)
Bug.hs:12:19: error:
    • Could not deduce (Show a)
      from the context: forall a. (Show a, Show (f a))
        bound by an instance declaration:
                   forall (f :: * -> *).
                   (forall a. (Show a, Show (f a))) =>
                   Show (Some f)
        at Bug.hs:12:19-67
      Possible fix: add (Show a) to the context of a quantified context
    • In the ambiguity check for an instance declaration
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the stand-alone deriving instance for
        ‘(forall a. (Show a, Show (f a))) => Show (Some f)’
   |
12 | deriving instance (forall a. (Show a, Show (f a))) => Show (Some f)
   |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

In particular, the add (Show a) to the context of a quantified context bit—I'm already doing that!

  • I would really like to write this program:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Coerce

newtype Wrap m a = Wrap (m a)

class Monad' m where
  join' :: m (m a) -> m a

instance (forall a. Coercible (m (m a)) (m (Wrap m a)), Monad' m) => Monad' (Wrap m) where
  join' = coerce @(forall a. m (m a) -> m a)
                 @(forall a. Wrap m (Wrap m a) -> Wrap m a)
                 join'

Or even this one:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where

import Data.Coerce

newtype Wrap m a = Wrap (m a)

class Monad' m where
  join' :: m (m a) -> m a

instance (forall a b. Coercible a b => Coercible (m a) (m b), Monad' m) => Monad' (Wrap m) where
  join' = coerce @(forall a. m (m a) -> m a)
                 @(forall a. Wrap m (Wrap m a) -> Wrap m a)
                 join'

Neither typecheck, to my surprise. Is this expected?

Iceland_jack added a subscriber: Iceland_jack.EditedJan 30 2018, 5:27 AM

Glad to get my hands on this. If you need examples / tests I have several in this reddit comment.

Using vocabulary from constraints:

-- witness of constraint `c`
data Dict :: Constraint -> Type where
  Dict :: c => Dict c

-- constraint a "entails" b
newtype (:-) :: Constraint -> Constraint -> Type where
  Sub :: (a => Dict b) -> a :- b

there is a possible bug. Since Eq is a superclass of Ord we know it is entailed by Ord: Ord a :- Eq a.

We can show that Ord1 entails itself (Ord1 f :- Ord1 f) but Ord1 does not entail Eq1:

class    (forall xx. Eq xx => Eq (f xx)) => Eq1 f
instance (forall xx. Eq xx => Eq (f xx)) => Eq1 f

class    (forall xx. Ord xx => Ord (f xx)) => Ord1 f
instance (forall xx. Ord xx => Ord (f xx)) => Ord1 f
Prelude> :t Sub Dict :: Ord1 f :- Eq1 f

<interactive>:1:5: error:
    • Could not deduce (Eq (f1 xx)) arising from a use of ‘Dict’
      from the context: Ord1 f1
        bound by a type expected by the context:
                   Ord1 f1 => Dict (Eq1 f1)
        at <interactive>:1:1-8
      or from: Eq xx bound by a quantified context at <interactive>:1:1
    • In the first argument of ‘Sub’, namely ‘Dict’
      In the expression: Sub Dict :: Ord1 f :- Eq1 f
Iceland_jack added a comment.EditedJan 30 2018, 5:43 AM

Potential bug?

{-# Language QuantifiedConstraints, DerivingStrategies, UndecidableInstances, RankNTypes, ConstraintKinds, DeriveFunctor #-}

newtype Free c a = Free { runFree :: forall r. c r => (a -> r) -> r } 
  deriving stock Functor 

instance Applicative (Free c) where 
  pure a = Free ($ a)
  Free ff <*> Free fx = Free $ \f -> ff $ \f' -> fx $ \x  -> f (f' x)

instance (forall xx. c (Free c xx)) => Monad (Free c) where 
  Free f >>= g = f g

should work but instead fails with

Z.hs:11:18: error:
    • Could not deduce: c (Free c b) arising from a use of ‘f’
      from the context: forall xx. c (Free c xx)
        bound by the instance declaration at Z.hs:10:10-53
    • In the expression: f g
      In an equation for ‘>>=’: Free f >>= g = f g
      In the instance declaration for ‘Monad (Free c)’
    • Relevant bindings include
        g :: a -> Free c b (bound at Z.hs:11:14)
        f :: forall r. c r => (a -> r) -> r (bound at Z.hs:11:8)
        (>>=) :: Free c a -> (a -> Free c b) -> Free c b
          (bound at Z.hs:11:10)
   |
11 |   Free f >>= g = f g 
   |                  ^^^

Fails on (source)

newtype Free c a
  = Free 
  { runFree :: forall b. c b => (a -> b) -> b 
  }

instance (forall a. Monoid a => c a) => Foldable (Free c) where
  foldMap = flip runFree
Iceland_jack added a comment.EditedJan 30 2018, 11:34 AM

I think all of these should be accepted (taken from Kmett)

apply :: (a => b, a) :- b
apply = Sub Dict

constC :: a :- (b => a)
constC = Sub Dict

jot :: () :- (a => a)
jot = Sub Dict

jot' :: () :- (forall xx. xx => xx)
jot' = Sub Dict

reifyC :: (a :- b) -> Dict (a => b)
reifyC (Sub Dict) = Dict

curryC :: ((a, b) => c) :- (a => b => c)
curryC = Sub Dict

uncurry :: (a => b => c) :- ((a, b) => c)
uncurry = Sub Dict
gertjanb added a subscriber: gertjanb.EditedJan 31 2018, 9:22 AM

First of all: Thanks for implementing this!

Below are some observations I made:

  • This example seems to break some assert statement:
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}

class (forall m. Monad m => Monad (t m)) => Trans t where
  lift :: Monad m => m a -> (t m) a

newtype ((t1 :: (* -> *) -> * -> *) * (t2 :: (* -> *) -> * -> *)) m a = C { runC :: t1 (t2 m) a }

instance (Trans t1, Trans t2) => Trans (t1 * t2) where
  lift x = C (lift (lift x))

Resulting in this error message:

ex2.hs: ex2.hs: panic! (the 'impossible' happened)
  (GHC version 8.5.20180128 for x86_64-unknown-linux):
	ASSERT failed!
  df_a27c
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
        pprPanic, called at compiler/utils/Outputable.hs:1206:5 in ghc:Outputable
        assertPprPanic, called at compiler/ghci/ByteCodeLink.hs:136:51 in ghc:ByteCodeLink
  • This (slightly artificial) example should work:
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE UndecidableInstances  #-}

class A a where {}
class B a where {}
class C a where {}
class (A a => C a) => D a where {}
class (B a => C a) => E a where {}

class C a => F a where {}
instance (B a, D a, E a) => F a where {}

But instead returns the following compile error:

ex4.hs:12:10: error:
    • Could not deduce (A a)
        arising from the superclasses of an instance declaration
      from the context: (B a, D a, E a)
        bound by the instance declaration
        at /home/gertjan/Dropbox/PhD/QCC Examples/ex4.hs:12:10-31
      Possible fix: add (A a) to the context of the instance declaration
    • In the instance declaration for ‘F a’
   |
12 | instance (B a, D a, E a) => F a where {}
   |          ^^^^^^^^^^^^^^^^^^^^^^

However, when the order of the instance context is changed, it does work:

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE UndecidableInstances  #-}

class A a where {}
class B a where {}
class C a where {}
class (A a => C a) => D a where {}
class (B a => C a) => E a where {}

class C a => F a where {}
instance (B a, E a, D a) => F a where {}

The (A a => C a) and (B a => C a) axioms overlap and the compiler will simply pick the first one.
It seems rather confusing for the programmer that this ordering should determine whether or not the code is accepted...
Maybe a better solution here would be to simply reject programs containing overlapping axioms? Or maybe even investigate backtracking (where the compiler would try the first axiom, fail and then try the second one) for these situations?

  • This example seems to break some assert statement:

That example may be https://ghc.haskell.org/trac/ghc/ticket/14735 because it's solved in the latest version. That other concern though..

Re roles and Coercible, see Trac Trac #9123 comment:42

Great comments thanks.

For comments on specifics of the code, use Phab. But for comments about the design (i.e. most of the feedback above) use the ticket. It's more durable into the future.

This is quite straightforward for something so useful!

compiler/typecheck/TcCanonical.hs
590

But what if there's no forall? e.g.

f :: forall a. (D a => C (F a)) => ...

I can't think of a practical example, but it seems strange to use FM_SubstOnly here.

644

s/Wanted/Given/

compiler/typecheck/TcEvidence.hs
779

This looks highly suspicious. If it's right, it certainly needs a comment.

compiler/typecheck/TcSMonad.hs
2733

You comment on this function that it's gross. But it's not really needed, I don't think: just have a variant of buildImplication that takes a WantedConstraints instead of a TcS result. I think that's quite a bit simpler, really.

compiler/typecheck/TcValidity.hs
1389

I would expect recurring on all the PredTypes on the LHS, too.

2026

I doubt that's right. But it's all to do with the termination check, which hasn't been worked out in our brave new world yet.

simonpj added inline comments.Feb 5 2018, 10:32 AM
compiler/typecheck/TcValidity.hs
731

class classifyPredType!

ekmett added a subscriber: ekmett.Apr 10 2018, 12:32 PM

This is already quite useful! I've been experimenting with this branch and can use it to remove a bunch of manual dictionary opening/closing code.

Going further, would it be possible to use this with a bit of tweaking to improve the power of UndecidableSuperClasses?

If we have a => b modeled as a function behind the scenes, couldn't that allow you to bypass the strictness condition that requires you can iterate everything out to a fixed point in advance? e.g. could UndecidableSuperClasses be upgraded to ignore the right hand side of the =>'s of its superclasses when QuantifiedConstraints is also enabled? That would allow something like

data Succ k
class (() => Foo (Succ k)) => Foo k
instance Foo k => Foo (Succ k)

to work, and seems like it could fix the old broken categories example I offered up before where Nat k k was a category given k was a category, but where since this was an infinitely deep "tower" UndecidableSuperClasses couldn't help. All I'd need to do is drop in a quantified constraint at the right point to break the cycle.

> could UndecidableSuperClasses be upgraded to ignore the right hand side of the =>'s of its superclasses when QuantifiedConstraints is also enabled?

That seems horribly ad hoc. And (worse) others have specifically called for superclass expansion of quantified constraints. The GHC proposal explicitly includes that, and it's in the implementation. Maybe I'm misunderstanding

bgamari abandoned this revision.May 3 2018, 10:16 PM

This was merged with dbcf8d0b9076ae32b9138623eb84f67c18ed3da.

RyanGlScott added a comment.EditedMay 4 2018, 6:00 AM

This was merged with dbcf8d0b9076ae32b9138623eb84f67c18ed3da.

It was? I don't see this on master.

This was merged with dbcf8d0b9076ae32b9138623eb84f67c18ed3da.

It was? I don't see this on master.

No it was not. This was a test. This was only a test...

Nevertheless, I think this diff has likely served its purpose.

Note: this has been superseded by D4724.