QuantifiedConstraints: Adding to the context causes failure
With Simon's latest changes (ticket:14733##14832) this works:
{-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #-}
import Control.Category
import Data.Kind
import Data.Coerce
data With cls a b where
With :: cls a b => With cls a b
type Coercion = With Coercible
type Refl rel = (forall xx. rel xx xx :: Constraint)
type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint)
instance Refl rel => Category (With rel) where
id = With
(.) = undefined
But strengthening the context with Trans rel
:
instance (Refl rel, Trans rel) => Category (With rel) where
causes it to fail
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( J.hs, interpreted )
J.hs:15:10: error:
• Could not deduce: rel xx zz
from the context: (Refl rel, Trans rel)
bound by an instance declaration:
forall k (rel :: k -> k -> Constraint).
(Refl rel, Trans rel) =>
Category (With rel)
at J.hs:15:10-53
or from: (rel xx yy, rel yy zz)
bound by a quantified context at J.hs:15:10-53
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the instance declaration for ‘Category (With rel)’
|
15 | instance (Refl rel, Trans rel) => Category (With rel) where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
J.hs:15:10: error:
• Could not deduce: rel xx xx
from the context: (Refl rel, Trans rel)
bound by an instance declaration:
forall k (rel :: k -> k -> Constraint).
(Refl rel, Trans rel) =>
Category (With rel)
at J.hs:15:10-53
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the instance declaration for ‘Category (With rel)’
|
15 | instance (Refl rel, Trans rel) => Category (With rel) where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
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 |