Opened 22 months ago

Closed 21 months ago

Last modified 18 months ago

#14733 closed bug (fixed)

Won't use (forall xx. f xx) with -XQuantifiedConstraints

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

Description

{-# Language QuantifiedConstraints #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}

data D c where
  D :: c => D c

proof :: (forall xx. f xx) => D (f a)
proof = D

Running this program with wip/T2893 gives

GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 174-quantifiedconstraints.hs, interpreted )

174-quantifiedconstraints.hs:9:9: error:
    • Could not deduce: f a arising from a use of ‘D’
      from the context: forall xx. f xx
        bound by the type signature for:
                   proof :: forall (f :: * -> Constraint) a.
                            (forall xx. f xx) =>
                            D (f a)
        at 174-quantifiedconstraints.hs:8:1-37
    • In the expression: D
      In an equation for ‘proof’: proof = D
    • Relevant bindings include
        proof :: D (f a) (bound at 174-quantifiedconstraints.hs:9:1)
  |
9 | proof = D
  |         ^

How can I instantiate xx to a?

Change History (13)

comment:1 Changed 22 months ago by Iceland_jack

Keywords: QuantifiedContexts added

comment:2 Changed 22 months ago by Iceland_jack

Keywords: wipT2893 added

comment:3 Changed 22 months ago by simonpj

Currently this is by-design, but we could change the design.

These forall-constraints currently behave just like a local version of a top-level instance declaration, and those are all for classes. You can't say

instance ... => f Int

although it'd make sense to do so. So similarly you currently can't do that with the local-foralld constraints.

  • If we retain the restriction to class constraints only, we should reject the type signature with a civilised error message.
  • How bad is the restriction? You can always say
    class f a => C f a 
    
    proof :: (forall xx. C f xx) => D (f a)
    
    Would that do? Or what do your use-cases look like?

It'd be a moderate pain to generalise the facility, mainly because InstEnv (in which we look up instances) has class constraints as a deeply-baked-in assumption.

comment:4 Changed 22 months ago by simonpj

Keywords: QuantifiedConstraints added; QuantifiedContexts removed

comment:5 Changed 22 months ago by sjoerd_visscher

How about adding the workaround internally? I.e. add

class c => SomeInteralClass c
instance c => SomeInternalClass c

and translate (forall xx. f xx) to (forall xx. SomeInternalClass (f xx))

comment:6 Changed 22 months ago by Iceland_jack

Only moderate pain? ;-) Here are some use cases

  • (Phab) Vocabulary of constraints: constC :: a :- (b => a). In fact lifting this restriction lets us define a :- b as Dict (a => b)
    pattern SubDict :: a => b => (a :- b)
    pattern SubDict = Dict
    
  • (Phab)
    newtype Free cls a = Free (forall xx. cls xx => (a -> xx) -> xx) 
    
    instance (forall xx. cls (Free cls xx)) => Monad (Free cls)
    
  • (Phab)
    type cls ~=> cls' = forall xx. cls xx => cls' xx
    
    instance Monoid ~=> mon => Foldable (Free mon)
    
  • (Phab by Ryan) The need for Coercible1 has been discussed elsewhere, current design prevents Coercible from being abstracted out.
    type Coercible1 m = forall xx yy. Coercible xx yy => Coercible (m xx) (m yy),
    
  • We might similarly want to parameterize Coercion by Coercible
    type Coercion = With Coercible
    type (:~:)    = With (~)
    type (:~~:)   = With (~~)
    
    data With cls a b where
      With :: cls a b => With cls a b
    

.. without losing that Category instance:

-- Constraint-enriched category
type Refl  rel = forall a.     ()                 => rel a a
type Trans rel = forall a b c. (rel a b, rel b c) => rel a c

instance (Refl rel, Trans rel) => Category (With rel) where
  id :: With rel a a
  id = With

  (.) :: With rel b c -> With rel a b -> With rel a c
  With . With = With

Your class f a => C f a solution didn't work for me (using latest version): here is my full code and error messages.

Echoing Sjoerd if there is a mechanical translation can't GHC do it?

Last edited 21 months ago by Iceland_jack (previous) (diff)

comment:7 in reply to:  3 Changed 22 months ago by Iceland_jack

Replying to simonpj:

Currently this is by-design, but we could change the design.

I'm +1 on change but that's easy to say, how big of a task is it

How bad is the restriction?

Hard to say. If it's a matter of encoding them as class aliases then it is a huge improvement over the current situation, otherwise may rule out a lot of fun examples.

Last edited 22 months ago by Iceland_jack (previous) (diff)

comment:8 in reply to:  5 Changed 22 months ago by RyanGlScott

Replying to sjoerd_visscher:

How about adding the workaround internally? I.e. add

class c => SomeInteralClass c
instance c => SomeInternalClass c

and translate (forall xx. f xx) to (forall xx. SomeInternalClass (f xx))

That's one idea. But does that idea even work if you write it out by hand? I tried:

{-# Language QuantifiedConstraints #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}
{-# Language FlexibleInstances #-}
{-# Language UndecidableInstances #-}
{-# Language UndecidableSuperClasses #-}

class c => SomeInternalClass c
instance c => SomeInternalClass c

data D c where
  D :: c => D c

proof :: (forall xx. SomeInternalClass (f xx)) => D (f a)
proof = D

But that fails with:

Bug.hs:15:9: error:
    • Could not deduce: f a arising from a use of ‘D’
      from the context: forall xx. SomeInternalClass (f xx)
        bound by the type signature for:
                   proof :: forall (f :: * -> Constraint) a.
                            (forall xx. SomeInternalClass (f xx)) =>
                            D (f a)
        at Bug.hs:14:1-57
    • In the expression: D
      In an equation for ‘proof’: proof = D
    • Relevant bindings include proof :: D (f a) (bound at Bug.hs:15:1)
   |
15 | proof = D
   |         ^

Granted, it does work if you change the proof to:

proof :: (forall xx. SomeInternalClass (f xx)) => D (SomeInternalClass (f a))
proof = D

But that would require pervasively inserting SomeInternalClass everywhere in your program, and not just on the quantified constraints which lack an explicit type class constructor.

comment:9 Changed 21 months ago by simonpj

I have fixed this (on branch wip/TT2893); and updated the proposal to reflect it

Would you like to try now?

comment:10 Changed 21 months ago by Iceland_jack

Thank you! I played with it yesterday and it works great with a few kinks.

comment:11 Changed 21 months ago by simonpj

Great! Keep identifying the kinks; it's extremely helpful.

comment:12 Changed 21 months ago by RyanGlScott

Resolution: fixed
Status: newclosed

This featurette was fixed in c477f53799deb46b4987ac788ad67d1bcbb8eb0c.

comment:13 Changed 18 months ago by RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.