[GHC] #14878: Can't witness transitivity ((.)) of isomorphism of Constraints
GHC
ghc-devs at haskell.org
Fri Mar 2 18:02:36 UTC 2018
#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
More information about the ghc-tickets
mailing list