#14822 closed bug (invalid)
-XQuantifiedConstraints: Turn term-level entailments (:-) into constraints (=>)
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
This code works fine:
{-# Language TypeOperators, RankNTypes, KindSignatures, GADTs, DataKinds, MultiParamTypeClasses, FlexibleInstances, ConstraintKinds, ScopedTypeVariables #-} import Data.Kind -- 'constraints' machinery data Dict c where Dict :: c => Dict c newtype a :- b = Sub (a => Dict b) -- entailment -- 'singletons' machinery data SBool :: Bool -> Type where SFalse :: SBool 'False STrue :: SBool 'True class SBoolI (bool::Bool) where sbool :: SBool bool instance SBoolI 'False where sbool = SFalse instance SBoolI 'True where sbool = STrue -- VVV Example VVV class Funny (b::Bool) (b'::Bool) instance Funny 'False b' instance Funny 'True 'True instance Funny 'True 'False proof :: forall b b'. (SBoolI b, SBoolI b') :- Funny b b' proof = Sub (case (sbool :: SBool b, sbool :: SBool b') of (SFalse, _) -> Dict (STrue, SFalse) -> Dict (STrue, STrue) -> Dict) -- ^^^ Example ^^^
What I'm interested in is the entailment:
Singletons for b
and b'
entail Funny b b'
. This is witnessed by proof
.
Given that we have a branch for -XQuantifiedConstraints
, it is tantalizing to convert this into an implication constraint (SBoolI b, SBoolI b') => Funny b b'
.
Is such a thing sensible (wrt coherence) and if so is it at all possible to do this on WIPT2893?
Change History (5)
comment:2 Changed 19 months ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
I fully agree with kcsongor's analysis. This is essentially asking for a way to violate the open-world assumption, which isn't going to fly. If you want to use (SBoolI b, SBoolI b') => Funny b b'
as a quantified constraint, then write an instance for it.
comment:3 Changed 18 months ago by
I claim I don't rely on Bool
being closed. I wouldn't expect forall b. C b
to be resolved, it is more like pi b. C b
(forall b. SBoolI b => C b
) which is subtly different.
Instead I ultimately rely on SBool
being closed. I found a way to emulate this with unsafeCoerce
. Here is an example for the open kind Type
:
{-# Language KindSignatures, GADTs, ConstraintKinds, QuantifiedConstraints, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables, RankNTypes #-} import Data.Kind import Unsafe.Coerce -- constraints data Dict :: Constraint -> Type where Dict :: c => Dict c class (a => b) => Implies a b instance (a => b) => Implies a b type a |- b = Dict (a `Implies` b) -- Representation of two types: Int and Bool data S :: Type -> Type where SInt :: S Int SBool :: S Bool -- Can be passed implicitly class SI a where s :: S a instance SI Int where s = SInt instance SI Bool where s = SBool -- Can be eliminated with an if-then-else sElim :: S a -> (Int ~ a => res) -> (Bool ~ a => res) -> res sElim SInt i _ = i sElim SBool _ b = b -- (SI a) entails (Str a) class Str a where str :: String instance Str Int where str = "INT" instance Str Bool where str = "BOOL" -- Attach the instance I want to this wrapper, that has the same -- representation as `a'. -- -- So I define an instance -- -- SI a => Str (Wrap a) -- -- and then unsafeCoerce between -- -- SI a |- Str (Wrap a) -- SI a |- Str a -- newtype Wrap a = Wrap a instance SI a => Str (Wrap a) where str = sElim (s @a) (str @a) (str @a) wit :: forall a. SI a |- Str a wit = wrapElim Dict where wrapElim :: (SI a |- Str (Wrap a)) -> (SI a |- Str a) wrapElim = unsafeCoerce -- >> siStr @Int -- "INT!" -- >> siStr @Bool -- "BOOL!" siStr :: forall a. SI a => String siStr = go wit where go :: SI a => (SI a |- Str a) -> String go Dict = str @a ++ "!"
I claim that SI a |- Str a
dictionary describes something like
instance SI a => Str a where str :: String str = sElim (s @a) (str @a) (str @a)
Where we handle both cases: SI Int
(str @a
) and SI Bool
(str @a
). “Can't the user add SI
instances that we have no way of handling?”, only with garbage s = undefined
because there are only two S a
-constructors but they are already defined and handled. The above hack seems to work (and is sensible to boot unless I'm missing something). Is there a problem with this?
comment:4 Changed 18 months ago by
Using #14292 this can be coerce
d rather than unsafeCoerce
d if only we turn on -XIncoherentInstances
and mark some parameters representational
type role Implies nominal representational type role Str representational
comment:5 Changed 16 months ago by
Keywords: | wipT2893 removed |
---|
What would the conditions of generating such an implication constraint be?
To me it seems like this would make use of the fact that the kind
Bool
is closed, and in theory, a constraintforall (b :: Bool). C b
could be discharged by having individual instances forC 'True
andC 'False
. Or in terms of implication constraints, thatforall (b :: Bool). C b => D b
could be built from the individual constituents.If my understanding is correct as written above, then I don't think it would make sense.
When I see a quantified implication constraint, like
forall a. C a => D a
, I expect it to be parametric ina
, which means that the solution of that constraint should be a function that uses the dictionary forC a
to build the dictionary forD a
, regardless of whata
is instantiated to. (This expectation is grounded in the open world assumption.)For what it's worth, I think the question can be reformulated as whether the constraint
(forall a b. Funny a b)
should be solved based on your provided instances (to which I would answer no).