Opened 19 months ago

Closed 19 months ago

Last modified 16 months ago

#14840 closed bug (fixed)

QuantifiedConstraints: Can't define class alias

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 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 s a. Reifies s (Def cls a) => cls (Lift cls a s)) => ReifiableConstraint cls
instance (forall s a. Reifies s (Def cls a) => cls (Lift cls a s)) => ReifiableConstraint cls

gives an error

$ ghci -ignore-dot-ghci Bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/Bug.hs, interpreted )

/tmp/Bug.hs:14:10: error:
    • Could not deduce: cls (Lift cls a s)
        arising from the superclasses of an instance declaration
      from the context: forall (s :: k) a.
                        Reifies s (Def cls a) =>
                        cls (Lift cls a s)
        bound by the instance declaration at /tmp/Bug.hs:14:10-93
      or from: Reifies s (Def cls a)
        bound by a quantified context at /tmp/Bug.hs:1:1
    • In the instance declaration for ‘ReifiableConstraint cls’
   |
14 | instance (forall s a. Reifies s (Def cls a) => cls (Lift cls a s)) => ReifiableConstraint cls
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude> 

This is a rare occasion that the class alias trick fails for me so ~+~yay~+~. But is it intended?

Change History (8)

comment:1 Changed 19 months ago by Iceland_jack

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
Last edited 19 months ago by Iceland_jack (previous) (diff)

comment:2 Changed 19 months ago by RyanGlScott

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 comment:1 seems to be of an entirely different nature.

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

comment:3 Changed 19 months ago by Iceland_jack

Resolution: fixed
Status: newclosed

Thanks! And comment:1 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)
Last edited 19 months ago by Iceland_jack (previous) (diff)

comment:4 Changed 19 months ago by simonpj

OK so the Description is not-a-bug.

I don't understand comment:1. 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 comment:1 holds water somehow.

comment:5 Changed 19 months ago by Iceland_jack

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

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

comment:6 Changed 19 months ago by simonpj

Given this interesting collection of tickets on quantified constraints 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!

comment:7 Changed 19 months ago by Iceland_jack

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.

comment:8 Changed 16 months ago by RyanGlScott

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