#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:2 Changed 19 months ago by
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.
comment:3 Changed 19 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
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)
comment:4 Changed 19 months ago by
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
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
comment:6 Changed 19 months ago by
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
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
Keywords: | wipT2893 removed |
---|
I have a feeling this isn't expected to work, but encoding sums and existentials causes trouble