Can't witness transitivity ((.)) of isomorphism of Constraints
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 = Dictbut 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 = Dictgiving 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> Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |