#14878 closed bug (invalid)
Can't witness transitivity ((.)) of isomorphism of 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 compiles,
{-# Language QuantifiedConstraints, GADTs, ConstraintKinds, TypeOperators, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-} data Dict c where Dict :: c => Dict c class (a => b) => Implies a b instance (a => b) => Implies a b type a -:- b = Dict (Implies a b, Implies b a) -- isomorphism of constraints, should be an equivalence relation id_ :: a-:-a id_ = Dict sym_ :: a-:-b -> b-:-a sym_ Dict = Dict -- comp_ :: a-:-b -> b-:-c -> a-:-c -- comp_ Dict Dict = Dict
but uncommenting comp_
and GHC doesn't know how to deduce b
(the location message is weird)
$ ghci -ignore-dot-ghci hs/206-bug-quantified-constraints.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( hs/206-bug-quantified-constraints.hs, interpreted ) hs/206-bug-quantified-constraints.hs:1:1: error: Could not deduce: b from the context: (Implies a b, Implies b a) bound by a pattern with constructor: Dict :: forall (c :: Constraint). c => Dict c, in an equation for ‘comp_’ at hs/206-bug-quantified-constraints.hs:18:7-10 or from: (Implies b c, Implies c b) bound by a pattern with constructor: Dict :: forall (c :: Constraint). c => Dict c, in an equation for ‘comp_’ at hs/206-bug-quantified-constraints.hs:18:12-15 or from: c bound by a quantified context at hs/206-bug-quantified-constraints.hs:1:1 | 1 | {-# Language QuantifiedConstraints, GADTs, ConstraintKinds, TypeOperators, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-} | ^ hs/206-bug-quantified-constraints.hs:1:1: error: Could not deduce: b from the context: (Implies a b, Implies b a) bound by a pattern with constructor: Dict :: forall (c :: Constraint). c => Dict c, in an equation for ‘comp_’ at hs/206-bug-quantified-constraints.hs:18:7-10 or from: (Implies b c, Implies c b) bound by a pattern with constructor: Dict :: forall (c :: Constraint). c => Dict c, in an equation for ‘comp_’ at hs/206-bug-quantified-constraints.hs:18:12-15 or from: a bound by a quantified context at hs/206-bug-quantified-constraints.hs:1:1 | 1 | {-# Language QuantifiedConstraints, GADTs, ConstraintKinds, TypeOperators, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-} | ^ Failed, no modules loaded. Prelude>
simplifying and uncurrying we get a more minimal example
{-# Language QuantifiedConstraints, GADTs, ConstraintKinds, TypeOperators, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-} data Dict c where Dict :: c => Dict c f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a f = Dict
giving a different and longer error message
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 206-bug-quantified-constraints.hs, interpreted ) 206-bug-quantified-constraints.hs:6:6: error: • Could not deduce: c0 from the context: (a => b, b => a, b => c, c => b, a => c, c) bound by the type signature for: f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint). (a => b, b => a, b => c, c => b, a => c, c) => Dict a at 206-bug-quantified-constraints.hs:6:6-58 • In the ambiguity check for ‘f’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 206-bug-quantified-constraints.hs:6:6: error: • Could not deduce: (b, c0) from the context: (a => b, b => a, b => c, c => b, a => c, c) bound by the type signature for: f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint). (a => b, b => a, b => c, c => b, a => c, c) => Dict a at 206-bug-quantified-constraints.hs:6:6-58 or from: a bound by a quantified context at 206-bug-quantified-constraints.hs:6:6-58 • In the type signature: f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 206-bug-quantified-constraints.hs:6:6: error: • Could not deduce: b0 from the context: (a => b, b => a, b => c, c => b, a => c, c) bound by the type signature for: f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint). (a => b, b => a, b => c, c => b, a => c, c) => Dict a at 206-bug-quantified-constraints.hs:6:6-58 or from: c0 bound by a quantified context at 206-bug-quantified-constraints.hs:6:6-58 • In the ambiguity check for ‘f’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 206-bug-quantified-constraints.hs:6:6: error: • Could not deduce: c0 from the context: (a => b, b => a, b => c, c => b, a => c, c) bound by the type signature for: f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint). (a => b, b => a, b => c, c => b, a => c, c) => Dict a at 206-bug-quantified-constraints.hs:6:6-58 or from: b0 bound by a quantified context at 206-bug-quantified-constraints.hs:6:6-58 • In the ambiguity check for ‘f’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 206-bug-quantified-constraints.hs:6:6: error: • Could not deduce: b from the context: (a => b, b => a, b => c, c => b, a => c, c) bound by the type signature for: f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint). (a => b, b => a, b => c, c => b, a => c, c) => Dict a at 206-bug-quantified-constraints.hs:6:6-58 or from: b0 bound by a quantified context at 206-bug-quantified-constraints.hs:6:6-58 • In the ambiguity check for ‘f’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 206-bug-quantified-constraints.hs:6:6: error: • Could not deduce: (b, b0) from the context: (a => b, b => a, b => c, c => b, a => c, c) bound by the type signature for: f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint). (a => b, b => a, b => c, c => b, a => c, c) => Dict a at 206-bug-quantified-constraints.hs:6:6-58 or from: a bound by a quantified context at 206-bug-quantified-constraints.hs:6:6-58 • In the type signature: f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | 6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Failed, no modules loaded. Prelude>
Change History (5)
comment:1 Changed 21 months ago by
comment:2 Changed 21 months ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
Ah that's sensible, and not too difficult to work around:
{-# Language QuantifiedConstraints, GADTs, ConstraintKinds, TypeOperators, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, TypeApplications, ScopedTypeVariables #-} import Data.Kind data Dict c where Dict :: c => Dict c class (a => b) => Implies a b instance (a => b) => Implies a b type a :- b = Dict (Implies a b) type a -:- b = Dict (Implies a b, Implies b a) type Iso s t a b = Dict (Implies a b, Implies s t) comp_ :: forall a b c. a-:-b -> b-:-c -> a-:-c comp_ Dict Dict = comp__ @c @b @a @b @a @c b1 a1 a2 b2 where a1 :: a:-b a1 = Dict a2 :: b:-a a2 = Dict b1 :: c:-b b1 = Dict b2 :: b:-c b2 = Dict comp__ :: s:-t -> a:-b -> t:-i -> b:-c -> Iso s i a c comp__ Dict Dict Dict Dict = Dict
comment:3 Changed 21 months ago by
This can additionally be witnessed by carrying the witness and composing it explicitly
type Cat ob = ob -> ob -> Type data ImpliesC :: Cat Constraint where ImpliesC :: (a => b) => ImpliesC a b data IsoC :: Cat Constraint where IsoC :: ImpliesC a b -> ImpliesC b a -> IsoC a b instance Category ImpliesC where id :: ImpliesC a a id = ImpliesC (.) :: ImpliesC b c -> ImpliesC a b -> ImpliesC a c ImpliesC . ImpliesC = ImpliesC instance Category IsoC where id :: IsoC a a id = IsoC id id (.) :: IsoC b c -> IsoC a b -> IsoC a c IsoC bc cb . IsoC ab ba = IsoC (bc . ab) (ba . cb)
IsoC
can be parameterised by a category IsoC :: Cat ob -> Cat ob
.
comment:5 Changed 18 months ago by
Keywords: | wipT2893 removed |
---|
Note: See
TracTickets for help on using
tickets.
I don't think this is a bug. Consider this example:
This works, because there is exactly one matching local instance (
c => d
) ford
. What about this example, which is closer to what you are writing?There is one matching local instance (
c => d
) ford
, so we try to deducec
. But there are multiple matching local instances forc
:a => c
andb => c
. Which one does GHC pick? As noted in the quantified constraints proposal, if GHC is ever in doubt about which local instance to pick, it simply rejects the code.