#14878: Can't witness transitivity ((.)) of isomorphism of Constraints -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints, wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This compiles, {{{#!hs {-# 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 {{{#!hs {-# 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> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14878 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler