QuantifiedConstraints: Can't define class alias

changed weight to 5

I have a feeling this isn't expected to work, but encoding sums and existentials causes trouble

class    (forall sum. (a => sum) => (b => sum) => sum) => Sum a b
instance (forall sum. (a => sum) => (b => sum) => sum) => Sum a b

class    (forall exists. (forall xx. f xx => exists) => exists) => Exists f
instance (forall exists. (forall xx. f xx => exists) => exists) => Exists f

I'm not sure that this is a bug. Here's a reduced version of your first program:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

data T a

class C1 a

class    (forall a. cls (T a)) => C2 cls
instance (forall a. cls (T a)) => C2 cls

Note that this works without PolyKinds, which should give you an idea of the underlying issue. If you compile this with -fprint-explicit-kinds, the error message is more enlightening:

Bug.hs:12:10: error:
    • Could not deduce: cls (T k0 a)
      from the context: forall (a :: k). cls (T k a)
        bound by an instance declaration:
                   forall k (cls :: * -> Constraint).
                   (forall (a :: k). cls (T k a)) =>
                   C2 cls
        at Bug.hs:12:10-40
    • In the ambiguity check for an instance declaration
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the instance declaration for ‘C2 cls’
   |
12 | instance (forall a. cls (T a)) => C2 cls
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

You can fix this by explicitly binding the kind of a:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

data T a

class C1 a

class    (forall k (a :: k). cls (T a)) => C2 cls
instance (forall k (a :: k). cls (T a)) => C2 cls

With that in mind, here's the fixed version of your first program:

{-# Language TypeInType, MultiParamTypeClasses, TypeFamilies, FlexibleContexts, FunctionalDependencies, AllowAmbiguousTypes, QuantifiedConstraints, GADTs, ConstraintKinds, KindSignatures, RankNTypes, FlexibleInstances, UndecidableInstances, TypeOperators #-}

import Data.Kind

class Reifies s a | s -> a where
  reflect :: proxy s -> a

newtype Lift :: forall k. (Type -> Constraint) -> Type -> k -> Type where
  Lift :: a -> Lift cls a s

data family Def :: (k -> Constraint) -> (k -> Type)

class    (forall k (s :: k) a. Reifies s (Def cls a) => cls (Lift cls a s)) => ReifiableConstraint cls
instance (forall k (s :: k) a. Reifies s (Def cls a) => cls (Lift cls a s)) => ReifiableConstraint cls

The program in ticket:14840#comment:149452 seems to be of an entirely different nature.

closed

Thanks! And ticket:14840#comment:149452 works with tricks but probably isn't much use once defined

class    (a => b) => a |- b
instance (a => b) => a |- b

class    (forall xx. f xx |- g xx) => f |~ g
instance (forall xx. f xx |- g xx) => f |~ g

class    (forall xx. f xx |- exists) => Exists1 f exists
instance (forall xx. f xx |- exists) => Exists1 f exists

class    exists => Exists2 f exists
instance exists => Exists2 f exists

class    Exists1 f |~ Exists2 f => Exists (f::k -> Constraint)
instance Exists1 f |~ Exists2 f => Exists (f::k -> Constraint)

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

OK so the Description is not-a-bug.

I don't understand ticket:14840#comment:149452. You seem to be giving a quantified constraint like

  forall (sum :: Constraint).  blah => sum

which asserts that for ANY constraint we can solve with this quantified constraint. That can't be right can it?

I'll close this ticket, but do open a new one if you think ticket:14840#comment:149452 holds water somehow.

I'm thinking of these as a Church encoding, I wanted to see how close I could get to something like sum or existential constraints and actually both Sum Exists work-for-some-definition-of-work! (with judicious aliasing)

Here is an example that works today, I can Church encode (a, b)

{-# Language TypeOperators, GADTs, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, ConstraintKinds, RankNTypes, QuantifiedConstraints #-}

data Dict c where
  Dict :: c => Dict c

class    (a => b) => (a |- b)
instance (a => b) => (a |- b)

We define a type class constraint of church encoded products (forall pair. (a -> b -> pair) -> pair)

class    (forall pair. (a |- b |- pair) |- pair) => ChurchPair a b
instance (forall pair. (a |- b |- pair) |- pair) => ChurchPair a b

And amazingly GHC can conclude ChurchPair a b from (a, b)!

type a :- b = Dict (a |- b)

wit :: (a, b) :- ChurchPair a b
wit = Dict

the other half of the isomorphism is too much for GHC

reductionStackOverflow :: ChurchPair a b :- (a, b)
reductionStackOverflow = Dict

which is as expected, from your response to one of the other tickets

Given this interestingcollectionofticketsonquantifiedconstraints it'd be great if someone (Iceland Jack? Ryan?) wanted to write a blog post or even a paper about what you can and cannot do; and why. These examples make my head hurt!

I will write a blog post, I would love to expand it into a paper but I'd probably require some guidance. I have a good idea what you can/cannot do but not always why.

added 1 deleted label

added Pnormal label

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

QuantifiedConstraints: Can't define class alias

Child items ...

Activity