#14822: -XQuantifiedConstraints: Turn term-level entailments (:-) into constraints (=>) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by kcsongor): 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 constraint `forall (b :: Bool). C b` could be discharged by having an instance for `C 'True` and `C 'False`. Or in terms of implication constraints, that `forall (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 in `a`, which means that the solution of that constraint should be a function that uses the dictionary for `C a` to build the dictionary for `D a`, regardless of what `a` 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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14822#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14822: -XQuantifiedConstraints: Turn term-level entailments (:-) into constraints (=>) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: invalid | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I don't make use of `Bool` being closed. I don't seek to discharge `forall b. C b` as you claim, rather `pi b. C b`. I found a way to emulate what I want with `unsafeCoerce`. Here is an example for the open kind `Type`: {{{#!hs {-# 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 explicitly class SI a where s :: S a instance SI Int where s = SInt instance SI Bool where s = SBool -- Can be eliminated like 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" newtype Wrap a = Wrap a instance SI a => Str (Wrap a) where str = sElim (s @a) (str @a) (str @a) wit :: forall ty. SI ty |- Str ty wit = wrapElim Dict where wrapElim :: (SI ty |- Str (Wrap ty)) -> (SI ty |- Str ty) wrapElim = unsafeCoerce -- >> siStr @Int -- "INT!" -- >> siStr @Bool -- "BOOL!" siStr :: forall ty. SI ty => String siStr = go wit where go :: SI ty => (SI ty |- Str ty) -> String go Dict = str @ty ++ "!" }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14822#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler